用Coq证明st X+ st Y= st Y+ (st X- 1) +1

Question

正如标题所述，我正在寻找一种方法来在Coq中证明st X + st Y = st Y + (st X - 1) + 1。我一直在尝试应用plus_comm、plus_assoc和plus_permute的各种组合，但是我还没能让它通过。有什么建议吗？

以下是目标窗口：

3 subgoal
n : nat
m : nat
st : state
H : st Y + st X = n + m /\ beval st (BNot (BEq (AId X) (ANum 0))) = true
______________________________________(1/3)
st Y + 1 + (st X - 1) = n + m

Answer 1

对于整数，无论是ring还是omega都应该能够解决这样的目标。这也可以手动完成。它有助于禁用符号，从而使函数名出现(为了使用SearchAbout查找有用的引理)。以下可能不是最短的证据，只是我发现的第一个证据：

Require Import ZArith.

Lemma simple: forall x y, (x + y)%Z = (y + (x - 1) + 1)%Z.
intros.
rewrite Z.add_sub_assoc.
replace ((y + x)%Z) with ((x + y)%Z).
Focus 2.
rewrite Z.add_comm.
reflexivity.
set (t := ((x + y)%Z)).
replace (1%Z) with (Z.succ 0).
Focus 2.
symmetry.
apply Z.one_succ.
rewrite Zminus_succ_r.
rewrite Z.add_succ_r.
rewrite <- Zminus_0_l_reverse.
rewrite <- Zplus_0_r_reverse.
rewrite Z.succ_pred.
reflexivity.
Qed. 

Answer 2

对于那些希望使用omega作为快速解决方案的人，有一种方法可以将目标转化为可以应用的形式：

inversion H. inversion H1. rewrite negb_true_iff in H3. apply beq_nat_false in H3. omega.

对于为什么omega在我们这样做之后才能工作，而不是当目标处于原始状态时，下面是Github用户jaewooklee93的一个很好的答案：

“这里不需要考虑plus_comm或类似的引理，因为omega可以解决这些简单的问题。你的目标几乎是微不足道的，但是欧米茄之所以坚持要明确目标，仅仅是因为nat之间的负数与我们已经知道的不一样；2-5=0，因为nat中没有消极的概念。所以如果你不提供st X大于0的事实，omega就不能为你清除目标。但是在H1中已经存在这种情况。因此，您应该做的唯一一件事就是简化H1并将引理应用于H1，使它能够正常工作。“