Summary of Curry-Howard Correspondence in Lean

Curry-Howard Correspondence

Here is a table of logical symbols/connectives/quantifiers and their computational equivalents.
Note that I slightly transformed Lean 4 inductives here: turned all structures into inductives (to make the format consistent), removed comments, and wrote all Type (max u v) as Type _ (just to save some space).

inductive False : Propinductive Empty : Type
inductive True : Prop where
| intro
inductive Unit : Type where
| unit
inductive And (a : Prop) (b : Prop) : Prop where
| intro (left : a) (right : b)
inductive Prod (α : Type u) (β : Type v) : Type _ where
| mk (fst : α) (snd : β)
inductive Or (a : Prop) (b : Prop) : Prop where
| inl  (h : a)
| inr (h : b)
inductive Sum (α : Type u) (β : Type v) : Type _ where
| inl (val : α)
| inr (val : β)
inductive Exists {α : Sort u} (p : α → Prop) : Prop where
| intro (w : α) (h : p w)
inductive Sigma {α : Type u} (β : α → Type v) : Type _ where
| mk (fst : α) (snd : β fst)

The only difference between the logical connectives and their computational equivalents is the fact that former return a Prop (Sort 0), and the latter return a Type _ (Sort 1+).

Elimination rules from formal logic correspond to matching. Whenever you declare an inductive, e.g. inductive MyType, Lean automatically gives you the match MyType.intro a b,  MyType.casesOn,  MyType.rec, and multiple other functions (in case of Exists and Or, Lean also gives us Exists.elim and Or.elim, but this is just syntax sugar). All of them compile to MyType.rec - a so-called recursor function.
Introduction rules from formal logic correspond to using type constructors (And.intro, Or.inl, Or.inr, etc.). For example, ∨I is represented as Or.inl proofOfA.

Some notation

Here is a table with notation for the types above.

inductive False, inductive EmptyFalse, Empty 
inductive True, inductive UnitTrue , Unit  
inductive And, inductive ProdAnd a b == a ∧ b
Prod α β== α × β
inductive Or, inductive SumOr a b == a ∨ b
Sum α β== α ⊕ β
inductive Exists, inductive SigmaExists (λ x : α => p)== ∃ x : α, p
Sigma (λ a : α => β a)== Σ a : α, β a
== (a : α) × β a

Notice how the notation we're used to refers to the use of the inductive type itself (and not to the use of its constructors). For example, a ∧ b means And a b (and not And.intro hA hB).

The only exceptions to this rule are:

  • (), which is sugar for Unit.unit (and not Unit); and
  • (2, 3), which is sugar for 2 3 (and not Prod 2 3).

Prod is also called a pair.
Sigma is also called a dependent pair.