constructor
Summary
If your goal is a proof which is “made up of subproofs” (for example a goal like ⊢ P ∧ Q
; to prove this you have to prove P
and Q
) then the constructor
tactic will turn your goal into these multiple simpler goals.
Examples
Faced with the goal
⊢ P ∧ Q
, theconstructor
tactic will turn it into two goals⊢ P
and⊢ Q
.Faced with the goal
⊢ P ↔ Q
,constructor
will turn it into two goals⊢ P → Q
and⊢ Q → P
.Something which always amuses me – faced with
⊢ True
,constructor
will solve the goal. This is becauseTrue
is made up of 0 subproofs, soconstructor
turns it into 0 goals.
Further notes
The refine
tactic is a more refined version of constructor
; faced with a goal of ⊢ P ∧ Q
, constructor
does the same as refine ⟨?_, ?_⟩,
. In fact refine
is more powerful than constructor
; faced with ⊢ P ∧ Q ∧ R
you would have to use constructor
twice to break it into three goals, whereas refine ⟨?_, ?_, ?_⟩
does the job in one go.
Historical remark
constructor
was called split
in Lean 3, but split
in Lean 4 now does what Lean 3’s split_ifs
tactic does.