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).
| Logic | Computation |
|---|---|
| inductive False : Prop | inductive 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.
Here is a table with notation for the types above.
| Inductives | Expression | Sugar |
|---|---|---|
| inductive False, inductive Empty | False, Empty | |
| inductive True, inductive Unit | True , Unit | |
| inductive And, inductive Prod | And a b | == a ∧ b |
Prod α β | == α × β | |
| inductive Or, inductive Sum | Or a b | == a ∨ b |
Sum α β | == α ⊕ β | |
| inductive Exists, inductive Sigma | Exists (λ 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 Prod.mk 2 3 (and not Prod 2 3).Prod is also called a pair.
Sigma is also called a dependent pair.