證明，如果再在其他勒柯克

Question

我是新的勒柯克和我想證明什麼非常基本的

引理eq_if_eq：FORALL A1 + A2，（如果beq_nat A1 + A2那麼A否則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

事實證明，簡單的remember策略是我所需要的。沿着remember (beq_nat a1 a2) as e; induction e; etc的方向行事。

Answer 2

一般爲這樣的事情，我用的是eqn變異毀滅的。它看起來像這樣：

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

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

它將添加相等性作爲假設。在8.4版本中，您可以用問號來代替問號，以符合假設。

Answer 3

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

intros. 
case_eq (beq_nat a1 a2). 
intuition. 
apply beq_nat_true_iff in H. 
intuition. 
intuition.