coq中的计算理论

Question

2个子目标X, y: NATH: x + 0 = y + 0

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

Answer 1

这是真的，在纸上你会简单地得出结论，因为x + 0 = x。在Coq中，你必须证明它，因为加法是左偏的(它通过查找它的第一个参数来计算)。

我建议首先证明

forall n, n + 0 = n

Answer 2

我会这样写:

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.