coq - 在 Coq 中证明 if then else

Question

我是 Coq 的新手，我试图证明一些非常基本的东西

Lemma eq_if_eq : forall a1 a2, (if beq_nat a1 a2 then a2 else 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

一般对于这种事情，我使用eqn破坏的变种。它看起来像这样:

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

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

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