Proof terms and Curry–Howard
Every tactic proof builds a term. Write proofs directly as functions, pairs and projections: an implication is a function type and a conjunction is a pair. The exercises grow from a single lambda to a proof assembled from several named parts.
Progress is kept in this browser until you sign in
- An implication is a functionfun hp => hp proves P → P.9 min
- A conjunction is a pair⟨hp, hq⟩ proves P ∧ Q.8 min
- Projectionsh.1 and h.2 read the halves of a conjunction.8 min
- Compose implicationsChaining P → Q and Q → R is function composition.10 min
- Eliminate a disjunctionh.elim takes one handler per case.11 min
- Existentials as dependent pairs⟨witness, proof⟩ proves ∃ n, p n.10 min
- Assemble a whole proof termName every component, then hand Lean one finished term.14 min