辅 enzyme Q/SSReflect : How to do case analysis when reflecting && and/\

Question

我有以下反射(reflect)谓词:

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

我正在尝试将 bool 合取与逻辑合取关联起来，并通过以下单行证明:

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

---

但是，我不明白最后的;按情况。 应用。当我们检查没有最后一个 的证明时；视情况而定。:

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. 单独，但这不起作用。 ;按案例一次承认这些子目标？

谢谢。

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.