CODEWITHSUNDEEP
coqcomputation-theory
user12043399
user12043399

Reputation:

computation theory in coq

2 subgoals x, y : nat H : x + 0 = y + 0

but after that I don't know how to to get rid of 0 in H.

Upvotes: 0

Views: 183

Answers (2)

Felipe Balbi
Felipe Balbi

Reputation: 157

I would go with something like this:

Theorem ex9: forall x y n, x + n = y + n -> x = y.
Proof.
 intros.
 induction n as [| n' IH].
 - rewrite add_0_r in H.      (* replace x + 0 with x *)
   rewrite add_0_r in H.      (* replace y + 0 with y *)
   assumption.
 - apply IH.                  (* replace x=y with x+n' = y+n' *)
   rewrite <- plus_n_Sm in H. (* replace x + S n' with S (x + n') *)
   rewrite <- plus_n_Sm in H. (* replace y + S n' with S (y + n') *)
   apply S_injective in H.    (* drop both S constructors *)
   assumption.
Qed.

Upvotes: 0

Th&#233;o Winterhalter
Th&#233;o Winterhalter

Reputation: 5108

It's true that on paper you would simply conclude because x + 0 = x. Well, in Coq you have to prove it because addition is left-biased (it computes by looking up its first argument).

I would suggest proving first that

forall n, n + 0 = n

Upvotes: 2

Related Questions