This post provides a technical walkthrough of fundamental propositional logic concepts and their formal implementation using the Lean 4 programming language and theorem prover. It serves as a practical guide for constructing proofs from first principles, starting with basic logical constants and advancing to mathematical structures like natural numbers.
The content is organized into logical building blocks, each containing inductive definitions, theorems, and practical examples.
This post details the foundational elements of logic through the following sections:
False.elim (the principle that anything follows from a contradiction).Not a as a β False, featuring theorems like not_not_intro and Not.elim.imp_intro and imp_imp_imp theorems.Iff in terms of And and implication.Beyond basic definitions, this guide explores complex logical applications:
Β¬(p β¨ q) β Β¬p β§ Β¬q), distributivity of And/Or, and commutativity.Eq.subst), congruence (congrArg), and transitivity.The preamble sets the foundational environment for the proofs using two specific Lean 4 commands. These commands define the scope and the computational behavior of the subsequent logic.
namespace Basic
πnamespace Basic
Encapsulation: This command groups all the definitions and theorems under the name Basic.
Naming Organization: By using a namespace, we avoid naming conflicts with Leanβs built-in library (the “Prelude”), allowing us to redefine fundamental structures like True, False, and And for educational purposes.
Access: To use these definitions later, one would typically refer to them as Basic.True or Basic.And.
noncomputable section
πnoncomputable section
Logic over Computation: Lean 4 is both a theorem prover and a programming language. By default, Lean tries to generate executable code for every definition.
Suppressing Code Generation: Marking a section as noncomputable tells Lean that it does not need to generate executable bytecode for these definitions.
Purpose: This is common in formal logic where the focus is on the mathematical properties and proofs of propositions rather than their efficiency as a running program.
This header introduces the simplest proposition in Lean 4, representing a statement that is always logically valid.
True is defined as an inductive type within the Basic namespace.
inductive True : Prop where
| intro : True
Inductive Definition: It is defined with a single constructor called intro. This means the only way to “prove” True is to provide this specific constructor.
Logical Symbol: The comments in the code use the symbol β€ (top) to represent the “true” proposition.
Here are two examples that illustrate how to interact with this type:
-- true
-- β’ β€
example : True := True.intro
-- a implies true
-- β’ a β β€
example : a β True := fun _ => True.intro
| Example | Lean 4 Code | Logical Meaning |
|---|---|---|
| Basic Proof | example : True := True.intro | To prove True, we simply use its constructor, True.intro. |
| Implication | example : a β True := fun _ => True.intro | Any proposition a implies True. This uses a “lambda” function (fun _ => ...) that ignores the input a and returns the proof of True. |
In Lean 4, the definition of False is the logical opposite of True. While True is defined by the existence of a proof, False is defined by the total absence of one.
False is declared as an inductive proposition with no constructors:
inductive False : Prop
Because there are no ways to construct an instance of False, it represents a logical contradiction.
Here are three fundamental ways False behaves in propositional logic:
The first example shows that False implies itself.
-- false implies false
-- β’ β₯ β β₯
example : False β False := fun false => false
Meaning: If you are given a proof of a contradiction, you can certainly return that same proof.
This is the rule that “from a falsehood, anything follows”.
-- false proves a
-- β₯ β’ a
def False.elim (false : False) : a :=
false.rec
Mechanism: It uses false.rec, which is the recursor for the False type. Since there are no cases to handle (no constructors), the proof is considered complete immediately.
Application: This can be used as a function False β a, meaning if you reach a contradiction, you can prove any proposition a.
Here are shorthand ways to invoke this elimination:
example (false : False) : a := false.elim.-- false proves a
-- β₯ β’ a
example (false : False) : a :=
False.elim false
example (false : False) : a := false.elim
fun false => show a from false.elim.-- false implies a
-- β’ β₯ β a
example : False β a :=
fun false => show a from false.elim
In Lean 4, negation is not a primitive concept; rather, it is defined through implication and falsehood. This header explores how we prove a statement is false by showing it leads to a contradiction.
Not a (symbolized as Β¬a) is defined as a function that takes a proof of a and returns a proof of False:
def Not (a : Prop) : Prop := a β False
This means that to prove “not a”, you must demonstrate that a being true is impossible because it would inevitably result in a logical contradiction (β₯).
This section provides several essential patterns for working with negation:
Not.intro): To prove Β¬a, you provide a function that assumes a and derives False.-- a implies false
-- proves not a
-- a β β₯ β’ Β¬a
theorem Not.intro
(af : a β False) : Not a :=
fun ha => show False from af ha
not_not_intro): If you have a proof of a, you can prove ¬¬a. This is because if someone claimed ¬a, you could use your proof of a to show they are wrong, creating a contradiction.-- a proves not not a
-- a ⒠¬¬a
theorem not_not_intro
(ha : a) : Not (Not a) :=
fun na => show False from na ha
Not.elim): If you have both a and Β¬a, you can prove anything (b). This is an application of the “Principle of Explosion” seen in the False section, as a and Β¬a together produce False.-- not a, a
-- proves b
-- Β¬a, a β’ b
def Not.elim (na : Not a) (ha : a) : b :=
have false : False := na ha
show b from false.elim
Not.imp): If a β b and you know Β¬b, then you can conclude Β¬a.-- a implies b, not b
-- proves not a
-- a β b, Β¬b β’ Β¬a
theorem Not.imp
(nb : Not b) (ab : a β b) : Not a :=
fun ha =>
have hb : b := ab ha
show False from nb hb
-- not false
-- β’ Β¬β₯
theorem not_false : Not False :=
fun false => false
-- not not true
-- ⒠¬¬β€
example : Not (Not True) :=
not_not_intro True.intro
-- a proves not a implies b
-- a β’ Β¬a β b
example (ha : a) : Not a β b :=
fun na => show b from na.elim ha
-- a implies not a implies b
-- β’ a β Β¬a β b
example : a β Not a β b :=
fun ha => fun na => show b from na.elim ha
example : a β Not a β b :=
fun ha na => show b from na.elim ha
In Lean 4, logical implication (a β b) is treated as a function: to prove that a implies b, you must show that given an arbitrary proof of a, you can produce a proof of b. This header focuses on how these functional “arrows” are constructed and manipulated.
Here are two primary examples of how implication functions:
imp_intro): If you already have a proof of a, then any other proposition b implies a. In Lean, this is implemented as a function that takes an argument of type b and simply ignores it, returning the existing proof of a.-- a proves b implies a
-- a β’ b β a
theorem imp_intro {a : Prop}
(ha : a) : b β a :=
fun _ => ha
imp_imp_imp): This theorem demonstrates how to transform an implication. If you can turn c into a, and turn b into d, then any process that turns a into b can be wrapped to turn c into d.-- c implies a, b implies d
-- proves (a implies b) implies (c implies d)
-- c β a, b β d β’ (a β b) β (c β d)
theorem imp_imp_imp {d : Prop}
(ca : c β a) (bd : b β d) :
(a β b) β (c β d) :=
fun ab => fun hc =>
have ha : a := ca hc
have hb : b := ab ha
show d from bd hb
Because Lean is based on the Curry-Howard Correspondence, implication behaves exactly like a function definition.
a β b, you use the syntax fun ha => ..., where ha is the assumed proof of a.a β b when you have a proof of a, you apply it just like a function: f ha.This header describes the logical conjunction (symbolized as β§), which represents a requirement that two propositions must both be true simultaneously. In Lean 4, this is implemented as a structure, which is essentially a container for two pieces of evidence.
And is defined as a structure with two fields:
structure And (a b : Prop) : Prop where
intro ::
left : a
right : b
left: A proof of the first proposition (a).right: A proof of the second proposition (b).To create a proof of And a b, you use the constructor And.intro, which requires you to provide a proof for both a and b.
This section demonstrates several fundamental operations for working with “and” statements:
Introduction (Creating And):
ha : a and hb : b, then And.intro ha hb creates a proof of a β§ b.-- a, b
-- proves a and b
-- a, b β’ a β§ b
example (ha : a) (hb : b) : And a b :=
And.intro ha hb
And.symm proves that if you have a β§ b, you can derive b β§ a by swapping the left and right fields.-- a and b
-- proves b and a
-- a β§ b β’ b β§ a
theorem And.symm
(and_ab: And a b) : And b a :=
have ha : a := and_ab.left
have hb : b := and_ab.right
intro hb ha
Elimination (Extracting from And):
and_ab, you can extract the individual proofs using and_ab.left or and_ab.right.-- a and b
-- proves a
-- a β§ b β’ a
example (and_ab : And a b) : a :=
and_ab.left
-- a and b
-- proves b
-- a β§ b β’ b
example (and_ab : And a b) : b :=
and_ab.right
And.elim abbreviation shows how to use an And proof to satisfy a function that requires two separate arguments (a β b β c).-- a implies b implies c, a and b
-- proves c
-- a β b β c, a β§ b β’ c
abbrev And.elim
(ab : a β b β c) (and_ab : And a b) : c :=
ab and_ab.left and_ab.right
-- true and true
-- β’ β€ β§ β€
example : And True True :=
And.intro True.intro True.intro
-- a proves a and a
-- a β’ a β§ a
example (ha : a) : And a a :=
And.intro ha ha
-- a implies a and a
-- β’ a β a β§ a
example : a β And a a :=
fun ha => And.intro ha ha
-- a implies b implies a and b
-- β’ a β b β a β§ b
example : a β b β And a b :=
fun ha hb => And.intro ha hb
This header explains the logical disjunction (symbolized as β¨), which represents a scenario where at least one of two propositions is true. Unlike the And structure which requires both sides, Or is an inductive type that allows for two distinct ways to build a proof.
In Lean 4, Or is defined with two constructors:
inductive Or (a b : Prop) : Prop where
| inl (h : a) : Or a b
| inr (h : b) : Or a b
inl (left): Takes a proof of a to prove a β¨ b.inr (right): Takes a proof of b to prove a β¨ b.This is how to both create and “use” an Or statement:
Introduction (Or.intro):
a, you can prove a β¨ b regardless of what b is.-- a proves a or b
-- a β’ a β¨ b
theorem Or.intro_left
(b : Prop) (h : a) : Or a b :=
inl h
b is sufficient to prove a β¨ b.-- b proves a or b
-- b β’ a β¨ b
theorem Or.intro_right
(a : Prop) (h : b) : Or a b :=
inr h
Elimination (Or.elim):
-- a or b, a implies c, b implies c
-- proves c
-- a β¨ b, a β c, b β c β’ c
theorem Or.elim {c : Prop}
(or_ab : Or a b) (ac : a β c) (bc : b β c) :
c :=
match or_ab with
| inl ha => ac ha
| inr hb => bc hb
To use a proof of a β¨ b to prove a third thing (c), you must provide two functions: one showing a β c and another showing b β c.
In Lean, this is often handled via pattern matching (match), where you provide a case for inl and a case for inr.
Resolving Alternatives:
-- a or b, not a
-- proves b
-- a β¨ b, Β¬a β’ b
theorem Or.resolve_left
(or_ab : Or a b) (na : Not a) : b :=
or_ab.elim
(fun ha => na.elim ha)
(fun hb => hb)
-- a or b, not b
-- proves a
-- a β¨ b, Β¬b β’ a
theorem Or.resolve_right
(or_ab: Or a b) (nb : Not b) : a :=
or_ab.elim
(fun ha => ha)
(fun hb => nb.elim hb)
The theorems Or.resolve_left and Or.resolve_right show that if you have a β¨ b and you can prove the negation of one side (e.g., Β¬a), then the other side (b) must be true.
-- true or b
-- β’ β€ β¨ b
example : Or True b :=
Or.intro_left b True.intro
-- b or true
-- β’ b β¨ β€
example : Or b True :=
Or.intro_right b True.intro
-- a or b
-- proves b or a
-- a β¨ b β’ b β¨ a
theorem Or.symm
(or_ab : Or a b) : Or b a :=
or_ab.elim
(fun ha => Or.intro_right b ha)
(fun hb => Or.intro_left a hb)
-- not a or b, a
-- proves b
-- Β¬a β¨ b, a β’ b
theorem Or.neg_resolve_left
(or_nab : Or (Not a) b) (ha : a) : b :=
or_nab.elim
(fun na => na.elim ha)
(fun hb => hb)
-- a or not b, b
-- proves a
-- a β¨ Β¬b, b β’ a
theorem Or.neg_resolve_right
(or_anb : Or a (Not b)) (hb : b) : a :=
or_anb.elim
(fun ha => ha)
(fun nb => nb.elim hb)
This header covers logical bi-implication (logical equivalence), symbolized as β. In Lean 4, this represents the condition where two propositions, a and b, are essentially “if and only if” versions of each other.
Iff is defined as a structure containing two primary fields:
structure Iff (a b : Prop) : Prop where
intro ::
mp : a β b
mpr : b β a
mp (modus ponens): A proof of the forward implication, a β b.mpr (modus ponens reverse): A proof of the backward implication, b β a.The section demonstrates how to construct and deconstruct equivalence proofs:
a β b by providing two separate functions: one that transforms a proof of a into b, and another that transforms b into a.-- a implies b, b implies a
-- proves a iff b
-- a β b, b β a β’ a β b
example
(ab : a β b) (ba : b β a) : Iff a b :=
Iff.intro ab ba
Iff a b, you can extract the forward or backward implications using .mp or .mpr respectively.-- a iff b
-- proves a implies b
-- a β b β’ a β b
example (iff_ab : Iff a b) : a β b :=
iff_ab.mp
-- a iff b
-- proves b implies a
-- a β b β’ b β a
example (iff_ab : Iff a b) : b β a :=
iff_ab.mpr
Iff.refl) and that equivalence is transitive β if a β b and b β c, then a β c (Iff.trans).-- a iff a
-- β’ a β a
theorem Iff.refl (a : Prop) : Iff a a :=
Iff.intro (fun ha => ha) (fun ha => ha)
-- a iff b, b iff c
-- proves a iff c
-- a β b, b β c β’ a β c
theorem Iff.trans
(iff_ab : Iff a b) (iff_bc : Iff b c) :
Iff a c :=
Iff.intro
(fun ha => iff_bc.mp (iff_ab.mp ha))
(fun hc => iff_ab.mpr (iff_bc.mpr hc))
Iff.symm proves that if a β b, then b β a.-- a iff b
-- proves b iff a
-- a β b β’ b β a
theorem Iff.symm
(iff_ab : Iff a b) : Iff b a :=
Iff.intro iff_ab.mpr iff_ab.mp
This section links Iff to other logical concepts:
iff_iff_implies_and_implies formally proves that a β b is logically equivalent to a β b β§ b β a.-- (a iff b)
-- iff ((a implies b) and (b implies a))
-- β’ (a β b) β ((a β b) β§ (b β a))
theorem iff_iff_implies_and_implies :
Iff (Iff a b) (And (a β b) (b β a)) :=
Iff.intro
(fun iff_ab =>
And.intro iff_ab.mp iff_ab.mpr)
(fun and_ab_ba =>
Iff.intro and_ab_ba.left and_ab_ba.right)
iff_true_intro (if a is true, then a β β€) and iff_false_intro (if Β¬a is true, then a β β₯).-- a proves a iff true
-- a β’ a β β€
theorem iff_true_intro
(ha : a) : Iff a True :=
iff_of_true ha True.intro
-- not a
-- proves a iff false
-- Β¬a β’ a β β₯
theorem iff_false_intro
(na : Not a) : Iff a False :=
iff_of_false na (fun false => false)
(a β b) β (b β a).-- (a iff b) iff (b iff a)
-- β’ (a β b) β (b β a)
theorem Iff.comm :
Iff (Iff a b) (Iff b a) :=
Iff.intro Iff.symm Iff.symm
-- true iff true
-- β’ β€ β β€
example : Iff True True :=
Iff.intro
(fun _ => True.intro)
(fun _ => True.intro)
-- false iff false
-- β’ β₯ β β₯
example : Iff False False :=
Iff.intro
(fun false => false)
(fun false => false)
-- (a implies b) implies
-- (b implies a) implies c, a iff b
-- proves c
-- (a β b) β (b β a) β c, a β b β’ c
def Iff.elim
(ab_ba : (a β b) β (b β a) β c)
(iff_ab : Iff a b) : c :=
ab_ba iff_ab.mp iff_ab.mpr
-- a, b
-- proves a iff b
-- a, b β’ a β b
theorem iff_of_true
(ha : a) (hb : b) : Iff a b :=
Iff.intro (fun _ => hb) (fun _ => ha)
-- not a, not b
-- proves a iff b
-- Β¬a, Β¬b β’ a β b
theorem iff_of_false
(na : Not a) (nb : Not b) : Iff a b :=
Iff.intro
(fun ha => na.elim ha)
(fun hb => nb.elim hb)
-- a iff true
-- proves a
-- a β β€ β’ a
theorem of_iff_true
(iff_at : Iff a True) : a :=
iff_at.mpr True.intro
-- a iff false
-- proves not a
-- a β β₯ β’ Β¬a
theorem not_of_iff_false :
(Iff a False) β Not a := Iff.mp
-- (a and b) iff (b and a)
-- β’ (a β§ b) β (b β§ a)
theorem And.comm :
Iff (And a b) (And b a) :=
Iff.intro And.symm And.symm
-- (a or b) iff (b or a)
-- β’ (a β¨ b) β (b β¨ a)
theorem Or.comm : Iff (Or a b) (Or b a) :=
Iff.intro Or.symm Or.symm
-- a iff b
-- proves not a iff not b
-- a β b β’ Β¬a β Β¬b
theorem not_congr
(iff_ab : Iff a b) : Iff (Not a) (Not b) :=
Iff.intro
(fun na => na.imp iff_ab.mpr)
(fun nb => nb.imp iff_ab.mp)
-- not not not a iff not a
-- ⒠¬¬¬a β Β¬a
theorem not_not_not :
Iff (Not (Not (Not a))) (Not a) :=
Iff.intro
(fun nnna => nnna.imp not_not_intro)
(fun na => not_not_intro na)
-- (a iff b) iff (b implies a) and (a implies b)
-- β’ (a β b) β (b β a) β§ (a β b)
theorem iff_def' :
Iff (Iff a b) (And (b β a) (a β b)) :=
Iff.trans iff_iff_implies_and_implies And.comm
This header has a collection of proofs for classic logical laws. It uses the foundational tools defined in the previous headers to prove well-known identities from formal logic.
The questions are sourced from Theorem Proving in Lean 4 and demonstrate how to handle complex nested propositions using constructors like And.intro, Or.elim, and Iff.intro.
The examples can be grouped into several logical categories:
Commutativity and Associativity:
And and Or does not change the truth value (e.g., p β§ q β q β§ p).-- p and q iff q and p
-- β’ p β§ q β q β§ p
example : Iff (And p q) (And q p) :=
Iff.intro
(fun and_pq =>
And.intro and_pq.right and_pq.left)
(fun and_qp =>
And.intro and_qp.right and_qp.left)
-- p or q iff q or p
-- β’ p β¨ q β q β¨ p
example : Iff (Or p q) (Or q p) :=
Iff.intro
(fun or_pq => or_pq.elim
(fun hp => Or.intro_right q hp)
(fun hq => Or.intro_left p hq))
(fun or_qp => or_qp.elim
(fun hq => Or.intro_right p hq)
(fun hp => Or.intro_left q hp))
(p β¨ q) β¨ r β p β¨ (q β¨ r)).-- (p and q) and r iff p and (q and r)
-- β’ (p β§ q) β§ r β p β§ (q β§ r)
example :
Iff (And (And p q) r) (And p (And q r)) :=
Iff.intro
(fun and_pq_r =>
And.intro
and_pq_r.left.left
(And.intro
and_pq_r.left.right
and_pq_r.right))
(fun and_p_qr =>
And.intro
(And.intro
and_p_qr.left
and_p_qr.right.left)
and_p_qr.right.right)
-- (p or q) or r iff p or (q or r)
-- β’ (p β¨ q) β¨ r β p β¨ (q β¨ r)
example :
Iff (Or (Or p q) r) (Or p (Or q r)) :=
Iff.intro
(fun or_pq_r => or_pq_r.elim
(fun or_pq => or_pq.elim
(fun hp => Or.intro_left (Or q r) hp)
(fun hq =>
Or.intro_right
p
(Or.intro_left r hq)))
(fun hr =>
Or.intro_right p (Or.intro_right q hr)))
(fun or_p_qr => or_p_qr.elim
(fun hp =>
Or.intro_left r (Or.intro_left q hp))
(fun or_qr => or_qr.elim
(fun hq =>
Or.intro_left r (Or.intro_right p hq))
(fun hr =>
Or.intro_right (Or p q) hr)))
Distributivity: Demonstrates how And distributes over Or (p β§ (q β¨ r) β (p β§ q) β¨ (p β§ r)) and vice versa.
-- p and (q or r) iff (p and q) or (p and r)
-- β’ p β§ (q β¨ r) β (p β§ q) β¨ (p β§ r)
example :
Iff (And p (Or q r))
(Or (And p q) (And p r)) :=
Iff.intro
(fun p_qr => p_qr.right.elim
(fun hq =>
Or.intro_left
(And p r)
(And.intro p_qr.left hq))
(fun hr =>
Or.intro_right
(And p q)
(And.intro p_qr.left hr)))
(fun pq_pr => pq_pr.elim
(fun pq =>
And.intro
pq.left
(Or.intro_left r pq.right))
(fun pr =>
And.intro
pr.left
(Or.intro_right q pr.right)))
-- p or (q and r) iff (p or q) and (q or r)
-- β’ p β¨ (q β§ r) β (p β¨ q) β§ (p β¨ r)
example :
Iff
(Or p (And q r))
(And (Or p q) (Or p r)) :=
Iff.intro
(fun p_qr => p_qr.elim
(fun hp => And.intro
(Or.intro_left q hp)
(Or.intro_left r hp))
(fun qr => And.intro
(Or.intro_right p qr.left)
(Or.intro_right p qr.right)))
(fun pq_pr => pq_pr.left.elim
(fun hp => Or.intro_left (And q r) hp)
(fun hq => pq_pr.right.elim
(fun hp => Or.intro_left (And q r) hp)
(fun hr =>
Or.intro_right p (And.intro hq hr))))
De Morgan’s Laws: Specifically proves that the negation of a disjunction is equivalent to the conjunction of negations: Β¬(p β¨ q) β Β¬p β§ Β¬q.
-- not (p or q) iff not p and not q
-- β’ Β¬(p β¨ q) β Β¬p β§ Β¬q
example :
Iff (Not (Or p q)) (And (Not p) (Not q)) :=
Iff.intro
(fun npq => And.intro
(fun hp => npq (Or.intro_left q hp))
(fun hq => npq (Or.intro_right p hq)))
(fun np_nq => fun pq => pq.elim
(fun hp => np_nq.left hp)
(fun hq => np_nq.right hq))
-- not p or not q implies not (p and q)
-- β’ Β¬p β¨ Β¬q β Β¬(p β§ q)
example :
(Or (Not p) (Not q) β Not (And p q)) :=
fun np_nq => np_nq.elim
(fun np => fun pq => np pq.left)
(fun nq => fun pq => nq pq.right)
Implication Identities:
(p β (q β r)) β (p β§ q β r).-- (p implies (q implies r))
-- iff (p and q implies r)
-- β’ (p β (q β r)) β (p β§ q β r)
example :
Iff (p β (q β r)) (And p q β r) :=
Iff.intro
(fun pqr => fun pq => pqr pq.left pq.right)
(fun pq_r => fun hp => fun hq =>
pq_r (And.intro hp hq))
(p β q) β (Β¬q β Β¬p).-- (p implies q) implies (not q implies not p)
-- β’ (p β q) β (Β¬q β Β¬p)
example : (p β q) β (Not q β Not p) :=
fun pq => fun nq => fun hp => nq (pq hp)
(Β¬p β¨ q) β (p β q).-- (not p or q) implies (p implies q)
-- β’ (Β¬p β¨ q) β (p β q)
example : Or (Not p) q β (p β q) :=
fun np_q => fun hp => np_q.elim
(fun np => (np hp).elim)
(fun hq => hq)
Here is a proof of the Law of Non-Contradiction β Not (And p (Not p)) β showing that a proposition and its negation cannot both be true.
-- not (p and not p)
-- β’ Β¬(p β§ Β¬p)
example : Not (And p (Not p)) :=
fun p_np => p_np.right p_np.left
We also feature a proof for Not (Iff p (Not p)), which demonstrates that no proposition can be logically equivalent to its own negation.
-- not (p iff not p)
-- β’ Β¬(p β Β¬p)
example : Not (Iff p (Not p)) :=
fun p_np =>
have np := fun hp => (p_np.mp hp) hp
np (p_np.mpr np)
-- ((p or q) implies r)
-- iff (p implies r) and (q implies r)
-- β’ ((p β¨ q) β r) β (p β r) β§ (q β r)
example :
Iff (Or p q β r) (And (p β r) (q β r)) :=
Iff.intro
(fun pq_r => And.intro
(fun hp => pq_r (Or.intro_left q hp))
(fun hq => pq_r (Or.intro_right p hq)))
(fun pr_qr => fun pq => pq.elim
(fun hp => pr_qr.left hp)
(fun hq => pr_qr.right hq))
-- p and not q implies not (p implies q)
-- β’ p β§ Β¬q β Β¬(p β q)
example : And p (Not q) β Not (p β q) :=
fun p_nq => fun pq =>
p_nq.right (pq p_nq.left)
-- not p implies (p implies q)
-- β’ Β¬p β (p β q)
example : Not p β (p β q) :=
fun np => fun p => (np p).elim
-- p or false implies p
-- β’ p β¨ False β p
example : Iff (Or p False) p :=
Iff.intro
(fun pf => pf.elim
(fun hp => hp)
(fun false => false.elim))
(fun hp => Or.intro_left False hp)
-- p and false iff false
-- β’ p β§ False β False
example : Iff (And p False) False :=
Iff.intro
(fun pf => pf.right)
(fun false => false.elim)
This header defines the concept of propositional equality, which is used to state that two terms of the same type are identical. In Lean 4, this is implemented as an inductive type that centers on the principle of reflexivity.
Eq is defined using a single constructor:
inductive Eq : Ξ± β Ξ± β Prop where
| refl (a : Ξ±) : Eq a a
refl (a : Ξ±): This states that any element a is equal to itself.
Logical Meaning: Equality is defined by the fact that a = a is the only fundamental way to construct a proof of equality.
We build a toolkit for manipulating equalities through several key proofs:
Substitution (Eq.subst): This is the most critical property of equality. If you know a = b, and you have a property that is true for a, you can conclude that the same property is true for b.
-- a = b β’ f a = f b
theorem Eq.subst {motive : Ξ± β Prop}
(eq_ab : Eq a b) (motive_a : motive a) :
motive b :=
ndrec motive_a eq_ab
Symmetry and Transitivity:
Eq.symm: Proves that if a = b, then b = a.-- a = b β’ b = a
theorem Eq.symm
(eq_ab : Eq a b) : Eq b a :=
have eq_aa : Eq a a := Eq.refl a
subst (motive := fun x => Eq x a) eq_ab eq_aa
Eq.trans: Proves that if a = b and b = c, then a = c.-- a = b, b = c β’ a = c
theorem Eq.trans
(eq_ab : Eq a b) (eq_bc : Eq b c) :
Eq a c :=
subst (motive := fun x => Eq a x) eq_bc eq_ab
Congruence:
congrArg: If a = b, then applying the same function to both results in equal outputs (f(a) = f(b)).-- a = b β’ f a = f b
theorem congrArg
(f : Ξ± β Ξ²) (eq_ab: Eq a b) :
Eq (f a) (f b) :=
have eq_fa_fa : Eq (f a) (f a) :=
Eq.refl (f a)
Eq.subst
(motive := fun x => Eq (f a) (f x))
eq_ab
eq_fa_fa
congrFun: If two functions are equal (f = g), then applying them to the same argument results in equal outputs (f(a) = g(a)).-- f = g β’ f a = g a
theorem congrFun
{Ξ² : Ξ± β Sort _} {f g : (x : Ξ±) β Ξ² x}
(eq_fg : Eq f g) (a : Ξ±) : Eq (f a) (g a) :=
have eq_fa_fa : Eq (f a) (f a) :=
Eq.refl (f a)
Eq.subst
(motive := fun x => Eq (f a) (x a))
eq_fg
eq_fa_fa
congr: A combination proving that if f = g and a = b, then f(a) = g(b).-- f = g, a = b β’ f a = g b
theorem congr {f g : Ξ± β Ξ²} {a b : Ξ±}
(eq_fg : Eq f g) (eq_ab : Eq a b) :
Eq (f a) (g b) :=
have eq_fa_fb : Eq (f a) (f b) :=
congrArg f eq_ab
Eq.subst
(motive := fun x => Eq (f a) (x b))
eq_fg
eq_fa_fb
The section introduces a powerful tool called propext:
-- β’ a β b β a = b
axiom propext : (Iff a b) β Eq a b
This axiom states that if two propositions are logically equivalent (a β b), they are actually equal as values. This allows the user to use Iff.subst to swap equivalent propositions within a larger logical context.
-- a β b, p a β’ p b
theorem Iff.subst {p : Prop β Prop}
(iff_ab : Iff a b) (pa : p a) : p b :=
Eq.subst (propext iff_ab) pa
def id (a : Ξ±) : Ξ± := a
-- β’ (id a) = a
theorem id_eq (a : Ξ±) : Eq (id a) a :=
Eq.refl a
-- β’ a = (id a)
theorem eq_id (a : Ξ±) : Eq a (id a) :=
Eq.refl a
abbrev Eq.ndrec {motive : Ξ± β Sort _}
(m : motive a) (h : Eq a b) : motive b :=
h.rec m
This header defines the standard Boolean type and provides theorems to bridge the gap between computational Booleans and propositional logic. While propositions (Prop) are for mathematical statements, Bool is a concrete data type used for computation.
Bool is an inductive type with two constructors:
inductive Bool : Type where
| false : Bool
| true : Bool
export Bool (false true)
false: Representing the boolean false.true: Representing the boolean true.The section focuses on “reflecting” boolean values into propositional proofs. Since true and false are distinct constructors, Lean can prove they are not equal.
Discrimination Theorems:
eq_false_of_ne_true: Proves that if a boolean is not true, it must be false.-- Β¬(b = true) β’ b = false
theorem eq_false_of_ne_true
(neq_bt : Not (Eq b true)) : Eq b false :=
match b with
| false => Eq.refl false
| true =>
have eq_tt : Eq true true := Eq.refl true
neq_bt.elim eq_tt
eq_true_of_ne_false: Proves that if a boolean is not false, it must be true.-- Β¬(b = false) β’ b = true
theorem eq_true_of_ne_false
(neq_bf : Not (Eq b false)) : Eq b true :=
match b with
| true => Eq.refl true
| false =>
have eq_ff : Eq false false := Eq.refl false
neq_bf.elim eq_ff
These are proved using pattern matching on the variable b. In the case where b matches the constructor that was supposed to be “not” equal, a contradiction is derived.
Handling Contradictions:
Bool.noConfusion: This is a built-in Lean tool used in these proofs to show that different constructors (like true and false) can never be equal.
The theorems ne_false_of_eq_true and ne_true_of_eq_false use this to formally prove that if a boolean is true, it is logically impossible for it to also be false.
-- b = true β’ Β¬(b = false)
theorem ne_false_of_eq_true
(eq_b_true : Eq b true) :
Not (Eq b false) :=
match b with
| true => fun eq_true_false =>
Bool.noConfusion eq_true_false.Root
| false => Bool.noConfusion eq_b_true.Root
-- b = false β’ Β¬(b = true)
theorem ne_true_of_eq_false
(eq_b_false : Eq b false) :
Not (Eq b true) :=
match b with
| true => Bool.noConfusion eq_b_false.Root
| false => fun eq_false_true =>
Bool.noConfusion eq_false_true.Root
We include utility functions (Eq.Root and Eq.FromRoot) to convert between the user-defined Eq in the Basic namespace and Leanβs built-in equality (_root_.Eq). This allows the custom proofs to utilize standard library tools like noConfusion.
def Eq.Root
(eq_ab : Eq a b) : _root_.Eq a b :=
match eq_ab with
| refl a => _root_.Eq.refl a
def Eq.FromRoot
(req_ab : _root_.Eq a b) : Eq a b :=
match req_ab with
| _root_.Eq.refl a => Eq.refl a
This header defines Natural Numbers using Peano axioms and establishes the foundational properties of arithmetic and order within Lean 4. This section demonstrates how logical proofs scale from simple propositions to mathematical structures.
Natural numbers are defined as an inductive type with two constructors:
inductive Nat where
| zero : Nat
| succ : Nat β Nat
zero: The base case (0).succ: The successor function, where succ n represents n + 1.We define addition and multiplication recursively, followed by proofs of their properties:
Addition (add): Defined by recursing on the second argument.
-- n + m
def Nat.add (n m : Nat) : Nat :=
match m with
| zero => n
| succ m => succ (add n m)
n + 0 = n (add_zero) and 0 + n = n (zero_add).-- β’ n + 0 = n
theorem Nat.add_zero
(n : Nat) : Eq (add n zero) n :=
Eq.refl (add n zero)
-- β’ 0 + n = n
theorem Nat.zero_add
(n : Nat) : Eq (add zero n) n :=
match n with
| zero => Eq.refl zero
| succ n => congrArg succ (Nat.zero_add n)
add_comm proves that n + m = m + n using induction and the helper theorem succ_add.-- β’ n + m = m + n
theorem Nat.add_comm
(n m : Nat) : Eq (add n m) (add m n) :=
match n, m with
| n, zero => Eq.symm (Nat.zero_add n)
| n, succ m =>
(congrArg succ (add_comm n m)).trans
(succ_add m n).symm
Multiplication (mul): Defined as repeated addition.
-- n * m
def Nat.mul (n m : Nat) : Nat :=
match m with
| zero => zero
| succ m => add n (mul n m)
n * 0 = 0 (mul_zero), 0 * n = 0 (zero_mul), and n * 1 = n (mul_one).-- β’ n * 0 = 0
theorem Nat.mul_zero
(n : Nat) : Eq (mul n zero) zero :=
Eq.refl (mul n zero)
-- β’ 0 * n = 0
theorem Nat.zero_mul
(n : Nat) : Eq (mul zero n) zero :=
match n with
| zero => Eq.refl zero
| succ n =>
((zero_mul n).symm.trans
((zero_add (mul zero n)).symm.trans
(mul_succ zero n).symm)).symm
-- β’ n * 1 = n
theorem Nat.mul_one
(n : Nat) : Eq (mul n (succ zero)) n :=
Eq.refl (mul n (succ zero))
To determine if two numbers are equal computationally, we provide beq:
-- n == m
def Nat.beq : Nat β Nat β Bool
| zero, zero => true
| zero, succ _ => false
| succ _, zero => false
| succ n, succ m => beq n m
eq_of_beq_eq_true: Proves that if the boolean check n == m is true, then the propositional equality n = m holds.-- (n == m) = true β’ n = m
theorem Nat.eq_of_beq_eq_true
(eq_beq_nm_true : Eq (beq n m) true) :
Eq n m :=
match n, m with
| zero, zero => Eq.refl Nat.zero
| zero, succ _ =>
Bool.noConfusion eq_beq_nm_true.Root
| succ _, zero =>
Bool.noConfusion eq_beq_nm_true.Root
| succ n, succ m =>
have eq_nm : Eq n m :=
eq_of_beq_eq_true eq_beq_nm_true
congrArg succ eq_nm
ne_of_beq_eq_false: Proves that if n == m is false, then the propositions are logically distinct (Β¬(m = n)).-- (n == m) = false β’ Β¬(m = n)
theorem Nat.ne_of_beq_eq_false
(eq_beq_nm_false : Eq (beq n m) false) :
Not (Eq n m) :=
match n, m with
| zero, zero =>
Bool.noConfusion eq_beq_nm_false.Root
| zero, succ _ => fun eq_nm =>
Nat.noConfusion eq_nm.Root
| succ _, zero => fun eq_nm =>
Nat.noConfusion eq_nm.Root
| succ n, succ m => fun eq_nm =>
have neq_nm : Not (Eq n m) :=
ne_of_beq_eq_false eq_beq_nm_false
Nat.noConfusion
eq_nm.Root
(fun req_nm =>
neq_nm.elim (Eq.FromRoot req_nm))
β€)
πThe concept of “less than or equal to” is defined as an inductive proposition Nat.le:
-- n β€ m
inductive Nat.le (n : Nat) : Nat β Prop
| refl : Nat.le n n
| step : Nat.le n m β Nat.le n (succ m)
Definition: A number n is β€ m if m is either n itself (refl) or the successor of a number that n is already β€ to (step).
Theorems of Order:
zero_le: Proves 0 β€ n for all n.-- β’ 0 β€ n
theorem Nat.zero_le : (n : Nat) β LE.le zero n
| zero => Nat.le.refl
| succ n => Nat.le.step (zero_le n)
le_trans: Proves that if n β€ m and m β€ k, then n β€ k.-- n β€ m β’ m β€ k β n β€ k
theorem Nat.le_trans {n : Nat}
(le_nm : LE.le n m) : LE.le m k β LE.le n k
| Nat.le.refl => le_nm
| Nat.le.step le_mk =>
Nat.le.step (Nat.le_trans le_nm le_mk)
not_succ_le_self: A proof by induction showing that a number’s successor can never be less than or equal to the number itself (Β¬((n + 1) β€ n)).-- β’ Β¬((n + 1) β€ n)
theorem Nat.not_succ_le_self :
(n : Nat) β Not (LE.le (succ n) n)
| zero => not_succ_le_zero _
| succ n => fun le_succ_n_n =>
(not_succ_le_self n).elim
(le_of_succ_le_succ le_succ_n_n)
-- β’ (n + 1) + m = (n + m) + 1
theorem Nat.succ_add
(n m : Nat) :
Eq (add (succ n) m) (succ (add n m)) :=
match n, m with
| n, zero => Eq.refl (succ (add n zero))
| n, succ m => congrArg succ (succ_add n m)
-- β’ n + (m + 1) = (n + m) + 1
theorem Nat.add_succ
(n m : Nat) :
Eq (add n (succ m)) (succ (add n m)) :=
Eq.refl (succ (add n m))
-- β’ n * (m + 1) = n + (n * m)
theorem Nat.mul_succ
(n m : Nat) :
Eq (mul n (succ m)) (add n (mul n m)) :=
Eq.refl (add n (mul n m))
class LE (Ξ± : Type _) where
le : Ξ± β Ξ± β Prop
instance instLENat : LE Nat where
le := Nat.le
-- β’ (n + 1) β€ 0 β β₯
theorem Nat.not_succ_le_zero
(n : Nat) : LE.le (succ n) zero β False :=
have eq_m_zero_implies:
(m : Nat) β Eq m zero β
LE.le (succ n) m β False :=
fun _ eq_m_zero le_succ_n_m =>
le.casesOn
(motive := fun m _ =>
Eq m Nat.zero β False)
le_succ_n_m
(fun eq_succ_n_zero =>
Nat.noConfusion eq_succ_n_zero.Root)
(fun _ eq_succ_m_zero =>
Nat.noConfusion eq_succ_m_zero.Root)
eq_m_zero
have eq_zero_zero : Eq zero zero :=
Eq.refl zero
eq_m_zero_implies zero eq_zero_zero
-- β’ n β€ m β (n + 1) β€ (m + 1)
theorem Nat.succ_le_succ :
LE.le n m β LE.le (succ n) (succ m)
| Nat.le.refl => Nat.le.refl
| Nat.le.step le_nm =>
Nat.le.step (succ_le_succ le_nm)
-- n β€ m β’ n β€ m + 1
theorem Nat.le_succ_of_le
(le_nm : LE.le n m) : LE.le n (succ m) :=
Nat.le.step le_nm
-- β’ n β€ (n + 1)
theorem Nat.le_succ
(n : Nat) : LE.le n (succ n) :=
Nat.le.step Nat.le.refl
-- β’ n β€ n
theorem Nat.le_refl
(n : Nat) : LE.le n n :=
Nat.le.refl
-- n - 1
def Nat.pred : Nat β Nat
| zero => zero
| succ n => n
-- β’ n β€ m β (n - 1) β€ (m - 1)
theorem Nat.pred_le_pred :
{n m : Nat} β
LE.le n m β LE.le (pred n) (pred m)
| _, _, Nat.le.refl =>
Nat.le.refl
| zero, succ _, Nat.le.step le_zero_m =>
le_zero_m
| succ _, succ _, Nat.le.step le_succ_n_m =>
Nat.le_trans (le_succ _) le_succ_n_m
-- β’ (n + 1) β€ (m + 1) β n β€ m
theorem Nat.le_of_succ_le_succ :
LE.le (succ n) (succ m) β LE.le n m :=
pred_le_pred
This was a comprehensive, bottom-up reconstruction of propositional logic and discrete mathematics using the Lean 4 proof assistant. By defining fundamental logical constants and building toward complex recursive structures, we demonstrated how formal verification translates abstract mathematical concepts into rigorous code.
A Solid Foundation: We established the “ground floor” of logic by defining True, False, And, Or, and Not, proving that even the most basic logical rules can be formally verified from first principles.
Operational Equality: Through the Eq and Bool sections, we illustrated how to handle identity and the relationship between computational values and logical proofs.
Mathematical Sophistication: The concluding section on Nat (Natural Numbers) successfully applied these logical tools to define Peano arithmetic, demonstrating that operations like addition and multiplication, as well as relations like inequality, can be proven correct through induction.
Ultimately, this collection of proofs highlights the power of the Curry-Howard Correspondence, where logical propositions are treated as types and proofs are treated as programs. It provides a blueprint for how a computer can “understand” and verify the laws of logic and mathematics with absolute certainty.