Lean crash course from IntroToLean4
What this is
This page is a computational crash course generated from the Lean tutorial repo:
The goal is to make it easy to inspect:
- the actual Lean source,
- the actual terminal output from running each file,
- and what in the repo appears directly reusable for a fast Lean-onboarding workflow.
Adaptation summary
What worked after a one-time local build of the prerequisite modules:
a01BasicSyntaxa02Propositionsa03Quantifiersa04Equalitiesa05Functionsa06NaturalNumbersa07Choicea08Subtypesa09Relationsa10Equivalencea11Ordersa12EmptyUnit
What still breaks in the upstream repo state:
a13ProductSumimportsa13EmptyUnit, but the repo file isa12EmptyUnit.leana14ListsMonoidsrefers to names that are not in scope under the current setup
So for our purposes, the repo is already very usable for the first twelve chapters, but the last two need cleanup before they belong in a “just run it in sequence” workflow.
Chapter 1: Basic Syntax
Example 1
Status: OK
-- # Basic Syntax
-- This is a comment
/-
This is a multi-line comment.
It can span multiple lines.
Useful for longer explanations.
-/
-- The `#check` command is used to inspect the type of
-- an expression, definition, or theorem in Lean
#check 42
#check 'h'
#check ['h', 'e', 'l', 'l', 'o']
#check "hello"
#check true
#check Nat
-- The `#print` command allows you to inspect
-- the definition of a function, theorem, or
-- other named entity
#print Bool
#print Nat
#print Char
#print List
#print String
-- We cannot `#print Type` because this is a built-in concept
-- in Lean's logical foundation, not a user-defined
-- term or definition
-- #print Type[no output]Example 2
Status: OK
-- The `def` keyword is used to define a function or a value
-- Definition of number pi
def pi : Float := 3.1415926
-- Definition of the sum of two natural numbers
def sum (a b : Nat) : Nat := a + b
-- The `fun` keyword is used to define anonymous
-- functions (also known as lambda functions).
-- We will write `\lambda` to write λ
-- Two anonymous ways of defining
-- the sum of two natural numbers
#check fun (a b : Nat) => a + b
#check λ (a b : Nat) => a + b
-- The function type
-- if A and B are types, then A → B is another type,
-- the type of all mappings from A to B
-- We will write `\to` to write the arrowfun a b => a + b : Nat → Nat → Nat
fun a b => a + b : Nat → Nat → NatExample 3
Status: OK
-- The type of all mappings from Nat to Nat
#check Nat → Nat
-- An example of an element of the above type
#check sum 3
-- Two new ways of defining the sum of two natural numbers
-- Using `fun`
def sum2 : Nat → Nat → Nat := fun a b => a + b
-- The next approach utilizes the keywords `by`, `intro`, and `exact`
-- The `by` keyword signals that the function definition will
-- be constructed interactively using *tactics*
-- Tactics are commands that assist in building definitions
-- or proofs step by step.
-- To enter the interactive proof mode, we indent the text.
-- Specifically, the `intro` tactic
-- is used to introduce the function's arguments, while the
-- `exact` tactic is used to provide the precise value
-- that satisfies the goal; in this case, producing
-- a natural number
def sum3 : Nat → Nat → Nat := by
intro a b
exact a + b
-- The `cases` tactic splits the definition into
-- two branches based on the value of the input
-- We will use it to define the `Negation` function
-- for Booleans
def BoolNot : Bool → Bool := by
intro b
cases b
-- b = false
exact true
-- b = true
exact false
-- The `match` keyword is used for pattern matching
-- This is a more concise way to handle different
-- cases of the input
def BoolNot2 : Bool → Bool := by
intro b
match b with
| false => exact true
| true => exact false
-- The `let` keyword is used to define local variables
-- or terms within a proof or expression
def sphereVolume (r : Float) : Float :=
let pi : Float := 3.1415926
(4/3) * pi * r^3
-- The `#eval` command is used to evaluate an expression
-- and display its result
#eval sum 3 4
#eval (sum 3) 4
#eval (fun (a b : Nat) => a + b) 3 4
--
#eval pi
#eval Nat.succ 4
#eval UInt32.isValidChar 104
#eval 'h'.val
#eval String.mk ['h', 'e', 'l', 'l', 'o']
#eval "hello".data7
7
7
3.141593
5
true
104
.tmp_lean_crash_course/a01BasicSyntax_trial.lean:82:6: warning: `String.mk` has been deprecated: Use `String.ofList` instead
"hello"
.tmp_lean_crash_course/a01BasicSyntax_trial.lean:83:14: warning: `String.data` has been deprecated: Use `String.toList` instead
['h', 'e', 'l', 'l', 'o']Example 4
Status: OK
-- The keyword `variable` is used to declare variables
-- that can be used later in the code
-- These variables are implicitly available in the
-- context of any theorem, definition, or proof that follows
variable (m n : Nat)
#check m
-- We can also create namespaces and define variables within
-- them. Namespaces help organize code and can be collapsed
-- in the editor to improve readability.
-- Variables defined inside a namespace are only
-- accessible within that namespace
namespace WorkSpace
-- Define a natural number `r` with the value 27
def r : Nat := 27
-- The variable `r` is perfectly defined within the namespace
#eval r
end WorkSpace
-- Evaluating `r` outside the namespace will result
-- in an error
-- #eval r -- Error: unknown identifier 'r'.tmp_lean_crash_course/a01BasicSyntax_emit.lean:82:6: warning: `String.mk` has been deprecated: Use `String.ofList` instead
"hello"
.tmp_lean_crash_course/a01BasicSyntax_emit.lean:83:14: warning: `String.data` has been deprecated: Use `String.toList` instead
['h', 'e', 'l', 'l', 'o']
m : Nat
27Example 5
Status: OK
-- To access `r`, we must reference it using its namespace
#eval WorkSpace.r -- Output: 27
-- The `open` keyword is used to bring definitions,
-- theorems, or namespaces into the current scope
open WorkSpace
#eval r.tmp_lean_crash_course/a01BasicSyntax_final.lean:82:6: warning: `String.mk` has been deprecated: Use `String.ofList` instead
"hello"
.tmp_lean_crash_course/a01BasicSyntax_final.lean:83:14: warning: `String.data` has been deprecated: Use `String.toList` instead
['h', 'e', 'l', 'l', 'o']
m : Nat
27
27
27Chapter 2: Propositions
Example 1
Status: OK
-- # Propositions
-- `Prop` is the type of all propositions in Lean
-- This is a built-in concept
#check Prop
-- #print Prop -- Returns error
-- Propositions are statements that express a definite claim
-- Examples of propositions are
#check 2 + 2 = 4
#check 3 < 1
-- In Lean, a proposition is a type that represents a
-- logical statement. Thus, propositions are itself types
variable (P : Prop)
variable (h : P)
-- We need to understand `h` as a proof of `P`
#check h
-- A proposition is considered true if and only if there
-- exists a term of its type. In other words, if you can
-- construct a term `h : P`, then `P` is true.
-- If no such term exists, then `P` is false.Prop : Type
2 + 2 = 4 : Prop
3 < 1 : Prop
h : PExample 2
Status: OK
-- ## First theorem
-- To enter the interactive proof mode, we indent the text
theorem Th1 (h : P) : P := by
exact h
-- `Th1` has type `∀ (P : Prop), P → P`
#check Th1
-- `Th1 P` has type `P → P`
#check Th1 P
-- `Th1 P h` has type `P`
#check Th1 P hTh1 (P : Prop) (h : P) : P
Th1 P : P → P
Th1 P h : PExample 3
Status: OK
-- `Th1` adapts to the input type
variable (Q : Prop)
-- `Th1 Q` has type `Q → Q`
#check Th1 Q
-- Lean automatically generalizes our original
-- definition of `Th1` to its most general form
#print Th1
-- Second theorem with implicit variables
theorem Th2 {P : Prop} (h : P) : P := by
exact h
-- `Th2` has type `∀ {P : Prop}, P → P`
#check Th2
-- `Th2 h` has type `P`
#check Th2 hTh1 Q : Q → Q
theorem Th1 : ∀ (P : Prop), P → P :=
fun P h => h
Th2 {P : Prop} (h : P) : P
Th2 h : PExample 4
Status: OK
-- Third theorem applying a previous theorem
theorem Th3 {P : Prop} (h : P) : P := by
apply Th2
exact h
-- Fourth theorem using `have` to get an intermediate result
theorem Th4 {P : Prop} (h : P) : P := by
have h2 : P := by
exact h
exact h2
-- We can ask Lean which theorem to `apply`
theorem Th5 {P : Prop} (h : P) : P := by
apply?
-- or which `exact` result is needed
theorem Th6 {P : Prop} (h : P) : P := by
exact?
-- ### First example
-- Examples are anonymous theorems
example (a : P) : P := by
exact a
-- ### Sorry
-- `sorry` allows you to temporarily
-- skip the proof of a theorem or definition
/- The following theorem uses `sorry`
theorem Th7 (h : P) : P := by
sorry
-/
-- ## Logical Connectives[no new output]Example 5
Status: OK
-- ### Conjunction (∧): Logical And
#check And P Q
#check P ∧ Q
#print And
-- To prove a proposition of the form `P ∧ Q`
-- we need a proof of `P` and a proof of `Q`
theorem ThAndIn (hP : P) (hQ : Q) : P ∧ Q := by
exact And.intro hP hQ
-- From a proof of `P ∧ Q`, we can obtain a proof of `P`
theorem ThAndOutl (h : P ∧ Q) : P := by
exact h.left
-- We can also obtain a proof for `Q`
theorem ThAndOutr (h : P ∧ Q) : Q := by
exact h.right
-- ### Disjunction (∨): Logical Or
#check Or P Q
#check P ∨ Q
#print Or
-- From a proof of `P`, we can obtain a proof of `P ∨ Q`
theorem ThOrInl (h : P) : P ∨ Q := by
exact Or.inl h
-- From a proof of `Q`, we can obtain a proof of `P ∨ Q`
theorem ThOrInr (h : Q) : P ∨ Q := by
exact Or.inr h
-- Inductive types allow us to prove by `cases`
-- From a proof of `P ∨ Q`, we can obtain a proof of `Q ∨ P`
theorem ThOrCases (h : P ∨ Q) : Q ∨ P := by
cases h
-- Case 1
rename_i hP
exact Or.inr hP
-- Case 2
rename_i hQ
exact Or.inl hQ
-- We can alternatively use the keyword `Or.elim`
theorem ThOrCases2 (h : P ∨ Q) : Q ∨ P := by
apply Or.elim h
-- Case P
intro hP
exact Or.inr hP
-- Case Q
intro hQ
exact Or.inl hQ
-- ### Implication
#check P → QP → Q : PropExample 6
Status: OK
-- From a proof of `Q`, we can obtain a proof of `P → Q`
theorem ThImpIn (hQ : Q) : P → Q := by
intro _ -- No need to name the hypothesis
exact hQ
-- From a proof `P → Q` and a proof of `P`,
-- we can obtain a proof of `Q`
theorem ThModusPonens (h : P → Q) (hP : P) : Q := by
exact h hP
-- ### Double implication
#check Iff P Q
#check P ↔ Q
#print Iff
-- `P ↔ Q` is a shorthand for `(P → Q) ∧ (Q → P)`
-- From `P ↔ Q` we can derive `(P → Q) ∧ (Q → P)`
theorem ThIffOut (h : P ↔ Q) : (P → Q) ∧ (Q → P) := by
apply And.intro
-- Left
exact h.mp
-- Right
exact h.mpr
-- From `(P → Q)` and `(Q → P)` we can derive `P ↔ Q`
theorem ThIffIn (h1 : P → Q) (h2 : Q → P) : P ↔ Q := by
exact Iff.intro h1 h2
-- ### True
#check True
#print TrueTrue : Prop
inductive True : Prop
number of parameters: 0
constructors:
True.intro : TrueExample 7
Status: OK
-- `True` can always be obtained
theorem ThTrueIn : True := by
exact True.intro
-- An alternative way to obtain a
-- proof of `True` is to write `trivial`
#check trivial
-- `Trivial` is an element of type `True`
theorem ThTrivial : True := by
exact trivial
-- ### False
#check False
#print False
-- Having an element of type `False`
-- leads to a contradiction.
-- Having `False` implies any other proposition
-- False implies any proposition
theorem ThExFalso : False → P := by
intro h
exact False.elim h
-- ### Negation
#check Not P
#check ¬P
#print Not
-- `¬P` is defined as `P → False`
-- In order to prove `¬P`, we must assume `P`
-- and obtain a contradiction
theorem ThModusTollens (h1 : P → Q) (h2 : ¬Q) : ¬P := by
-- Assume P is true (to prove ¬P, which is P → False).
intro h3
-- Derive Q from P → Q and P.
have h4 : Q := by
exact h1 h3
-- Use ¬Q (Q → False) and Q to derive False.
exact h2 h4
-- ## Decidable propositions
-- A proposition is `decidable` if we can
-- constructively determine whether it
-- is true or false
#check Decidable
#print DecidableDecidable (p : Prop) : Type
inductive Decidable : Prop → Type
number of parameters: 1
constructors:
Decidable.isFalse : {p : Prop} → ¬p → Decidable p
Decidable.isTrue : {p : Prop} → p → Decidable pExample 8
Status: OK
-- True is decidable
def DecidableTrue : Decidable True := by
exact isTrue trivial
-- False is decidable
def DecidableFalse : Decidable False := by
exact isFalse id
-- If `P` is decidable, then `¬ P` is decidable
def DecidableNot {P : Prop} : Decidable P → Decidable (¬ P) := by
intro hP
match hP with
| isFalse hP => exact isTrue (fun h => False.elim (hP h))
| isTrue hP => exact isFalse (fun h => False.elim (h hP))
-- If `P` and `Q` are decidable, then `P ∧ Q` is decidable
def DecidableAnd {P Q : Prop} : Decidable P → Decidable Q → Decidable (P ∧ Q) := by
intro hP hQ
match hP, hQ with
| isFalse hP, _ => exact isFalse (fun h => hP h.left)
| _ , isFalse hQ => exact isFalse (fun h => hQ h.right)
| isTrue hP , isTrue hQ => exact isTrue (And.intro hP hQ)
-- If `P` and `Q` are decidable, then `P ∨ Q` is decidable
def DecidableOr {P Q : Prop} : Decidable P → Decidable Q → Decidable (P ∨ Q) := by
intro hP hQ
match hP, hQ with
| isTrue hP , _ => exact isTrue (Or.inl hP)
| _ , isTrue hQ => exact isTrue (Or.inr hQ)
| isFalse hP, isFalse hQ => exact isFalse (fun h => h.elim hP hQ)
-- If `P` and `Q` are decidable, then `P → Q` is decidable
def DecidableImplies {P Q : Prop} : Decidable P → Decidable Q → Decidable (P → Q) := by
intro hP hQ
match hP, hQ with
| isFalse hP , _ => exact isTrue (fun h => False.elim (hP h))
| _ , isTrue hQ => exact isTrue (fun _ => hQ)
| isTrue hP , isFalse hQ => exact isFalse (fun h => hQ (h hP))
-- If `P` and `Q` are decidable, then `P ↔ Q` is decidable
def DecidableIff {P Q : Prop} : Decidable P → Decidable Q → Decidable (P ↔ Q) := by
intro hP hQ
have hPtoQ : Decidable (P → Q) := DecidableImplies hP hQ
have hQtoP : Decidable (Q → P) := DecidableImplies hQ hP
match hPtoQ, hQtoP with
| isFalse hPtoQ, _ => exact isFalse (fun h => hPtoQ h.mp)
| _, isFalse hQtoP => exact isFalse (fun h => hQtoP h.mpr)
| isTrue hPtoQ, isTrue hQtoP => exact isTrue (Iff.intro hPtoQ hQtoP)
-- ## Classical Logic
-- We open the `Classical` namespace
open Classical
-- We use `Classical.em` to prove the excluded middle
theorem ThExcludedMiddle : P ∨ ¬P := by
exact em P
-- Classical Logic allows proofs by contradiction
theorem ThDoubNeg : P ↔ ¬¬P := by
apply Iff.intro
-- Implication P → ¬¬P
intro hP
intro hNP
exact hNP hP
-- Implication ¬¬P → P
intro hNNP
have hF : ¬ P → False := by
intro hNP
exact hNNP hNP
apply byContradiction hF
-- Exercises extracted from Daniel Clemente webpage
-- EN https://www.danielclemente.com/logica/dn.en.pdf
namespace a02Exercises
variable (A B C D I L M P Q R : Prop)[no new output]Example 9
Status: OK
theorem T51 (h1 : P) (h2 : P → Q) : P ∧ Q := by
apply And.intro
exact h1
exact h2 h1
theorem T52 (h1 : P ∧ Q → R) (h2 : Q → P) (h3: Q) : R := by
have h4 : P ∧ Q := by
apply And.intro
exact h2 h3
exact h3
exact h1 h4
theorem T53 (h1 : P → Q) (h2 : Q → R) : P → (Q ∧ R) := by
intro h
apply And.intro
exact h1 h
exact h2 (h1 h)
theorem T54 (h1 : P) : Q → P := by
intro _
exact h1
theorem T55 (h1 : P → Q) (h2 : ¬Q) : ¬P := by
intro h3
exact h2 (h1 h3)
theorem T56 (h1 : P → (Q → R)) : Q → (P → R) := by
intro hQ hP
exact h1 hP hQ
theorem T57 (h1 : P ∨ (Q ∧ R)) : P ∨ Q := by
cases h1
-- inl
rename_i hP
exact Or.inl hP
-- inr
rename_i hQR
exact Or.inr hQR.left
theorem T58 (h1 : (L ∧ M) → ¬P) (h2 : I → P) (h3 : M) (h4 : I) : ¬L := by
intro h5
have h6 : L ∧ M := by
exact And.intro h5 h3
have h7 : ¬P := by exact h1 h6
have h8 : P := by exact h2 h4
exact h7 h8
theorem T59 : P → P := by
intro h
exact h
theorem T510 : ¬ (P ∧ ¬P) := by
intro h
exact h.right h.left
theorem T511 : P ∨ ¬P := by
exact em P
theorem T512 (h1 : P ∨ Q) (h2 : ¬P) : Q := by
cases h1
-- inl
rename_i h1
exact False.elim (h2 h1)
-- inr
rename_i h1
exact h1
theorem T513 (h1 : A ∨ B) (h2 : A → C) (h3 : ¬D → ¬B) : C ∨ D := by
cases h1
-- inl
rename_i h1
exact Or.inl (h2 h1)
-- inr
rename_i h1
have h4 : D ∨ ¬D := by exact em D
cases h4
-- inl
rename_i h4
exact Or.inr h4
-- inr
rename_i h4
apply False.elim
exact h3 h4 h1
theorem T514 (h1 : A ↔ B) : (A ∧ B) ∨ (¬A ∧ ¬B) := by
rw [h1]
simp
exact em B
end a02Exercises[no new output]Chapter 3: Quantifiers
Example 1
Status: OK
-- # Quantifiers
-- To avoid highlighting unused variables
set_option linter.unusedVariables false
-- We next introduce an arbitrary type `A`
variable (A : Type)
-- ## Predicates
-- A predicate `P` on `A` is a an element of type
-- `A → Prop`
variable (P Q : A → Prop)
-- ### Examples of predicates
-- `False` predicate
def PFalse {A : Type} : A → Prop := fun _ => False
-- `True` predicate
def PTrue {A : Type} : A → Prop := fun _ => True[no output]Example 2
Status: OK
-- ### Operations on predicates
-- We can
-- Intersection of two predicates
def PAnd {A : Type} (P Q : A → Prop) : A → Prop := by
intro a
exact P a ∧ Q a
-- We introduce notation for the intersection (`\and`)
notation : 65 lhs:65 " ∧ " rhs:66 => PAnd lhs rhs
#check P ∧ Q
-- Union of two predicates
def POr {A : Type} (P Q : A → Prop) : A → Prop := by
intro a
exact P a ∨ Q a
-- We introduce notation for the union (`\or`)
notation : 65 lhs:65 " ∨ " rhs:66 => POr lhs rhs
#check P ∨ Q
-- Implication of two predicates
def PImplies {A : Type} (P Q : A → Prop) : A → Prop := by
intro a
exact P a → Q a
-- We introduce notation for the implication (`\to`)
notation : 65 lhs:65 " → " rhs:66 => PImplies lhs rhs
#check P → Q
-- Double Implication of two predicates
def PDImplies {A : Type} (P Q : A → Prop) : A → Prop := by
intro a
exact P a ↔ Q a
-- We introduce notation for the double implication (`\iff`)
notation : 65 lhs:65 " ↔ " rhs:66 => PDImplies lhs rhs
#check P ↔ QP ↔ Q : A → PropExample 3
Status: OK
-- Negation of a predicate
def PNot {A : Type} (P : A → Prop) : A → Prop := by
intro a
exact ¬ (P a)
-- We introduce notation for negation (`\not`)
notation : 65 "¬" rhs:66 => PNot rhs
#check ¬P
-- ## Universal quantifier `∀` (`\forall`)
-- The expression `∀ (a : A), P a` is a proposition
-- that asserts that `P a` is true for every `a : A`
#check ∀ (a : A), P a
-- The binding of `∀` does not require to
-- explicitly recall the type of the variable
#check ∀a, P a
-- The binding of `∀` can also be implicit
#check ∀ {a : A}, P a
-- To prove a statement of the form `∀ (a : A), P a`,
-- we typically use the `intro` tactic (or just write a
-- `lambda` function directly in term mode)
-- This introduces an arbitrary element `a` of type `A`
-- and requires us to prove `P a` for that arbitrary `a`
/- theorem T1 uses `sorry`
theorem T1 : ∀ (a : A), P a := by
intro a
sorry
-/[no new output]Example 4
Status: OK
-- On the other hand, if we have a hypothesis
-- `h : ∀ (a : A), P a` and we want to use it
-- for a specific value `a : A`, we can apply
-- `h` on `a` to get `P a`
variable (a : A)
variable (h : ∀ (a : A), P a)
#check (h a)
-- The `specialize` tactic allows us
-- to instantiate a general hypothesis with particular
-- values, making it easier to work with in our proof
theorem T2 (z : A) (h : ∀ (a : A), P a) : P z := by
specialize h z
exact h
-- The `specialize` tactic does not work when
-- the binding is implicit. We can explicitly
-- introduce the variable using `@`
theorem T2b (z : A) (h : ∀ {a : A}, P a) : P z := by
specialize @h z
exact h
-- ## Existential quantifier `∃` (`\exists`)
-- The expression `∃ (a : A), P xa` is a proposition that
-- asserts that `P a` is true for some `a : A`
#check ∃ (a : A), P a
-- The binding of `∃` does not require to
-- explicitly recall the type of the variable
#check ∃ a, P a∃ a, P a : PropExample 5
Status: OK
-- The binding of `∃` cannot be implicit
-- The following returns error
-- `#check ∃ {a : A}, P a`
-- There is, however, an inductive type associated
-- to the existential quatifier called `Exists`
#check Exists P
#print Exists
-- The single constructor, `Exists.intro`, constructs
-- a proof of `Exists P` given a witness `a : A` and
-- a proof that `a` satisfies `P`
theorem T3 (z : A) (h : P z) : ∃ (a : A), P a := by
exact Exists.intro z h
-- Since `Exists` is an inductive type, we can use `cases`
-- on proofs of this type, recovering the witness and
-- the proof that is satisfies the predicate `P`
variable (R : Prop)
theorem T4 (h1 : ∃ (a : A), P a) (h2 : ∀ (a : A), P a → R) : R := by
cases h1
rename_i a h3
specialize h2 a
exact h2 h3
-- Another alternative is to use `Exists.elim`,
-- the eliminator of the `Exists` type
theorem T5 (h1 : ∃ (a : A), P a) (h2 : ∀ (a : A), P a → R) : R := by
apply Exists.elim h1
exact h2
namespace a03Exercises
-- Exercises
open Classical
variable (a b c : A)
variable (R : Prop)[no new output]Example 6
Status: OK
-- theorem E1 : (∃ (a : A), R) → R := by
-- intro h
-- cases h
-- rename_i a h
-- exact h
-- theorem E2 (a : A) : R → (∃ (a : A), R) := by
-- intro h
-- apply Exists.intro a
-- exact h
-- theorem E3 : (∃ (a : A), P a ∧ R) ↔ (∃ (a : A), P a) ∧ R := by
-- apply Iff.intro
-- -- (∃ a, P a ∧ R) → (∃ a, P a) ∧ R
-- intro h
-- cases h
-- rename_i a h
-- apply And.intro
-- -- Left
-- apply Exists.intro a
-- exact h.left
-- -- Right
-- exact h.right
-- -- (∃ a, P a) ∧ R → ∃ a, P a ∧ R
-- intro h
-- cases h.left
-- rename_i a h1
-- apply Exists.intro a
-- apply And.intro
-- exact h1
-- exact h.right
-- theorem E4 : (∃ (a : A), (P ∨ Q) a) ↔ (∃ (a : A), P a) ∨ (∃ (a : A), Q a) := by
-- apply Iff.intro
-- -- (∃ a, (P ∨ Q) a) → (∃ a, P a) ∨ ∃ a, Q a
-- intro h1
-- cases h1
-- rename_i a h1
-- cases h1
-- -- inl
-- rename_i h1
-- apply Or.inl
-- apply Exists.intro a
-- exact h1
-- -- inr
-- rename_i h1
-- apply Or.inr
-- apply Exists.intro a
-- exact h1
-- -- ((∃ a, P a) ∨ ∃ a, Q a) → ∃ a, (P ∨ Q) a
-- intro h1
-- cases h1
-- -- inl
-- rename_i h1
-- cases h1
-- -- inl
-- rename_i a h1
-- apply Exists.intro a
-- exact Or.inl h1
-- -- inr
-- rename_i h1
-- cases h1
-- rename_i a h1
-- apply Exists.intro a
-- exact Or.inr h1
-- theorem E5 : (∀ (a : A), P a) ↔ ¬(∃ (a : A), (¬P) a) := by
-- apply Iff.intro
-- -- (∀ (a : A), P a) → ¬∃a, (¬P) a
-- intro h1 h2
-- cases h2
-- rename_i a h2
-- exact h2 (h1 a)
-- -- (¬∃a, (¬P) a) → ∀ (a : A), P a
-- intro h1 a
-- false_or_by_contra
-- rename_i h2
-- have h3 : ∃ (a : A), (¬P) a := by
-- apply Exists.intro a
-- exact h2
-- exact h1 h3
-- theorem E6 : (∃ (a : A), P a) ↔ ¬ (∀ (a : A), (¬P) a) := by
-- apply Iff.intro
-- -- (∃a, P a) → ¬∀ (a : A), (¬P) a
-- intro h1 h2
-- cases h1
-- rename_i a h1
-- specialize h2 a
-- exact h2 h1
-- -- (¬∀ (a : A), (¬P) a) → ∃a, P a
-- intro h1
-- false_or_by_contra
-- rename_i h2
-- have h3 : ∀ (a : A), (¬ P) a := by
-- intro a
-- false_or_by_contra
-- rename_i h3
-- have h4 : P a ∨ ¬ P a := em (P a)
-- cases h4
-- -- inl
-- rename_i h4
-- have h5 : ∃ (a : A), P a := Exists.intro a h4
-- exact h2 h5
-- -- inr
-- rename_i h4
-- exact h3 h4
-- exact h1 h3
-- theorem E7 : (¬∃ (a : A), P a) ↔ (∀ (a : A), (¬P) a) := by
-- apply Iff.intro
-- -- (¬∃ a, P a) → ∀ (a : A), (¬P) a
-- intro h1 a h2
-- have h3 : ∃ (a : A), P a := Exists.intro a h2
-- exact h1 h3
-- -- (∀ (a : A), (¬P) a) → ¬∃ a, P a
-- intro h1 h2
-- cases h2
-- rename_i a h2
-- specialize h1 a
-- exact h1 h2
-- theorem E8 : (¬∀ (a : A), P a) ↔ (∃ (a : A), (¬P) a) := by
-- apply Iff.intro
-- -- (¬∀ (a : A), P a) → ∃ a, (¬P) a
-- intro h1
-- false_or_by_contra
-- rename_i h2
-- have h3 : ∀ (a : A), P a := by
-- intro a
-- false_or_by_contra
-- rename_i h3
-- have h4 : ∃ (a : A), (¬ P) a := Exists.intro a h3
-- exact h2 h4
-- exact h1 h3
-- -- (∃ a, (¬P) a) → ¬∀ (a : A), P a
-- intro h1 h2
-- cases h1
-- rename_i a h1
-- specialize h2 a
-- exact h1 h2
-- theorem E9 : (∀ (a : A), P a → R) ↔ (∃ (a : A), P a) → R := by
-- apply Iff.intro
-- -- (∀ (a : A), P a → R) → (∃a, P a) → R
-- intro h1 h2
-- cases h2
-- rename_i a h2
-- exact (h1 a) h2
-- -- ((∃ a, P a) → R) → ∀ (a : A), P a → R
-- intro h1 a h2
-- have h3 : ∃ (a : A), P a := Exists.intro a h2
-- exact h1 h3
-- theorem E10 (a : A) : (∃ (a : A), P a → R) → (∀ (a : A), P a) → R := by
-- intro h1 h2
-- cases h1
-- rename_i a2 h1
-- specialize h2 a2
-- exact h1 h2
-- theorem E11 (a : A) : (∃ (a : A), R → P a) → (R → ∃ (a : A), P a) := by
-- intro h1 h2
-- cases h1
-- rename_i a2 h1
-- apply Exists.intro a2
-- exact h1 h2
-- end a03Exercises[no new output]Chapter 4: Equalities
Example 1
Status: OK
-- # Equalities
variable (X : Type)
variable (x y a b c d : X)
variable (P : X → Prop)[no output]Example 2
Status: OK
-- ## Equality
#check Eq
#check Eq x y
#check x = y
#print Eq
-- Negation of Equality `≠` (`\neq`)
#check Ne
#check Ne x y
#check x ≠ y
-- ## Reflexivity
-- `Eq.rfl` is the unique constructor for `Eq`
-- It returns an element of type `a = a`
-- It can also be used as `rfl`, where the variable `a`
-- is implicit
theorem TEqRfl {a : X} : a = a := by
exact rfl
-- Lean will allow `rfl` on any pair of terms that are
-- definitionally equal
theorem T1 : 2 + 2 = 4 := by
exact rfl
-- ## Symmetry
-- If we have `a = b` as a hypothesis, we can infer
-- `b = a` by applying the symmetric property of equality
#print Eq.symmtheorem Eq.symm.{u} : ∀ {α : Sort u} {a b : α}, a = b → b = a :=
fun {α} {a b} h => h ▸ rflExample 3
Status: OK
theorem TEqSymm (h : a = b) : (b = a) := by
exact Eq.symm h -- also (exact h.symm)
-- ## Transitivity
-- If we have `a = b` and `b = c` as a hypothesis, we can
-- infer `a = c` by applying the transitive property of
-- equality
#print Eq.trans
theorem TEqTrans (h1 : a = b) (h2 : b = c) : (a = c) := by
exact Eq.trans h1 h2 -- also (exact h1.trans h2)
-- ## Rewrite
-- We can use an equality to `rewrite` occurrences of either
-- side of the equation, either globally throughout an
-- expression or selectively in specific locations
-- We can also use `rw`
theorem TEqRw (h1 : a = b) : P b ↔ P a := by
apply Iff.intro
-- P b → P a
intro h2
rewrite [h1] -- rewrites the goal using h1
exact h2
-- P a → P b
intro h2
rw [h1] at h2 -- rewrites h2 using h1
exact h2
-- ## Calc
-- The `calc` command is used to perform calculations
-- or proofs by chaining together a series of equalities
-- or inequalities
theorem TCalc (h1 : a = b) (h2 : b = c) (h3: c = d) : (a = d) := by
calc
a = b := by rw [h1]
_ = c := by rw [h2]
_ = d := by rw [h3]
-- ## Types with meaningful equality
-- While equality is defined for all types, its meaning
-- depends on the type
-- #eval x = y -- Returns error
#eval 2 + 2 = 4 -- Returns truetrueExample 4
Status: OK
-- Some types have decidable equality, meaning there is
-- an algorithm to determine whether two terms of that
-- type are equal
#check DecidableEq
#print DecidableEq
-- We provide a proof that `Bool` has decidable
-- equality. In it we use the keyword `noConfusion`
-- It expresses the fact that different constructors
-- of an inductive type are disjoint and injective
def DecidableEqBool : DecidableEq Bool := by
intro a b
match a, b with
| false, false => exact isTrue rfl
| false, true => exact isFalse (fun h => Bool.noConfusion h)
| true , false => exact isFalse (fun h => Bool.noConfusion h)
| true , true => exact isTrue rfl
-- Other examples of types with decidable equality
#check Nat.decEq
#check Int.decEq
#check String.decEq
-- The following function recieves two natural
-- numbers `n` and `m` and returns `true` if they
-- are equal and `false` otherwise
-- It uses the `by_cases` tactic
def Charp : Nat → Nat → Bool := by
intro n m
by_cases n = m
-- Case n = m
exact true
-- Case n ≠ m
exact false
-- This is an alternative description using
-- `if ... then ... else`
def Charp2 : Nat → Nat → Bool :=
fun n m => if n = m then true else false[no new output]Example 5
Status: OK
-- In general equality in an arbitrary type is
-- non necessarily computable. Thus, the above
-- function in an arbitrary type is marked as
-- `noncomputable`
noncomputable def Charpoint {A : Type} : A → A → Bool := by
intro a b
by_cases a = b
-- Case a = b
exact true
-- Case a ≠ b
exact false
-- To avoid the above modifier, we have to
-- explicitly assume that the arbitrary type `A`
-- has decidable equality
def Charpoint2 {A : Type} [DecidableEq A] : A → A → Bool :=
fun n m => if n = m then true else false
-- In `Prop` equality is logical equivalence (`↔`)
-- Equality in `Prop` is not decidable
#check propext
#print propext
-- `propext` is an axiom
-- Axioms are assumed by definition,
-- rather than being derived from existing theorems
theorem TEqProp {Q : Prop} : (Q ∧ True) = Q := by
apply propext
apply Iff.intro
-- Q ∧ True → Q
intro h2
exact h2.left
-- Q → Q ∧ True
intro h2
apply And.intro
exact h2
trivial
-- We can always check the axioms on which a theorem
-- relies upon using `#print axioms`
#print axioms TEqProp'TEqProp' depends on axioms: [propext]Chapter 5: Functions
Example 1
Status: OK
-- # Functions
-- Declare foue arbitrary types `A`, `B`, `C` and `D`
variable (A B C D : Type)[no output]Example 2
Status: OK
-- Check the type `A → B` of all functions from `A` to `B`
-- `A` is the domain and `B` the codomain
#check A → B
-- Declare a mapping `f`
variable (f : A → B)
-- Declare an element `a` of type `A`
variable (a : A)A → B : TypeExample 3
Status: OK
-- Apply the function `f` to `a`
-- This is an element of type `B`
#check f a
-- ## Equality
-- Two functions `f, g : A → B` are equal if and only if
-- they produce the same output for every input,
-- meaning that for all `a : A`, we have `f a = g a`
theorem TEqApl : f = g ↔ ∀ (a : A), f a = g a := by
apply Iff.intro
-- f = g → ∀ (a : A), f a = g a
intro h a
exact congrFun h a
-- (∀ (a : A), f a = g a) → f = g
intro h
exact funext h
-- ## Composition
-- If `f : A → B` and `g : B → C` are functions,
-- then its composition, written `g ∘ f` is an
-- element of type `A → C`
variable (g : B → C)
#check g ∘ f
-- Composition of functions is associative
theorem TCompAss {f : A → B} {g : B → C} {h : C → D} :
h ∘ (g ∘ f) = (h ∘ g) ∘ f := by
funext a
exact rfl
-- ## The identity function
#print id
-- We can disable the automatic insertion of implicit
-- parameters by using `@`
#check @id Adef id.{u} : {α : Sort u} → α → α :=
fun {α} a => a
id : A → AExample 4
Status: OK
-- The identity function is a neutral element
-- for composition, both on the left and on the right
theorem TIdNeutral : (f ∘ id = f) ∧ (id ∘ f = f) := by
apply And.intro
-- f ∘ id = f
funext a
exact rfl
-- id ∘ f = f
funext a
exact rfl
namespace Inj
-- Definition of injective function
def injective {A B : Type} (f : A → B) : Prop :=
∀{a1 a2 : A}, (f a1 = f a2) → (a1 = a2)
-- Definition of monomorphism
def monomorphism {A B : Type} (f : A → B) : Prop :=
∀{C : Type}, ∀{g h : C → A}, f∘g = f∘h → g = h
-- Left inverse
def hasleftinv {A B : Type} (f : A → B) : Prop :=
∃ (g : B → A), g∘f = id[no new output]Example 5
Status: OK
-- The identity is injective
theorem TIdInj : injective (@id A) := by
-- rw [injective] -- rw to recover the definition
intro a1 a2 h
calc
a1 = id a1 := by exact rfl
_ = id a2 := by exact h
_ = a2 := by exact rfl
-- The identity is a monomorphism
theorem TIdMon : monomorphism (@id A) := by
-- rw [monomorphism] -- rw to recover the definition
intro C g h h1
calc
g = id ∘ g := by exact rfl
_ = id ∘ h := by exact h1
_ = h := by exact rfl
-- The identity has a left inverse
theorem TIdHasLeftInv : hasleftinv (@id A) := by
-- rw [hasleftinv] -- rw to recover the definition
apply Exists.intro id
exact rfl
-- ## Exercises
namespace a05InjExercises
-- Negation of injective
theorem TNegInj {A B : Type} {f: A → B} : ¬ (injective f) ↔ ∃ (a1 a2 : A),
f a1 = f a2 ∧ a1 ≠ a2 := by
-- sorry
apply Iff.intro
-- ¬injective f → ∃ a1 a2, f a1 = f a2 ∧ a1 ≠ a2
intro h1
rw [injective] at h1
false_or_by_contra
rename_i h2
have h3 : ∀ {a1 a2 : A}, f a1 = f a2 → a1 = a2 := by
intro a1 a2 h3
false_or_by_contra
rename_i h4
have h5 : ∃ (a1 a2 : A), f a1 = f a2 ∧ a1 ≠ a2 := by
apply Exists.intro a1
apply Exists.intro a2
apply And.intro
exact h3
exact h4
exact h2 h5
exact h1 h3
-- (∃ a1 a2, f a1 = f a2 ∧ a1 ≠ a2) → ¬injective f
intro h1
cases h1
rename_i a1 h1
cases h1
rename_i a2 h1
intro h
rw [injective] at h
specialize h h1.left
exact h1.right h
-- The composition of injective functions is injective
theorem TCompInj {A B : Type} {f : A → B} {g : B → C} (h1 : injective f) (h2 : injective g) :
injective (g∘f) := by
-- sorry
intro a1 a2 h3
specialize h2 h3
exact h1 h2
-- If the composition (g∘f) is injective, then f is injective
theorem TCompRInj {A B : Type} {f : A → B} {g : B → C} (h1: injective (g∘f)) : (injective f) := by
intro a1 a2 h
have h2 : g (f a1) = g (f a2) := by
exact congrArg g h
exact h1 h2
-- Injective and Monomorphisms are equivalent concepts
theorem TCarMonoInj {A B : Type} {f : A → B} : injective f ↔ monomorphism f := by
apply Iff.intro
-- injective f → monomorphism f
intro h1
intro C g h h2
funext c
have h3 : f (g c) = f (h c) := by
calc
f (g c) = (f ∘ g) c := by exact rfl
_ = (f ∘ h) c := by exact congrFun h2 c
_ = f (h c) := by exact rfl
exact h1 h3
-- monomorphism f → injective f
intro h1
intro a1 a2 h2
rw [monomorphism] at *
let g : Bool → A := by
intro _
exact a1
let h : Bool → A := by
intro _
exact a2
have h3 : f ∘ g = f ∘ h := by
funext z
calc
(f ∘ g) z = f a1 := by exact rfl
_ = f a2 := by exact h2
_ = (f ∘ h) z := by exact rfl
specialize h1 h3
calc
a1 = g true := by exact rfl
_ = h true := by exact congrFun h1 true
_ = a2 := by exact rfl
-- If a function has left inverse then it is injective
theorem THasLeftInvtoInj {A B : Type} {f : A → B} : hasleftinv f → injective f := by
intro h1 a1 a2 h2
cases h1
rename_i g h1
calc
a1 = id a1 := by exact rfl
_ = (g ∘ f) a1 := by exact congrFun h1.symm a1
_ = g (f a1) := by exact rfl
_ = g (f a2) := by exact congrArg g h2
_ = (g ∘ f) a2 := by exact rfl
_ = id a2 := by exact congrFun h1 a2
_ = a2 := by exact rfl
end a05InjExercises
end Inj
namespace Surj
-- Definition of surjective function
def surjective {A B : Type} (f : A → B) : Prop :=
∀{b : B}, ∃ (a : A), f a = b[no new output]Example 6
Status: OK
-- Definition of epimorphism
def epimorphism {A B : Type} (f : A → B) : Prop :=
∀{C : Type}, ∀{g h : B → C}, g∘f = h∘f → g = h
-- Right inverse
def hasrightinv {A B : Type} (f : A → B) : Prop :=
∃ (g : B → A), f∘ g = id[no new output]Example 7
Status: OK
-- The identity is surjective
theorem TIdSurj : surjective (@id A) := by
-- rw [surjective] -- rw to recover the definition
intro a
apply Exists.intro a
exact rfl
-- The identity is an epimorphism
theorem TIdMon : epimorphism (@id A) := by
-- rw [epimorphism] -- rw to recover the definition
intro C g h h1
calc
g = g ∘ id := by exact rfl
_ = h ∘ id := by exact h1
_ = h := by exact rfl
-- The identity has a right inverse
theorem TIdHasRightInv : hasrightinv (@id A) := by
-- rw [hasrightinv] -- rw to recover the definition
apply Exists.intro id
exact rfl
-- ## Exercises
namespace a05SurjExercises
-- Negation of surjective
theorem TNegSurj {A B : Type} {f: A → B} : ¬ (surjective f) ↔ ∃ (b : B), ∀ (a : A), f a ≠ b := by
apply Iff.intro
-- ¬surjective f → ∃ b, ∀ (a : A), f a ≠ b
intro h1
rw [surjective] at h1
false_or_by_contra
rename_i h2
have h3 : ∀{b : B}, ∃ (a : A), f a = b := by
intro b
false_or_by_contra
rename_i h4
have h5 : ∃ (b : B), ∀ (a : A), f a ≠ b := by
apply Exists.intro b
intro a
false_or_by_contra
rename_i h5
have h6 : ∃ (a : A), f a = b := by
exact Exists.intro a h5
exact h4 h6
exact h2 h5
exact h1 h3
-- (∃ b, ∀ (a : A), f a ≠ b) → ¬surjective f
intro h1
cases h1
rename_i b h1
intro h2
have h3 : ∃ (a : A), f a = b := h2
cases h3
rename_i a h3
specialize h1 a
exact h1 h3
-- The composition of surjective functions is surjective
theorem TCompSurj {A B : Type} {f : A → B} {g : B → C} (h1 : surjective f)
(h2 : surjective g) : surjective (g∘f) := by
intro c
have h3 : ∃ (b : B), g b = c := h2
cases h3
rename_i b h3
have h4 : ∃ (a : A), f a = b := h1
cases h4
rename_i a h4
apply Exists.intro a
calc
(g ∘ f) a = g (f a) := by exact rfl
_ = g b := by exact congrArg g h4
_ = c := by exact h3
-- If the composition (g∘f) is surjective, then g is surjective
theorem TCompLSurj {f : A → B} {g : B → C} (h1: surjective (g∘f))
: (surjective g) := by
intro c
have h2 : ∃ (a : A), (g ∘ f) a = c := h1
cases h2
rename_i a h2
apply Exists.intro (f a)
exact h2
-- Surjective and Epimorphism are equivalent concepts
theorem TCarEpiSurj {A B : Type} {f : A → B} : surjective f ↔ epimorphism f := by
apply Iff.intro
-- surjective f → epimorphism f
intro h1
intro C g h h2
funext b
have h3 : ∃ (a : A), f a = b := h1
cases h3
rename_i a h3
calc
g b = g (f a) := by exact congrArg g h3.symm
_ = (g ∘ f) a := by exact rfl
_ = (h ∘ f) a := by exact congrFun h2 a
_ = h (f a) := by exact rfl
_ = h b := by exact congrArg h h3
-- epimorphism f → surjective f
intro h1 b
rw [epimorphism] at h1
false_or_by_contra
rename_i h2
let g : B → Prop := by
intro z
exact ∃ (a : A), f a = z
let h : B → Prop := by
intro _
exact True
have h3 : g ∘ f = h ∘ f := by
funext a
apply propext
apply Iff.intro
-- (g ∘ f) a → (h ∘ f) a
intro _
exact trivial
-- (h ∘ f) a → (g ∘ f) a
intro _
apply Exists.intro a
exact rfl
have h4 : g = h := by exact h1 h3
have h5 : g b = h b := by exact congrFun h4 b
have h6 : True := trivial
have h7 : h b = True := by exact rfl
have h8 : g b = ∃ (a : A), f a = b := by exact rfl
rw [h7.symm, h5.symm, h8] at h6
exact h2 h6
-- If a function has right inverse then it is surjective
theorem THasRightInvtoInj {A B : Type} {f : A → B} : hasrightinv f → surjective f := by
intro h b
cases h
rename_i g h
apply Exists.intro (g b)
calc
f (g b) = (f ∘ g) b := by exact rfl
_ = id b := by exact congrFun h b
_ = b := by exact rfl
end a05SurjExercises
end Surj[no new output]Example 8
Status: OK
-- namespace Bij
-- open Surj Inj a05InjExercises a05SurjExercises[no new output]Example 9
Status: OK
-- -- Definition of bijective function
-- def bijective {A B : Type} (f : A → B) : Prop :=
-- injective f ∧ surjective f
-- Definition of isomorphism
def isomorphism {A B : Type} (f : A → B) : Prop :=
∃ (g : B → A), g∘f = id ∧ f∘g = id[no new output]Example 10
Status: OK
-- -- The identity is bijective
-- theorem TIdBij : bijective (@id A) := by
-- -- rw [bijective] -- rw to recover the definition
-- apply And.intro
-- exact TIdInj A
-- exact TIdSurj A
-- -- The identity is an isomorphism
-- theorem TIdMon : isomorphism (@id A) := by
-- rw [isomorphism] -- rw to recover the definition
-- apply Exists.intro id
-- apply And.intro
-- exact rfl
-- exact rfl
-- -- ## Exercises
-- namespace a05BijExercises
-- -- The composition of bijective functions is bijective
-- theorem TCompBij {A B : Type} {f : A → B} {g : B → C} (h1 : bijective f)
-- (h2 : bijective g) : bijective (g∘f) := by
-- rw [bijective] at *
-- apply And.intro
-- apply TCompInj
-- exact h1.left
-- exact h2.left
-- apply TCompSurj
-- exact h1.right
-- exact h2.right
-- -- A function is an isomorphism if and only if
-- -- it has left and right inverse
-- theorem TCarIso {A B : Type} {f : A → B} : isomorphism f ↔ (hasleftinv f ∧ hasrightinv f) := by
-- apply Iff.intro
-- -- isomorphism f → hasleftinv f ∧ hasrightinv f
-- intro h
-- cases h
-- rename_i g h1
-- apply And.intro
-- -- hasleftinv f
-- exact Exists.intro g h1.left
-- -- hasrightinv f
-- exact Exists.intro g h1.right
-- -- hasleftinv f ∧ hasrightinv f → isomorphism f
-- intro ⟨h1, h2⟩
-- cases h1
-- rename_i g h1
-- cases h2
-- rename_i h h2
-- have h3 : g = h := by
-- calc
-- g = g ∘ id := by exact rfl
-- _ = g ∘ (f ∘ h) := by exact congrArg (Function.comp g) h2.symm
-- _ = (g ∘ f) ∘ h := by exact rfl
-- _ = id ∘ h := by exact congrFun (congrArg Function.comp h1) h
-- _ = h := by exact rfl
-- apply Exists.intro g
-- apply And.intro
-- exact h1
-- rw [h3]
-- exact h2
-- -- Every isomorphism is bijective
-- theorem TCarIsotoBij {A B : Type} {f : A → B} : isomorphism f → bijective f := by
-- intro h1
-- have h2 : hasleftinv f := by exact (TCarIso.mp h1).left
-- have h3 : hasrightinv f := by exact (TCarIso.mp h1).right
-- have h4 : injective f := by exact THasLeftInvtoInj h2
-- have h5 : surjective f := by exact THasRightInvtoInj h3
-- exact And.intro h4 h5
-- end a05BijExercises
-- end Bij[no new output]Chapter 6: Natural Numbers
Example 1
Status: OK
-- # Natural Numbers
import a05Functions
open Inj
-- The type of Natural Numbers `Nat`
#check Nat
#print Nat
-- Lean comes with the `Nat` type already
-- implemented, along with many theorems related
-- to natural numbers. However, to gain a deeper
-- understanding of how natural numbers can be
-- constructed and reasoned about, we will define
-- our own custom type, which we will call `N`
inductive N : Type where
| z : N
| s : N → N
deriving ReprNat : Type
inductive Nat : Type
number of parameters: 0
constructors:
Nat.zero : Nat
Nat.succ : Nat → NatExample 2
Status: OK
#check N
#print N
-- According to our definition, we have defined
-- the structure (N, z, s), where `z`
-- (representing zero) is an element of type `N`
-- and `s` (representing the successor) is a
-- function from `N` to `N`
#check N.z
#check N.s
-- To work with `N` without needing to prefix everything with `N.`,
-- we can open the namespace to bring its notation into scope
open NN : Type
inductive N : Type
number of parameters: 0
constructors:
N.z : N
N.s : N → N
N.z : N
N.s : N → NExample 3
Status: OK
#check z
#check s
-- ## Cases
-- Let's define a function from `N` to `Bool` by `cases`.
-- The function will compare an element of type `N` with zero
-- If they are equal, it will return `true`
-- If they are different, it will return `false`
def Eqzero : N → Bool := by
intro n
cases n
-- Case zero
exact true
-- Case successor
exact false
-- ## Match
-- We will define an alternative to `Eqzero`
-- using the keyword `match` for pattern matching
def Eqzero2 : N → Bool := by
intro n
match n with
| z => exact true
| s _ => exact false
-- ## Injection
-- Note that the type `N` gives us a
-- Dedekind–Peano algebra. We can think of this
-- structure as the free algebra generated by a
-- constant `z` and a unary operation `s`.
-- In this setup, `z` can never be equal to
-- `s n` for any `n : N`.
theorem TZInj : ∀ {n : N}, z ≠ s n := by
intro n
intro h
cases h
-- Similarly, the successor function `s` is
-- injective. For this we use the tactic
-- `injection` which states that constructors
-- of inductive data types are injective
theorem TSuccInj : injective s := by
intro n m h
injection h
-- ## noConfusion
-- We can also apply the `noConfusion` principle
theorem TSuccInjAlt : injective s := by
intro n m h
exact N.noConfusion h id
-- ## Induction
-- Let's prove some theorems about the type `N`.
-- The proofs will be carried out by **induction**.
-- The `induction` tactic can be used on any inductive type
theorem TInd {P : N → Prop} (h0 : P z) (hi : ∀ (n : N), P n → P (s n)) : ∀ (n : N), P n := by
intro n
induction n
-- Base case: `z`
exact h0
-- Inductive step: assume the property holds for `n`,
-- and prove it for `s n`
rename_i n hn
exact (hi n) hn
-- ## Recursion[no new output]Example 4
Status: OK
-- ### Maximum
-- Recursive definition of the maximum of two natural numbers
def maxi : N → N → N := by
intro n m
match n, m with
| z, m => exact m
| n, z => exact n
| s n', s m' => exact s (maxi n' m')
-- ### Minimum
-- Recursive definition of the minimumm of two natural numbers
def mini : N → N → N := by
intro n m
match n, m with
| z, _ => exact z
| _, z => exact z
| s n', s m' => exact s (mini n' m')
-- ### Addition
-- We define the addition of natural numbers recursively
-- Note that the recursion is on the first argument
def Addition : N → N → N := by
intro n m
cases n with
| z => exact m
| s n => exact s (Addition n m)
-- Notation for Addition
notation : 65 lhs:65 " + " rhs:66 => Addition lhs rhs[no new output]Example 5
Status: OK
-- ### Fibonacci
-- We define the Fibonacci function recursively
def Fib : N → N := by
intro n
match n with
| z => exact z
| s z => exact (s z)
| s (s n) => exact n + (s n)
def four : N := s (s (s (s z)))
#eval Fib (four)
-- ### Multiplication
-- We define the multiplication of natural numbers recursively
-- Note that the recursion is on the first argument
def Multiplication : N → N → N := by
intro n m
cases n with
| z => exact z
| s n => exact (Multiplication n m) + m
-- Notation for Multiplication
notation : 70 lhs:70 " * " rhs:71 => Multiplication lhs rhsN.s (N.s (N.s (N.s (N.s (N.z)))))Example 6
Status: OK
-- #### Factorial
-- We define the factorial function recursively
def Fact : N → N := by
intro n
cases n with
| z => exact (s z)
| s n => exact (s n) * (Fact n)
def three : N := s (s (s z))
#eval Fact (three)
-- ## Decidable Equality
-- The recursive nature of `N` allows us to prove
-- that they have a decidable equality
def instDecidableEqN : DecidableEq N := by
intro n m
match n, m with
| z, z => exact isTrue rfl
| z, s _ => exact isFalse (by intro h; cases h)
| s _, z => exact isFalse (by intro h; cases h)
| s n', s m' =>
match instDecidableEqN n' m' with
| isTrue h => exact isTrue (congrArg s h)
| isFalse h => exact isFalse (fun h' => N.noConfusion h' (fun h'' => h h''))
namespace a06Exercises
-- Prove that no natural number is equal
-- to its own successor
theorem TInjSucc {n : N} : ¬ (n = s n) := by
-- We proceed by induction on `n`
induction n
-- Base case
intro h
cases h
-- Inductive step
rename_i n hi
intro h
injection h with h
exact hi h
-- ## Maximum
-- `Max (z, n) = n`
theorem TMaxzL : ∀ {n : N}, (maxi z n) = n := by
intro n
cases n
-- z
exact rfl
-- s n
exact rfl
-- `Max (n, z) = n`
theorem TMaxzR : ∀ {n : N}, (maxi n z) = n := by
intro n
cases n
-- z
exact rfl
-- s n
exact rfl
-- `Max (n, m) = Max (m, n)`
theorem TMaxComm : ∀ {n m : N}, (maxi n m) = (maxi m n) := by
intro n m
match n, m with
| z, _ => rw [TMaxzL, TMaxzR]
| _, z => rw [TMaxzL, TMaxzR]
| (s n'), (s m') => rw [maxi, congrArg s (TMaxComm), maxi]
-- `Max (n, m) = n ∨ Max (n, m) = m`
theorem TMaxOut : ∀ {n m : N}, ((maxi n m) = n) ∨ ((maxi n m) = m) := by
intro n m
match n, m with
| z, _ => exact Or.inr TMaxzL
| _, z => exact Or.inl TMaxzR
| (s n'), (s m') => match (@TMaxOut n' m') with
| Or.inl h => exact Or.inl (congrArg s h)
| Or.inr h => exact Or.inr (congrArg s h)
-- `Max (n, n) = n`
theorem TMaxIdpt : ∀ {n : N}, maxi n n = n := by
intro n
match (@TMaxOut n n) with
| Or.inl h => exact h
| Or.inr h => exact h
-- ## Minimum
-- `Min (z, n) = z`
theorem TMinzL : ∀ {n : N}, (mini z n) = z := by
intro n
cases n
-- z
exact rfl
-- s n
exact rfl
-- `Min (n, z) = z`
theorem TMinzR : ∀ {n : N}, (mini n z) = z := by
intro n
cases n
-- z
exact rfl
-- s n
exact rfl
-- `Min (n, m) = Min (m, n)`
theorem TMinComm : ∀ {n m : N}, (mini n m) = (mini m n) := by
intro n m
match n, m with
| z, _ => rw [TMinzL, TMinzR]
| _, z => rw [TMinzL, TMinzR]
| (s n'), (s m') => rw [mini, congrArg s (TMinComm), mini]
-- `Min (n, m) = n ∨ Min (n, m) = m`
theorem TMinOut : ∀ {n m : N}, ((mini n m) = n) ∨ ((mini n m) = m) := by
intro n m
match n, m with
| z, _ => exact Or.inl TMinzL
| _, z => exact Or.inr TMinzR
| (s n'), (s m') => match (@TMinOut n' m') with
| Or.inl h => exact Or.inl (congrArg s h)
| Or.inr h => exact Or.inr (congrArg s h)
-- `Min (n, n) = n`
theorem TMinIdpt : ∀ {n : N}, mini n n = n := by
intro n
match (@TMinOut n n) with
| Or.inl h => exact h
| Or.inr h => exact h
-- `Min (n, m) = Max (n, m) → n = m `
theorem TMinMaxEq : ∀ {n m : N}, mini n m = maxi n m → n = m := by
intro n m h1
cases n
calc
z = mini z m := TMinzL.symm
_ = maxi z m := h1
_ = m := TMaxzL
rename_i n'
cases m
calc
n'.s = maxi n'.s z := TMaxzR.symm
_ = mini n'.s z := h1.symm
_ = z := TMinzR
rename_i m'
apply congrArg
injection h1 with h1
exact TMinMaxEq h1
-- `Min (n, m) = n ↔ Max (n, m) = m`
theorem TMinMax : ∀ {n m : N}, mini n m = n ↔ maxi n m = m := by
intro n m
apply Iff.intro
-- mini n m = n → maxi n m = m
intro h
cases (@TMaxOut n m)
-- maxi n m = n
rename_i h1
have h2 : n = m := by
apply TMinMaxEq
exact h.trans (h1.symm)
rw [h2]
exact TMaxIdpt
-- maxi n m = m
rename_i h1
exact h1
-- maxi n m = m → mini n m = n
intro h
cases (@TMinOut n m)
-- mini n m = n
rename_i h1
exact h1
-- mini n m = m
rename_i h1
have h2 : n = m := by
apply TMinMaxEq
exact h1.trans (h.symm)
rw [h2]
exact TMinIdpt
-- ## Addition
-- `z` is a left identity for addition
theorem TAdd0L : ∀ {n : N}, z + n = n := by
intro n
exact rfl
-- `z` is a right identity for addition
theorem TAdd0R : ∀ {n : N}, n + z = n := by
intro n
induction n
-- Base case
exact rfl
-- Inductive step
rename_i n hi
calc
s n + z = s (n + z) := rfl
_ = s n := congrArg s hi
-- Addition of natural numbers
-- is commutative up to a successor
theorem TAddOne : ∀ {n m : N}, (s n) + m = n + (s m) := by
intro n m
induction n
-- Base case
exact rfl
-- Inductive step
rename_i n hi
calc
s (s n) + m = s (s n + m) := rfl
_ = s (n + s m) := congrArg s hi
_ = (s n) + (s m) := rfl
-- Addition is commutative
theorem TAddComm : ∀ {n m : N}, n + m = m + n := by
intro n m
induction n
-- Base case
calc
z + m = m := rfl
_ = m + z := TAdd0R.symm
-- Inductive step
rename_i n hi
calc
(s n) + m = s (n + m) := rfl
_ = s (m + n) := congrArg s hi
_ = (s m) + n := rfl
_ = m + (s n) := TAddOne
-- If the sum of two natural numbers is `z`,
-- then the first number must be `z`
theorem TAddZ : ∀ {n m : N}, n + m = z → n = z := by
intro n m h
cases n
-- Case z
exact rfl
-- Case s n -- This case is impossible
cases h
-- If the sum of two natural numbers is `z`,
-- then both numbers are `z`
theorem TAddZ2 : ∀ {n m : N}, n + m = z → (n = z) ∧ (m = z) := by
intro n m h
apply And.intro
-- Left
exact TAddZ h
-- Right using commutativity
rw [TAddComm] at h
exact TAddZ h
-- Addition is associative
theorem TAddAss : ∀{n m p : N}, (n + m) + p = n + (m + p) := by
intro n m p
induction n
-- Case z
exact rfl
-- Case s n
rename_i n hi
calc
((s n) + m) + p = (s (n + m)) + p := rfl
_ = s ((n + m) + p) := rfl
_ = s (n + (m + p)) := congrArg s hi
_ = (s n) + (m + p) := rfl
-- `n` can never be equal to `n + s k`
theorem TAddSucc : ∀ {n k : N}, n = n + (s k) → False := by
intro n k h
induction n
-- Case z
cases h
-- Case s n
rename_i n hi
have h1 : s n = s (n + (s k)) := by
calc
s n = s n + s k := h
_ = s (n + s k) := rfl
injection h1 with h1
exact hi h1
-- A number cannot be both ahead of and
-- behind another number by a positive amount
theorem TIncAdd : ∀ {n m k : N}, m = n + (s k) → n = m + (s k) → False := by
intro n m k h1 h2
rw [h2, TAddAss] at h1
exact (@TAddSucc m (k + s k)) h1
-- Right congruence of addition
theorem TAddCongR : ∀ {n m k : N}, m = k → n + m = n + k := by
intro n m k h1
rw [h1]
-- Left congruence of addition
theorem TAddCongL : ∀ {n m k : N}, m = k → m + n = k + n := by
intro n m k h1
rw [h1]
-- Addition on the left is cancellative
theorem TAddCancL : ∀ {n m k : N}, n + m = n + k → m = k := by
intro n m k h
induction n
-- Case z
exact h
-- Case s n
rename_i n hi
have h1 : s (n + m) = s (n + k) := h
injection h1 with h1
exact hi h1
-- Addition on the right is cancellative
theorem TAddCancR : ∀ {n m k : N}, m + n = k + n → m = k := by
intro n m k h
have h1 : n + m = n + k := by
calc
n + m = m + n := TAddComm
_ = k + n := h
_ = n + k := TAddComm
exact TAddCancL h1
-- Left cancellation property of addition with zero
theorem TAddCancLZ : ∀ {n m : N}, n + m = n → m = z := by
intro n m h
apply @TAddCancL n m z
rw [h]
exact TAdd0R.symm
-- Right cancellation property of addition with zero
theorem TAddCancRZ : ∀ {n m : N}, m + n = n → m = z := by
intro n m h
apply @TAddCancR n m z
rw [h]
exact TAdd0L
-- ## Multiplication
-- `z` is a left zero for multiplication
theorem TMult0L : ∀ {n : N}, z * n = z := by
intro n
exact rfl
-- `z` is a right zero for multiplication
theorem TMult0R : ∀ {n : N}, n * z = z := by
intro n
induction n
-- Case z
exact rfl
-- Case s n
rename_i n hi
calc
(s n) * z = n * z + z := rfl
_ = z + z := congrFun (congrArg Addition hi) z
_ = z := rfl
-- We introduce `one`
def one : N := s z[no new output]Example 7
Status: OK
-- `one + n = s n`
theorem TOneAddR : ∀ {n : N}, one + n = s n := by
intro n
exact rfl
-- `n + one = s n`
theorem TOneAddL : ∀ {n : N}, n + one = s n := by
intro n
apply TAddComm
-- The different cases for two numbers adding to one
theorem TAddOneCases : ∀ {n m : N}, n + m = one → (n = z ∧ m = one) ∨ (n = one ∧ m = z) := by
intro n m h
cases n
-- Case z
apply Or.inl
apply And.intro
exact rfl
exact h
-- Case s n
rename_i n
injection h with h
apply Or.inr
apply And.intro
rw [TAddZ h]
exact rfl
rw [TAddComm] at h
exact TAddZ h
-- `one` is a left identity for multiplication
theorem TMult1L : ∀ {n : N}, one * n = n := by
intro n
exact rfl
-- `one` is a right identity for multiplication
theorem TMult1R : ∀ {n : N}, n * one = n := by
intro n
induction n
-- Base case
exact rfl
-- Inductive step
rename_i n hi
calc
s n * one = n * one + one := rfl
_ = n + one := congrFun (congrArg Addition hi) one
_ = n + (s z) := rfl
_ = (s n) + z := TAddOne.symm
_ = s n := TAdd0R
-- Multiplications is left distributive over addition
theorem TMultDistL : ∀ {n m k : N}, (n + m) * k = (n * k) + (m * k) := by
intro n m k
induction n
-- Base case
exact rfl
-- Inductive step
rename_i n hi
calc
((s n) + m) * k = (s (n + m)) * k := rfl
_ = (n + m) * k + k := rfl
_ = (n * k) + (m * k) + k := TAddCongL hi
_ = (n * k) + ((m * k) + k) := TAddAss
_ = (n * k) + (k + (m * k)) := TAddCongR TAddComm
_ = (n * k) + k + (m * k) := TAddAss.symm
_ = ((s n) * k) + (m * k) := rfl
-- Multiplications is right distributive over addition
theorem TMultDistR : ∀ {n m k : N}, n * (m + k) = (n * m) + (n * k) := by
intro n m k
induction n
-- Base case
exact rfl
-- Inductive step
rename_i n hi
calc
(s n) * (m + k) = n * (m + k) + (m + k) := rfl
_ = n * m + n * k + (m + k) := congrFun (congrArg Addition hi) (m + k)
_ = n * m + n * k + (k + m) := TAddCongR TAddComm
_ = n * m + (n * k + (k + m)) := TAddAss
_ = n * m + (n * k + k + m) := TAddCongR TAddAss.symm
_ = n * m + (n * k + k) + m := TAddAss.symm
_ = n * m + ((n * k + k) + m) := TAddAss
_ = n * m + (m + (n * k + k)) := TAddCongR TAddComm
_ = n * m + (m + n * k + k) := TAddCongR TAddAss.symm
_ = n * m + (m + n * k) + k := TAddAss.symm
_ = n * m + m + n * k + k := TAddCongL TAddAss.symm
_ = (s n) * m + n * k + k := rfl
_ = (s n) * m + (n * k + k) := TAddAss
_ = (s n) * m + (s n) * k := rfl
-- Multiplication is commutative
theorem TMultComm : ∀ {n m : N}, n * m = m * n := by
intro n m
induction n
-- Base case
calc
z * m = z := rfl
_ = m * z := TMult0R.symm
-- Inductive step
rename_i n hi
calc
(s n) * m = n * m + m := rfl
_ = m * n + m := TAddCongL hi
_ = m + (m * n) := TAddComm
_ = (m * one) + (m * n) := TAddCongL (TMult1R.symm)
_ = m * (one + n) := TMultDistR.symm
_ = m * (s n) := rfl
-- If the product of two natural numbers is `z`,
-- then one of them must be `z`
theorem TMultZ : ∀ {n m : N}, n * m = z → (n = z) ∨ (m = z) := by
intro n m h
cases n
-- Case z
apply Or.inl
exact rfl
-- Case s n
rename_i n
apply Or.inr
have h1 : (n * m = z) ∧ (m = z) := TAddZ2 h
exact h1.right
-- Right congruence of multiplication
theorem TMultCongR : ∀ {n m k : N}, m = k → n * m = n * k := by
intro n m k h1
rw [h1]
-- Left congruence of addition
theorem TMultCongL : ∀ {n m k : N}, m = k → m * n = k * n := by
intro n m k h1
rw [h1]
-- Multiplication is associative
theorem TMultAss : ∀{n m p : N}, (n * m) * p = n * (m * p) := by
intro n m p
induction n
-- Case z
exact rfl
-- Case s n
rename_i n hi
calc
((s n) * m) * p = (n * m + m) * p := rfl
_ = ((n * m) * p) + m * p := TMultDistL
_ = (n * (m * p)) + m * p := TAddCongL hi
_ = (n * (m * p)) + (one * (m * p)) := TAddCongR TMult1L
_ = (n + one) * (m * p) := TMultDistL.symm
_ = (s n) * (m * p) := TMultCongL TOneAddL
-- Fix points for multiplication
theorem TMultFix : ∀{n m : N}, n * m = n → n = z ∨ m = one := by
intro n m h1
cases m
-- Case z
apply Or.inl
rw [TMult0R] at h1
exact h1.symm
-- Case s m
rename_i m
have h2 : n * m + n = n := by
calc
n * m + n = n * m + n * one := by rw [TMult1R]
_ = n * (m + one) := TMultDistR.symm
_ = n * (s m) := by rw [TOneAddL]
_ = n := h1
have h3 : n * m = z := TAddCancRZ h2
apply Or.elim (TMultZ h3)
-- Case Left
intro h4
exact Or.inl h4
-- Case Right
intro h5
apply Or.inr
rw [h5]
exact rfl
-- `one` is the unique idempotent for multiplication
theorem TMultOne : ∀ {n m : N}, n * m = one ↔ (n = one ∧ m = one) := by
intro n m
apply Iff.intro
-- n * m = one → n = one ∧ m = one
intro h1
induction n
-- Case z
rw [TMult0L] at h1
cases h1
-- Case s n
rename_i n hi
apply Or.elim (TAddOneCases h1)
-- Case Left
intro ⟨h3, h4⟩
apply Or.elim (TMultZ h3)
-- Case Left
intro h5
rw [h5]
exact And.intro rfl h4
-- Case Right (impossible)
intro h5
rw [h5] at h4
cases h4
-- Case Right (impossible)
intro ⟨h2, h3⟩
have h4 : m = one := (hi h2).right
rw [h4] at h3
cases h3
-- n = one ∧ m = one → n * m = one
intro ⟨h3, h4⟩
rw [h3, h4, TMult1L]
end a06Exercises[no new output]Chapter 7: Choice
Example 1
Status: OK
-- # Choice
import a05Functions
-- ## Inhabited
-- `Inhabited α` is a typeclass that says that `α`
-- has a designated element, called `(default : α)`
-- This is sometimes referred to as a "pointed type".
#print Inhabited
-- A typeclass in Lean is a special kind of structure that
-- specifies a set of properties or operations that a type
-- can have. We will learn more about
-- To define an specific example of a class we will use the
-- `instance` or `def` keywords. For the typeclass
-- `Inhabited` we only need to provide the default element
instance InBool : Inhabited Bool := {
default:= true
}
#check InBool
#print InBool
#eval InBool.default
-- Lean already has some instances of inhabited types
#print instInhabitedBool -- default := false
#print instInhabitedProp -- default := True
#print instInhabitedNat -- default := Nat.zero
-- ## Nonempty
-- The `Nonempty` type is an inductive proposition
-- that asserts the existence of at least one element
-- in a given type
#print Nonemptyinductive Nonempty.{u} : Sort u → Prop
number of parameters: 1
constructors:
Nonempty.intro : ∀ {α : Sort u} (val : α), Nonempty αExample 2
Status: OK
-- For example, we can provide a proof of `Nonempty Bool`
theorem TNEBool : Nonempty Bool := Nonempty.intro true
-- ### Inhabited implies Nonempty
-- We have a straightforward implication,
-- if a type is inhabited, then it is also nonempty
def InhabitedToNonempty {A : Type} : Inhabited A → Nonempty A := by
intro h
exact Nonempty.intro h.default
-- The reverse implication, `Nonempty A → Inhabited A`,
-- does not always hold in constructive logic
-- A proof of `Nonempty A` only asserts the existence of
-- an element without providing a specific one, whereas
-- `Inhabited A` requires a concrete, predefined
-- default value
-- ## Classical.choice
-- In classical logic, we can recover `Inhabited A`
-- from `Nonempty A` using the axiom of choice
-- (`Classical.choice`), but this is noncomputable,
-- meaning we cannot explicitly construct the
-- default element
#print Classical.choice
-- `Classical.choice` is an axiom
-- Many axioms, such as `Classical.choice`, are
-- nonconstructive in nature, meaning they assert
-- the existence of certain objects without providing
-- explicit constructions
-- As a result, these axioms are often `noncomputable`[no new output]Example 3
Status: OK
-- ### Nonempty implies Inhabited in Classical Logic
-- We can now define the reverse implication
-- in Classical Logic
noncomputable def NonemptyToInhabited {A : Type} : Nonempty A → Inhabited A := by
intro h
have a : A := Classical.choice h
exact Inhabited.mk a
-- The function above is marked as `noncomputable`
-- because the choice of an element is nonconstructive
-- ### Classical.choose
-- The command `Classical.choose` is a function from
-- classical logic that allows for the selection of an
-- element satisfying a given predicate
#check Classical.choose
-- The command `Classical.choose_spec` guarantees that
-- the extracted element satisfies the given predicate
#check Classical.choose_spec
-- Alternative commands are
#check Exists.choose
#check Exists.choose_spec.tmp_lean_crash_course/a07Choice_emit.lean:17:0: warning: Definition `NonemptyToInhabited` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
Classical.choose.{u} {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α
Classical.choose_spec.{u} {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (Classical.choose h)
Exists.choose.{u_1} {α : Sort u_1} {p : α → Prop} (P : ∃ a, p a) : α
Exists.choose_spec.{u_1} {α : Sort u_1} {p : α → Prop} (P : ∃ a, p a) : p P.chooseExample 4
Status: OK
-- -- We prove that `Nonempty A ↔ ∃ (a : A), a = a`
-- theorem TInj {A : Type} : Nonempty A ↔ ∃ (a : A), a = a := by
-- apply Iff.intro
-- -- Nonempty A → ∃ a, a = a
-- intro h
-- apply Exists.intro (Classical.choice h)
-- exact rfl
-- -- (∃ a, a = a) → Nonempty A
-- intro h
-- have a : A := Exists.choose h
-- exact Nonempty.intro a
-- -- ## Exercises
-- namespace a06Exercises
-- open Inj
-- open Surj
-- open Bij
-- open a05BijExercises
-- -- Under `Classical.Choice`, if a function is injective and
-- -- the domain is `Nonempty` then the function has a left inverse
-- theorem TInjtoHasLeftInv {A B : Type} {f : A → B} : injective f → Nonempty A → hasleftinv f := by
-- intro h1 h2
-- let g : B → A := by
-- intro b
-- by_cases h3 : ∃ (a : A), f a = b
-- --
-- exact Exists.choose h3 -- The alternative h3.choose is also valid
-- --
-- exact Classical.choice h2
-- apply Exists.intro g
-- funext a
-- have h3 : ∃ (a' : A), f a' = f a := by
-- apply Exists.intro a
-- exact rfl
-- have h4 : f (Exists.choose h3) = f a := Exists.choose_spec h3
-- calc
-- (g ∘ f) a = g (f a) := by exact rfl
-- _ = Exists.choose h3 := by exact dif_pos h3
-- _ = a := by exact h1 h4
-- _ = id a := by exact rfl
-- -- Under `Classical.Choice`, every surjective function
-- -- has a right inverse
-- noncomputable def Inverse {A B : Type} (f : A → B) (h : surjective f) : B → A := by
-- intro b
-- specialize @h b
-- exact Exists.choose h
-- -- Under `Classical.Choice`, the inverse of a surjective
-- -- function is a right inverse
-- theorem InvR {A B : Type} (f : A → B) (h : surjective f) : f ∘ (Inverse f h) = id := by
-- funext b
-- specialize @h b
-- exact Exists.choose_spec h
-- -- Under `Classical.Choice`, every surjective function has a right inverse
-- theorem TSurjtoHasRightInv {A B : Type} {f : A → B} : surjective f → hasrightinv f := by
-- intro h
-- apply Exists.intro (Inverse f h)
-- exact InvR f h
-- -- Under `Classical.Choice`, the inverse of a bijective function is a left inverse
-- theorem InvL {A B : Type} (f : A → B) (h : bijective f) : (Inverse f h.right) ∘ f = id := by
-- funext a
-- have hs : surjective f := h.right
-- specialize @hs (f a)
-- exact h.left (Exists.choose_spec hs)
-- -- Under `Classical.Choice` bijective and isomorphism are
-- -- equivalent concepts
-- theorem TCarBijIso {A B : Type} {f : A → B} : bijective f ↔ isomorphism f := by
-- apply Iff.intro
-- -- bijective f → isomorphism f
-- intro h
-- apply Exists.intro (Inverse f h.right)
-- apply And.intro
-- exact InvL f h
-- exact InvR f h.right
-- -- isomorphism f → bijective f
-- exact TCarIsotoBij
-- end a06Exercises.tmp_lean_crash_course/a07Choice_final.lean:17:0: warning: Definition `NonemptyToInhabited` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
Classical.choose.{u} {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α
Classical.choose_spec.{u} {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (Classical.choose h)
Exists.choose.{u_1} {α : Sort u_1} {p : α → Prop} (P : ∃ a, p a) : α
Exists.choose_spec.{u_1} {α : Sort u_1} {p : α → Prop} (P : ∃ a, p a) : p P.chooseChapter 8: Subtypes
Example 1
Status: OK
-- # Subtypes
import a03Quantifiers
import a05Functions
open Inj Surj Bij
-- set_option linter.unusedVariables false
-- We define variables `A : Type` and
-- `P : A → Prop`, a predicate on `A`
variable (A : Type)
variable (P : A → Prop)
-- With this information we can obtain `Subtype P`
-- the subtype of all the elements of type `A`
-- that satisfy `P`
#check Subtype P
-- An alternative notation is
#check { a : A // P a }
#print SubtypeSubtype P : Type
{ a // P a } : Type
structure Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)
number of parameters: 2
fields:
Subtype.val : α
Subtype.property : p self.val
constructor:
Subtype.mk.{u} {α : Sort u} {p : α → Prop} (val : α) (property : p val) : Subtype pExample 2
Status: OK
-- ### Examples of Subtypes (from a03Quantifiers)
-- #### The False Subtype
def SFalse {A : Type} := { a : A // PFalse a}
-- #### The True Subtype
def STrue {A : Type} := { a : A // PTrue a}
-- ## The Image Subtype
def Im {A B : Type} (f : A → B) : Type := { b : B // ∃ (a : A), f a = b}
-- ## Elements of a Subtype type
-- To create an element of a `Subtype P`, we use
-- the `Subtype.mk a` function, which maps an element `a : A`
-- and a proof of `P a` to an element of type `Subtype P`
variable (a : A)
variable (h : P a)
#check Subtype.mk a h
-- Two elements of type `Subtype P` are equal
-- if and only if the corresponding values in `A` are equal
#check Subtype.eq -- `a1.val = a2.val → a1 = a2`
#check Subtype.eq_iff -- `a1.val = a2.val ↔ a1 = a2`⟨a, h⟩ : Subtype P
Subtype.eq.{u} {α : Sort u} {p : α → Prop} {a1 a2 : { x // p x }} : a1.val = a2.val → a1 = a2
Subtype.eq_iff.{u_1} {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }} : a1 = a2 ↔ a1.val = a2.valExample 3
Status: OK
-- ### The inclusion function
-- The inclusion function
def inc {A : Type} {P : A → Prop} : Subtype P → A := by
intro a
exact a.val
-- The inclusion function is injective
theorem Tincinj {A : Type} {P : A → Prop} : injective (@inc A P) := by
intro a1 a2 h1
exact Subtype.eq h1
-- ## Restriction
-- The restriction of a function
def rest {A B : Type} {P : A → Prop} (f : A → B) : Subtype P → B := by
intro a
exact f a.val
-- ## Correstriction
-- Correstriction of a function
def correst {A B : Type} {Q : B → Prop} (f : A → B) (h : ∀ (b : Im f), Q b.val) : A → Subtype Q := by
intro a
have ha : ∃ (a1 : A), f a1 = f a := by
apply Exists.intro a
exact rfl
apply Subtype.mk (f a) (h ⟨f a, ha⟩)
-- ## Birrestriction
-- Birrestriction of a function `birrest = correst ∘ rest`
def birrest {A B : Type} {P : A → Prop} {Q : B → Prop} (f : A → B) (h : ∀ (a : A), P a → Q (f a)) : Subtype P → Subtype Q := by
apply correst (rest f)
intro ⟨b, ⟨a, ha⟩⟩
simp
specialize h a.val
have hb : f a.val = b := ha
rw [hb] at h
exact h a.property
-- In particular, if a predicate `P1` on `A` implies a predicate
-- `P2` on `A` then there exists a way of transforming elements
-- of type `Subtype P1` into elements of `Subtype P2`
-- For this we simply birrestrict the identity
def SubtoSub {A : Type} {P1 P2 : A → Prop} (h : ∀ (a : A), P1 a → P2 a) : Subtype P1 → Subtype P2 := birrest id h.tmp_lean_crash_course/a08Subtypes_emit.lean:52:8: warning: `Subtype.eq` has been deprecated: Use `Subtype.ext` insteadExample 4
Status: OK
namespace a08Exercises
-- If two predicates are equivalent, then the
-- corresponding subtypes are equal
theorem TEqSubtype {A : Type} {P1 P2 : A → Prop} (h : ∀ (a : A), P1 a ↔ P2 a) : Subtype P1 = Subtype P2 := by
have h1 : P1 = P2 := by
funext a
apply propext
exact h a
rw [h1]
-- Universal property of subtypes
-- Im (inc) = Subtype
theorem TUPSub {A : Type} {P : A → Prop} : Im (@inc A P) = Subtype P := by
apply TEqSubtype
intro a1
apply Iff.intro
-- (∃ a, inc a = a1) → P a1
intro h1
apply Exists.elim h1
intro a2 h2
rw [h2.symm]
apply Subtype.property
-- P a1 → ∃ a, inc a = a1
intro h1
apply Exists.intro (Subtype.mk a1 h1)
exact rfl
-- Restriction `rest f = f ∘ inc`
theorem TRest {A B : Type} {f : A → B} {P : A → Prop}: (@rest A B P f) = f ∘ (@inc A P) := by
exact rfl
-- Universal property of the correstriction
-- `f = inc ∘ correst`
theorem TUPCorrest {A B : Type} {Q : B → Prop} {f : A → B} (h : ∀ (b : Im f), Q b.val) : f = (@inc B Q) ∘ (correst f h) := by
exact rfl
-- Unicity
theorem TUPCorrestUn {A B : Type} {Q : B → Prop} {f : A → B} (h : ∀ (b : Im f), Q b.val) (g : A → Subtype Q) (h1 : f = (@inc B Q) ∘ g) : (correst f h) = g := by
apply funext
intro a
apply Subtype.eq
calc
(correst f h a).val = ((@inc B Q) ∘ (correst f h)) a := by exact rfl
_ = f a := by exact congrFun (TUPCorrest h) a
_ = ((@inc B Q) ∘ g) a := by exact congrFun h1 a
_ = (g a).val := by exact rfl
end a08Exercises
namespace Equalizers
-- ## Equalizers
-- The equalizer of two functions `f g : A → B`
-- is the type of elements `a : A` such that `f a = g a`
-- It is a subtype of `A`
def Eq {A B : Type} (f g : A → B) : Type := { a : A // f a = g a}.tmp_lean_crash_course/a08Subtypes_trial.lean:52:8: warning: `Subtype.eq` has been deprecated: Use `Subtype.ext` insteadExample 5
Status: OK
-- The inclusion function from the equalizer to `A`
def incEq {A B : Type} (f g : A → B) : Eq f g → A := @inc A (fun a => f a = g a).tmp_lean_crash_course/a08Subtypes_emit.lean:52:8: warning: `Subtype.eq` has been deprecated: Use `Subtype.ext` insteadExample 6
Status: OK
-- The inclusion function satisfies that `f ∘ (incEq f g) = g ∘ (incEq f g)`
theorem TEqInc {A B : Type} (f g : A → B) : f ∘ (incEq f g) = g ∘ (incEq f g) := by
apply funext
intro a
calc
(f ∘ (incEq f g)) a = f a.val := rfl
_ = g a.val := a.property
_ = (g ∘ (incEq f g)) a := rfl
-- Universal property of the equalizer
-- If there is another function `h : C → A` satisfying
-- `f ∘ h = g ∘ h`, then there exists a function `u : C → Eq f g`
def u {A B C : Type} {f g : A → B} {h : C → A} (h1 : f ∘ h = g ∘ h) : C → Eq f g := by
intro c
exact Subtype.mk (h c) (congrFun h1 c)
-- The function `u` satisfies that `incEq f g ∘ u = h`
theorem TEqIncEq {A B C : Type} {f g : A → B} {h : C → A} (h1 : f ∘ h = g ∘ h) : (incEq f g) ∘ (u h1) = h := by
apply funext
intro c
exact rfl
-- The function `u` is unique in the sense that if there is another function
-- `v : C → Eq f g` satisfying `incEq f g ∘ v = h`, then `v = u`
theorem TEqUni {A B C : Type} {f g : A → B} {h : C → A} (h1 : f ∘ h = g ∘ h) (v : C → Eq f g) (h2 : (incEq f g) ∘ v = h) : v = u h1 := by
apply funext
intro c
apply Subtype.eq
calc
(v c).val = ((incEq f g) ∘ v) c := rfl
_ = h c := congrFun h2 c
_ = (u h1 c).val := rfl
namespace a08ExercisesEq
-- The function `incEq` is a monomorphism
theorem TincEqMono {A B : Type} {f g : A → B} : monomorphism (incEq f g) := by
intro C v1 v2 h1
apply funext
intro a
apply Subtype.eq
calc
(v1 a).val = (incEq f g ∘ v1) a := rfl
_ = (incEq f g ∘ v2) a := congrFun h1 a
_ = (v2 a).val := rfl
-- An epic `incEq` is an isomorphism
theorem TincEqEpi {A B : Type} {f g : A → B} : epimorphism (incEq f g) → isomorphism (incEq f g) := by
intro h1
have h2 : f = g := by
apply @h1 B f g
exact TEqInc f g
let fu : A → Eq f g := by
apply @u A B A f g id
exact h2
apply Exists.intro fu
apply And.intro
-- fu ∘ incEq f g = id
funext a
apply Subtype.eq
exact rfl
-- incEq f g ∘ fu = id
apply TEqIncEq
end a08ExercisesEq
end Equalizers.tmp_lean_crash_course/a08Subtypes_trial.lean:52:8: warning: `Subtype.eq` has been deprecated: Use `Subtype.ext` insteadChapter 9: Relations
Example 1
Status: OK
-- # Relations
-- set_option linter.unusedVariables false
-- A relation on a type `A` is a predicate
-- of type `A → A → Prop`. That is, a relation
-- `R : A → A → Prop` considers two elements `a b : A`
-- and returns the proposition `R a b`, whenever `a` and `b`
-- are related under `R`
-- Note that, since relations are predicates on two
-- input variables we can prove that two relations are equal
-- if and only if they relate the same elements
-- (using `funext` twice) if and only if the predicates
-- are equivalent on the same elements (using `propext`)
theorem TEqRel {A : Type} {R S : A → A → Prop} : R = S ↔ ∀ (a1 a2 : A), R a1 a2 ↔ S a1 a2 := by
apply Iff.intro
-- R = S → ∀ (a1 a2 : A), R a1 a2 ↔ S a1 a2
intro h a1 a2
apply Iff.intro
-- R a1 a2 → S a1 a2
intro hR
rw [h.symm]
exact hR
-- S a1 a2 → R a1 a2
intro hS
rw [h]
exact hS
-- (∀ (a1 a2 : A), R a1 a2 ↔ S a1 a2) → R = S
intro h
apply funext
intro a1
apply funext
intro a2
apply propext
exact h a1 a2
-- ### Some interesting relations on `A`
-- The `empty` relation on `A` relates no elements at all
def empty {A : Type} : A → A → Prop := fun _ _ => False[no output]Example 2
Status: OK
-- The `total` relation on `A` relates all the element of `A`
def total {A : Type} : A → A → Prop := fun _ _ => True
-- The `diag` (diagonal) relation on `A`, where each
-- element is related only to itself
def diag {A : Type} : A → A → Prop := fun x y => (x = y)
namespace Relations
-- ## Types of relations
-- We introduce some interesting relations
-- **Reflexive** relation
def Reflexive {A : Type} (R : A → A → Prop) : Prop :=
∀{a : A}, R a a
-- **Symmetric** relation
def Symmetric {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 : A}, R a1 a2 → R a2 a1
-- **Antisymmetric** relation
def Antisymmetric {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 : A}, R a1 a2 → R a2 a1 → (a1 = a2)
-- **Transitive** relation
def Transitive {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 a3 : A}, R a1 a2 → R a2 a3 → R a1 a3
-- **Serial** relation
def Serial {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 : A}, ∃ (a2 : A), R a1 a2
-- **Euclidean** relation
def Euclidean {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 a3 : A}, R a1 a2 → R a1 a3 → R a2 a3[no output]Example 3
Status: OK
-- **Partially Functional** relation
def PartiallyFunctional {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 a3 : A}, R a1 a2 → R a1 a3 → a2 = a3
-- **Functional** relation
def Functional {A : Type} (R : A → A → Prop) : Prop :=
∀(a1 : A), ∃ (a2 : A), ∀(a3 : A), R a1 a3 ↔ a2 = a3
-- **Weakly Dense** relation
def WeaklyDense {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 : A}, (R a1 a2 → ∃ (a3 : A), (R a1 a3) ∧ (R a3 a2))
-- **Weakly Connected** relation
def WeaklyConnected {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 a3 : A}, R a1 a2 → R a1 a3 → ((R a2 a3) ∨ (a2 = a3) ∨ (R a3 a2))
-- **Weakly Directed** relation
def WeaklyDirected {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 a3 : A}, R a1 a2 → R a1 a3 →
∃ (a4 : A), ((R a2 a4) ∧ (R a3 a4))[no output]Example 4
Status: OK
-- namespace Diagonal
-- -- ### An example: the diagonal
-- -- The diagonal is reflexive
-- theorem TDiagRefl {A : Type} : Reflexive (@diag A) := by
-- intro a
-- exact rfl
-- -- The diagonal is symmetric
-- theorem TDiagSymm {A : Type} : Symmetric (@diag A) := by
-- intro a1 a2 h
-- exact h.symm
-- -- The diagonal is antisymmetric
-- theorem TDiagASymm {A : Type} : Antisymmetric (@diag A) := by
-- intro a1 a2 h1 _
-- exact h1
-- -- The diagonal is transitive
-- theorem TDiagTrans {A : Type} : Transitive (@diag A) := by
-- intro a1 a2 a3 h1 h2
-- exact h1.trans h2
-- -- The diagonal is serial
-- theorem TDiagSer {A : Type} : Serial (@diag A) := by
-- intro a
-- apply Exists.intro a
-- exact rfl
-- -- The diagonal is Euclidean
-- theorem TDiagEucl {A : Type} : Euclidean (@diag A) := by
-- intro a1 a2 a3 h1 h2
-- exact h1.symm.trans h2
-- -- The diagonal is partially functional
-- theorem TDiagPFunc {A : Type} : PartiallyFunctional (@diag A) := by
-- intro a1 a2 a3 h1 h2
-- exact h1.symm.trans h2
-- -- The diagonal is functional
-- theorem TDiagFunc {A : Type} : Functional (@diag A) := by
-- intro a
-- apply Exists.intro a
-- intro z
-- apply Iff.intro
-- -- diag a z → a = z
-- intro h
-- exact h
-- -- a = z → diag a z
-- intro h
-- exact h
-- -- The diagonal is weakly dense
-- theorem TDiagWDense {A : Type} : WeaklyDense (@diag A) := by
-- intro a1 a2 h1
-- apply Exists.intro a1
-- apply And.intro
-- -- Left
-- exact rfl
-- -- Right
-- exact h1
-- -- The diagonal is weakly connected
-- theorem TDiagWConn {A : Type} : WeaklyConnected (@diag A) := by
-- intro a1 a2 a3 h1 h2
-- exact Or.inl (h1.symm.trans h2)
-- -- The diagonal is weakly directed
-- theorem TDiagWDir {A : Type} : WeaklyDirected (@diag A) := by
-- intro a1 a2 a3 h1 h2
-- apply Exists.intro a1
-- apply And.intro
-- -- Left
-- exact h1.symm
-- -- Right
-- exact h2.symm
-- end Diagonal
-- ### Exercises
namespace a08RelExercises
-- Extracted from Zach, R. (2019). Boxes and Diamonds: An Open Introduction to Modal Logic
-- https://builds.openlogicproject.org/courses/boxes-and-diamonds/bd-screen.pdf[no output]Example 5
Status: OK
variable (A : Type)
variable (R : A → A → Prop)[no output]Example 6
Status: OK
-- -- Reflexive implies serial
-- theorem TRefltoSerial : Reflexive R → Serial R := by
-- intro h
-- intro a
-- apply Exists.intro a
-- exact h
-- -- For a symmetric relation, transitive and Euclidean are equivalent
-- theorem TSymmTransIffSer (hS : Symmetric R) : Transitive R ↔ Euclidean R := by
-- apply Iff.intro
-- -- Transitive R → Euclidean R
-- intro hT
-- intro a1 a2 a3 h1 h2
-- have h3 : R a2 a1 := hS h1
-- exact hT h3 h2
-- -- Euclidean R → Transitive R
-- intro hE a1 a2 a3 h1 h2
-- have h3 : R a2 a1 := hS h1
-- exact hE h3 h2
-- -- If a relation is symmetric then it is weakly directed
-- theorem TSymmtoWDir : Symmetric R → WeaklyDirected R := by
-- intro hS
-- intro a1 a2 a3 h1 h2
-- apply Exists.intro a1
-- apply And.intro
-- -- Left
-- exact hS h1
-- -- Right
-- exact hS h2
-- -- If a relation is Euclidean and antisymmetric,
-- -- then it is weakly directed
-- theorem TEuclASymmtoWDir : Euclidean R → Antisymmetric R → WeaklyDirected R := by
-- intro hE hA a1 a2 a3 h1 h2
-- have h3 : R a2 a3 := hE h1 h2
-- have h4 : R a3 a2 := hE h2 h1
-- have h5 : a2 = a3 := hA h3 h4
-- apply Exists.intro a2
-- apply And.intro
-- -- Left
-- rw [h5.symm] at h3
-- exact h3
-- -- Right
-- exact h4
-- -- If a relation is Euclidean, then it is weakly connected
-- theorem TEucltoWConn : Euclidean R → WeaklyConnected R := by
-- intro hE a1 a2 a3 h1 h2
-- apply Or.inl
-- exact hE h1 h2
-- -- If a relation is functional, then it is serial
-- theorem TFunctoSer : Functional R → Serial R := by
-- intro hF a
-- specialize hF a
-- cases hF
-- rename_i Fa h
-- apply Exists.intro Fa
-- specialize h Fa
-- rw [h]
-- -- If a relation is symmetric and transitive,
-- -- then it is Euclidean
-- theorem TSymmTranstoEucl : Symmetric R → Transitive R → Euclidean R := by
-- intro hS hT a1 a2 a3 h1 h2
-- exact hT (hS h1) h2
-- -- If a relation is reflexive and Euclidean,
-- -- then it is symmetric
-- theorem TReflEucltoSymm : Reflexive R → Euclidean R → Symmetric R := by
-- intro hR hE a1 a2 h1
-- have h2 : R a1 a1 := by exact hR
-- exact hE h1 h2
-- -- If a relation is symmetric and Euclidean,
-- -- then it is transitive
-- theorem TSymmEucltoTrans : Symmetric R → Euclidean R → Transitive R := by
-- intro hS hE a1 a2 a3 h1 h2
-- exact hE (hS h1) h2
-- -- If a relation is serial, symmetric and transitive,
-- -- then it is reflexive
-- theorem TSerSymmTranstoRefl : Serial R → Symmetric R → Transitive R → Reflexive R := by
-- intro hSe hSy hT a
-- specialize @hSe a
-- cases hSe
-- rename_i a1 h1
-- exact hT h1 (hSy h1)
-- end a08RelExercises
-- end Relations
namespace Operations
-- In this section we define operations on relations
variable (A : Type)
variable (R S : A → A → Prop)[no output]Example 7
Status: OK
-- Composition of two relations
def composition {A : Type} (R S : A → A → Prop) : A → A → Prop := by
intro a1 a3
exact ∃ (a2 : A), (R a1 a2) ∧ (S a2 a3)
-- We introduce notation for the composition (`\circ`)
notation : 65 lhs:65 " ∘ " rhs:66 => composition lhs rhs
#check R ∘ S
-- Inverse of a relation
def inverse {A : Type} (R : A → A → Prop) : A → A → Prop := by
intro a1 a2
exact R a2 a1
-- We introduce notation for the inverse (`^`)
notation : 65 lhs:65 "^" => inverse lhs
#check R^
-- Meet of two relations
def meet {A : Type} (R S : A → A → Prop) : A → A → Prop := by
intro a1 a2
exact (R a1 a2) ∧ (S a1 a2)
-- We introduce notation for the meet (`\and`)
notation : 65 lhs:65 " ∧ " rhs:66 => meet lhs rhs
#check R ∧ S
-- Join of two relations
def join {A : Type} (R S : A → A → Prop) : A → A → Prop := by
intro a1 a2
exact (R a1 a2) ∨ (S a1 a2)
-- We introduce notation for the join (`\or`)
notation : 65 lhs:65 " ∨ " rhs:66 => join lhs rhs
#check R ∨ SR ∨ S : A → A → PropExample 8
Status: OK
-- ### Exercises
namespace a08OpExercises
variable {A : Type}
variable (R S T : A → A → Prop)[no new output]Example 9
Status: OK
-- -- Associativity of composition
-- theorem TAssComp : R ∘ (S ∘ T) = (R ∘ S) ∘ T := by
-- funext a1 a2
-- apply propext
-- apply Iff.intro
-- -- (R ∘ (S ∘ T)) a1 a2 → (R ∘ S ∘ T) a1 a2
-- intro h1
-- apply Exists.elim h1
-- intro a3 ⟨h1, h2⟩
-- apply Exists.elim h2
-- intro a4 ⟨h3, h4⟩
-- apply Exists.intro a4
-- apply And.intro
-- apply Exists.intro a3
-- apply And.intro
-- exact h1
-- exact h3
-- exact h4
-- -- (R ∘ S ∘ T) a1 a2 → (R ∘ (S ∘ T)) a1 a2
-- intro h1
-- apply Exists.elim h1
-- intro a3 ⟨h2, h3⟩
-- apply Exists.elim h2
-- intro a4 ⟨h4, h5⟩
-- apply Exists.intro a4
-- apply And.intro
-- exact h4
-- apply Exists.intro a3
-- apply And.intro
-- exact h5
-- exact h3
-- -- The diagonal is a left neutral element for the composition
-- theorem TDiagL : R ∘ (@diag A) = R := by
-- funext a1 a2
-- apply propext
-- apply Iff.intro
-- -- (R ∘ diag) a1 a2 → R a1 a2
-- intro h1
-- apply Exists.elim h1
-- intro a3 ⟨h2, h3⟩
-- rw [h3.symm]
-- exact h2
-- -- R a1 a2 → (R ∘ diag) a1 a2
-- intro h1
-- apply Exists.intro a2
-- apply And.intro
-- exact h1
-- exact rfl
-- -- The diagonal is a right neutral element for the composition
-- theorem TDiagR : (@diag A) ∘ R = R := by
-- funext a1 a2
-- apply propext
-- apply Iff.intro
-- -- (diag ∘ R) a1 a2 → R a1 a2
-- intro h1
-- apply Exists.elim h1
-- intro a3 ⟨h2, h3⟩
-- rw [h2]
-- exact h3
-- -- R a1 a2 → (diag ∘ R) a1 a2
-- intro h1
-- apply Exists.intro a1
-- apply And.intro
-- exact rfl
-- exact h1
-- -- Inverse properties
-- -- The inverse relation of the inverse relation
-- -- is the original relation
-- theorem TInvInv : (R^)^ = R := by
-- funext a1 a2
-- apply propext
-- apply Iff.intro
-- -- (R^ ^) a1 a2 → R a1 a2
-- intro h1
-- exact h1
-- -- R a1 a2 → (R^ ^) a1 a2
-- intro h1
-- exact h1
-- -- The inverse of the composition
-- theorem TInvComp : (R ∘ S)^ = (S^) ∘ (R^) := by
-- funext a1 a3
-- apply propext
-- apply Iff.intro
-- -- (R ∘ S^) a1 a2 → (S^ ∘ (R^)) a1 a2
-- intro h1
-- apply Exists.elim h1
-- intro a2 ⟨h2, h3⟩
-- apply Exists.intro a2
-- apply And.intro
-- exact h3
-- exact h2
-- -- (S^ ∘ (R^)) a1 a3 → (R ∘ S^) a1 a3
-- intro h1
-- apply Exists.elim h1
-- intro a2 ⟨h2, h3⟩
-- apply Exists.intro a2
-- apply And.intro
-- exact h3
-- exact h2
-- -- The inverse of the meet
-- theorem TInvMeet : (R ∧ S)^ = (S^) ∧ (R^) := by
-- funext a1 a2
-- apply propext
-- apply Iff.intro
-- -- (R ∧ S)^ a1 a2 → ((S^) ∧ (R^)) a1 a2
-- intro ⟨h1, h2⟩
-- apply And.intro
-- exact h2
-- exact h1
-- -- ((S^) ∧ (R^)) a1 a2 → (R ∧ S)^ a1 a2
-- intro ⟨h1, h2⟩
-- apply And.intro
-- exact h2
-- exact h1
-- -- The inverse of the join
-- theorem TInvJoin : (R ∨ S)^ = (S^) ∨ (R^) := by
-- funext a1 a2
-- apply propext
-- apply Iff.intro
-- -- (R ∨ S)^ a1 a2 → ((S)^ ∨ (R^)) a1 a2
-- intro h1
-- cases h1
-- -- inl
-- rename_i h1
-- exact Or.inr h1
-- -- inr
-- rename_i h1
-- exact Or.inl h1
-- -- ((S)^ ∨ (R^)) a1 a2 → (R ∨ S)^ a1 a2
-- intro h1
-- cases h1
-- -- inl
-- rename_i h1
-- exact Or.inr h1
-- -- inr
-- rename_i h1
-- exact Or.inl h1
-- -- Distributivity of composition on the left over join
-- theorem TDisL : R ∘ (S ∨ T) = (R ∘ S) ∨ (R ∘ T) := by
-- funext a1 a3
-- apply propext
-- apply Iff.intro
-- -- (R ∘ (S ∨ T)) a1 a2 → (R ∘ S ∨ (R ∘ T)) a1 a2
-- intro ⟨a2, ⟨h1,h2⟩⟩
-- cases h2
-- -- inl
-- rename_i h2
-- apply Or.inl
-- apply Exists.intro a2
-- exact And.intro h1 h2
-- -- inr
-- rename_i h2
-- apply Or.inr
-- apply Exists.intro a2
-- exact And.intro h1 h2
-- -- (R ∘ S ∨ (R ∘ T)) a1 a3 → (R ∘ (S ∨ T)) a1 a3
-- intro h1
-- cases h1
-- -- inl
-- rename_i h1
-- apply Exists.elim h1
-- intro a2 ⟨h2,h3⟩
-- apply Exists.intro a2
-- apply And.intro
-- exact h2
-- exact Or.inl h3
-- -- inr
-- rename_i h1
-- apply Exists.elim h1
-- intro a2 ⟨h2,h3⟩
-- apply Exists.intro a2
-- apply And.intro
-- exact h2
-- exact Or.inr h3
-- -- Distributivity of composition on the right over join
-- theorem TDisR : (R ∨ S) ∘ T = (R ∘ T) ∨ (S ∘ T) := by
-- funext a1 a3
-- apply propext
-- apply Iff.intro
-- -- (R ∨ S ∘ T) a1 a3 → (R ∘ T ∨ (S ∘ T)) a1 a3
-- intro h1
-- apply Exists.elim h1
-- intro a2 ⟨h2, h3⟩
-- cases h2
-- -- inl
-- rename_i h2
-- apply Or.inl
-- apply Exists.intro a2
-- exact And.intro h2 h3
-- -- inr
-- rename_i h2
-- apply Or.inr
-- apply Exists.intro a2
-- exact And.intro h2 h3
-- -- (R ∘ T ∨ (S ∘ T)) a1 a3 → (R ∨ S ∘ T) a1 a3
-- intro h1
-- cases h1
-- -- inl
-- rename_i h1
-- apply Exists.elim h1
-- intro a2 ⟨h2, h3⟩
-- apply Exists.intro a2
-- apply And.intro
-- exact Or.inl h2
-- exact h3
-- -- inr
-- rename_i h1
-- apply Exists.elim h1
-- intro a2 ⟨h2, h3⟩
-- apply Exists.intro a2
-- apply And.intro
-- exact Or.inr h2
-- exact h3
-- -- Empty is a left zero for the composition
-- theorem TEmptLZ : (@empty A) ∘ R = (@empty A) := by
-- funext a1 a2
-- apply propext
-- apply Iff.intro
-- -- (empty ∘ R) a1 a2 → empty a1 a2
-- intro h1
-- apply Exists.elim h1
-- intro a3 ⟨h2, _⟩
-- exact False.elim h2
-- -- empty a1 a2 → (empty ∘ R) a1 a2
-- intro h1
-- exact False.elim h1
-- -- Empty is a right zero for the composition
-- theorem TEmptRZ : R ∘ (@empty A) = (@empty A) := by
-- funext a1 a2
-- apply propext
-- apply Iff.intro
-- -- (R ∘ empty) a1 a2 → empty a1 a2
-- intro h1
-- apply Exists.elim h1
-- intro a3 ⟨_, h3⟩
-- exact False.elim h3
-- -- empty a1 a2 → (R ∘ empty) a1 a2
-- intro h1
-- exact False.elim h1
-- end a08OpExercises
-- end Operations[no new output]Chapter 10: Equivalence
Example 1
Status: OK
-- # Equivalences
import a05Functions
import a07Choice
import a08Subtypes
import a09Relations
open Inj
open Surj
open Bij
open Relations
open Diagonal
namespace Equivalence
-- ## Equivalence relations
-- An **Equivalence** relation is a relation that is
-- `Reflexive`, `Symmetric` and `Transitive`
-- This is already implemented as `Equivalence`
#check Equivalence
#print EquivalenceEquivalence.{u} {α : Sort u} (r : α → α → Prop) : Prop
structure Equivalence.{u} {α : Sort u} (r : α → α → Prop) : Prop
number of parameters: 2
fields:
Equivalence.refl : ∀ (x : α), r x x
Equivalence.symm : ∀ {x y : α}, r x y → r y x
Equivalence.trans : ∀ {x y z : α}, r x y → r y z → r x z
constructor:
Equivalence.mk.{u} {α : Sort u} {r : α → α → Prop} (refl : ∀ (x : α), r x x) (symm : ∀ {x y : α}, r x y → r y x)
(trans : ∀ {x y z : α}, r x y → r y z → r x z) : Equivalence rExample 2
Status: OK
-- ### Examples (from a08Relations)
-- The diagonal relation is an equivalence relation
theorem TDiagEqv {A : Type} : Equivalence (@diag A) := {
refl := by
intro a
exact TDiagRefl
symm := by
intro a1 a2
exact TDiagSymm
trans := by
intro a1 a2 a3
exact TDiagTrans
}
-- The total relation is an equivalence relation
theorem TTotalEqv {A : Type} : Equivalence (@total A) := {
refl := by
intro _
exact trivial
symm := by
intro a1 a2 _
exact trivial
trans := by
intro a1 a2 a3 _ _
exact trivial
}[no new output]Example 3
Status: OK
-- ## The Kernel of a function
-- We introduce the kernel of a function
def Ker {A B : Type} (f : A → B) : A → A → Prop := by
intro a1 a2
exact f a1 = f a2
-- The kernel of a function is an equivalence relation
theorem TKerEqv {A B : Type} {f : A → B} : Equivalence (Ker f) := {
refl := by
intro a
exact rfl
symm := by
intro a1 a2 h1
exact h1.symm
trans := by
intro a1 a2 a3 h1 h2
exact h1.trans h2
}
end Equivalence
namespace Eqvgen
-- ## Equivalence generated by a relation
-- The equivalence generated by a relation `R` is
-- the smallest equivalence relation that contains `R`
inductive Eqvgen {A : Type} (R : A → A → Prop) : A → A → Prop where
| base : ∀ {a1 a2 : A}, (R a1 a2 → Eqvgen R a1 a2)
| refl : ∀ (a : A), Eqvgen R a a
| symm : ∀ {a1 a2 : A}, Eqvgen R a1 a2 → Eqvgen R a2 a1
| trans : ∀ {a1 a2 a3 : A}, (Eqvgen R a1 a2) → (Eqvgen R a2 a3) → (Eqvgen R a1 a3)
-- The equivalence generated by a relation is an equivalence relation
theorem TEqvgen {A : Type} (R : A → A → Prop) : Equivalence (Eqvgen R) := {
refl := Eqvgen.refl
symm := Eqvgen.symm
trans := Eqvgen.trans
}[no new output]Example 4
Status: OK
-- end Eqvgen
namespace Quotient
--https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Setoid
open Equivalence
-- ## Setoid
-- A **Setoid** is a type class that encapsulates
-- an equivalence relation on a given type.
#print Setoid
variable (A : Type)
variable (S : Setoid A)class Setoid.{u} (α : Sort u) : Sort (max 1 u)
number of parameters: 1
fields:
Setoid.r : α → α → Prop
Setoid.iseqv : Equivalence Setoid.r
constructor:
Setoid.mk.{u} {α : Sort u} (r : α → α → Prop) (iseqv : Equivalence r) : Setoid αExample 5
Status: OK
-- Elements of type `Setoid A` have two fields `r`,
-- the equivalence relation, and `iseqv`, a proof
-- of `r` being an equivalence relation
#check S.r
#check S.iseqv
/-
-- ### Equality of setoids
-- Two setoids are equal if if and only if
-- their associated relations are equal
theorem TEqSetoid {A : Type} {S T : Setoid A} : S = T ↔ S.r = T.r := by
apply Iff.intro
-- S = T → Setoid.r = Setoid.r
intro h
rw [h]
-- Setoid.r = Setoid.r → S = T
intro h
cases S
cases T
simp at *
congr
-/Setoid.r : A → A → Prop
Setoid.iseqv : Equivalence Setoid.rExample 6
Status: OK
-- -- ### Examples of Setoids
-- -- #### The diagonal Setoid
-- instance DiagSetoid {A : Type} : Setoid A := {
-- r := @diag A
-- iseqv := TDiagEqv
-- }
-- #### The total Setoid
instance TotalSetoid {A : Type} : Setoid A := {
r := @total A
iseqv := TTotalEqv
}[no new output]Example 7
Status: OK
-- -- #### The Kernel Setoid
-- instance KerSetoid {A B : Type} (f : A → B) : Setoid A := {
-- r := Ker f
-- iseqv := TKerEqv
-- }
-- ## Quotients
-- Setoids are used to make quotients
#print Quot
#print Quotient
-- Note that for a type `A` and `S : Setoid A`,
-- `Quotient S` is a type
#check Quotient SQuotient primitive Quot.{u} : {α : Sort u} → (α → α → Prop) → Sort u
def Quotient.{u} : {α : Sort u} → Setoid α → Sort u :=
fun {α} s => Quot Setoid.r
Quotient S : TypeExample 8
Status: OK
-- -- ### Examples of Quotients
-- -- #### The diagonal quotient `A/diag`
-- def QDiag {A : Type} := Quotient (@DiagSetoid A)
-- #### The total quotient `A/total`
def Qtotal {A : Type} := Quotient (@TotalSetoid A)[no new output]Example 9
Status: OK
-- -- #### The total quotient `A/Ker f`
-- def QKer {A B : Type} (f : A → B) := Quotient (KerSetoid f)
-- ### Elements of type `Quotient S`
-- To make an element of type `Quotient S`
-- we use the `Quotient.mk` keyword
-- This returns the class of `a` with respect to
-- the relation `S.r`, that is, all the elements of
-- of type `A` that are `S.r`-related with `a`
variable (a : A)
#check Quotient.mk S a
-- This in particular allows us to define the projection
-- function from a type `A` to its quotient
def pr {A : Type} (S : Setoid A) : A → Quotient S := by
intro a
exact Quotient.mk S a
-- All the elements of type `Quotient S`
-- are of this form, that is we can always find a
-- representative. This is done using `Quotient.exists_rep`
#check Quotient.exists_repQuotient.mk S a : Quotient S
Quotient.exists_rep.{u} {α : Sort u} {s : Setoid α} (q : Quotient s) : ∃ a, Quotient.mk s a = qExample 10
Status: OK
-- -- As a consequence, the projection function is surjective
-- theorem TprSurj {A : Type} (S : Setoid A) : surjective (pr S) := by
-- intro q
-- apply Quotient.exists_rep
-- -- Two classes are equal if, and only if,
-- -- their representatives are related. This double implication
-- -- is proven using the `Quotient.exact` and `Quotient.sound` keywords
-- theorem TEqQuotient {A : Type} {S : Setoid A} {a1 a2 : A} : (Quotient.mk S a1 = Quotient.mk S a2) ↔ (S.r a1 a2) := by
-- apply Iff.intro
-- -- Quotient.mk S a1 = Quotient.mk S a2 → Setoid.r a1 a2
-- apply Quotient.exact
-- -- Setoid.r a1 a2 → Quotient.mk S a1 = Quotient.mk S a2
-- apply Quotient.sound
-- -- ## Astriction
-- -- The astriction of a function
-- def ast {A B : Type} {S : Setoid B} (f : A → B) : A → Quotient S := by
-- intro a
-- exact Quotient.mk S (f a)
-- -- ## Coastriction
-- -- Coastriction of a function
-- -- For this we use `Quotient.lift`
-- def coast {A B : Type} {R : Setoid A} (f : A → B) (h : ∀ (a1 a2 : A), R.r a1 a2 → (Ker f) a1 a2) : Quotient R → B := by
-- apply Quotient.lift f
-- intro a1 a2 h1
-- exact (h a1 a2) h1
-- -- ## Biastriction
-- -- Biastriction of a function `biast = coast ∘ ast`
-- def biast {A B : Type} {R : Setoid A} {S : Setoid B} (f : A → B) (h : ∀ (a1 a2 : A), R.r a1 a2 → S.r (f a1) (f a2)) : Quotient R → Quotient S := by
-- apply coast (ast f)
-- intro a1 a2 hR
-- specialize h a1 a2
-- apply Quotient.sound
-- exact h hR
-- -- In particular, for two setoids `R1` and `R2` on `A`
-- -- satisfying that `R1.r` implies `R2.r` then there
-- -- exists a way of transforming elements
-- -- of type `Quotient R1` into elements of `Quotient R2`
-- -- For this we will biastrict the identity
-- def QuottoQuot {A : Type} {R1 R2 : Setoid A} (h : ∀ (a1 a2 : A), R1.r a1 a2 → R2.r a1 a2) : Quotient R1 → Quotient R2 := biast id h
end Quotient[no new output]Example 11
Status: OK
namespace Coequalizers
open Eqvgen Quotient
-- ## Coequalizers
-- The coequalizer of two functions `f g : A → B`
-- is the type of elements `b : B` up to the fact that elements
-- `f a` and `g a` are considered to be equal
-- It is a quotient type of `B`
-- We define the relation on `B` relating elements of the form
-- `f a` and `g a` for some `a : A`
def CoeqRel {A B : Type} (f g : A → B) : B → B → Prop := by
intro b1 b2
exact ∃ (a : A), (f a = b1) ∧ (g a = b2)
-- We next consider the equivalence relation
-- generated by the previous relation
def CoeqEqv {A B : Type} (f g : A → B) := Eqvgen (CoeqRel f g)[no new output]Example 12
Status: OK
-- ## The Coequalizer Setoid
-- This is the corresponding setoid
instance CoeqSetoid {A B : Type} (f g : A → B): Setoid B := {
r := CoeqEqv f g
iseqv := TEqvgen (CoeqRel f g)
}[no new output]Example 13
Status: OK
-- ## The coequalizer `Coeq f g`
-- We finally consider the quotient `Coeq f g`
def Coeq {A B : Type} (f g : A → B) : Type := Quotient (CoeqSetoid f g)[no new output]Example 14
Status: OK
-- The projection function from `B` to the coequalizer
def prCoeq {A B : Type} (f g : A → B) : B → Coeq f g := @pr B (CoeqSetoid f g)[no new output]Example 15
Status: OK
-- The projection function satisfies that `(prCoeq f g) ∘ f = (prCoeq f g) ∘ g`
theorem TCoeqPr {A B : Type} (f g : A → B) : (prCoeq f g) ∘ f = (prCoeq f g) ∘ g := by
apply funext
intro a
apply Quotient.sound
apply Eqvgen.base
apply Exists.intro a
apply And.intro
exact rfl
exact rfl
-- Universal property of the coequalizer
-- If there is another function `h : B → C` satisfying
-- `h ∘ f = h ∘ g`, then there exists a function `u : Coeq f g → C`
def u {A B C : Type} {f g : A → B} {h : B → C} (h1 : h ∘ f = h ∘ g) : Coeq f g → C := by
apply Quotient.lift h
intro b1 b2 h2
induction h2
-- Base case
rename_i c1 c2 h2
apply Exists.elim h2
intro a ⟨h2, h3⟩
calc
h c1 = h (f a) := congrArg h (h2.symm)
_ = (h ∘ f) a := rfl
_ = (h ∘ g) a := congrFun h1 a
_ = h (g a) := rfl
_ = h c2 := congrArg h h3
-- Rfl Case
rename_i c
exact rfl
-- Symm Case
rename_i c1 c2 _ h3
exact h3.symm
-- Trans Case
rename_i c1 c2 c3 _ _ h4 h5
exact h4.trans h5
-- The function `u` satisfies that `u ∘ prCoeq f g = h`
theorem TCoeqPrEq {A B C : Type} {f g : A → B} {h : B → C} (h1 : h ∘ f = h ∘ g) : (u h1) ∘ (prCoeq f g) = h := by
apply funext
intro b
exact rfl
-- The function `u` is unique in the sense that if there is another function
-- `v : Coeq f g → C` satisfying `v ∘ (prCoeq f g) = h`, then `v = u`
theorem TCoeqUni {A B C : Type} {f g : A → B} {h : B → C} (h1 : h ∘ f = h ∘ g) (v : Coeq f g → C) (h2 : v ∘ (prCoeq f g) = h) : v = u h1 := by
apply funext
intro z
have h3 : ∃ (b : B), Quotient.mk (CoeqSetoid f g) b = z := Quotient.exists_rep z
apply Exists.elim h3
intro b h4
calc
v z = v (prCoeq f g b) := congrArg v (h4.symm)
_ = (v ∘ prCoeq f g) b := rfl
_ = h b := congrFun h2 b
_ = ((u h1) ∘ (prCoeq f g)) b := congrFun (TCoeqPrEq h1) b
_ = (u h1) (prCoeq f g b) := rfl
_ = (u h1) z := congrArg (u h1) (h4)
namespace a10ExercisesCoeq
-- The function `prCoeq` is an epimorphism
theorem TprCoeqEpi {A B : Type} {f g : A → B} : epimorphism (prCoeq f g) := by
intro C v1 v2 h1
apply funext
intro z
have h3 : ∃ (b : B), Quotient.mk (CoeqSetoid f g) b = z := Quotient.exists_rep z
apply Exists.elim h3
intro b h4
calc
v1 z = v1 (prCoeq f g b) := congrArg v1 (h4.symm)
_ = (v1 ∘ prCoeq f g) b := rfl
_ = (v2 ∘ prCoeq f g) b := congrFun h1 b
_ = v2 (prCoeq f g b) := rfl
_ = v2 z := congrArg v2 (h4)
-- A monic `prCoeq` is an isomorphism
theorem TprCoeqMon {A B : Type} {f g : A → B} : monomorphism (prCoeq f g) → isomorphism (prCoeq f g) := by
intro h1
have h2 : f = g := by
apply @h1 A f g
exact TCoeqPr f g
let fu : Coeq f g → B := by
apply @u A B B f g id
exact h2
apply Exists.intro fu
apply And.intro
-- fu ∘ prCoeq f g = id
apply TCoeqPrEq
-- prCoeq f g ∘ fu = id
funext z
have h3 : ∃ (b : B), Quotient.mk (CoeqSetoid f g) b = z := Quotient.exists_rep z
apply Exists.elim h3
intro b h4
rw [h4.symm]
calc
(prCoeq f g ∘ fu) (Quotient.mk (CoeqSetoid f g) b) = (prCoeq f g) ((fu ∘ prCoeq f g) b) := congrArg (prCoeq f g) rfl
_ = (prCoeq f g) (id b) := congrArg (prCoeq f g) rfl
_ = (prCoeq f g) b := rfl
_ = id (Quotient.mk (CoeqSetoid f g) b) := rfl
end a10ExercisesCoeq
end Coequalizers
namespace a10Exercises
open a06Exercises
open Equivalence
open Quotient[no new output]Example 16
Status: OK
-- ## Exercises
-- The meet of two equivalence relations is
-- an equivalence relation
theorem TMeetEqv {A : Type} {R S : A → A → Prop} (hR : Equivalence R) (hS : Equivalence S) : Equivalence (R ∧ S) := {
refl := by
intro a
exact And.intro (hR.refl a) (hS.refl a)
symm := by
intro a1 a2 ⟨h1, h2⟩
exact And.intro (hR.symm h1) (hS.symm h2)
trans := by
intro a1 a2 a3 ⟨h1, h2⟩ ⟨h3, h4⟩
exact And.intro (hR.trans h1 h3) (hS.trans h2 h4)
}[no new output]Example 17
Status: OK
-- -- If two setoids have equivalent underlying relations
-- -- then the corresponding quotient types are equal
-- theorem TEqQuotype {A : Type} {R1 R2 : Setoid A}
-- (h : ∀ (a1 a2 : A), R1.r a1 a2 ↔ R2.r a1 a2) : Quotient R1 = Quotient R2 := by
-- have h1 : R1 = R2 := by
-- cases R1
-- rename_i R1r R1rEqv
-- cases R2
-- rename_i R2r R2rEqv
-- congr
-- funext a1 a2
-- apply propext
-- exact h a1 a2
-- rw [h1]
-- -- Universal property of quotient types
-- -- Ker (pr) = Setoid.r
-- theorem TUPQuot {A : Type} {R : Setoid A} : Ker (pr R) = R.r := by
-- funext a1 a2
-- apply propext
-- apply Iff.intro
-- -- Ker (pr R) a1 a2 → Setoid.r a1 a2
-- apply Quotient.exact
-- -- Setoid.r a1 a2 → Ker (pr R) a1 a2
-- apply Quotient.sound
-- -- Astriction `ast f = pr ∘ f`
-- theorem TAst {A B : Type} {f : A → B} {S : Setoid B}: (@ast A B S f) = (@pr B S) ∘ f := by
-- exact rfl
-- -- Universal property of the coastriction
-- -- `f = coast ∘ pr`
-- theorem TUPCoast {A B : Type} {R : Setoid A} {f : A → B} (h : ∀ (a1 a2 : A), R.r a1 a2 → (Ker f) a1 a2) : f = (coast f h) ∘ (@pr A R) := by
-- exact rfl
-- -- Unicity
-- theorem TUPCoastUn {A B : Type} {R : Setoid A} {f : A → B} (h : ∀ (a1 a2 : A), R.r a1 a2 → (Ker f) a1 a2) (g : Quotient R → B) (h1 : f = g ∘ (@pr A R)) : (coast f h) = g := by
-- apply funext
-- intro q
-- have ha : ∃ (a : A), Quotient.mk R a = q := Quotient.exists_rep q
-- apply Exists.elim ha
-- intro a haq
-- rw [haq.symm]
-- calc
-- coast f h (Quotient.mk R a) = ((coast f h) ∘ (@pr A R)) a := by exact rfl
-- _ = f a := by exact congrFun (TUPCoast h) a
-- _ = (g ∘ (@pr A R)) a := by exact congrFun h1 a
-- _ = g (Quotient.mk R a) := by exact rfl
-- -- ## Bijective types
-- -- We introduce the subtype of all
-- -- isomorphisms from a type `A` to a type `B`
-- def Iso (A B : Type) := {f : A → B // isomorphism f}[no new output]Example 18
Status: OK
-- -- We say that two types `A` and `B` are isomorphic if
-- -- there is some isomorphism from `A` to `B`
-- def Isomorphic : Type → Type → Prop := by
-- intro A B
-- exact Nonempty (Iso A B)
-- -- Notation for Isomorphic types (`\cong`)
-- notation : 65 lhs:65 " ≅ " rhs:66 => Isomorphic lhs rhs[no new output]Example 19
Status: OK
-- -- Being isomorphic is an equivalence relation
-- theorem TIsoEqv : Equivalence Isomorphic := {
-- refl := by
-- intro A
-- apply Nonempty.intro
-- apply Subtype.mk (@id A)
-- exact TIdMon A
-- symm := by
-- intro A B h
-- let f : Iso A B := Classical.choice h
-- apply Exists.elim f.property
-- intro g ⟨h1, h2⟩
-- apply Nonempty.intro
-- apply Subtype.mk g
-- apply Exists.intro f.val
-- apply And.intro
-- exact h2
-- exact h1
-- trans := by
-- intro A B C h1 h2
-- let f : Iso A B := Classical.choice h1
-- apply Exists.elim f.property
-- intro g ⟨h3, h4⟩
-- let h : Iso B C := Classical.choice h2
-- apply Exists.elim h.property
-- intro i ⟨h5, h6⟩
-- apply Nonempty.intro
-- apply Subtype.mk (h.val ∘ f.val)
-- apply Exists.intro (g ∘ i)
-- apply And.intro
-- calc
-- (g ∘ i) ∘ h.val ∘ f.val = g ∘ (i ∘ h.val) ∘ f.val := by exact rfl
-- _ = g ∘ id ∘ f.val := by rw [h5]
-- _ = g ∘ f.val := by exact rfl
-- _ = id := by rw [h3]
-- calc
-- (h.val ∘ f.val) ∘ g ∘ i = h.val ∘ (f.val ∘ g) ∘ i := by exact rfl
-- _ = h.val ∘ id ∘ i := by rw [h4]
-- _ = h.val ∘ i := by exact rfl
-- _ = id := by rw [h6]
-- }[no new output]Example 20
Status: OK
-- -- Under `Classical.choice`, every type `A` is isomorphic
-- -- to `A/diag`
-- theorem TDiag {A : Type} : A ≅ @QDiag A := by
-- apply Nonempty.intro
-- apply Subtype.mk (@pr A DiagSetoid)
-- let g : (@QDiag A) → A := by
-- apply (coast (@id A))
-- intro a1 a2 h
-- exact h
-- apply Exists.intro g
-- apply And.intro
-- -- Left
-- exact rfl
-- -- Right
-- funext q
-- let a : A := Classical.choose (Quotient.exists_rep q)
-- have hq : Quotient.mk (DiagSetoid) a = q := Classical.choose_spec (Quotient.exists_rep q)
-- rw [hq.symm]
-- apply Quotient.sound
-- exact rfl
-- -- Under `Classical.choice`, if two types `A` and `B` are
-- -- `Nonempty`, then `A/Total` and `B/Total` are isomorphic
-- theorem TTotal {A B : Type} (hA : Nonempty A) (hB : Nonempty B) : @Qtotal A ≅ @Qtotal B := by
-- apply Nonempty.intro
-- let f : A → B := by
-- intro _
-- exact Classical.choice hB
-- let fb : @Qtotal A → @Qtotal B := by
-- apply biast f
-- intro a1 a2 _
-- exact trivial
-- let g : B → A := by
-- intro _
-- exact Classical.choice hA
-- let gb : @Qtotal B → @Qtotal A := by
-- apply biast g
-- intro b1 b2 _
-- exact trivial
-- apply Subtype.mk fb
-- apply Exists.intro gb
-- apply And.intro
-- -- Left
-- funext q
-- let a : A := Classical.choose (Quotient.exists_rep q)
-- have hq : Quotient.mk (TotalSetoid) a = q := Classical.choose_spec (Quotient.exists_rep q)
-- rw [hq.symm]
-- apply Quotient.sound
-- exact trivial
-- -- Right
-- funext q
-- let b : B := Classical.choose (Quotient.exists_rep q)
-- have hq : Quotient.mk (TotalSetoid) b = q := Classical.choose_spec (Quotient.exists_rep q)
-- rw [hq.symm]
-- apply Quotient.sound
-- exact trivial
-- -- Under `Classical.choice`, for every function `f : A → B`
-- -- the quotient `A/Ker f` is isomorphic to `Im f`
-- theorem TKerIm {A B : Type} (f : A → B) : QKer f ≅ Im f := by
-- let fe : A → Im f := by
-- apply correst f
-- intro b
-- exact b.property
-- let fb : QKer f → Im f := by
-- apply coast fe
-- intro a1 a2 h
-- apply Subtype.eq
-- exact h
-- apply Nonempty.intro
-- apply Subtype.mk fb
-- apply TCarBijIso.mp
-- apply And.intro
-- -- Injective
-- intro q1 q2 h1
-- let a1 : A := Classical.choose (Quotient.exists_rep q1)
-- have hq1 : Quotient.mk (KerSetoid f) a1 = q1 := Classical.choose_spec (Quotient.exists_rep q1)
-- let a2 : A := Classical.choose (Quotient.exists_rep q2)
-- have hq2 : Quotient.mk (KerSetoid f) a2 = q2 := Classical.choose_spec (Quotient.exists_rep q2)
-- rw [hq1.symm, hq2.symm] at h1
-- rw [hq1.symm, hq2.symm]
-- apply Quotient.sound
-- have h3 : f a1 = f a2 := by
-- calc
-- f a1 = (fe a1).val := rfl
-- _ = (fe a2).val := by exact congrArg Subtype.val h1
-- _ = f a2 := rfl
-- exact h3
-- -- Surjective
-- intro b
-- cases b.property
-- rename_i a h2
-- apply Exists.intro (Quotient.mk (KerSetoid f) a)
-- apply Subtype.eq
-- exact h2
-- end a10Exercises[no new output]Chapter 11: Orders
Example 1
Status: OK
-- # Orders
import a03Quantifiers
import a06NaturalNumbers
import a09Relations
import a10Equivalence
open Operations
open N
open a06Exercises[no output]Example 2
Status: OK
-- Definition of a preorder
structure Preorder {A : Type} (R : A → A → Prop) : Prop where
refl : ∀ (a : A), R a a
trans : ∀ {a b c : A}, R a b → R b c → R a c
-- Definition of a partial order
structure PartialOrder {A : Type} (R : A → A → Prop) : Prop where
toPreorder : Preorder R
antisymm : ∀ {a b : A}, R a b → R b a → a = b
-- Definition of a poset
structure Poset where
base : Type
R : base → base → Prop
toPartialOrder : PartialOrder R
-- ## Inverse Partial Order
-- If `R` is a preorder, then `R^` is a preorder
theorem TPreorderInv {A : Type} (R : A → A → Prop) : Preorder R → Preorder (inverse R) := by
intro h
apply Preorder.mk
-- Refl
intro a
rw [inverse]
exact h.refl a
-- Trans
intro a b c h1 h2
rw [inverse] at *
exact h.trans h2 h1
-- If `R` is a partial ordre, then `R^` is a partial order
theorem TPartialOrderInv {A : Type} (R : A → A → Prop) : PartialOrder R → PartialOrder (inverse R) := by
intro h
apply PartialOrder.mk
-- toPreoder
exact TPreorderInv R (h.toPreorder)
-- antisymm
intro a b h1 h2
exact h.antisymm h2 h1
-- ## Special Elements
-- `z` is a **least element** with respect to `R` if `R z a`, for every `a : A`
def Least {A : Type} (R : A → A → Prop) (z : A) : Prop := ∀ {a : A}, R z a
-- `z` is a **greatest element** with respect to `R` if `R a z`, for every `a : A`
def Greatest {A : Type} (R : A → A → Prop) (z : A) : Prop := ∀ {a : A}, R a z[no output]Example 3
Status: OK
-- `z` is a **minimal element** if no strictly smaller element exists
def Minimal {A : Type} (R : A → A → Prop) (z : A) : Prop := ∀ {a : A}, R a z → a = z
-- `z` is a **maximal element** if no strictly greater element exists
def Maximal {A : Type} (R : A → A → Prop) (z : A) : Prop := ∀ {a : A}, R z a → a = z[no output]Example 4
Status: OK
-- -- ### Bounded Posets
-- -- Posets with a least and greatest element
-- structure BoundedPoset extends Poset where
-- l : base
-- least : Least R l
-- g : base
-- greatest : Greatest R g
-- -- ### Exercises
-- -- If `R` is a partial order and `z1` and `z2` are least
-- -- elements, then they are equal
-- theorem LeastUnique {A : Type} (R : A → A → Prop) (z1 z2 : A) (h : PartialOrder R) (h1 : Least R z1) (h2 : Least R z2) : z1 = z2 := h.antisymm h1 h2[no output]Example 5
Status: OK
-- -- If `R` is a partial order and `z1` and `z2` are greatest
-- -- elements, then they are equal
-- theorem GreatestUnique {A : Type} (R : A → A → Prop) (z1 z2 : A) (h : PartialOrder R) (h1 : Greatest R z1) (h2 : Greatest R z2) : z1 = z2 := h.antisymm h2 h1[no output]Example 6
Status: OK
-- -- If `R` is a partial order and `z` is the least element,
-- -- then it is a minimal element
-- def LeasttoMinimal {A : Type} (R : A → A → Prop) (z : A) (h : PartialOrder R) : Least R z → Minimal R z := by
-- intro h1 a h2
-- exact h.antisymm h2 h1
-- -- If `R` is a partial order and `z` is the greatest element,
-- -- then it is a maximal element
-- def GreatesttoMaximal {A : Type} (R : A → A → Prop) (z : A) (h : PartialOrder R) : Greatest R z → Maximal R z := by
-- intro h1 a h2
-- exact h.antisymm h1 h2
-- -- A least element for `R` is a greatest element for `R^`
-- def LeasttoGreatestInv {A : Type} (R : A → A → Prop) (z : A) : Least R z → Greatest (inverse R) z := by
-- intro h1 a
-- exact h1
-- -- A greatest element for `R` is a least element for `R^`
-- def GreatesttoLeastInv {A : Type} (R : A → A → Prop) (z : A) : Greatest R z → Least (inverse R) z := by
-- intro h1 a
-- exact h1
-- -- A minimal element for `R` is a maximal element for `R^`
-- def MinimaltoMaximalInv {A : Type} (R : A → A → Prop) (z : A) : Minimal R z → Maximal (inverse R) z := by
-- intro h1 a
-- exact h1
-- -- A maximal element for `R` is a minimal element for `R^`
-- def MaximaltoMinimalInv {A : Type} (R : A → A → Prop) (z : A) : Maximal R z → Minimal (inverse R) z := by
-- intro h1 a
-- exact h1
-- -- ## Orders Relative to Subtypes
-- -- The `Restriction` of a relation to a Subtype
-- def Restriction {A : Type} (R : A → A → Prop) (P : A → Prop) : Subtype P → Subtype P → Prop := by
-- intro a1 a2
-- exact R a1.val a2.val
-- -- If `R` is a preorder then `Restriction R P`, for a
-- -- predicate `P`, is a preorder
-- theorem TPRestriction {A : Type} (R : A → A → Prop) (P : A → Prop) : Preorder R → Preorder (Restriction R P) := by
-- intro h
-- apply Preorder.mk
-- --refl
-- intro a
-- exact h.refl a.val
-- -- trans
-- intro a b c h1 h2
-- exact h.trans h1 h2
-- -- If `R` is a partial order then `Restriction R P`, for a
-- -- predicate `P`, is a partial ordre
-- theorem TPORestriction {A : Type} (R : A → A → Prop) (P : A → Prop) : PartialOrder R → PartialOrder (Restriction R P) := by
-- intro h
-- apply PartialOrder.mk
-- -- toPreorder
-- exact TPRestriction R P (h.toPreorder)
-- -- antisymm
-- intro a b h1 h2
-- apply Subtype.eq
-- exact h.antisymm h1 h2
-- -- ### Special Elements relative to a Subtype
-- -- `z` is an **upper bound** of a subtype `P` if it is above
-- -- all the elements of `Subtype P`
-- def UpperBound {A : Type} (R : A → A → Prop) (P : A → Prop) (z : A) : Prop := ∀ (a : A), P a → R a z[no output]Example 7
Status: OK
-- -- `z` is the **supremum** of a subtype `P` if it is an
-- -- upper bound, and any other upper bound is greater
-- -- or equal than `z`
-- structure Supremum {A : Type} (R : A → A → Prop) (P : A → Prop) (z : A) : Prop where
-- -- Upper Bound
-- UB : (UpperBound R P z)
-- -- Least Upper Bound
-- LUB : ∀ (x : A), (UpperBound R P x → R z x)
-- -- `z` is the **maximum** element of a subtype `P` if it
-- -- is the Greatest element of subtype `P`
-- structure Maximum {A : Type} (R : A → A → Prop) (P : A → Prop) (z : A) : Prop where
-- -- Supremum
-- toSupremum : (Supremum R P z)
-- -- In Subtype P
-- Sub : P z
-- -- `z` is a **lower bound** of a subtype `P` if it is below
-- -- all the elements of `Subtype P`
-- def LowerBound {A : Type} (R : A → A → Prop) (P : A → Prop) (z : A) : Prop := ∀ (a : A), P a → R z a[no output]Example 8
Status: OK
-- -- `z` is the **infimum** of a subtype `P` if it is a
-- -- lower bound, and any other lower bound is smaller
-- -- or equal than `z`
-- structure Infimum {A : Type} (R : A → A → Prop) (P : A → Prop) (z : A) : Prop where
-- -- Lower Bound
-- LB : (LowerBound R P z)
-- -- Greatest Lower Bound
-- GLB : ∀ (x : A), (LowerBound R P x → R x z)
-- -- `z` is the **minimum** element of a subtype `P` if it
-- -- is the Least element of subtype `P`
-- structure Minimum {A : Type} (R : A → A → Prop) (P : A → Prop) (z : A) : Prop where
-- -- Infimum
-- toInfimum : (Infimum R P z)
-- -- In Subtype P
-- Sub : P z
-- -- #### Exercises
-- -- The supremum of the False predicate is the least element
-- theorem TLeastSupPFalse {A : Type} (R : A → A → Prop) (z : A) : Least R z ↔ Supremum R PFalse z := by
-- apply Iff.intro
-- -- Least R z → Supremum R PFalse z
-- intro h
-- apply Supremum.mk
-- -- UpperBound R PFalse z
-- intro a ha
-- exact False.elim ha
-- -- ∀ (x : A), UpperBound R PFalse x → R z x
-- intro x _
-- exact h
-- -- Supremum R PFalse z → Least R z
-- intro ⟨_, h2⟩ a
-- specialize h2 a
-- apply h2
-- intro x hx
-- exact False.elim hx
-- -- The infimum of the False predicate is the greatest element
-- theorem TGreatestInfPFalse {A : Type} (R : A → A → Prop) (z : A) : Greatest R z ↔ Infimum R PFalse z := by
-- apply Iff.intro
-- -- Greatest R z → Infimum R PFalse z
-- intro h
-- apply Infimum.mk
-- -- LowerBound R PFalse z
-- intro a ha
-- exact False.elim ha
-- -- ∀ (x : A), LowerBound R PFalse x → R x z
-- intro x _
-- exact h
-- -- Infimum R PFalse z → Greatest R z
-- intro ⟨_, h2⟩ a
-- specialize h2 a
-- apply h2
-- intro x hx
-- exact False.elim hx
-- -- The infimum of the True predicate is the least element
-- theorem TLeastInfPTrue {A : Type} (R : A → A → Prop) (z : A) : Least R z ↔ Infimum R PTrue z := by
-- apply Iff.intro
-- -- Least R z → Infimum R PTrue z
-- intro h1
-- apply Infimum.mk
-- -- LowerBound R PTrue z
-- intro a _
-- exact h1
-- -- ∀ (x : A), LowerBound R PTrue x → R x z
-- intro a h2
-- apply h2
-- exact trivial
-- -- Infimum R PTrue z → Least R z
-- intro ⟨h1, _⟩ a
-- apply h1
-- exact trivial
-- -- The supremum of the True predicate is the greatest element
-- theorem TGreatestSupPTrue {A : Type} (R : A → A → Prop) (z : A) : Greatest R z ↔ Supremum R PTrue z := by
-- apply Iff.intro
-- -- Greatest R z → Supremum R PTrue z
-- intro h1
-- apply Supremum.mk
-- -- UpperBound R PTrue z
-- intro a _
-- exact h1
-- -- ∀ (x : A), UpperBound R PTrue x → R z x
-- intro a h2
-- apply h2
-- exact trivial
-- -- Supremum R PTrue z → Greatest R z
-- intro ⟨h1, _⟩ a
-- apply h1
-- exact trivial
-- -- ### Lattice
-- -- Posets with a infimum and supremum for every pair of elements
-- @[ext] structure Lattice extends Poset where
-- meet : base → base → base
-- infimum : ∀ {a b : base}, Infimum R (fun (x : base) => (x = a) ∨ (x = b)) (meet a b)
-- join : base → base → base
-- supremum : ∀ {a b : base}, Supremum R (fun (x : base) => (x = a) ∨ (x = b)) (join a b)
-- -- There is an alternative way to describe a lattice
-- -- as an algebra `(A, ∧, ∨)` with two binary, commutative
-- -- and associative operations satisfying the absorption laws
-- @[ext] structure LatticeAlg where
-- base : Type
-- meet : base → base → base
-- join : base → base → base
-- meetcomm : ∀ {a b : base}, meet a b = meet b a
-- joincomm : ∀ {a b : base}, join a b = join b a
-- meetass : ∀ {a b c : base}, meet (meet a b) c = meet a (meet b c)
-- joinass : ∀ {a b c : base}, join (join a b) c = join a (join b c)
-- abslaw1 : ∀ {a b : base}, join a (meet a b) = a
-- abslaw2 : ∀ {a b : base}, meet a (join a b) = a
-- -- The opposite of a Lattice, intercharging meet and join
-- def LatticeAlgOp : LatticeAlg → LatticeAlg := by
-- intro C
-- refine {
-- base := C.base,
-- meet := C.join,
-- join := C.meet,
-- meetcomm := C.joincomm,
-- joincomm := C.meetcomm,
-- meetass := C.joinass,
-- joinass := C.meetass,
-- abslaw1 := C.abslaw2,
-- abslaw2 := C.abslaw1
-- }
-- -- The opposite of the opposite is the original Lattice
-- theorem TIdLatticeAlgOp : LatticeAlgOp ∘ LatticeAlgOp = id := by
-- funext C
-- apply LatticeAlg.ext
-- -- Base
-- exact rfl
-- -- Meet
-- exact HEq.refl ((LatticeAlgOp ∘ LatticeAlgOp) C).meet
-- -- Join
-- exact HEq.refl ((LatticeAlgOp ∘ LatticeAlgOp) C).join
-- -- There are usually 2 more laws regarding the idempotency
-- -- of the meet and join operations that can be derived
-- -- from the other axioms
-- theorem meetidpt {C : LatticeAlg} : ∀ (a : C.base), C.meet a a = a := by
-- intro a
-- calc
-- C.meet a a = C.meet a (C.join a (C.meet a a)) := congrArg (C.meet a) C.abslaw1.symm
-- _ = a := C.abslaw2
-- theorem joinidpt {C : LatticeAlg} : ∀ (a : C.base), C.join a a = a := by
-- intro a
-- calc
-- C.join a a = C.join a (C.meet a (C.join a a)) := congrArg (C.join a) C.abslaw2.symm
-- _ = a := C.abslaw1
-- -- The following result will be of interest later
-- theorem meetjoin {C : LatticeAlg} : ∀ {a b : C.base}, (C.meet a b = a) ↔ (C.join a b = b) := by
-- intro a b
-- apply Iff.intro
-- -- C.meet a b = a → C.join a b = b
-- intro h
-- rw [C.meetcomm] at h
-- rw [C.joincomm, h.symm]
-- exact C.abslaw1
-- -- C.join a b = b → C.meet a b = a
-- intro h
-- rw [h.symm]
-- exact C.abslaw2
-- -- Any Lattice induces a LatticeAlg
-- def LatticetoLatticeAlg : Lattice → LatticeAlg := by
-- intro C
-- refine {
-- base := C.base,
-- meet := C.meet,
-- join := C.join,
-- meetcomm := by
-- intro a b
-- apply C.toPoset.toPartialOrder.antisymm
-- -- C.R (C.meet a b) (C.meet b a)
-- apply C.infimum.GLB
-- intro z h
-- cases h
-- -- b
-- rename_i hz
-- apply C.infimum.LB
-- exact Or.inr hz
-- -- a
-- rename_i hz
-- apply C.infimum.LB
-- exact Or.inl hz
-- -- C.R (C.meet b a) (C.meet a b)
-- apply C.infimum.GLB
-- intro z h
-- cases h
-- -- a
-- rename_i hz
-- apply C.infimum.LB
-- exact Or.inr hz
-- -- b
-- rename_i hz
-- apply C.infimum.LB
-- exact Or.inl hz
-- joincomm := by
-- intro a b
-- apply C.toPoset.toPartialOrder.antisymm
-- -- C.R (C.join a b) (C.join b a)
-- apply C.supremum.LUB
-- intro z h
-- cases h
-- -- a
-- rename_i hz
-- apply C.supremum.UB
-- exact Or.inr hz
-- -- b
-- rename_i hz
-- apply C.supremum.UB
-- exact Or.inl hz
-- -- C.R (C.join b a) (C.join a b)
-- apply C.supremum.LUB
-- intro z h
-- cases h
-- -- b
-- rename_i hz
-- apply C.supremum.UB
-- exact Or.inr hz
-- -- a
-- rename_i hz
-- apply C.supremum.UB
-- exact Or.inl hz
-- meetass := by
-- intro a b c
-- apply C.toPoset.toPartialOrder.antisymm
-- -- C.R (C.meet (C.meet a b) c) (C.meet a (C.meet b c))
-- apply C.infimum.GLB
-- intro z h
-- cases h
-- -- a
-- rename_i hz
-- have h1 : C.R (C.meet (C.meet a b) c) (C.meet a b) := by
-- apply C.infimum.LB
-- exact Or.inl rfl
-- have h2 : C.R (C.meet a b) z := by
-- apply C.infimum.LB
-- exact Or.inl hz
-- exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
-- -- C.meet b c
-- rename_i hz
-- rw [hz]
-- apply C.infimum.GLB
-- intro d hd
-- cases hd
-- -- b
-- rename_i hd
-- rw [hd]
-- have h1 : C.R (C.meet (C.meet a b) c) (C.meet a b) := by
-- apply C.infimum.LB
-- exact Or.inl rfl
-- have h2 : C.R (C.meet a b) b := by
-- apply C.infimum.LB
-- exact Or.inr rfl
-- exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
-- -- c
-- rename_i hd
-- apply C.infimum.LB
-- exact Or.inr hd
-- -- C.R (C.meet a (C.meet b c)) (C.meet (C.meet a b) c)
-- apply C.infimum.GLB
-- intro z h
-- cases h
-- -- C.meet a b
-- rename_i hz
-- rw [hz]
-- apply C.infimum.GLB
-- intro d hd
-- cases hd
-- -- a
-- rename_i hd
-- apply C.infimum.LB
-- exact Or.inl hd
-- -- b
-- rename_i hd
-- rw [hd]
-- have h1 : C.R (C.meet a (C.meet b c)) (C.meet b c) := by
-- apply C.infimum.LB
-- exact Or.inr rfl
-- have h2 : C.R (C.meet b c) b := by
-- apply C.infimum.LB
-- exact Or.inl rfl
-- exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
-- -- c
-- rename_i hz
-- have h1 : C.R (C.meet a (C.meet b c)) (C.meet b c) := by
-- apply C.infimum.LB
-- exact Or.inr rfl
-- have h2 : C.R (C.meet b c) z := by
-- apply C.infimum.LB
-- exact Or.inr hz
-- exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
-- joinass := by
-- intro a b c
-- apply C.toPoset.toPartialOrder.antisymm
-- -- C.R (C.join (C.join a b) c) (C.join a (C.join b c))
-- apply C.supremum.LUB
-- intro z h
-- cases h
-- -- C.join a b
-- rename_i hz
-- rw [hz]
-- apply C.supremum.LUB
-- intro d hd
-- cases hd
-- -- a
-- rename_i hd
-- apply C.supremum.UB
-- exact Or.inl hd
-- -- b
-- rename_i hd
-- have h1 : C.R d (C.join b c) := by
-- apply C.supremum.UB
-- exact Or.inl hd
-- have h2 : C.R (C.join b c) (C.join a (C.join b c)) := by
-- apply C.supremum.UB
-- exact Or.inr rfl
-- exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
-- -- c
-- rename_i hz
-- have h1 : C.R z (C.join b c) := by
-- apply C.supremum.UB
-- exact Or.inr hz
-- have h2 : C.R (C.join b c) (C.join a (C.join b c)) := by
-- apply C.supremum.UB
-- exact Or.inr rfl
-- exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
-- -- C.R (C.join a (C.join b c)) (C.join (C.join a b) c)
-- apply C.supremum.LUB
-- intro z h
-- cases h
-- -- a
-- rename_i hz
-- have h1 : C.R z (C.join a b) := by
-- apply C.supremum.UB
-- exact Or.inl hz
-- have h2 : C.R (C.join a b) (C.join (C.join a b) c) := by
-- apply C.supremum.UB
-- exact Or.inl rfl
-- exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
-- -- C.join b c
-- rename_i hz
-- rw [hz]
-- apply C.supremum.LUB
-- intro d hd
-- cases hd
-- -- b
-- rename_i hd
-- have h1 : C.R d (C.join a b) := by
-- apply C.supremum.UB
-- exact Or.inr hd
-- have h2 : C.R (C.join a b) (C.join (C.join a b) c) := by
-- apply C.supremum.UB
-- exact Or.inl rfl
-- exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
-- -- c
-- rename_i hd
-- apply C.supremum.UB
-- exact Or.inr hd
-- abslaw1 := by
-- intro a b
-- apply C.toPoset.toPartialOrder.antisymm
-- -- C.R (C.join a (C.meet a b)) a
-- apply C.supremum.LUB
-- intro d hd
-- cases hd
-- -- a
-- rename_i hd
-- rw [hd]
-- apply C.toPoset.toPartialOrder.toPreorder.refl
-- -- C.meet a b
-- rename_i hd
-- rw [hd]
-- apply C.infimum.LB
-- exact Or.inl rfl
-- -- C.R a (C.join a (C.meet a b))
-- apply C.supremum.UB
-- exact Or.inl rfl
-- abslaw2 := by
-- intro a b
-- apply C.toPoset.toPartialOrder.antisymm
-- -- C.R (C.meet a (C.join a b)) a
-- apply C.infimum.LB
-- exact Or.inl rfl
-- -- C.R a (C.meet a (C.join a b))
-- apply C.infimum.GLB
-- intro d hd
-- cases hd
-- -- a
-- rename_i hd
-- rw [hd]
-- apply C.toPoset.toPartialOrder.toPreorder.refl
-- -- C.join a b
-- rename_i hd
-- rw [hd]
-- apply C.supremum.UB
-- exact Or.inl rfl
-- }
-- -- Every LatticeAlg induces a relation on its base
-- def LAR {C : LatticeAlg} : C.base → C.base → Prop := by
-- intro a b
-- exact C.meet a b = a
-- -- `LAR` is a preorder
-- theorem TLARPreorder {C : LatticeAlg} : Preorder (@LAR C) := by
-- apply Preorder.mk
-- -- refl
-- intro a
-- rw [LAR]
-- exact meetidpt a
-- -- trans
-- intro a b c h1 h2
-- rw [LAR] at *
-- rw [h1.symm, C.meetass, h2]
-- -- `LAR` is a partial order
-- theorem TLARPartialOrder {C : LatticeAlg} : PartialOrder (@LAR C) := by
-- apply PartialOrder.mk
-- -- toPreorder
-- exact TLARPreorder
-- -- antisymm
-- intro a b h1 h2
-- calc
-- a = C.meet a b := h1.symm
-- _ = C.meet b a := C.meetcomm
-- _ = b := h2
-- -- Every LatticeAlg induces a Poset
-- def LatticeAlgtoPoset : LatticeAlg → Poset := by
-- intro C
-- refine {
-- base := C.base,
-- R := @LAR C,
-- toPartialOrder := TLARPartialOrder
-- }
-- -- Every LatticeAlg induces a Lattice
-- def LatticeAlgtoLattice : LatticeAlg → Lattice := by
-- intro C
-- refine {
-- toPoset := {
-- base := C.base,
-- R := @LAR C,
-- toPartialOrder := TLARPartialOrder
-- }
-- meet := C.meet,
-- infimum := by
-- intro a b
-- apply Infimum.mk
-- -- LowerBound
-- intro z hz
-- cases hz
-- -- a
-- rename_i hz
-- rw [hz]
-- have h1 : C.meet (C.meet a b) a = (C.meet a b) := by
-- calc
-- C.meet (C.meet a b) a = C.meet a (C.meet a b) := C.meetcomm.symm
-- _ = C.meet (C.meet a a) b := C.meetass.symm
-- _ = C.meet a b := congrArg (fun x => C.meet x b) (meetidpt a)
-- exact h1
-- -- b
-- rename_i hz
-- rw [hz]
-- have h1 : C.meet (C.meet a b) b = (C.meet a b) := by
-- calc
-- C.meet (C.meet a b) b = C.meet a (C.meet b b) := C.meetass
-- _ = C.meet a b := congrArg (fun x => C.meet a x) (meetidpt b)
-- exact h1
-- -- Greatest LowerBound
-- intro x h
-- have ha : C.meet x a = x := by
-- apply h
-- exact Or.inl rfl
-- have hb : C.meet x b = x := by
-- apply h
-- exact Or.inr rfl
-- have h1 : C.meet x (C.meet a b) = x := by
-- calc
-- C.meet x (C.meet a b) = C.meet (C.meet x a) b := C.meetass.symm
-- _ = C.meet x b := congrArg (fun z => C.meet z b) ha
-- _ = x := hb
-- exact h1
-- join := C.join,
-- supremum := by
-- intro a b
-- apply Supremum.mk
-- -- UpperBound
-- intro z hz
-- cases hz
-- -- a
-- rename_i hz
-- rw [hz]
-- exact C.abslaw2
-- -- b
-- rename_i hz
-- rw [hz, C.joincomm]
-- exact C.abslaw2
-- -- Least UpperBound
-- intro x h
-- have ha : C.meet a x = a := by
-- apply h
-- exact Or.inl rfl
-- have hb : C.meet b x = b := by
-- apply h
-- exact Or.inr rfl
-- have hax : C.join a x = x := meetjoin.mp ha
-- have hbx : C.join b x = x := meetjoin.mp hb
-- have h1 : C.join (C.join a b) x = x := by
-- calc
-- C.join (C.join a b) x = C.join a (C.join b x) := C.joinass
-- _ = C.join a x := congrArg (fun z => C.join a z) hbx
-- _ = x := hax
-- exact meetjoin.mpr h1
-- }
-- --
-- theorem TIdLattice : LatticeAlgtoLattice ∘ LatticetoLatticeAlg = id := by
-- funext C
-- apply Lattice.ext
-- -- base
-- exact rfl
-- -- R
-- have hR : (LatticeAlgtoLattice (LatticetoLatticeAlg C)).R = C.R := by
-- funext a b
-- apply propext
-- apply Iff.intro
-- -- ((LatticeAlgtoLattice ∘ LatticetoLatticeAlg) C).R a b → C.R a b
-- intro h
-- have hs : C.meet a b = a := h
-- rw [hs.symm]
-- apply C.infimum.LB
-- exact Or.inr rfl
-- -- C.R a b → (LatticeAlgtoLattice (LatticetoLatticeAlg C)).R a b
-- intro h
-- have hs : C.meet a b = a := by
-- apply C.toPoset.toPartialOrder.antisymm
-- -- C.R (C.meet a b) a
-- apply C.infimum.LB
-- exact Or.inl rfl
-- -- C.R a (C.meet a b)
-- apply C.infimum.GLB
-- intro z hz
-- cases hz
-- -- a
-- rename_i hz
-- rw [hz]
-- exact C.toPoset.toPartialOrder.toPreorder.refl a
-- -- b
-- rename_i hz
-- rw [hz]
-- exact h
-- exact hs
-- exact heq_of_eq hR
-- -- meet
-- exact HEq.refl C.meet
-- -- join
-- exact HEq.refl C.join
-- --
-- theorem TIdLatticeAlg : LatticetoLatticeAlg ∘ LatticeAlgtoLattice = id := by
-- funext C
-- apply LatticeAlg.ext
-- -- base
-- exact rfl
-- -- meet
-- exact HEq.refl C.meet
-- -- join
-- exact HEq.refl C.join
-- -- ## Distributive Lattice
-- -- Distributive Lattice
-- @[ext] structure DistLatticeAlg extends LatticeAlg where
-- dist : ∀ {a b c : base}, meet a (join b c) = join (meet a b) (meet a c)
-- def LatticeAlgtoDistLatticeAlg {C : LatticeAlg} : (∀ {a b c : C.base}, (@LAR C) (C.meet a (C.join b c)) (C.join (C.meet a b) (C.meet a c))) → DistLatticeAlg := by
-- intro h
-- refine {
-- toLatticeAlg := C,
-- dist := by
-- intro a b c
-- apply (@TLARPartialOrder C).antisymm
-- -- (C.meet a (C.join b c)) ≤ (C.join (C.meet a b) (C.meet a c))
-- exact h
-- -- (C.join (C.meet a b) (C.meet a c)) ≤ (C.meet a (C.join b c))
-- apply (@LatticeAlgtoLattice C).infimum.GLB
-- intro z h1
-- cases h1
-- -- z = a
-- rename_i h1
-- rw [h1]
-- apply (@LatticeAlgtoLattice C).supremum.LUB
-- intro w h2
-- cases h2
-- rename_i h2
-- rw [h2]
-- apply (@LatticeAlgtoLattice C).infimum.LB
-- exact Or.inl rfl
-- rename_i h2
-- rw [h2]
-- apply (@LatticeAlgtoLattice C).infimum.LB
-- exact Or.inl rfl
-- -- z = b ∨ c
-- rename_i h1
-- rw [h1]
-- apply (@LatticeAlgtoLattice C).supremum.LUB
-- intro w h2
-- cases h2
-- rename_i h2
-- rw [h2]
-- have h3 : (LatticeAlgtoLattice C).R (C.meet a b) b := by
-- apply (@LatticeAlgtoLattice C).infimum.LB
-- exact Or.inr rfl
-- have h4 : (LatticeAlgtoLattice C).R b (C.join b c) := by
-- apply (@LatticeAlgtoLattice C).supremum.UB
-- exact Or.inl rfl
-- exact (@LatticeAlgtoLattice C).toPoset.toPartialOrder.toPreorder.trans h3 h4
-- rename_i h2
-- rw [h2]
-- have h3 : (LatticeAlgtoLattice C).R (C.meet a c) c := by
-- apply (@LatticeAlgtoLattice C).infimum.LB
-- exact Or.inr rfl
-- have h4 : (LatticeAlgtoLattice C).R c (C.join b c) := by
-- apply (@LatticeAlgtoLattice C).supremum.UB
-- exact Or.inr rfl
-- exact (@LatticeAlgtoLattice C).toPoset.toPartialOrder.toPreorder.trans h3 h4
-- }
-- -- ### Complete Lattice
-- -- Posets with a infimum and supremum for every subtype
-- structure CompleteLattice extends Poset where
-- meet : (base → Prop) → base
-- infimum : ∀ {P : base → Prop}, Infimum R P (meet P)
-- join : (base → Prop) → base
-- supremum : ∀ {P : base → Prop}, Supremum R P (join P)
-- -- Every CompleteLattice is a Bounded Poset
-- def CompleteLatticetoBoundedPoset : CompleteLattice → BoundedPoset := by
-- intro C
-- refine {
-- toPoset := C.toPoset,
-- l := C.join (PFalse),
-- least := (TLeastSupPFalse C.R (C.join PFalse)).mpr (C.supremum)
-- g := C.meet (PFalse),
-- greatest := (TGreatestInfPFalse C.R (C.meet PFalse)).mpr (C.infimum)
-- }
-- -- Every CompleteLattice is a Lattice
-- def CompleteLatticetoLattice : CompleteLattice → Lattice := by
-- intro C
-- refine {
-- toPoset := C.toPoset,
-- meet := (fun a b => C.meet (fun (x : C.base) => (x = a) ∨ (x = b))),
-- infimum := fun {a b} => C.infimum
-- join := (fun a b => C.join (fun (x : C.base) => (x = a) ∨ (x = b))),
-- supremum := fun {a b} => C.supremum
-- }
-- namespace NLeq
-- -- The `≤` relation for `N`
-- def NLeq : N → N → Prop := by
-- intro n m
-- exact ∃ (k : N), n + k = m
-- -- Notation for `≤`
-- notation : 65 lhs:65 " ≤ " rhs:66 => NLeq lhs rhs[no output]Example 9
Status: OK
-- -- `≤` is a preorder
-- theorem TPreorderNLeq : Preorder NLeq := by
-- apply Preorder.mk
-- -- refl
-- intro n
-- apply Exists.intro z
-- exact TAdd0R
-- -- trans
-- intro n m p h1 h2
-- apply Exists.elim h1
-- intro a h3
-- apply Exists.elim h2
-- intro b h4
-- apply Exists.intro (a + b)
-- calc
-- n + (a + b) = (n + a) + b := TAddAss.symm
-- _ = m + b := TAddCongL h3
-- _ = p := h4
-- -- `≤` is a partial order
-- theorem TPartialOrderNLeq : PartialOrder NLeq := by
-- apply PartialOrder.mk
-- -- toPreorder
-- exact TPreorderNLeq
-- -- antisymm
-- intro n m h1 h2
-- apply Exists.elim h1
-- intro a h1
-- apply Exists.elim h2
-- intro b h2
-- rw [h1.symm, TAddAss] at h2
-- have h3 : (a + b) = z := TAddCancLZ h2
-- have h4 : a = z := TAddZ h3
-- rw [h4] at h1
-- rw [h1.symm]
-- exact TAdd0R.symm
-- -- `(N,≤)` is a partially ordered type
-- def instPosetNLeq : Poset := {
-- base := N,
-- R := NLeq,
-- toPartialOrder := TPartialOrderNLeq
-- }[no output]Example 10
Status: OK
-- -- `z` is the least element
-- theorem TNLeqzL : ∀ {n : N}, z ≤ n := by
-- intro n
-- apply Exists.intro n
-- exact rfl
-- -- No `s n` is below `z`
-- theorem TNLeqzR : ∀ {n : N}, ¬ (s n ≤ z) := by
-- intro n h1
-- apply Exists.elim h1
-- intro a h2
-- cases h2
-- -- If `n ≤ m` then `s n ≤ s m`
-- theorem TNLeqSuccT : ∀ {n m : N}, (n ≤ m) → (s n ≤ s m) := by
-- intro n m h1
-- apply Exists.elim h1
-- intro a h2
-- apply Exists.intro a
-- rw [h2.symm]
-- exact rfl
-- -- If `n ≰ m` then `s n ≰ s m`
-- theorem TNLeqSuccF : ∀ {n m : N}, (¬ (n ≤ m)) → (¬ (s n ≤ s m)) := by
-- intro n m h1 h2
-- apply Exists.elim h2
-- intro a h3
-- injection h3 with h3
-- have h4 : n ≤ m := by
-- apply Exists.intro a
-- exact h3
-- exact h1 h4
-- -- `≤` is decidable
-- def instDecidableNLeq : ∀ {n m : N}, Decidable (n ≤ m) := by
-- intro n m
-- match n, m with
-- | z, _ => exact isTrue TNLeqzL
-- | s n', z => exact isFalse TNLeqzR
-- | s n', s m' =>
-- match @instDecidableNLeq n' m' with
-- | isTrue h => exact isTrue (TNLeqSuccT h)
-- | isFalse h => exact isFalse (TNLeqSuccF h)
-- -- `min n m` is a lower bound of `n`
-- theorem TMinNLeqL : ∀ {n m : N}, (mini n m) ≤ n := by
-- intro n m
-- cases n
-- -- z
-- rw [TMinzL]
-- exact TNLeqzL
-- -- s n
-- rename_i n
-- cases m
-- -- z
-- rw [TMinzR]
-- exact TNLeqzL
-- -- s m
-- rename_i m
-- rw [mini]
-- apply TNLeqSuccT
-- exact TMinNLeqL
-- -- `min n m` is a lower bound of `m`
-- theorem TMinNLeqR : ∀ {n m : N}, (mini n m) ≤ m := by
-- intro n m
-- rw [TMinComm]
-- exact TMinNLeqL
-- -- `min n m` is the infimum for `n` and `m`
-- theorem TInfNLeq : ∀ {n m : N}, Infimum NLeq (fun (x : N) => (x = n) ∨ (x = m)) (mini n m) := by
-- intro n m
-- apply Infimum.mk
-- -- LowerBound
-- intro a h
-- cases h
-- -- a = n
-- rename_i h
-- rw [h]
-- exact TMinNLeqL
-- -- a = m
-- rename_i h
-- rw [h]
-- exact TMinNLeqR
-- --
-- intro p h
-- apply h
-- exact TMinOut
-- -- `max n m` is an upper bound of `n`
-- theorem TMaxNLeqL : ∀ {n m : N}, n ≤ (maxi n m) := by
-- intro n m
-- cases n
-- -- z
-- rw [TMaxzL]
-- exact TNLeqzL
-- -- s n
-- rename_i n
-- cases m
-- -- z
-- rw [TMaxzR]
-- exact (TPreorderNLeq.refl (s n))
-- -- s m
-- rename_i m
-- rw [maxi]
-- apply TNLeqSuccT
-- exact TMaxNLeqL
-- -- `max n m` is an upper bound of `m`
-- theorem TMaxNLeqR : ∀ {n m : N}, m ≤ (maxi n m) := by
-- intro n m
-- rw [TMaxComm]
-- exact TMaxNLeqL
-- -- `max n m` is the supremum of `n` and `m`
-- theorem TSupNLeq : ∀ {n m : N}, Supremum NLeq (fun (x : N) => (x = n) ∨ (x = m)) (maxi n m) := by
-- intro n m
-- apply Supremum.mk
-- -- LowerBound
-- intro a h
-- cases h
-- -- a = n
-- rename_i h
-- rw [h]
-- exact TMaxNLeqL
-- -- a = m
-- rename_i h
-- rw [h]
-- exact TMaxNLeqR
-- --
-- intro p h
-- apply h
-- exact TMaxOut
-- -- `(N,≤)` is a lattice
-- def instLatticeNLeq : Lattice := {
-- toPoset := instPosetNLeq,
-- meet := mini,
-- infimum := TInfNLeq,
-- join := maxi,
-- supremum := TSupNLeq
-- }[no output]Example 11
Status: OK
-- -- `min n (max m p) = max (min n m) (min n p)`
-- theorem TDistNLeq : ∀ {n m p : N}, mini n (maxi m p) = maxi (mini n m) (mini n p) := by
-- intro n m p
-- apply TPartialOrderNLeq.antisymm
-- -- mini n (maxi p q) ≤ maxi (mini n p) (mini n q)
-- apply TSupNLeq.UB
-- match (@TMaxOut m p) with
-- | Or.inl h1 => exact Or.inl (congrArg (fun x => mini n x) h1)
-- | Or.inr h1 => exact Or.inr (congrArg (fun x => mini n x) h1)
-- -- maxi (mini n p) (mini n q) ≤ mini n (maxi p q)
-- apply TInfNLeq.GLB
-- intro x h1
-- cases h1
-- --
-- rename_i h1
-- rw [h1]
-- apply TSupNLeq.LUB
-- intro y h2
-- cases h2
-- --
-- rename_i h2
-- rw [h2]
-- exact TMinNLeqL
-- --
-- rename_i h2
-- rw [h2]
-- exact TMinNLeqL
-- --
-- rename_i h1
-- rw [h1]
-- apply TSupNLeq.LUB
-- intro y h2
-- cases h2
-- --
-- rename_i h2
-- rw [h2]
-- have h2 : mini n m ≤ m := TMinNLeqR
-- have h3 : m ≤ maxi m p := TMaxNLeqL
-- exact TPreorderNLeq.trans h2 h3
-- --
-- rename_i h2
-- rw [h2]
-- have h2 : mini n p ≤ p := TMinNLeqR
-- have h3 : p ≤ maxi m p := TMaxNLeqR
-- exact TPreorderNLeq.trans h2 h3
-- -- `(N,≤)` is a distributive lattice
-- def instDistLatticeAlgNLeq : DistLatticeAlg := {
-- toLatticeAlg := @LatticetoLatticeAlg instLatticeNLeq,
-- dist := TDistNLeq
-- }[no output]Example 12
Status: OK
-- end NLeq
-- -----------
namespace NDiv
-- The `∣` (divisor) relation for `N`
def NDiv : N → N → Prop := by
intro n m
exact ∃ (k : N), n * k = m
-- Notation for divisor (`\mid`)
notation : 65 lhs:65 " ∣ " rhs:66 => NDiv lhs rhs[no output]Example 13
Status: OK
-- -- `∣` is a preorder
-- theorem TPreorderNDiv : Preorder NDiv := by
-- apply Preorder.mk
-- -- refl
-- intro n
-- apply Exists.intro one
-- exact TMult1R
-- -- trans
-- intro n m p h1 h2
-- apply Exists.elim h1
-- intro a h3
-- apply Exists.elim h2
-- intro b h4
-- apply Exists.intro (a * b)
-- rw [TMultAss.symm, h3, h4]
-- -- `|` is a partial order
-- theorem TPartialOrderNDiv : PartialOrder NDiv := by
-- apply PartialOrder.mk
-- -- toPreorder
-- exact TPreorderNDiv
-- -- antisymm
-- intro n m h1 h2
-- apply Exists.elim h1
-- intro a h3
-- apply Exists.elim h2
-- intro b h4
-- rw [h3.symm, TMultAss] at h4
-- cases (TMultFix h4)
-- -- Left
-- rename_i h5
-- rw [h5, TMult0L, h5.symm] at h3
-- exact h3
-- -- Right
-- rename_i h5
-- have h6 : a = one := (TMultOne.mp h5).left
-- rw [h6, TMult1R] at h3
-- exact h3
-- -- `(N, ∣)` is a partially ordered type
-- def instPosetNDiv : Poset := {
-- base := N,
-- R := NDiv,
-- toPartialOrder := TPartialOrderNDiv
-- }[no output]Example 14
Status: OK
-- -- `one` is the `least` element for `∣`
-- theorem TNDivOne : Least NDiv one := by
-- intro n
-- apply Exists.intro n
-- exact rfl
-- -- `z` is the `greatest` element for `∣`
-- theorem TNDivZ : Greatest NDiv z := by
-- intro n
-- apply Exists.intro z
-- exact TMult0R
-- -- `(N, ∣)` is a bounded partially ordered type
-- def instBoundedPosetNDiv : BoundedPoset := {
-- base := N,
-- R := NDiv,
-- toPartialOrder := TPartialOrderNDiv,
-- l := one,
-- least := TNDivOne,
-- g := z,
-- greatest := TNDivZ
-- }
-- `z` does not divide any successor
theorem TNDivzL : ∀ {n : N}, ¬ (z ∣ s n) := by
intro n h1
apply Exists.elim h1
intro a h2
rw [TMult0L] at h2
cases h2
end NDiv[no output]Example 15
Status: OK
-- namespace PropLeq
-- -- The `→` relation for `Prop`
-- def PropLeq : Prop → Prop → Prop := by
-- intro P Q
-- exact P → Q
-- -- `→` is a preorder
-- theorem TPreorderPropLeq : Preorder PropLeq := by
-- apply Preorder.mk
-- -- refl
-- intro P h
-- exact h
-- -- trans
-- intro P Q R h1 h2 h3
-- exact h2 (h1 h3)
-- -- `→` is a partial order
-- theorem TPartialOrderPropLeq : PartialOrder PropLeq := by
-- apply PartialOrder.mk
-- -- toPreorder
-- exact TPreorderPropLeq
-- -- antisymm
-- intro P Q h1 h2
-- apply propext
-- exact Iff.intro h1 h2
-- -- `(Prop, →)` is a partially ordered type
-- def instPosetPropLeq : Poset := {
-- base := Prop,
-- R := PropLeq,
-- toPartialOrder := TPartialOrderPropLeq
-- }[no output]Example 16
Status: OK
-- -- `False` is the `least` element for `→`
-- theorem TPropLeqFalse : Least PropLeq False := by
-- intro P h
-- exact False.elim h
-- -- `True` is the `greatest` element for `→`
-- theorem TPropLeqTrue : Greatest PropLeq True := by
-- intro P _
-- exact trivial
-- -- `(Prop, →)` is a bounded partially ordered type
-- def instBoundedPropLeq : BoundedPoset := {
-- base := Prop,
-- R := PropLeq,
-- toPartialOrder := TPartialOrderPropLeq,
-- l := False,
-- least := TPropLeqFalse,
-- g := True,
-- greatest := TPropLeqTrue
-- }[no output]Example 17
Status: OK
-- -- `(Prop, ∧, ∨)` is a lattice (as an algebra)
-- def instLatticeAlgProp : LatticeAlg := {
-- base := Prop,
-- meet := And,
-- join := Or,
-- meetcomm := by
-- intro P Q
-- apply propext
-- apply Iff.intro
-- -- P ∧ Q → Q ∧ P
-- intro ⟨hP, hQ⟩
-- exact ⟨hQ, hP⟩
-- -- Q ∧ P → P ∧ Q
-- intro ⟨hQ, hP⟩
-- exact ⟨hP, hQ⟩
-- joincomm := by
-- intro P Q
-- apply propext
-- apply Iff.intro
-- -- P ∨ Q → Q ∨ P
-- intro h
-- match h with
-- | Or.inl h => exact Or.inr h
-- | Or.inr h => exact Or.inl h
-- -- Q ∨ P → P ∨ Q
-- intro h
-- match h with
-- | Or.inl h => exact Or.inr h
-- | Or.inr h => exact Or.inl h
-- meetass := by
-- intro P Q R
-- apply propext
-- apply Iff.intro
-- -- (P ∧ Q) ∧ R → P ∧ Q ∧ R
-- intro ⟨⟨hP, hQ⟩, hR⟩
-- exact ⟨hP, ⟨hQ, hR⟩⟩
-- -- P ∧ Q ∧ R → (P ∧ Q) ∧ R
-- intro ⟨hP, ⟨hQ, hR⟩⟩
-- exact ⟨⟨hP, hQ⟩, hR⟩
-- joinass := by
-- intro P Q R
-- apply propext
-- apply Iff.intro
-- -- (P ∨ Q) ∨ R → P ∨ Q ∨ R
-- intro h
-- match h with
-- | Or.inl h => match h with
-- | Or.inl h => exact Or.inl h
-- | Or.inr h => exact Or.inr (Or.inl h)
-- | Or.inr h => exact Or.inr (Or.inr h)
-- -- P ∨ Q ∨ R → (P ∨ Q) ∨ R
-- intro h
-- match h with
-- | Or.inl h => exact Or.inl (Or.inl h)
-- | Or.inr h => match h with
-- | Or.inl h => exact Or.inl (Or.inr h)
-- | Or.inr h => exact Or.inr h
-- abslaw1 := by
-- intro P Q
-- apply propext
-- apply Iff.intro
-- -- P ∨ P ∧ Q → P
-- intro h
-- match h with
-- | Or.inl h => exact h
-- | Or.inr h => exact h.left
-- -- P → P ∨ P ∧ Q
-- intro h
-- exact Or.inl h
-- abslaw2 := by
-- intro P Q
-- apply propext
-- apply Iff.intro
-- -- P ∧ (P ∨ Q) → P
-- intro ⟨hP, _⟩
-- exact hP
-- -- P → P ∧ (P ∨ Q)
-- intro h
-- exact And.intro h (Or.inl h)
-- }[no output]Example 18
Status: OK
-- -- `(Prop, →)` is a complete lattice
-- def instCompleteLatticeProp : CompleteLattice := {
-- base := Prop,
-- R := PropLeq,
-- toPartialOrder := TPartialOrderPropLeq,
-- meet := (fun ℙ => ∀ (Q : Prop), ℙ Q → Q),
-- infimum := by
-- intro ℙ
-- apply Infimum.mk
-- -- Lower Bound
-- intro R hR hF
-- exact (hF R) hR
-- -- Least Lower Bound
-- intro R hLBR hR Q hQ
-- apply hLBR
-- exact hQ
-- exact hR
-- join := (fun ℙ => ∃ (Q : Prop), ℙ Q ∧ Q),
-- supremum := by
-- intro ℙ
-- apply Supremum.mk
-- -- Upper Bound
-- intro R hPR hR
-- apply Exists.intro R
-- exact ⟨hPR, hR⟩
-- -- Greatest Upper Bound
-- intro R hUBR hEQ
-- apply Exists.elim hEQ
-- intro Q ⟨hPQ, hQ⟩
-- apply hUBR Q
-- exact hPQ
-- exact hQ
-- }[no output]Example 19
Status: OK
-- end PropLeq
namespace PredLeq
-- The `→` relation for predicates on `A`
def PredLeq {A : Type} : (A → Prop) → (A → Prop) → Prop := by
intro P Q
exact ∀ {a : A}, P a → Q a
-- Notation for `→` (`\subseteq`)
notation : 65 lhs:65 " ⊆ " rhs:66 => PredLeq lhs rhs[no output]Example 20
Status: OK
-- -- `⊆` is a preorder
-- theorem TPreorderPredLeq {A : Type} : Preorder (@PredLeq A) := by
-- apply Preorder.mk
-- -- refl
-- intro P a h
-- exact h
-- -- trans
-- intro P Q R h1 h2
-- intro a h3
-- exact h2 (h1 h3)
-- -- `⊆` is a partial order
-- theorem TPartialOrderPredLeq {A : Type} : PartialOrder (@PredLeq A) := by
-- apply PartialOrder.mk
-- -- toPreorder
-- exact TPreorderPredLeq
-- -- antisymm
-- intro P Q h1 h2
-- funext a
-- apply propext
-- exact Iff.intro h1 h2
-- -- `(A → Prop, →)` is a partially ordered type
-- def instPosetPredLeq {A : Type} : Poset := {
-- base := A → Prop,
-- R := PredLeq,
-- toPartialOrder := TPartialOrderPredLeq
-- }[no output]Example 21
Status: OK
-- -- `PFalse` is the `least` element for `⊆`
-- theorem TPredLeqPFalse {A : Type} : Least (@PredLeq A) PFalse := by
-- intro P a h
-- exact False.elim h
-- -- `PTrue` is the `greatest` element for `⊆`
-- theorem TPredLeqPTrue {A : Type} : Greatest (@PredLeq A) PTrue := by
-- intro P a _
-- exact trivial
-- -- `(A → Prop, →)` is a bounded partially ordered type
-- def instBoundedPosetPredLeq {A : Type} : BoundedPoset := {
-- base := A → Prop,
-- R := PredLeq,
-- toPartialOrder := TPartialOrderPredLeq,
-- l := PFalse,
-- least := TPredLeqPFalse,
-- g := PTrue,
-- greatest := TPredLeqPTrue
-- }[no output]Example 22
Status: OK
-- -- `(A → Prop, ∧, ∨)` is a lattice (as an algebra)
-- def instLatticeAlgPredLeq {A : Type} : LatticeAlg := {
-- base := A → Prop,
-- meet := by
-- intro P Q a
-- exact P a ∧ Q a,
-- join := by
-- intro P Q a
-- exact P a ∨ Q a,
-- meetcomm := by
-- intro P Q
-- funext a
-- apply propext
-- apply Iff.intro
-- -- P ∧ Q → Q ∧ P
-- intro ⟨h1, h2⟩
-- exact ⟨h2, h1⟩
-- -- Q ∧ P → P ∧ Q
-- intro ⟨h1, h2⟩
-- exact ⟨h2, h1⟩,
-- joincomm := by
-- intro P Q
-- funext a
-- apply propext
-- apply Iff.intro
-- -- P ∨ Q → Q ∨ P
-- intro h1
-- cases h1 with
-- | inl h2 => exact Or.inr h2
-- | inr h2 => exact Or.inl h2
-- -- Q ∨ P → P ∨ Q
-- intro h1
-- cases h1 with
-- | inl h2 => exact Or.inr h2
-- | inr h2 => exact Or.inl h2,
-- meetass := by
-- intro P Q R
-- funext a
-- apply propext
-- apply Iff.intro
-- -- (P ∧ Q) ∧ R → P ∧ (Q ∧ R)
-- intro ⟨⟨h1, h2⟩, h3⟩
-- exact ⟨h1, ⟨h2, h3⟩⟩
-- -- P ∧ (Q ∧ R) → (P ∧ Q) ∧ R
-- intro ⟨h1, ⟨h2, h3⟩⟩
-- exact ⟨⟨h1, h2⟩, h3⟩,
-- joinass := by
-- intro P Q R
-- funext a
-- apply propext
-- apply Iff.intro
-- -- (P ∨ Q) ∨ R → P ∨ (Q ∨ R)
-- intro h1
-- cases h1 with
-- | inl h2 => cases h2 with
-- | inl h3 => exact Or.inl h3
-- | inr h3 => exact Or.inr (Or.inl h3)
-- | inr h2 => exact Or.inr (Or.inr h2)
-- -- P ∨ (Q ∨ R) → (P ∨ Q) ∨ R
-- intro h1
-- cases h1 with
-- | inl h2 => exact Or.inl (Or.inl h2)
-- | inr h2 => cases h2 with
-- | inl h3 => exact Or.inl (Or.inr h3)
-- | inr h3 => exact Or.inr h3
-- abslaw1 := by
-- intro P Q
-- funext a
-- apply propext
-- apply Iff.intro
-- -- P ∨ (P ∧ Q) → P
-- intro h1
-- cases h1 with
-- | inl h2 => exact h2
-- | inr h2 => exact h2.1
-- -- P → P ∨ (P ∧ Q)
-- intro h1
-- exact Or.inl h1
-- abslaw2 := by
-- intro P Q
-- funext a
-- apply propext
-- apply Iff.intro
-- -- P ∧ (P ∨ Q) → P
-- intro ⟨h1, _⟩
-- exact h1
-- -- P → P ∧ (P ∨ Q)
-- intro h1
-- exact ⟨h1, Or.inl h1⟩
-- }[no output]Example 23
Status: OK
-- -- `(A → Prop, →)` is a complete lattice
-- def instCompleteLatticePredLeq {A : Type} : CompleteLattice := {
-- base := A → Prop,
-- R := PredLeq,
-- toPartialOrder := TPartialOrderPredLeq,
-- meet := (fun ℙ => (fun a => ∀ (P: A → Prop), ℙ P → P a)),
-- infimum := by
-- intro ℙ
-- apply Infimum.mk
-- -- Lower Bound
-- intro P hP a h
-- exact (h P) hP
-- -- Least Lower Bound
-- intro P hLBP a hPa Q hQ
-- apply hLBP
-- exact hQ
-- exact hPa
-- join := (fun ℙ => (fun a => ∃ (P: A → Prop), ℙ P ∧ P a)),
-- supremum := by
-- intro ℙ
-- apply Supremum.mk
-- -- Upper Bound
-- intro P hP a h
-- apply Exists.intro P
-- exact ⟨hP, h⟩
-- -- Greatest Upper Bound
-- intro P hLBP a hPa
-- apply Exists.elim hPa
-- intro Q ⟨hQ, hPQ⟩
-- apply hLBP Q
-- exact hQ
-- exact hPQ
-- }
end PredLeq[no output]Example 24
Status: OK
namespace RelLeq
-- The `→` relation for relations on `A`
def RelLeq {A : Type} : (A → A → Prop) → (A → A → Prop) → Prop := by
intro R S
exact ∀ {a b : A}, R a b → S a b
-- Notation for `→` (`\subseteq`)
notation : 65 lhs:65 " ⊆ " rhs:66 => RelLeq lhs rhs[no output]Example 25
Status: OK
-- -- `⊆` is a preorder
-- theorem TPreorderRelLeq {A : Type} : Preorder (@RelLeq A) := by
-- apply Preorder.mk
-- -- refl
-- intro R a b h
-- exact h
-- -- trans
-- intro R S T h1 h2
-- intro a b h3
-- exact h2 (h1 h3)
-- -- `⊆` is a partial order
-- theorem TPartialOrderRelLeq {A : Type} : PartialOrder (@RelLeq A) := by
-- apply PartialOrder.mk
-- -- toPreorder
-- exact TPreorderRelLeq
-- -- antisymm
-- intro R S h1 h2
-- funext a b
-- apply propext
-- exact Iff.intro h1 h2
-- -- `(A → A → Prop, →)` is a partially ordered type
-- def instPosetRelLeq {A : Type} : Poset := {
-- base := A → A → Prop,
-- R := RelLeq,
-- toPartialOrder := TPartialOrderRelLeq
-- }[no output]Example 26
Status: OK
-- -- `empty` is the `least` element for `⊆`
-- theorem TRelLeqEmpty {A : Type} : Least (@RelLeq A) empty := by
-- intro R a b h
-- apply False.elim h
-- -- `total` is the `greatest` element for `⊆`
-- theorem TRelLeqPTrue {A : Type} : Greatest (@RelLeq A) total := by
-- intro R a b _
-- exact trivial
-- -- `(A → A → Prop, →)` is a bounded partially ordered type
-- def instBoundedPosetRelLeq {A : Type} : BoundedPoset := {
-- base := A → A → Prop,
-- R := RelLeq,
-- toPartialOrder := TPartialOrderRelLeq,
-- l := empty,
-- least := TRelLeqEmpty,
-- g := total,
-- greatest := TRelLeqPTrue
-- }[no output]Example 27
Status: OK
-- -- `(A → A → Prop, ∧, ∨)` is a lattice (as an algebra)
-- def instLatticeAlgRelLeq {A : Type} : LatticeAlg := {
-- base := A → A → Prop,
-- meet := by
-- intro R S a b
-- exact R a b ∧ S a b,
-- join := by
-- intro R S a b
-- exact R a b ∨ S a b,
-- meetcomm := by
-- intro R S
-- funext a b
-- apply propext
-- apply Iff.intro
-- -- R ∧ S → S ∧ R
-- intro ⟨h1, h2⟩
-- exact ⟨h2, h1⟩
-- -- S ∧ R → R ∧ S
-- intro ⟨h1, h2⟩
-- exact ⟨h2, h1⟩,
-- joincomm := by
-- intro R S
-- funext a b
-- apply propext
-- apply Iff.intro
-- -- R ∨ S → S ∨ R
-- intro h1
-- cases h1 with
-- | inl h2 => exact Or.inr h2
-- | inr h2 => exact Or.inl h2
-- -- S ∨ R → R ∨ S
-- intro h1
-- cases h1 with
-- | inl h2 => exact Or.inr h2
-- | inr h2 => exact Or.inl h2,
-- meetass := by
-- intro R S T
-- funext a b
-- apply propext
-- apply Iff.intro
-- -- (R ∧ S) ∧ T → R ∧ (S ∧ T)
-- intro ⟨⟨h1, h2⟩, h3⟩
-- exact ⟨h1, ⟨h2, h3⟩⟩
-- -- R ∧ (S ∧ T) → (R ∧ S) ∧ T
-- intro ⟨h1, ⟨h2, h3⟩⟩
-- exact ⟨⟨h1, h2⟩, h3⟩,
-- joinass := by
-- intro R S T
-- funext a b
-- apply propext
-- apply Iff.intro
-- -- (R ∨ S) ∨ T → R ∨ (S ∨ T)
-- intro h1
-- cases h1 with
-- | inl h2 => cases h2 with
-- | inl h3 => exact Or.inl h3
-- | inr h3 => exact Or.inr (Or.inl h3)
-- | inr h2 => exact Or.inr (Or.inr h2)
-- -- R ∨ (S ∨ T) → (R ∨ S) ∨ T
-- intro h1
-- cases h1 with
-- | inl h2 => exact Or.inl (Or.inl h2)
-- | inr h2 => cases h2 with
-- | inl h3 => exact Or.inl (Or.inr h3)
-- | inr h3 => exact Or.inr h3
-- abslaw1 := by
-- intro R S
-- funext a b
-- apply propext
-- apply Iff.intro
-- -- R ∨ (R ∧ S) → R
-- intro h1
-- cases h1 with
-- | inl h2 => exact h2
-- | inr h2 => exact h2.1
-- -- R → R ∨ (R ∧ S)
-- intro h1
-- exact Or.inl h1
-- abslaw2 := by
-- intro R S
-- funext a b
-- apply propext
-- apply Iff.intro
-- -- R ∧ (R ∨ S) → R
-- intro ⟨h1, _⟩
-- exact h1
-- -- R → R ∧ (R ∨ S)
-- intro h1
-- exact ⟨h1, Or.inl h1⟩
-- }[no output]Example 28
Status: OK
-- -- `(A → A → Prop, →)` is a complete lattice
-- def instCompleteLatticeRelLeq {A : Type} : CompleteLattice := {
-- base := A → A → Prop,
-- R := RelLeq,
-- toPartialOrder := TPartialOrderRelLeq,
-- meet := (fun ℝ => (fun a b => ∀ (R : A → A → Prop), ℝ R → R a b)),
-- infimum := by
-- intro ℙ
-- apply Infimum.mk
-- -- Lower Bound
-- intro R hR a b h
-- exact (h R) hR
-- -- Least Lower Bound
-- intro R hLB a b hRab Q hQ
-- apply hLB
-- exact hQ
-- exact hRab
-- join := (fun ℝ => (fun a b => ∃ (R : A → A → Prop), ℝ R ∧ R a b)),
-- supremum := by
-- intro ℙ
-- apply Supremum.mk
-- -- Upper Bound
-- intro R hR a b h
-- apply Exists.intro R
-- exact ⟨hR, h⟩
-- -- Greatest Upper Bound
-- intro R hLB a b hPab
-- apply Exists.elim hPab
-- intro Q ⟨hQ, hPQ⟩
-- apply hLB Q
-- exact hQ
-- exact hPQ
-- }
end RelLeq[no output]Chapter 12: Empty Unit
Example 1
Status: OK
import a05Functions
open Inj
open Surj
namespace Empty
-- ## Empty type
-- The empty type is a type that has no values
-- It is denoted by `Empty` in Lean
#check Empty
#print EmptyEmpty : Type
inductive Empty : Type
number of parameters: 0
constructors:Example 2
Status: OK
-- This means that if we have a value of type `Empty`,
-- we can use it to construct a value of any other type
def emptyToAny {A : Type} : Empty → A := by
intro x
exact Empty.elim x
-- The interesting thing about the `emptytoAny` function
-- is that it is unique up to definitional equality
theorem emptyToAnyUnique {A : Type} {f g : Empty → A} : f = g := by
funext x
exact Empty.elim x
-- This implies that the `emptyToAny` function with codomain `Empty`, is
-- in particular, the identity function on `Empty`
theorem emptyToAnyId : @emptyToAny Empty = id := by
funext x
exact Empty.elim x
-- All the elements of `Empty` are equal
theorem emptyUnique : ∀ (x y : Empty), x = y := by
intro x _
exact Empty.elim x
-- The `emptyToAny` function is injective
theorem emptyToAnyInj {A : Type} : injective (@emptyToAny A) := by
intro x _ _
exact Empty.elim x
-- Under `Classical.choice`, if the `emptyToAny` function is surjective,
-- the codomain cannot be `nonempty`
theorem emptyToAnySurj {A : Type} : surjective (@emptyToAny A) ↔ ¬ (Nonempty A) := by
apply Iff.intro
-- surjective emptyToAny → ¬ Nonempty A
intro h1 h2
have a : A := Classical.choice h2
have h3 : ∃ (x : Empty), emptyToAny x = a := by
exact h1
apply Exists.elim h3
intro z _
exact Empty.elim z
-- ¬ Nonempty A → surjective emptyToAny
intro h1 a
have h2 : Nonempty A := Nonempty.intro a
apply False.elim (h1 h2)
end Empty
namespace Unit
-- ## Unit type
-- The unit type is a type that has exactly one value
-- It is denoted by `Unit` in Lean
#check Unit
#print UnitUnit : Type
@[reducible] def Unit : Type :=
PUnitExample 3
Status: OK
-- The unit type has one value, denoted by `()`
#check ()
-- There is always a function from any type to the unit type
def anyToUnit {A : Type} : A → Unit := by
intro _
exact ()
-- The `anyToUnit` function is unique up to definitional equality
theorem anyToUnitUnique {A : Type} {f g : A → Unit} : f = g := by
funext x
exact rfl
-- This implies that the `anyToUnit` function with codomain `Unit`, is
-- in particular, the identity function on `Unit`
theorem anyToUnitId : @anyToUnit Unit = id := by
funext x
exact rfl
-- All the elements of `Unit` are equal
theorem unitUnique : ∀ (x y : Unit), x = y := by
intro x _
exact rfl
-- The `anyToUnit` function is injective if,
-- and only if, the domain has only one element
theorem anyToUnitInj {A : Type} : injective (@anyToUnit A) ↔ (∀ (a1 a2 : A), a1 = a2) := by
apply Iff.intro
-- injective anyToUnit → ∀ (a1 a2 : A), a1 = a2
intro h1 a1 a2
have h2 : anyToUnit a1 = anyToUnit a2 := by
exact rfl
exact h1 h2
-- ∀ (a1 a2 : A), a1 = a2 → injective anyToUnit
intro h1 x y _
exact h1 x y
-- Under `Classical.choice`, the `anyToUnit` function is
-- surjective if and only if the domain is `Nonempty`
theorem anyToUnitSurj {A : Type} : surjective (@anyToUnit A) ↔ Nonempty A := by
apply Iff.intro
-- surjective anyToUnit → Nonempty A
intro h1
have h2 : ∃ (a : A), anyToUnit a = () := by
exact h1
apply Exists.elim h2
intro a _
exact Nonempty.intro a
-- Nonempty A → surjective anyToUnit
intro h1
intro a
apply Exists.intro (Classical.choice h1)
exact rfl
end Unit[no new output]Chapter 13: Product Sum
Upstream note: this chapter does not compile cleanly in the current IntroToLean4 repo state, so the examples below are shown as source only to avoid flooding the document with misleading execution errors.
Example 1
Status: source only
import a05Functions
import a10Equivalence
import a13EmptyUnit
import Paperproof
open Inj
open Surj
open Bij
open Empty
open Unit[execution skipped because this upstream chapter is currently broken]Example 2
Status: source only
namespace Product
-- ## Product type
-- The product type is a type that has two values
-- It is denoted by `A × B` in Lean `times`
#check Prod
#print Prod[execution skipped because this upstream chapter is currently broken]Example 3
Status: source only
variable (A B : Type)
#check A × B[execution skipped because this upstream chapter is currently broken]Example 4
Status: source only
-- To produce a value of type `A × B`, we need to provide
-- a value of type `A` and a value of type `B`
def toPair {A B : Type} : A → B → A × B := by
intro a b
exact ⟨a, b⟩
-- We can also use the `Prod.mk` constructor to produce a value of type `A × B`
def toPair' {A B : Type} : A → B → A × B := by
intro a b
exact Prod.mk a b
-- The `Prod` type has two projections, `fst` and `snd`,
-- that allow us to extract the first and second values, respectively
def π1 {A B : Type} : (A × B) → A := by
intro p
exact p.fst
def π2 {A B : Type} : (A × B) → B := by
intro p
exact p.snd
-- Two values of type `A × B` are equal if and only if
-- their first and second components are equal
-- For this we can use the `Prod.ext` function
theorem prodEq {A B : Type} (p1 p2 : A × B) : (p1 = p2) ↔ (π1 p1 = π1 p2) ∧ (π2 p1 = π2 p2) := by
apply Iff.intro
-- p1 = p2 → π1 p1 = π1 p2 ∧ π2 p1 = π2 p2
intro h
apply And.intro
exact congrArg π1 h
exact congrArg π2 h
-- π1 p1 = π1 p2 ∧ π2 p1 = π2 p2 → p1 = p2
intro ⟨h1, h2⟩
apply Prod.ext
exact h1
exact h2
-- The universal property of the product type is that
-- if we have a function `f : C → A` and a function `g : C → B`,
-- we can construct a function `h : C → A × B` such that
-- `π1 ∘ h = f` and `π2 ∘ h = g`
def toProd {A B C : Type} (f : C → A) (g : C → B) : (C → A × B) := by
intro c
exact Prod.mk (f c) (g c)
-- The `toProd` function satisfies that the corresponding
-- composition with the projections `π1` and `π2`
-- give us back the original functions `f` and `g`
theorem toProdp1 {A B C : Type} (f : C → A) (g : C → B) : π1 ∘ (toProd f g) = f := by
funext c
exact rfl
theorem toProdp2 {A B C : Type} (f : C → A) (g : C → B) : π2 ∘ (toProd f g) = g := by
funext c
exact rfl
-- The universal property also states that if we have
-- a function `h : C → A × B`, satisfying `π1 ∘ h = f`
-- and `π2 ∘ h = g`, then `h` must be equal to `toProd f g`
theorem toProdUnique {A B C : Type} {f : C → A} {g : C → B} {h : C → A × B} : (π1 ∘ h = f) → (π2 ∘ h = g) → (h = toProd f g) := by
intro h1 h2
funext c
apply Prod.ext
exact congrFun h1 c
exact congrFun h2 c
-- ## Product type of a family of types
-- For a type of indices `I`, the product type of
-- a family of types `𝔸 : I → Type` is a type
-- that has a value for each type in the family
-- It is denoted by `∀ (i : I), 𝔸 i` in Lean
variable (I : Type)
variable (𝔸 : I → Type)
#check ∀ (i : I), 𝔸 i[execution skipped because this upstream chapter is currently broken]Example 5
Status: source only
-- To produce a value of type `∀ (i : I), 𝔸 i`, we need to
-- provide a value of type `𝔸 i` for every `i : I`
def toPairg {I : Type} {𝔸 : I → Type} : ((i : I) → 𝔸 i) → ∀ (i : I), 𝔸 i := by
intro 𝕗 i
exact 𝕗 i
-- The `∀ (i : I), 𝔸 i` type has a projection
-- that allows us to extract the value for a given `i : I`
def π {I : Type} {𝔸 : I → Type} (i : I) : (∀ (i : I), 𝔸 i) → 𝔸 i := by
intro 𝕒
exact 𝕒 i
-- Two values of type `∀ (i : I), 𝔸 i` are equal if and only if
-- their `i`-th components are equal for every `i : I`
theorem prodEqg {I : Type} {𝔸 : I → Type} (𝕒1 𝕒2 : ∀ (i : I), 𝔸 i) : (𝕒1 = 𝕒2) ↔ ∀ (i : I), π i 𝕒1 = π i 𝕒2 := by
apply Iff.intro
-- 𝕒1 = 𝕒2 → ∀ (i : I), π i 𝕒1 = π i 𝕒2
intro h i
exact congrArg (π i) h
-- (∀ (i : I), π i 𝕒1 = π i 𝕒2) → 𝕒1 = 𝕒2
intro h
funext i
exact h i
-- The universal property of the product type is that
-- if we have a function `𝕗 i : C → 𝔸 i` for every `i : I`
-- we can construct a function `h : C → ∀ (i : I), 𝔸 i` such that
-- `(π i) ∘ h = 𝕗 i` for every `i : I`
def toProdg {I C : Type} {𝔸 : I → Type} (𝕗 : (i : I) → C → 𝔸 i) : C → (∀ (i : I), 𝔸 i) := by
intro c i
exact (𝕗 i) c
-- The `toProdg` function satisfies that the corresponding
-- composition with the projections `π i`
-- give us back the original functions `𝕗 i`
theorem toProdpg {I C : Type} {𝔸 : I → Type} (𝕗 : (i : I) → C → 𝔸 i) (i : I) : (π i) ∘ (toProdg 𝕗) = 𝕗 i := by
funext c
exact rfl
-- The universal property also states that if if we have
-- a function `h : C → ∀ (i : I), 𝔸 i`, satisfying `(π i) ∘ h = (𝕗 i)`
-- for every `i : I` then `h` must be equal to `toProdg f`
theorem toProdgUnique {I C : Type} {𝔸 : I → Type} {𝕗 : (i : I) → C → 𝔸 i} {h : C → ∀ (i : I), 𝔸 i} : (∀ (i : I), (π i) ∘ h = (𝕗 i)) → (h = toProdg 𝕗) := by
intro hp
funext c
funext i
exact congrFun (hp i) c
-- ## Exercises
-- The product is commutative
theorem prodComm {A B : Type} : (A × B) ≅ (B × A) := by
let f : (A × B) → (B × A) := toProd π2 π1
let g : (B × A) → (A × B) := toProd π2 π1
let h : isomorphism f := by
apply Exists.intro g
apply And.intro
-- g ∘ f = id
funext e
exact Prod.ext rfl rfl
-- f ∘ g = id
funext e
exact Prod.ext rfl rfl
apply Nonempty.intro
exact Subtype.mk f h
-- The product is associative
theorem prodAssoc {A B C : Type} : ((A × B) × C) ≅ (A × (B × C)) := by
let f : ((A × B) × C) → (A × (B × C)) := toProd (π1 ∘ π1) (toProd (π2 ∘ π1) π2)
let g : (A × (B × C)) → ((A × B) × C) := toProd (toProd π1 (π1 ∘ π2)) (π2 ∘ π2)
let h : isomorphism f := by
apply Exists.intro g
apply And.intro
-- g ∘ f = id
funext e
exact Prod.ext rfl rfl
-- f ∘ g = id
funext e
exact Prod.ext rfl rfl
apply Nonempty.intro
exact Subtype.mk f h
-- Empty is a left zero
theorem TEmptyProdL {A : Type} : (Empty × A) ≅ Empty := by
let f : (Empty × A) → Empty := π1
let g : Empty → (Empty × A) := toProd id emptyToAny
let h : isomorphism f := by
apply Exists.intro g
apply And.intro
-- g ∘ f = id
funext e
exact Empty.elim e.fst
-- f ∘ g = id
exact toProdp1 id emptyToAny
apply Nonempty.intro
exact Subtype.mk f h
-- Empty is a right zero
theorem TEmptyProdR {A : Type} : (A × Empty) ≅ Empty := by
let f : (A × Empty) → Empty := π2
let g : Empty → (A × Empty) := toProd emptyToAny id
let h : isomorphism f := by
apply Exists.intro g
apply And.intro
-- g ∘ f = id
funext e
exact Empty.elim e.snd
-- f ∘ g = id
exact toProdp2 emptyToAny id
apply Nonempty.intro
exact Subtype.mk f h
-- Unit is a right unit
theorem TUnitProdR {A : Type} : (A × Unit) ≅ A := by
let f : (A × Unit) → A := π1
let g : A → (A × Unit) := toProd id anyToUnit
let h : isomorphism f := by
apply Exists.intro g
apply And.intro
-- g ∘ f = id
funext e
exact Prod.ext rfl rfl
-- f ∘ g = id
exact toProdp1 id anyToUnit
apply Nonempty.intro
exact Subtype.mk f h
-- Unit is a left unit
theorem TUnitProdL {A : Type} : (Unit × A) ≅ A := by
let f : (Unit × A) → A := π2
let g : A → (Unit × A) := toProd anyToUnit id
let h : isomorphism f := by
apply Exists.intro g
apply And.intro
-- g ∘ f = id
funext e
exact Prod.ext rfl rfl
-- f ∘ g = id
exact toProdp2 anyToUnit id
apply Nonempty.intro
exact Subtype.mk f h
end Product[execution skipped because this upstream chapter is currently broken]Example 6
Status: source only
namespace Sum
open Product
-- ## Sum type
-- The sum type is a type that has two values
-- It is denoted by `A ⊕ B` in Lean `oplus`
#check Sum
#print Sum[execution skipped because this upstream chapter is currently broken]Example 7
Status: source only
variable (A B : Type)
#check A ⊕ B[execution skipped because this upstream chapter is currently broken]Example 8
Status: source only
-- The `Sum` type has two injections, `ι1` and `ι2`,
-- that allow us to provide an element of type `A ⊕ B`
-- (using `Sum.inl` and `Sum.inr`, respectively)
def ι1 {A B : Type} : A → A ⊕ B := by
intro a
exact Sum.inl a
def ι2 {A B : Type} : B → A ⊕ B := by
intro b
exact Sum.inr b
-- Two values of type `A ⊕ B` are equal if and only if
-- they are both injections on the same element
theorem sumEq {A B : Type} (p1 p2 : A ⊕ B) : (p1 = p2) ↔ (∃ (a : A), (((ι1 a) = p1) ∧ ((ι1 a) = p2))) ∨ (∃ (b : B), (((ι2 b) = p1) ∧ ((ι2 b) = p2))) := by
apply Iff.intro
-- p1 = p2 → (∃ a, ι1 a = p1 ∧ ι1 a = p2) ∨ ∃ b, ι2 b = p1 ∧ ι2 b = p2
intro h
cases p1 with
| inl a => cases p2 with
| inl b =>
injection h with h1
apply Or.inl
apply Exists.intro a
apply And.intro rfl
rw [h1]
exact rfl
| inr b =>
exact Sum.noConfusion h
| inr a => cases p2 with
| inl b =>
exact Sum.noConfusion h
| inr b =>
injection h with h1
apply Or.inr
apply Exists.intro a
apply And.intro rfl
rw [h1]
exact rfl
-- ((∃ a, ι1 a = p1 ∧ ι1 a = p2) ∨ ∃ b, ι2 b = p1 ∧ ι2 b = p2) → p1 = p2
intro h
cases h with
| inl h =>
apply Exists.elim h
intro a ⟨h1, h2⟩
exact h1.symm.trans h2
| inr h =>
apply Exists.elim h
intro b ⟨h1, h2⟩
exact h1.symm.trans h2
-- The universal property of the sum type is that
-- if we have a function `f : A → C` and a function `g : B → C`,
-- we can construct a function `h : A ⊕ B → C` such that
-- `h ∘ ι1 = f` and `h ∘ ι2 = g`
def fromSum {A B C : Type} (f : A → C) (g : B → C) : (A ⊕ B) → C := by
intro o
cases o with
| inl a => exact f a
| inr b => exact g b
-- The `fromSum` function satisfies that the corresponding
-- composition with the injections `ι1` and `ι2`
-- give us back the original functions `f` and `g`
theorem fromSumi1 {A B C : Type} (f : A → C) (g : B → C) : (fromSum f g) ∘ ι1 = f := by
funext a
exact rfl
theorem fromSumi2 {A B C : Type} (f : A → C) (g : B → C) : (fromSum f g) ∘ ι2 = g := by
funext b
exact rfl
-- The universal property also states that if we have
-- a function `h : A ⊕ B → C`, satisfying `h ∘ ι1 = f`
-- and `h ∘ ι2 = g`, then `h` must be equal to `fromSum f g`
theorem fromSumUnique {A B C : Type} {f : A → C} {g : B → C} {h : (A ⊕ B) → C} : (h ∘ ι1 = f) → (h ∘ ι2 = g) → (h = fromSum f g) := by
intro h1 h2
funext o
cases o with
| inl a => exact congrFun h1 a
| inr b => exact congrFun h2 b
-- ## Sum type of a family of types
-- The sum type of a family of types is a type
-- that has a value for some type in the family
-- It is denoted by `(Σ (i : I), 𝔸 i)` in Lean
variable (I : Type)
variable (𝔸 : I → Type)
#check Σ i, 𝔸 i
#check (Σ (i : I), 𝔸 i)[execution skipped because this upstream chapter is currently broken]Example 9
Status: source only
#check Sigma 𝔸
#print Sigma[execution skipped because this upstream chapter is currently broken]Example 10
Status: source only
-- The `(Σ (i : I), 𝔸 i)` type has an injection
-- that allows us to insert the value for a given `i : I`
def ι {I : Type} {𝔸 : I → Type} (i : I) : 𝔸 i → (Σ (i : I), 𝔸 i) := by
intro a
exact ⟨i, a⟩
-- Two values of type `(Σ (i : I), 𝔸 i)` are equal if and
-- only if they are both `ι i` of some `a : 𝔸 i`
-- For this we will use `Sigma.ext`
theorem sumEqg {I : Type} {𝔸 : I → Type} (𝕒1 𝕒2 : (Σ (i : I), 𝔸 i)) : (𝕒1 = 𝕒2) ↔ ∃ (i : I), ∃ (a : 𝔸 i), (𝕒1 = ι i a) ∧ (𝕒2 = ι i a) := by
apply Iff.intro
-- 𝕒1 = 𝕒2 → ∃ i a, 𝕒1 = ι i a ∧ 𝕒2 = ι i a
intro h
cases 𝕒1 with
| mk i a => cases 𝕒2 with
| mk j b =>
injection h with h1 h2
apply Exists.intro i
apply Exists.intro a
apply And.intro rfl
exact Sigma.ext h1.symm h2.symm
-- ∃ i a, 𝕒1 = ι i a ∧ 𝕒2 = ι i a → 𝕒1 = 𝕒2
intro ⟨i, ⟨a, ⟨h1, h2⟩⟩⟩
exact h1.trans h2.symm
-- The universal property of the sum type is that
-- if we have a function `𝕗 i : 𝔸 i → C` for every `i : I`
-- we can construct a function `h : (Σ (i : I), 𝔸 i) → C` such that
-- `h ∘ (ι i) = 𝕗 i` for every `i : I`
def fromSumg {I C : Type} {𝔸 : I → Type} (𝕗 : (i : I) → 𝔸 i → C) : (Σ (i : I), 𝔸 i) → C := by
intro ⟨i, a⟩
exact 𝕗 i a
-- The `fromSumg` function satisfies that the corresponding
-- composition with the injections `ι i`
-- give us back the original functions `𝕗 i`
theorem fromSumig {I C : Type} {𝔸 : I → Type} (𝕗 : (i : I) → 𝔸 i → C) (i : I) : (fromSumg 𝕗) ∘ (ι i) = 𝕗 i := by
funext c
exact rfl
-- The universal property also states that if we have
-- a function `h : (Σ (i : I), 𝔸 i) → C`, satisfying `h ∘ (ι i) = 𝕗 i`
-- for every `i : I` then `h` must be equal to `fromSumg 𝕗`
theorem fromSumgUnique {I C : Type} {𝔸 : I → Type} {𝕗 : (i : I) → 𝔸 i → C} {h : (Σ (i : I), 𝔸 i) → C} : (∀ (i : I), h ∘ (ι i) = (𝕗 i)) → (h = fromSumg 𝕗) := by
intro hs
funext ⟨i, a⟩
exact congrFun (hs i) a
-- ## Exercises
-- The sum is commutative
theorem sumComm {A B : Type} : (A ⊕ B) ≅ (B ⊕ A) := by
let f : (A ⊕ B) → (B ⊕ A) := fromSum (ι2) (ι1)
let g : (B ⊕ A) → (A ⊕ B) := fromSum (ι2) (ι1)
let h : isomorphism f := by
apply Exists.intro g
apply And.intro
-- g ∘ f = id
funext e
match e with
| inl a => rfl
| inr b => rfl
-- f ∘ g = id
funext e
match e with
| inl a => rfl
| inr b => rfl
apply Nonempty.intro
exact Subtype.mk f h
-- The sum is associative
theorem sumAssoc {A B C : Type} : ((A ⊕ B) ⊕ C) ≅ (A ⊕ (B ⊕ C)) := by
let f : ((A ⊕ B) ⊕ C) → (A ⊕ (B ⊕ C)) := fromSum (fromSum (ι1) (ι2 ∘ ι1)) (ι2 ∘ ι2)
let g : (A ⊕ (B ⊕ C)) → ((A ⊕ B) ⊕ C) := fromSum (ι1 ∘ ι1) (fromSum (ι1 ∘ ι2) (ι2))
let h : isomorphism f := by
apply Exists.intro g
apply And.intro
-- g ∘ f = id
funext e
match e with
| inl ab => match ab with
| inl a => rfl
| inr b => rfl
| inr c => rfl
-- f ∘ g = id
funext e
match e with
| inl a => rfl
| inr bc => match bc with
| inl b => rfl
| inr c => rfl
apply Nonempty.intro
exact Subtype.mk f h
-- Empty is a left unit
theorem TEmptySumL {A : Type} : (Empty ⊕ A) ≅ A := by
let f : (Empty ⊕ A) → A := fromSum emptyToAny id
let g : A → (Empty ⊕ A) := ι2
let h : isomorphism f := by
apply Exists.intro g
apply And.intro
-- g ∘ f = id
funext e
match e with
| inl z => exact Empty.elim z
| inr a => rfl
-- f ∘ g = id
funext e
exact rfl
apply Nonempty.intro
exact Subtype.mk f h
-- Empty is a right unit
theorem TEmptySumR {A : Type} : (A ⊕ Empty) ≅ A := by
let f : (A ⊕ Empty) → A := fromSum id emptyToAny
let g : A → (A ⊕ Empty) := ι1
let h : isomorphism f := by
apply Exists.intro g
apply And.intro
-- g ∘ f = id
funext e
match e with
| inl a => rfl
| inr z => exact Empty.elim z
-- f ∘ g = id
funext e
exact rfl
apply Nonempty.intro
exact Subtype.mk f h
-- Product distributes over sum on the right
theorem TProdSumDistR {A B C : Type} : (A × (B ⊕ C)) ≅ ((A × B) ⊕ (A × C)) := by
let f : (A × (B ⊕ C)) → ((A × B) ⊕ (A × C)) := by
intro ⟨a, bc⟩
match bc with
| inl b => exact Sum.inl (⟨a, b⟩)
| inr c => exact Sum.inr (⟨a, c⟩)
let g : ((A × B) ⊕ (A × C)) → (A × (B ⊕ C)) := fromSum (toProd π1 (ι1 ∘ π2)) (toProd π1 (ι2 ∘ π2))
let h : isomorphism f := by
apply Exists.intro g
apply And.intro
-- g ∘ f = id
funext ⟨a, bc⟩
match bc with
| inl b => rfl
| inr c => rfl
-- f ∘ g = id
funext e
match e with
| inl ⟨a,b⟩ => rfl
| inr ⟨a,c⟩ => rfl
apply Nonempty.intro
exact Subtype.mk f h
-- Product distributes over sum on the left
theorem TProdSumDistL {A B C : Type} : ((A ⊕ B) × C) ≅ ((A × C) ⊕ (B × C)) := by
let f : ((A ⊕ B) × C) → ((A × C) ⊕ (B × C)) := by
intro ⟨ab, c⟩
match ab with
| inl a => exact Sum.inl (⟨a, c⟩)
| inr b => exact Sum.inr (⟨b, c⟩)
let g : ((A × C) ⊕ (B × C)) → ((A ⊕ B) × C) := fromSum (toProd (ι1 ∘ π1) π2) (toProd (ι2 ∘ π1) π2)
let h : isomorphism f := by
apply Exists.intro g
apply And.intro
-- g ∘ f = id
funext ⟨ab, c⟩
match ab with
| inl a => rfl
| inr b => rfl
-- f ∘ g = id
funext e
match e with
| inl ⟨a,c⟩ => rfl
| inr ⟨b,c⟩ => rfl
apply Nonempty.intro
exact Subtype.mk f h
end Sum[execution skipped because this upstream chapter is currently broken]Chapter 14: Lists Monoids
Upstream note: this chapter does not compile cleanly in the current IntroToLean4 repo state, so the examples below are shown as source only to avoid flooding the document with misleading execution errors.
Example 1
Status: source only
-- Lists and Monoids
import a05Functions
import a06NaturalNumbers
open Bij
open N
open a10Exercises[execution skipped because this upstream chapter is currently broken]Example 2
Status: source only
-- ## Definition
-- A list is a sequence of elements of a given type
-- A list can be empty or it can have one or more elements
-- A nonempty list is defined by its head and tail
-- The head is the first element of the list
-- The tail is the rest of the list
-- The empty list is denoted by `[]`
-- The list constructor is denoted by `::`
-- The list constructor takes an element and a list and returns a new list
#print List
#print List.nil
#print List.cons
#print List.append
-- ## Notation
-- `[]` is the empty list
-- `::` is the list constructor[execution skipped because this upstream chapter is currently broken]Example 3
Status: source only
-- ## Examples
#check []
#check z::[]
-- `[]` is the empty list
-- `1::[]` is a list with one element
-- `1::2::[]` is a list with two elements[execution skipped because this upstream chapter is currently broken]Example 4
Status: source only
namespace Monoids
-- ## Definition
-- A monoid is a set with an associative binary operation and an identity element
@[ext] structure Monoid.{u} where
base : Type u
mul : base → base → base
one : base
assoc : ∀ {a b c : base}, mul a (mul b c) = mul (mul a b) c
idl : ∀ {a : base}, mul one a = a
idr : ∀ {a : base}, mul a one = a
@[ext] structure MonoidHom (M N : Monoid) where
map : M.base → N.base
map_mul : ∀ {a b : M.base}, map (M.mul a b) = N.mul (map a) (map b)
map_one : map M.one = N.one
-- (N, +, 0) is a monoid
def instMonoidNAdd : Monoid where
base := N
mul := Addition
one := z
-- associativity
assoc := TAddAss.symm
-- id is the identity element on the left
idl := TAdd0L
idr := TAdd0R
-- (N, *, 1) is a monoid
def instMonoidNMul : Monoid where
base := N
mul := Multiplication
one := one
-- associativity
assoc := TMultAss.symm
-- id is the identity element on the left
idl := TMult1L
idr := TMult1R
-- (List α, ++, []) is a monoid for any type α
def FreeMonoid {α : Type u} : Monoid where
base := List α
mul := List.append
one := []
-- associativity
assoc := by
intro a b c
induction a with
| nil => simp [List.append]
| cons x xs ih => simp [List.append, ih]
-- id is the identity element on the left
idl := by
intro a
induction a with
| nil => simp [List.append]
| cons x xs ih => simp [List.append, ih]
-- id is the identity element on the right
idr := by
intro a
induction a with
| nil => simp [List.append]
| cons x xs ih => simp [List.append, ih]
-- ## Universal Property
-- Insertion of generators
def η {α : Type u} : α → (@FreeMonoid α).base := by
intro a
exact List.cons a []
-- The universal property of the `FreeMonoid α` is that every function `f` from
-- the base `α` to the base of any other monoid `M` can be
-- extended to a unique monoid homomorphism `Lift f` from `FreeMonoid α` to `M` satisfying that
-- `Lift f ∘ η = f` where `η` is the insertion of generators
def Lift {α : Type u} {M : Monoid} (f : α → M.base) : (@FreeMonoid α).base → M.base := by
intro xs
cases xs with
| nil => exact M.one
| cons x xs => exact M.mul (f x) (Lift f xs)
-- The function `Lift f` is a monoid homomorphism from the free monoid to the monoid `M`
def LiftMonoidHom {α : Type u} {M : Monoid} (f : α → M.base) : MonoidHom (@FreeMonoid α) M where
map := Lift f
map_mul := by
intro a b
induction a with
| nil => calc
Lift f (FreeMonoid.mul [] b) = Lift f b := rfl
_ = M.mul (M.one) (Lift f b) := M.idl.symm
_ = M.mul (Lift f []) (Lift f b) := congrArg (fun x => M.mul x (Lift f b)) rfl
| cons x xs ih => calc
Lift f (FreeMonoid.mul (x::xs) b) = Lift f (x :: (FreeMonoid.mul xs b)) := rfl
_ = M.mul (f x) (Lift f (FreeMonoid.mul xs b)) := rfl
_ = M.mul (f x) (M.mul (Lift f xs) (Lift f b)) := congrArg (fun y => M.mul (f x) y) ih
_ = M.mul (M.mul (f x) (Lift f xs)) (Lift f b) := M.assoc
_ = M.mul (Lift f (x::xs)) (Lift f b) := congrArg (fun y => M.mul y (Lift f b)) rfl
map_one := rfl
-- The function `Lift f` satsifies the property that `Lift f ∘ η = f`
theorem LiftEta {α : Type u} {M : Monoid} (f : α → M.base) : Lift f ∘ η = f := by
funext a
calc
Lift f (η a) = Lift f (a::[]) := rfl
_ = M.mul (f a) (Lift f []) := rfl
_ = M.mul (f a) M.one := congrArg (fun x => M.mul (f a) x) rfl
_ = f a := M.idr
-- The function `Lift f` is the unique monoid homomorphism from the free monoid to the monoid `M`
-- satisfying the property that `Lift f ∘ η = f`
theorem LiftUnique {α : Type u} {M : Monoid} (f : α → M.base) (g : MonoidHom (@FreeMonoid α) M) : g.map ∘ η = f → g = LiftMonoidHom f := by
intro h
apply MonoidHom.ext
funext a
induction a with
| nil => calc
g.map [] = M.one := g.map_one
_ = (LiftMonoidHom f).map [] := (LiftMonoidHom f).map_one
| cons x xs ih => calc
g.map (x::xs) = g.map (FreeMonoid.mul (η x) xs) := rfl
_ = M.mul (g.map (η x)) (g.map xs) := g.map_mul
_ = M.mul (f x) (g.map xs) := congrArg (fun y => M.mul y (g.map xs)) (congrFun h x)
_ = M.mul ((LiftMonoidHom f).map (η x)) (g.map xs) := congrArg (fun y => M.mul y (g.map xs)) (congrFun (LiftEta f).symm x)
_ = M.mul ((LiftMonoidHom f).map (η x)) ((LiftMonoidHom f).map xs) := congrArg (fun y => M.mul ((LiftMonoidHom f).map (η x)) y) ih
_ = (LiftMonoidHom f).map (FreeMonoid.mul (η x) xs) := (LiftMonoidHom f).map_mul.symm
_ = (LiftMonoidHom f).map (x::xs) := rfl
-- The definition of the length of a list is the number of elements in the list
-- It can be defined as a monoid homomorphism from the free monoid to the monoid of
-- natural numbers
def Len : α → N := by
intro _
exact one
-- The length of a list is a monoid homomorphism from the free monoid
-- to the monoid of natural numbers
def Length {α : Type u} : (@FreeMonoid α).base → instMonoidNAdd.base := Lift Len[execution skipped because this upstream chapter is currently broken]Example 5
Status: source only
end Monoids[execution skipped because this upstream chapter is currently broken]Example 6
Status: source only
namespace a14Exercises
open Monoids[execution skipped because this upstream chapter is currently broken]Example 7
Status: source only
-- ## Exercises
@[ext] structure MonoidIso (M N : Monoid) extends (MonoidHom M N) where
iso : isomorphism map
def g : N → (List Unit) := by
intro n
match n with
| z => exact []
| s n => exact ()::(g n)
-- Prove that the monoids `instMonoidNAdd` and `@FreeMonoid Unit` are isomorphic
def NFreeMonoidIso : MonoidIso (@FreeMonoid Unit) instMonoidNAdd where
map := @Length Unit
map_mul := (@LiftMonoidHom Unit instMonoidNAdd Len).map_mul
map_one := (@LiftMonoidHom Unit instMonoidNAdd Len).map_one
iso := by
apply Exists.intro g
apply And.intro
--
funext l
induction l with
| nil => exact rfl
| cons x xs ih => calc
g (Length (x::xs)) = g (s (Length xs)) := rfl
_ = ()::(g (Length xs)) := rfl
_ = ()::xs := congrArg (fun y => ()::y) ih
_ = (x::xs) := rfl
--
funext n
induction n with
| z => exact rfl
| s n ih => calc
Length (g (s n)) = Length (()::(g n)) := rfl
_ = one + (Length (g n)) := rfl
_ = one + n := congrArg (fun y => one + y) ih
_ = s n := rfl
end a14Exercises[execution skipped because this upstream chapter is currently broken]