Local Sequence tactial and Incorrect number of goals

Using Rocq
1

Hi,

Is there way in Ltac to express following case in a concise, but structured, manner without try tactic:

Theorem seq_try: (False \/ 3 = 3 /\ True) /\ ((4 = 4 /\ True) \/ False ).
Proof. 
  split; [ right | left ]; split; try apply eq_refl; apply I.
Qed.

Theorem seq_rep (False \/ 3 = 3 /\ True) /\ ((4 = 4 /\ True) \/ False ).
Proof.
  split; [ right | left ]; split; [ apply eq_refl | apply I | apply eq_refl | apply I].
Qed.

Theorem seq_notry: (False \/ 3 = 3 /\ True) /\ ((4 = 4 /\ True) \/ False ).
Proof.
  Fail split; [ right | left ]; split; [ apply eq_refl | apply I].
  Abort.

Error: Tactic failure: Incorrect number of goals (expected 4 tactics).

2

split; [ right | left ]; (split; [ apply eq_refl | apply I]).? (note the ())

1 Like