CODEWITHSUNDEEP
coqproof
Adam
Adam

Reputation: 10036

Proving st X + st Y = st Y + (st X - 1) + 1 using Coq

Just like the title says, I'm looking for a way to prove st X + st Y = st Y + (st X - 1) + 1 in Coq. I've been trying applying various combinations of plus_comm, plus_assoc and plus_permute but I haven't been able to make it go through. Any suggestions?

Here is the goal 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

Upvotes: 1

Views: 158

Answers (2)

Adam
Adam

Reputation: 10036

For those looking to use omega as a quick-fix, here's one way to get the goal into a form where it can be applied:

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

For why omega works after we do this and not when the goal was in the original state, here is a great answer by Github user 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."

Upvotes: 0

Atsby
Atsby

Reputation: 2327

For integers, either ring or omega should be able to solve such a goal. It can also be done manually. It helps to disable notations so that function names appear (in order use SearchAbout to find useful lemmas). The following is probably not the shortest possible proof, just the first I found:

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.

Upvotes: 1

Related Questions