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.

Solution

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.