CODEWITHSUNDEEP
coqcoq-tacticssreflect
Atharva Shukla
Atharva Shukla

Reputation: 2137

Coq/SSReflect: How to do case analysis when reflecting && and /\

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.

Upvotes: 3

Views: 567

Answers (2)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

The behavior of sequential composition for tactics changed a bit in recent years. Nowadays, tactics like constructor can backtrack while executing their continuation. Because your definition of reflect is a bit different from the standard one, if you just call constructor, Coq will immediately apply ReflectT, leading to a stuck goal in three of the cases:

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

When you use sequential composition, the constructor tactic backtracks, correctly finding the ReflectF constructor.

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

Upvotes: 3

Anton Trunov
Anton Trunov

Reputation: 15404

I'm not sure why you are getting 6 subgoals: case b1; case b2; constructor produces 4 subgoals, corresponding to the four possible cases for combinations of boolean values:

  true /\ true

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

The first one is considered trivial by //.

Set Printing Coercions will tell you that your subgoals or actually as follows:

  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)

Unfolding is_true might help: 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)

The 3 last subgoal are of the form (_ /\ _) -> False (because ~ P stands for not P, which unfolds to P -> False.

Thus the case tactic added after constructor destructs the top assumptions turning the last three goals into the following:

  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

Here, we have false = true as one of the assumptions in each subgoal, meaning we got a contradiction that SSReflect can immediately recognize and finish the proof using the principle of explosion.

Upvotes: 1

Related Questions