使用 Coq 证明 st X + st Y = st Y + (st X - 1) + 1
Proving st X + st Y = st Y + (st X - 1) + 1 using Coq
正如标题所说，我正在寻找一种在 Coq 中证明 st X + st Y = st Y + (st X - 1) + 1 的方法。我一直在尝试应用 plus_comm、plus_assoc 和 plus_permute 的各种组合，但一直未能成功。有什么建议么？
这是目标 window:
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
对于整数，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.
对于那些希望使用 omega 作为快速修复的人来说，这里有一种方法可以将目标转化为可以应用的形式：
inversion H.
inversion H1.
rewrite negb_true_iff in H3.
apply beq_nat_false in H3.
omega.
为什么 omega 在我们这样做之后起作用，而不是在目标处于原始状态时起作用，这是 Github 用户 jaewooklee93 的一个很好的回答：
"You don't need to think about plus_comm or similar lemmas here, because omega can solve those easy problems. Your goals are almost trivial, but the reason why omega hesistates to clear the goals is just because the minus between nat is not the same as the one we already know; 2-5=0, since there is no notion of negative in nat. So if you don't provide the fact that st X is greater than zero, omega cannot clear the goal for you. But you already have that condition in H1. Therefore, the only thing you should do is to simplify H1 and apply lemmas to H1 to make it st X<>0 .Then omega can properly work."
正如标题所说，我正在寻找一种在 Coq 中证明 st X + st Y = st Y + (st X - 1) + 1 的方法。我一直在尝试应用 plus_comm、plus_assoc 和 plus_permute 的各种组合，但一直未能成功。有什么建议么？
这是目标 window:
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
对于整数，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.
对于那些希望使用 omega 作为快速修复的人来说，这里有一种方法可以将目标转化为可以应用的形式：
inversion H.
inversion H1.
rewrite negb_true_iff in H3.
apply beq_nat_false in H3.
omega.
为什么 omega 在我们这样做之后起作用，而不是在目标处于原始状态时起作用，这是 Github 用户 jaewooklee93 的一个很好的回答：
"You don't need to think about plus_comm or similar lemmas here, because omega can solve those easy problems. Your goals are almost trivial, but the reason why omega hesistates to clear the goals is just because the minus between nat is not the same as the one we already know; 2-5=0, since there is no notion of negative in nat. So if you don't provide the fact that st X is greater than zero, omega cannot clear the goal for you. But you already have that condition in H1. Therefore, the only thing you should do is to simplify H1 and apply lemmas to H1 to make it st X<>0 .Then omega can properly work."