Proving · 9 min

Implication proofs

To prove P → P, assume a proof of P and return it. This is the same shape as an identity function. intro h names the assumption; exact h supplies it as the solution.

Tactics transform the goal. When reading a proof, track which assumptions you have and what proposition remains to prove. Error diagnostics often show this proof state when a tactic fails.

Exercise

Prove P → Q → P for arbitrary propositions P and Q.

theorem keep_first (P Q : Prop) : P → Q → P := by
  sorry

theorem keep_first (P Q : Prop) : P → Q → P := by
  intro hp hq
  exact hp

Related example