Coq / SSReflect: как выполнить анализ случая при отражении && и / \ - PullRequest
Новая
       98

Coq / SSReflect: как выполнить анализ случая при отражении && и / \

3 голосов
/ 05 октября 2019

У меня есть следующий предикат отражения: 

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 допускает эти подцели одновременно?

Спасибо.

Ответы [ 2 ]

3 голосов
/ 05 октября 2019

Поведение последовательной композиции для тактики немного изменилось в последние годы. В настоящее время такие тактики, как 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.
1 голос
/ 05 октября 2019

Я не уверен, почему вы получаете 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 может немедленно распознать и завершитьдоказательство с использованием принципа взрыва .

...