Foundations · 6 min
Proofs are terms
The Curry–Howard correspondence connects logic with types: a proposition is a type, and a proof is a term of that type. In Lean, P : Prop says that P is a proposition; hp : P says that hp proves it.
An ordinary identity function has type Nat → Nat and body fun n => n. A proof of P → P has the same form: fun hp => hp. It accepts a proof of P and returns that proof.
More generally, a proof of P → Q is a function that turns a proof of P into a proof of Q. If hpq : P → Q and hp : P, then hpq hp has type Q. Tactics build these proof terms for you; Lean’s kernel checks their types.
Lean treats propositions differently from data: proofs in Prop are erased from compiled programs. This lets programs carry checked properties without executing the proof as part of main.
Exercise
Replace sorry with the identity function fun hp => hp. It must prove P → P for any proposition P.
Open exercise in editortheorem identityProof (P : Prop) : P → P :=
sorry
Hint
hp has type P. Returning hp therefore gives the required proof of P.
Solution
theorem identityProof (P : Prop) : P → P :=
fun hp => hp