在Coq中使用自反 [英] Using reflexivity in Coq

问题描述

我正在尝试从Coq文档软件基金会（ http://www.cis.upenn.edu/~bcpierce/sf/current/Induction.html#lab40 ），当我注意到要解决该示例时，请输入以下链接：

I was trying out the examples from the Coq documentation Software Foundations (http://www.cis.upenn.edu/~bcpierce/sf/current/Induction.html#lab40) when I noticed that to solve the example give in the link:

Theorem andb_true_elim1 : ∀b c : bool,
  andb b c = true → b = true.
Proof.
  intros b c H.
  destruct b.
  Case "b = true". (* <----- here *)
    reflexivity.
  Case "b = false". (* <---- and here *)
    rewrite ← H.
    reflexivity.
Qed.

我们正在破坏b，它出现在c的左侧，表示 andb。但是要进行本书中的练习，即

we are destructing b which appears on the left of c for "andb". However to do the exercise that follows in the book i.e.

Theorem andb_true_elim2 : ∀b c : bool,
  andb b c = true → c = true.
Proof.
  (* FILL IN HERE *) Admitted.

我发现相同的方法无济于事。我认为自反性无济于事，原因是子目标中 b的位置。最终，我以以下方式完成了证明：

I found the same method does not help. "reflexivity" did not help which I assume is due to the position of 'b' in the subgoal. Eventually I completed the proof in the following manner:

Theorem andb_true_elim2 : forall b c:bool,
andb b c = true -> c = true.
Proof.
intros b c H.
destruct c.
Case "c=true".
reflexivity.
Case "c=false".
rewrite <- H.
destruct b.
reflexivity.
reflexivity.
Qed.

有人可以解释为什么上面的代码起作用并产生以下缺陷吗？

Can someone explain why the above code worked and the following dint?

Theorem andb_true_elim2 : forall b c:bool,
andb b c = true -> c = true.
Proof.
intros b c H.
destruct c.
Case "c=true".
reflexivity.
Case "c=false".
rewrite <- H.
reflexivity.

推荐答案

最后一个证明不起作用的原因是 andb 的定义方式以及Coq简化此类定义的方式（自反性在目标中进行了一些简化 ）。

The reason the last proof doesn't work is the way andb defined and the way Coq simplifies such definitions (reflexivity performs some simplifications in the goal).

以下是Coq中 andb 的定义。

Here is the definition of andb in Coq.

Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.

请注意，我们基于 first 参数进行决策。因此，当您在 first 参数上使用 destruct 然后使用 reflexivity 时，您可以Coq以减少 andb bc （减少为 false 或减少为 c ）。

Notice that we make decision basing on the first parameter. So, when you use destruct on the first argument and then use reflexivity, you allow Coq to reduce andb b c (to false or to c).

由于 andb 的定义不对称，因此在 second 上进行了案例分析参数不起作用，因为Coq无法在函数主体中减小 if 表达式。

Because of the unsymmetrical definition of andb, case analysis on the second argument doesn't work, since Coq can't reduce the if expression in the function's body.

这篇关于在Coq中使用自反的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！