Getting started
Curry–Howard correspondence
A proposition is a type; a proof is a term of that type.
Open CurryHoward.lean in editor-- An ordinary function takes a value and returns it.
def keepNumber : Nat → Nat := fun n => n
-- A proof of P → P takes a proof of P and returns it.
theorem keepProof (P : Prop) : P → P := fun hp => hp
-- The same proof, written with tactics.
example (P : Prop) : P → P := by
intro hp
exact hp
-- Function application also applies an implication.
theorem applyProof (P Q : Prop) (hpq : P → Q) (hp : P) : Q :=
hpq hp
-- These are two proofs of the same concrete proposition.
example : 2 + 2 = 4 := rfl
example : 2 + 2 = 4 := keepProof (2 + 2 = 4) rfl
#eval keepNumber 42
Explanation
P : Prop
P is a proposition. A term hp : P is a proof of P. This is the propositions-as-types view of the Curry–Howard correspondence.
P → Q
An implication is a function from proofs of P to proofs of Q. Applying hpq to hp produces a proof of Q.
fun hp => hp
The identity function works for proofs as well as data. A tactic proof builds a proof term that Lean’s kernel checks.
Prop · Type
Lean distinguishes propositions from data types. Proofs in Prop are erased from compiled programs; the correspondence does not mean proofs are printed when main runs.
Expected output
Reference only. Run the file to check its actual result.
42
Exercise
Write a proof of P → Q → P using fun hp _hq => hp.