5

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

引理 eq_if_eq ：对于所有 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.
4

3 回答 3

3

一般这种东西，我使用eqndestruct的变种。它看起来像这样：

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

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

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

于 2013-05-15T03:14:20.927 回答
2

做你所要求的策略是case_eq。以下脚本证明了 8.4pl3 中的引理：

intros.
case_eq (beq_nat a1 a2).
intuition.
apply beq_nat_true_iff in H.
intuition.
intuition.
于 2015-03-18T03:00:42.490 回答
0

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

于 2013-06-03T05:57:12.777 回答