在Coq中证明是否接着

Question

我是Coq的新手,我正在努力证明一些非常基本的东西

引理eq_if_eq:forall a1 a2,(如果beq_nat a1 a2则a2否a1)= a1.

我努力通过下面发布的解决方案,但我认为必须有更好的方法.理想情况下,我希望beq_nat a1 a2在将案例值放入假设列表时干净利落.有没有一种策略t可以使用t (beq_nat a1 a2)两个子句,一个在哪里beq_nat a1 a2 = true,另一个在哪里beq_nat a1 a2 = false？显然,induction非常接近,但它失去了它的历史.

这是我努力的证明:

Proof.
Hint Resolve beq_nat_refl.
Hint Resolve beq_nat_eq.
Hint Resolve beq_nat_true.
Hint Resolve beq_nat_false.
intros.
compare (beq_nat a1 a2) true.
intros. assert (a1 = a2). auto. 
replace (beq_nat a1 a2) with true. auto.
intros. assert (a1 <> a2). apply beq_nat_false.
apply not_true_is_false. auto.
assert (beq_nat a1 a2 = false). apply not_true_is_false. auto.
replace (beq_nat a1 a2) with false. auto.
Qed.

Answer 1

一般来说，对于这种事情，我使用eqndestruct 的变体。它看起来像这样：

destruct (beq_nat a1 a2) as []_eqn. (* Coq <= 8.3 *)

destruct (beq_nat a1 a2) as []eqn:? (* Coq >= 8.4 *)

它将添加等式作为假设。在 8.4 变体中，您可以用一个名称替换问号以赋予假设。

Answer 2

事实证明，简单的remember策略就是我所需要的。类似的东西remember (beq_nat a1 a2) as e; induction e; etc。