Coq/SSReflect:如何在反射时进行案例分析&与/\

Question

我有以下反映谓词：

Require Import mathcomp.ssreflect.all_ssreflect.

Inductive reflect (P : Prop) (b : bool) : Prop :=
| ReflectT (p : P) (e : b = true)
| ReflectF (np : ~ P) (e :  b = false).

我试图把布尔连接和逻辑连接联系起来，下面的一行证明是这样的：

Lemma andP (b1 b2 : bool) : reflect (b1 /\ b2) (b1 && b2).
Proof.
  case b1; case b2; constructor =>//; by case.
Qed.

但是，我不明白最后一个; by case.是如何应用的。当我们检查没有最后一个; by case.的证明时

Lemma andP (b1 b2 : bool) : reflect (b1 /\ b2) (b1 && b2).
Proof.
  case b1; case b2; constructor =>//.

我们得到了6个子目标(其中2个是琐碎的事实)：

6 subgoals (ID 45)

  b1, b2 : bool
  ============================
  true /\ false

subgoal 2 (ID 46) is:
 true && false = true
subgoal 3 (ID 116) is:
 false /\ true
subgoal 4 (ID 117) is:
 false && true = true
subgoal 5 (ID 187) is:
 false /\ false
subgoal 6 (ID 188) is:
 false && false = true

我不知道如何从这里开始，因为它们都是false --我们如何证明这一点？我试着单独做. case.，但这不起作用。; by case是如何同时承认这些子目标的？

谢谢。

Answer 1

近年来，战术顺序构图的行为发生了一些变化。现在，像constructor这样的战术可以在执行它们的延续时回溯。由于您对reflect的定义与标准定义略有不同，如果您只调用constructor，Coq将立即应用ReflectT，从而导致以下三种情况下的目标卡住：

Lemma andP (b1 b2 : bool) : reflect (b1 /\ b2) (b1 && b2).
Proof.
case b1; case b2=> /=.
- constructor=> //.
- (* constructor. *) (* Stuck *)

当您使用顺序组合时，constructor策略倒退，正确地找到ReflectF构造函数。

  constructor; by try case.
- constructor; by try case.
- constructor; by try case.
Qed.

Answer 2

我不知道为什么要获得6个子目标：case b1; case b2; constructor生成4个子目标，对应于布尔值组合的四种可能情况：

  true /\ true

subgoal 2 (ID 13) is:
 ~ (true /\ false)
subgoal 3 (ID 15) is:
 ~ (false /\ true)
subgoal 4 (ID 17) is:
 ~ (false /\ false)

第一个问题被//认为是微不足道的。

Set Printing Coercions会告诉您您的子目标或实际目标如下：

  is_true true /\ is_true true

subgoal 2 (ID 13) is:
 ~ (is_true true /\ is_true false)
subgoal 3 (ID 15) is:
 ~ (is_true false /\ is_true true)
subgoal 4 (ID 17) is:
 ~ (is_true false /\ is_true false)

展开is_true可能有帮助：case b1; case b2; constructor; rewrite /is_true.

  true = true /\ true = true

subgoal 2 (ID 19) is:
 ~ (true = true /\ false = true)
subgoal 3 (ID 20) is:
 ~ (false = true /\ true = true)
subgoal 4 (ID 21) is:
 ~ (false = true /\ false = true)

最后三个子目标是表单(_ /\ _) -> False (因为~ P代表not P，它是P -> False )。

因此，在case之后添加的constructor策略破坏了最重要的假设，将最后三个目标转化为以下三个目标：

  true = true -> false = true -> False

subgoal 2 (ID 145) is:
 false = true -> true = true -> False
subgoal 3 (ID 155) is:
 false = true -> false = true -> False

这里，我们把false = true作为每个子目标中的一个假设，这意味着我们有一个矛盾，SSReflect可以立即识别并使用爆炸原理完成证明。