3

I have the following reflect predicate:

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).

And I am trying to relate the boolean conjunction to the logical one and the following one-line proof goes through:

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

However, I don't understand how the last ; by case. is applied. When we examine the proof without the last ; by case.:

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

We get 6 subgoals (2 are trivially true):

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

I'm not sure how to proceed from here because they all are false - how can we prove that? I tried doing . case. individually but that doesn't work. How does ; by case admit these subgoals all at once?

Thank you.

4

2 回答 2

3

近年来，战术顺序组合的行为发生了一些变化。如今，诸如此类的战术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.
于 2019-10-05T18:24:51.417 回答
1

我不确定你为什么得到 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)

最后 3 个子目标的形式为(_ /\ _) -> 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 可以立即识别并使用爆炸原理完成证明。

于 2019-10-05T18:20:42.150 回答