UNDER CONSTRUCTION
Code for this chapter

Foundations in Lean

by Eric Klavins

The notes presented here were initially developed for a special topics graudate course on Lean I taught in the Winter of 2025. The course was taken mainly by Electrical and Computer Engineers with standard programming experience, some engineering mathematics background, and a variety of different application areas in mind. The main reading for the course included all the standard Lean references and books. These notes are merely a supplement for those excellent resources.

That said, I hope the material presented here presents a unique and useful perspective that arose over several decades of my periodically checking in on proof assistants, becoming enamored for a while, and then moving on to other projects. For me, the alure of theorem provers is the possibility of once and for all connecting the foundations of mathematics (Type Theory in the case of Lean) with the work of practicing mathematicians and engineers. Thus, my presentation focuses on foundations, whereas other resources may focus more on the use of Lean for particular applications.

Every new generation of proof assistant gets a bit closer to realizing the goal of making all of mathematics easily formalized. Of all of the tools available, from Agda to Rocq, none has captured my attention like Lean 4 has. I think it is the combination of tooling in VS Code, the self-boostrapping nature of Lean 4 being written in Lean 4, the simultaneous blossoming of machine learning, and the inspiring community of researchers exploring how to use Lean 4. These taken together seem to be giving Lean considerable momentum.

My hope is that these notes are useful for students wishing to understand the type theoretic foundations of Lean and similar tools. I think such an understanding is useful for a variety of reasons. First, I think learning a computer programming language is aided by an understanding of how the language is executed or intepreted. For a language like C, it is hard to imagine becoming a true expert without understanding assembly language, stacks, memory allocation, and compilation. Just using a C debugger like gdb requires a fair amount of knowledge about the underlying model of computation. For Lean, the model is the lambda calculus, type checking, and type inference. When Lean doesn't work, students can spend hours trying various incantations to make it do what they want. With some understanding of the underlying model of computation, getting unstuck becomes easier. Second, there is no reason to think that the development of proof checkers is somehow complete with Lean as the final solution to the problems that have plagued such tools for decades. Understanding how Lean works will hopefully inspire someone (perhaps even me) to write their own proof checker someday, using Lean and its foundations as a reference architecture.

Finally, the study of the foundations of mathematics is incredibly rich and interesting in its own right, like topology or number theory. I encourage the interested student to dig deeply into this material and then read the primary literature on Type Theory, to gain at least an appreciation if not a mastery of the wonders that underpin how Lean and its cohort of proof checkers work.

Acknowledgements

I would like to acknowledge the students who took my special topics course offered the Winter of 2025 at the University of Washington. We all learned Lean together. At first, I was a few weeks ahead, and by the end of the course I was a few weeks behind. Much of the material here was developed in response to their questions and ideas.

UNDER CONSTRUCTION
Code for this chapter

A Tour of Lean 4

Installing Lean

The easiest way to install Lean is to follow the quickstart guide at

• Lean Quickstart

You will need first install VS Code:

• VS Code

Then go to View > Extensions and search for "Lean 4" and install it.

This will put a ∀ in the upper right menu bar of VS Code. From there, you can create a new project, which should install Lean and all of the associated tools.

Lean "Project" Types

With the VS Code Extension, you can install two types of projects:

• Standalone project. Just the basics.

• Mathlib project. Includes a huge library of most basic and several advanced areas of mathematics. Choose this if in particular if you want to use real numbers, algebra, sets, matrices, etc.

Despite its size, I recommend starting a Mathlib based project. You never know when you might need something from Mathlib.

Notes:

• Wait for the tool to completely finish before opening or changing anything.
• I don't like the option where it creates a new workspace
• Don't make a new project every time you want to try something out. You will use up all the space on your hard drive. Instead, create a single monolithic project and mkae subdirectores for ideas you want to explore.

Directory Structure

If you create a new project called MyProject, you will get a whole directory of stuff:

   MyProject
     .github/
     .lake/
     MyProject/                    <-- put your code here
       Basic.lean
     .gitignore
     MyProject.lean
     lake-manifest.json
     lakefile.toml
     lean-toolchain
     README.md

For now, you mainly need to know that the subdirectory with the same name as your project is where you can put your .lean files. It has one in it already, called Basic.lean. Open this and you can start playing with Lean.

Testing an Installation

Try replacing the code in Basic.lean with the following:

import Mathlib.Tactic.Linarith

#eval 1+2

example (x y z : ℚ)
        (h1 : 2*x < 3*y)
        (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0) : False := by
  linarith

If it is not open already, open Lean infoview via the ∀ menu.

• Put your curor over 1+2. You should see 3 in the messages.
• Put your cursor just before by you will get some goals.
• Rut it after linarith you will see "No Goals", since the theorem is proved.

Fancy Characters

You can enter fancy characters in Lean using escape sequences

  →                   \to
  ↔                   \iff
  ∀                   \forall
  ∃                   \exists
  ℕ                   \N
  xᵢ                  x\_i

Go to

  ∀ > Documentation > ... Unicode ...

for a complete list.

Type Checking

Lean is based on type theory. This means that every term has a very well defined type. To find the type of an expression, use #check. The result will show up in the Infoview.

#check 1
#check "1"
#check ∃ (x : Nat) , x > 0
#check λ x => x+1
#check (4,5)
#check ℕ × ℕ
#check Type

Evaluation

You can use Lean to evaluate expressions using the #eval command. The result will show up in the Infoview.

#eval 1+1
#eval "hello".append " world"
#eval if 2 > 2 then "the universe has a problem" else "everything is ok"
#eval Nat.Prime 741013183

Proofs

We will go into proofs in great detail next week. For now, know that you can state theorems using the theorem keyword.

theorem my_amazing_result (p : Prop) : p → p :=
  λ h => h

In this expression,

my_amazing_result is the name of the theorem (p : Prop) is an assumption that p is a proposition (true or false statement) p → p is the actual theory := delinates the statement of the theorem from the proof λ h => h (the identity function) is the proof

You can use your theorems to prove other theorems:

theorem a_less_amazing_result : True → True :=
  my_amazing_result True

Examples vs Proofs

Results don't have to be named, which is useful for trying things out or when you don't need the result again.

example (p : Prop) : p → p :=
  λ h => h

example (p q r : Prop) : (p → q) ∧ (q → r) → (p → r) :=
  λ ⟨ hpq, hqr ⟩ hp => hqr (hpq hp)

The Tactic Language and sorry

The examples above use fairly low level Lean expressions to prove statements. Lean provides a very powerful, higher level DSL (domain specific language) for proving. You enter the Tactic DSL using by.

Proving results uses the super sorry keyword. Here is an example of Tactics and sorry.

example (p q r : Prop) : (p → q) ∧ (q → r) → (p → r) := by
  intro h hp
  have hpq := h.left
  have hqr := h.right
  exact hqr (hpq hp)

which can be built up part by part into

example (p q r : Prop) : (p → q) ∧ (q → r) → (p → r) := by
  intro ⟨ hpq, hqr ⟩
  intro hp
  have hq : q := hpq hp
  have hr : r := hqr hq
  exact hr

Don't worry if none of this makes sense. We'll go into all the gory details later.

Programming

Lean is also a full-fledged functional programming language. For example, much of Lean is programmed in Lean (and then compiled). That said, the Lean Programming Language is not really general purpose: You would probably lose your mind trying to build an operating system with Lean. Rather, Lean is a programming language designed first for programming Lean itself, and second for build mathematical data structures and algorithms.

If you are not familiar with functional programming: you will be by then end of this book.

Here is an example program:

def remove_zeros (L : List ℕ) : List ℕ := match L with
  | [] => List.nil
  | x::Q => if x = 0 then remove_zeros Q else x::(remove_zeros Q)

#check remove_zeros

#eval remove_zeros [1,2,3,0,5,0,0]

Note the similarity between def and theorem. The latter is simply a special kind of definition.

Documentation

• Loogle - Google for Lean

• Zulip Chat

• Lean Theorem Proving Book

• Lean Functional Programming Book

• Lean Metaprogramming -- Advanced!

• Mathematics in Lean

• Tactics

• The Standard Library

UNDER CONSTRUCTION
Code for this chapter

The Simply Typed λ-Lambda Calculus

Background

The λ-calculus was introduced in the 1930s by Alonzo Church as a way to represent how functions on natural numbers are calculated using symbols. The goal was to determine whether every function on the natural numbers had an effective means of being calculated.

Said differently, the question is: Does every function have an algorithm? Astonishingly, Church showed that the answer is "no". In fact, there are functions on the natural numbers for which there is no effective algorithm. Church's 1935 paper "An unsolvable problem in elementary number theory" proved this result.

The reasoning, roughly, is this:

• Devise a simple programming language, the λ-calculus
• Define computation as rewriting operations on λ-calculus terms
• Correspond to every term a natural number
• Conclude that questions about terms are thus questions about numbers
• Show there are more functions from terms into terms than there are terms.

A specific problem that Church showed to be unsolvable is: Given λ-calculus terms M and N, show there does not exist a λ-calculus function that can determine whether M can be rewritten as N. Those who have studied theoretical computer science, may be familiar with Alan Turing's similar result which shows there is no Turing Machine that can determine whether a given Turing Machine eventually terminates. In fact, the λ-calculus can simulate Turing Machines and vice verse.

The Church-Turing Thesis is the observation that all formalizations of computation are in fact equivalent to the λ-calculus or, equivalently, Turing Machines. The former is more convenient for symbolic reasoning, while the latter is more akin to how electromechanical computers actually work.

Programming Languages

Thus, the λ-calclus and the formal notion of computation has its roots in the foundations of mathematics. Later, around the 1960s, linguists and computer scientists realized that the λ-calculus was an useful framework for the theory and design of programming languages.

Simultaenously, logicians were becoming frustrated with Set Theory as a foundation for mathematics and started exploring Type Theory as an alternative. Around the 1990s many of these ideas came together, especially through the work of Thierry Coquand on the Calculus of Constructions. It was observed that typed programming languages were not only an ideal foundation for all of mathematics, they could be used to develop computational proof assistants and theoerm provers.

Curry's Paradox

The original formulation of the λ-calculus allowed for infinite loops, as do most programming languages. This made the λ-calculus expressive enough for Church to prove his undecidability results, but it caused other problems when logicians wished to use formalisms like the λ-calculus as systems of logic.

Haskel Curry discovered that one could encode the following paradox:

• Consider the self-referential statement X = X → Y where Y is any statement.
• Certainly X → X is true for any statement X.
• Substituting X → Y for the second X gives X → (X → Y)
• This statement is equivalent to X → Y, which is the same as X
• Thus X is true
• So Y is true since X → Y

For example, X → Y could mean "If this sentence is true, then 1 > 0." Any framework in which you can make this argument allows you to prove any statement Y, and so the framework is useless logically.

Types

The solution was to give types to all terms in the λ-calculus. We will see below that certain self referential programs are impossible to assign types to. At the same time, infinite loops are no longer allowed, making the formalism not as powerful from a computational point of view.

Thus was born the simply-typed λ-calculus. Eventually, more complicated types were added, in which type definitions could depend on other types or on even terms. Most modern programming languages and some logical frameworks have these properties.

Church's paper on the subject is quite complicated, elucidating ideas that were fairly novel at the time. Since then, comptuer scientists have refined the ideas into a very simple framework, which is presented here, and which can be found in numerous textbooks. The notes in the first part of this section follow video lectures by students of Prof. Uwe Nestmann at the Technical University of Berlin, except that I have restated the formulas in Lean. A link to the videos can be found in the references at the end of this chapter. A Google search will yield hundreds of similar lectures, notes, books, and papers.

Basic Types

The simply typed λ-calculus is an extremely simple programming language that nevertheless captures the essence of computation. It uses type expressions and terms that have those types. We start with the types. First, we assume a base type. In Lean the base type is called Type. You can ask lean what Type is using the #check directive (which stands for "Type Check").

#check Type

Lean tells you Type has Type 1, which is a synonym for Type. Don't worry about this right now and just accept that Type is a type. One constructs new types using the arrow → as in the following examples:

#check Type → Type
#check Type → (Type → Type)
#check (Type → Type) → Type

That is, whenevever τ is a type, so is τ → τ. Arrow types are supposed to denote function types. So τ → τ is the type of any function that takes objects in τ and returns objects in τ. Note that the arrow → associates to the right. So the second expression above is equivalent to Type → Type → Type.

Type Variables and Applications

You can also define type variables using def

def A := Type
def B := Type → Type

Which looks a bit more like what you would see in a textbook on type theory. Now you can construct more types.

#check A → B

Terms

Next, we define the terms of the lambda calculus. These are the programs. We start with variables, for example x and f, which we declare in Lean as follows:

variable (x : A)               -- declare a variable x of type a
variable (f : A → A)           -- declare a function f from A into A

#check x
#check f

What we've said here is that x is a simple object with type A, while f is an function type from A into A. Next we have applications. These have the form e₁ e₁ where e₁ and e₂ are terms. For example,

#check f x
#check f (f x)
#check f (f (f x))

are all applications of terms to terms.

Abstractions

Finally, we have abstractions, which have the form λ (x : τ) => e where τ is a type and e is a term. The x in this expression is said to be bound to the abstraction. It is a dummy variable and could be renamed without any change in meaning. For example, the following are terms in the λ-calculus:

#check λ (y : A) => y
#check λ (g : A → A) => λ (y : A) => g y

In the first example, the abstraction defines a function that simply returns its argument. In the second example, the abstraction defines a function that takes another function g and returns yet another abstraction that takes an object y and returns g applied to y.

Note that the parentheses group to the right, so the second example is equivalent to:

#check λ (g : A → A) => ( λ (y : A) => g y )

In Lean, we can also abbreviate a chained lamdba abstractions by writing:

#check λ (g : A → A) (y : A) => g y

Equivalence with def

A lambda abstraction is basically an unamed function. You could also give your functions names and use def.

def inc₁ (x : Nat) : Nat := x + 1
def inc₂ := λ x => x + 1

#eval inc₁ 3
#eval inc₂ 3
#eval (λ x => x + 1) 3

Currying

Consider the lambda abstraction

variable (X : Type)
variable (a : X)

#check λ (g : X → X) => λ (x: X) => g x

If we apply the abstraction to particular function, then we get another function.

#reduce (λ (g : X → X) => λ (x: X) => g x) (λ x => x)

This way this new function is obtained is called Currying after Haskel Curry. The function can then be applied again:

#reduce (λ (g : X → X) => λ (x: X) => g x) (λ x => x) a

Type Derivation

All terms have types. These can be found using type theory's derivation rules:

VAR: Variables are declared either globally to have a given type (using Lean's variable command) or are bound in a λ-expression.

ABST: The type of an abstraction is always of the form A → B where A is the type of the argument and B is the type of the result.

APPL: If f : A → B and x : A, then the type of the application of f to x is B.

These derivation rules are applied automatically by Lean in the process of type checking using the #check directive. We can see the types Lean derives as follows.

def h₁ := λ (y : A) => y
def h₂ := λ (g : A → A) => λ (y : A) => g y

#check x
#check h₁
#check h₂
#check h₁ x
#check h₂ h₁               --> Example of currying
#check h₂ h₁ x

Note: Currying is named after the Logician Haskel Curry, who studied Electrical Engineering at MIT in the 1920s, although he eventually switched to Physics.

Type Errors

The typed lambda calculus disallows expressions that do not follow typing rules. For example, the following expression produces a type error

#check_failure λ (g : A) => λ (y : A) => g y

because g is not declared to be a function type and therefore cannot be applied to y.

Another example is

#check_failure λ (y : A) => q

about which Lean complains because q has not been declared in the present context.

Judgements and Contexts

When you hover over a #check directive, Lean shows the results of the type derivation as what is called a judgement. It is an expression in two parts separated by a turnstile ⊢. For example: #check h₁ x produces

x : A
f : A → A
⊢ A

Before the turnstile is the context, a list of all the variables introduced so far. After the turnstile is the type of (h₁ x), which in this case is A. In the literature, this written:

{ x : A, f : A → A }  ⊢  h₁ x : A

which reads: "If A has type A and f has type A → A, then we can derive h₁ x has type A". In an expression such as

λ (y : A) => f y

the variable f is not bound to an enclosing lambda. In this case it is called free. The variable y on the other hand is bound. Free variables have to be declared in Lean for expressions to use them. And they have to have types consistent to how they are used. When this is done properly, you will see the free variable declarations in the context part of Lean's results.

Beta Reduction

An abstraction can be applied to another term to produce a new term. This is called β-reduction. It is defined like this:

(λ (x:α) => M) N   —β→   M[x:=N]

The notation M[x:=N] means: take all free occurances of x in M and replace them with the expression N. We have to be careful that N does not use the variable x freely. Lean does this internally for us The bound version of x above is, internally, a completely unique variable that is just displayed as x for our convenience.

To apply β-reduction in Lean, you can use the #reduce directive. For example, we can see that

(λ (g : α → α) => λ (y : α) => g y) f   —β→   λ (y : α) => f y

This is obtained by replacing g in g y with f, as the rule describes. You can have Lean do this for you using the #reduce directive. The #reduce directive needs permission to be aggressive, which we can do using the (types := true) option.

#reduce (types:=true) (λ (y : A) => y) x
#reduce (types:=true) (λ (g : A → A) => λ (y : A) => g y) (λ (y : A) => y)
#reduce (types:=true) (λ (g : A → A) => λ (y : A) => g y) (λ (y : A) => y) x

Properties of the Simply Typed λ-calculus

Some interesting observations are in order. We won't prove these here, but they are good to know:

Uniqueness of Types: Every term has exacly one type.

Subject Reduction Lemma: If M₁ : α and M₁ —β→ M₂ then M₂ : α. That is, beta reduction does't change the type of expressions. It just simplifies them.

Church-Rosser Theorem: If M —β→ N₁ and M —β→ N₂ then there is some N₃ such that N₁ —β→ N₃ and N₂ —β→ N₃. That is, it doesn't matter what order you β-reduce an expression's sub-expressions in, you always end up with the same term.

Strong Normalization: β-reduction eventually stops at an irreducible term. This is a very strong statement. In most programming languages, you can write infinite loops. But not in the simply typed λ-calculus!

Extended Example: Church Numerals

Even though the simply typed λ-calculus looks simple, you can encode quite a bit of math with it. The goal of this next section is to show you how do do arithmetic with only what we have so far (simple arrow types and terms depending only on terms). We do this not because it is efficient -- it isn't! Instead, we want to show that the essence of arithmetic is captured by the simply typed λ-calculus.

First, we need a way to represent numbers. Church devised the following scheme, where c₀ is the Church Numeral for 0 and so on.

def α := Type

def c₀ := λ ( f : α → α ) => λ ( x : α ) => x
def c₁ := λ ( f : α → α ) => λ ( x : α ) => f x
def c₂ := λ ( f : α → α ) => λ ( x : α ) => f (f x)
def c₃ := λ ( f : α → α ) => λ ( x : α ) => f (f (f x))

You can check the type of a Church numeral:

#check c₂

For convenience, let's give this type a name:

def N := (α → α) → α → α

#check N

Arithmetic

We can define functions on numbers. For example, the successor function is defined below.

def succ := λ (m : N) => λ (f : α → α) => λ (x: α) => f (m f x)

To see how this works, let's apply succ to c₀. We omit the types to make it easier to read. Note for clarity we use the dummy variables g and y in c₀ instead of f and x.

succ c₀ = ( λ m => λ f => λ x => f (m f x) ) ( λ g => λ y => y ) —β—> λ f => λ x => f ( ( λ g => λ y => y ) f x ) [note, g is not used, so f x disappears] —β—> λ f => λ x => f ( ( λ y => y ) x ) —β—> λ f => λ x => f x = c₁

This is a lot of work, so let's let Lean do this for us:

#reduce (types := true ) succ c₀
#reduce (types := true ) succ c₃

Other Operations

We can also add two numbers together:

def add := λ (m : N) => λ (n : N) => λ (f : α → α) => λ (x: α) => m f (n f x)

#reduce (types := true) add c₃ c₂
#reduce (types := true) add (succ c₃) (add c₁ c₂)

And here is multiplication:

def mul :=  λ (m : N) => λ (n : N) => λ (f : α → α) => λ (x: α) => m (n f) x

#reduce (types := true) mul c₃ c₂

We can even do a sort of if-statement:

def ifzero := λ (m : N) => λ (n : N) => λ (p : N) =>
              λ (f : α → α) => λ (x: α) =>
              n (λ ( y : _ ) => p f x) (m f x)

#reduce (types := true) ifzero c₂ c₀ c₃
#reduce (types := true) ifzero c₂ c₁ c₃

LEAN CAN PROVE 1+1 = 2

theorem one_plus_one_is_two : add c₁ c₁ = c₂ :=
  rfl

You can prove this by rfl because, as we will see, two lambda expressions that beta reduce to the same thing are considered definitionally equal. Although this is not scalable and in fact Lean has a much more expressive type system that we will harness soon.

Church Numerals are Inconvenient

You can define other opertations on the natural numbers in a similar fashion. It is also fairly straightforward to define Booleans and Boolean Logic, as well as a number of other basic mathematical structures.

Building up from these basic ideas to more complex mathematics is the point of Lean. Eventually, we will arrive at cutting edge mathematics in Lean. Because it is defined in terms of thee basic building blocks, we always have a proof that goes from the high level mathematica statements to the low level meaning in terms of the typed λ-calculus: That is, a proof from first princples.

That said, it will ultimately be better to define a richer set of types. For example, we'll define the natural numbers and almost every other mathematical object in Lean using what are called Inductive Types.

Type Theory Questions

Now that we have a simple programming language and a way to assign types to terms in that language, we can explore a number of problems in type theory, each with its own purpose and challenges.

TYPE CHECKING: In a given context, does a term M have a given type σ?

Γ ⊢ M : σ

WELL TYPEDNESS: Does there exist a context in which a type be assigned to a term M? Another way of saying this is "is M a legal term?"

? ⊢ M : ?

TYPE INFERENCE: Can M be assigned a type consistent with a given context?

Γ ⊢ M : ?

INHABITATION: Does there exist a term of a given type? If σ is a logical statement, then this is the question of whether σ has a proof.

Γ ⊢ ? : σ

Type Inference

Lean is good at type inference. We can go a step further with Lean and leave out types in expressions, letting Lean infer what they must be. For example, the Church numerals can be written more consicely, skipping some of the type declarations and using multi-argument lambdas, as follows:

#check λ _ y => y
#check λ ( g : α → α ) y => g y
#check λ ( g : α → α ) y => g (g y)

We haven't said what the type of y is in these expressions. And we haven't even given the first bound variable in c₀ a name, since it isn't used in the the body of the abstraction. Lean infers that y must have type α because it is being acted upon by a function from α to α. We can also write the other operations, like multiplication, more concisely:

#check λ (m n : N) f x => m (n f) x

We can't leave out all of the type information though. Consider:

#check_failure λ g y => g y

In the above, there are any number of ways types could be assigned to g and y, so Lean complains that it can't assign types to them. So while the expression is typeable, Lean can't infer a type for it and you have to give it more information.

Self-application is Untypeable

Dropping types for the moment, define the term

Ω := λ x => x x

and consider Ω applied to itself Ω:

(λ x => x x) (λ x => x x)       —β—>       (λ x => x x) (λ x => x x)

producing an infinite loop. Suppose you could give M M a type:

M M : σ

For this to work, M has to be a function:

M : τ → σ

But since M is operating on itself, M has to be of type τ:

M : τ

So M has two different types, which is not possible. Lean is not able to find a type for x. The placeholder symbol _ is used by Lean as a way to ask the type checker to infer a type.

#check_failure (λ (M:_) => M M)

Propositions

Lean has a special type called Prop which stands for Proposition. It treats this type somewhat differently than all other types, but in most ways it ist just another type.

variable (p : Prop)
#check Prop
#check p

If p is of type Prop, then an element hp : p is evidence that the type p is not empty. Alternatively, you can think of hp as a proof of p.

Furthermore, arrow types which above denoted functions, can be thought of as denoting implication if Prop is involved.

#check p → p

Armed with the lambda calculus and we can now prove theorems involving implication:

example (p : Prop) : p → p :=
  λ hp => hp

example (p q : Prop) : p → (p → q) → q :=
  λ hp => λ hpq => hpq hp

Why is it Called "Simply Typed"?

You might be asking yourself, is there a non-simply typed λ-calculus? The answer is yes! We will get there eventually. Here's a preview:

Simple types: Terms depend on other tems. This is what we've covered so far. For example, the body of a lambda abstraction (a term) depends on the bound variable (also a term).

#check (λ x : Nat => x+1) --- the term x+1 depends on the term x.

Polymorphism: Terms can depend on types. Polymorphism allows us to write functions that operate on a variety of types, instead of just a single type, by taking the type to be operated on as an argument. For example, the identity function λ x : A => x only operates on elements of type x. What if we wanted to define an arbitrary identity function for any type. Here is one way:

#check (λ α : Type => λ x : α => x) -- a polymorphic identity function.

A better way would be:

universe u
def my_id {α : Type u} (x : α) := x

#check my_id 1
#check my_id "one"
#check my_id my_id

Note the curly braces around α : Type u specify that the argument α is implicit. That is, that Lean should try to infer what it is. In the the examples #check statements above, Lean figures out which type the argument is, and therefor which type the overall expression is, by inspection.

Parameterized Types: Types can depend on types. The idea here is to build a type from other types. For example, a List type is fine, but it would nice to avoid having two make a separate data type for lists of different types of objects. In fact, Lean's standard library defines List as a parameterized type. You can see in the first #check below that making a list requires a type as an argument

#check List            -- Requires a type as an argument
#check List Nat        -- The type of a list of natural numbers
#check List (List Nat) -- The type of a a list of list of natural numbers

Lean is also good at figuring out what kind of list you are talking about in most contexts, as the following examples show.

#check [1,2,3]
#check ["one","two","three"]

Dependent types: Types can depend on terms. Finally, we can have types that depend on terms. For example, the type of vectors (from Lean's standard library) of natural numbers of length 10 depends on the term 10.

#check Vector Nat 10 -- Vectors of 10 Nats

Calculus of Constructions: If we allow all of the above in type theory, we get what is called the Calculus of Constructions, or CoC. This theory was first described by Thierry Coqrand and emboded in the Coq proof assistant, now called Rocq. Lean and other proof assistants are also based on CoC.

Inductive Types: Types can be defined inductively. For example, the natural numbers are defined by a base case (zero) and a successor function (succ), from which all other natural numbers can be constructed. This is discussed in more detail in the chapter on Inductive Types.

Quotients: Quotients of types via equivalence relations. For example, a real number is defined to be the set of all Cauchy sequences of rational numbers that converge to it. That is, the reals are the quotient of the set of Cauchy Sequences by Cauchy equivalence. This is discussed in more detail in the chapter on Quotients.

Looking ahead: the Curry-Howard Correspondence

The most important problem in using type theory for proofs is INHABITATION, followed by TYPE CHECKING. To motivate why, we will see later the following remarkable fact, called the Curry-Howard corresponence, which says that in the judgement Γ ⊢ M : σ,

• Γ can be considered a set of givens or assumptions
• σ can be considered a mathematical statement like a theorem or lemma
• M can be considered a proof of the theorem assuming the statements in Γ.

Thus, type checking amounts to checking that M is a proof of σ, which is a relatively straightfoward problem and we have seen that Lean is quite good at it. This is why tools like Lean are called proof assistants. They check to make sure your proofs are correct.

On the other hand, type inhabitation amounts to finding a proof of σ. This is a very difficult problem, essentially the job of the working mathematician. From a computational point of view, finding a proof means searching over terms M until one finds one that has type σ. Depending on how expressive the programming language for terms is, this can either be a computationally intractable problem (meaning search is the best you can do) or it can be a computationally unsolvable problem (meaning there may not be an algorithm that is guaranteed to find an M of type σ). Both of these observations are job security for mathematicians!

Going a step further, we'll see that an abstraction

λ p : σ => q

which may have type

σ → τ

is the general form of a proof of the statement σ → τ where → means "implies". It can be thought of as a transformation taking a proof of σ, which one assumes is available, and returning a proof of τ, which is thought of as a goal to be proved. Writing the details of what q is amounts to programming.

As a computer scientist myself it is very satisfying to know that programming functions with given type specifications is the same thing as proving theorems!

This idea is not merely cute. By building on it, as Lean and similar tools do, one can enocde an astonishingly large set of all of mathematics, and presumably knowledge in general. We'll learn how to take advantage of the Curry-Howard corresponence soon.

References

Alonzo Church An Unsolvable Problem of Elementary Number Theory. American Journal of Mathematics, 1936.

Haskell B Curry The Inconsistency of Certain Formal Logics. The Journal of Symbolic Logic, 1942.

Alonzo Church A formulation of the simple theory of types. Journal of Symbolic Logic, 1940

Uwe Nestmann and Students The Lambda Cube Unboxed. YouTube, 2020

UNDER CONSTRUCTION
Code for this chapter

Propositional Logic

Propositions

A proposition is a statement that is either true or false. The following are examples:

• It is raining outside.
• All cats are animals.
• Darth Vader is Luke's Father.
• Four is greater than five.

In propositional logic, we assign propositional variables to represent the value of these statments. So we might make the assignments:

• p := It is raining outside.
• q := All cats are animals.
• r := Darth Vader is Luke's Father.
• s := Four is greater than five.

In Lean, we declare propositional variables as follows:

variable (p q r s : Prop)

Note that we are not saying p is the English language sentence "It is raining outside". We are not doing natural language processing here. Rather, we are saying that p is a propositional variable that is true when it actually is raining outside, and false otherwise. To determine the truth value of p, we would need some way to check whether it is raining outside (as well as some specifics like outside where and when? For now, we'll just be informal about such things).

Atomic vs Compound Propositions

A propsition that corresponds to a direct measurement or other basic truth is called atomic. It cannot be sub-divided into more basic propositions. Otherwise it is called compound. For example, the proposition

• It is raining outside or all cats are animals.

is a compound proposition that uses the connective "or", written as ∨ to connect two atomic propositions. Symbolically, we write

#check p ∨ q

to check that the compound p ∨ q is a proposition.

Students used to digital logic will wonder why we are using ∨ instead of the symbol +. The main reason is that + will usually mean actual addition when things get more complicated. Thus, mathematicans have invented new symbols for logical connectives. Here are the most important for our current purposes:

#check ¬p               -- not p
#check p ∨ q            -- p or q
#check p ∧ q            -- p and q
#check p → q            -- p implies q
#check p ↔ q            -- p if and only if q
#check True
#check False

We also have the propositional False which denotes absurdity. In intuitionistic logic, ¬p is just shorthand for

p → False

#check False
#check p → False

Also note that ↔ is just shorthand for → in both directions

p ↔ q  ≡  p → q ∧ q → p

Constructive Proofs

The goal is this chapter is to define a mathematical framework in which we prove statements by constructing proofs. In particular,

• To prove p ∧ q we construct a proof of p and another proof of q.
• To prove p ∨ q we construct a proof of p or we construct a proof of q.
• To prove p → q we supply a method for converting a proof of p into a proof of q
• To prove ¬p (which is p → ⊥) we supply a method to convert a proof of p to ⊥

Example: A Constructive Proof in Lean

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
  Iff.intro
    (λ h : p ∧ (q ∨ r) =>
      have hp : p := h.left
      have hqr : q ∨ r := h.right
      Or.elim hqr
        (λ hq : q => Or.inl (And.intro hp hq))
        (λ hr : r => Or.inr (And.intro hp hr))
    )
    (λ h : (p ∧ q) ∨ (p ∧ r) =>
      Or.elim h
        (λ hpq : p ∧ q => And.intro hpq.left (Or.inl hpq.right))
        (λ hpr : p ∧ r => And.intro hpr.left (Or.inr hpr.right))
    )

Don't worry if this doesn't make sense right now. It will soon.

Comparison to Classical Logic

We have defined intuitionistic logic or constructive logic, different from classical logic. In classical logic, the truth of a statement like

p ∨ ¬p

is guaranteed by the law of the exluded middle. You know one of them must be true. In constructive mathematics, you have to either construct a proof of p or construct a proof of ¬p. As an example, consider the proposition:

The universe is infinite or the universe is finite.

Neither part of this compound proposition currently has a proof. Classically, we would still conclude it is true, but constructively we are just stuck. Similar issues arise with famous mathematical conjectures such as

P = NP or P ≠ NP

and

There are either a finite number of twin primes, or an infinite number of twin primes.

These statements may be proved some day, but for now, we cannot conclude they are true using constructive mathematics.

Double Negation

Similar to the law of the excluded middle is double negation:

¬¬p ↔ p

Classically, this is a tautology (a proposition that is always true). But constructively, from a proof of "it is not the case that p is not true" one cannot necessarily construct a proof that p is true.

As a result, proof by contradiction is not valid constructively, because in proof by contradition one follows the procedure:

To prove `p`, assume `¬p` and derive `False`.

Just because we have a way to transform a proof of ¬p into False does not mean we can have a construction of a proof of p.

Classical Logic

TODO

Contexts

We now begin to build a framework for proving theorems in propositional logic. The first thing we need is a way to keep track of what propositions we currently know in the course of proving something.

To this end we define a context to be a finite set of propositions. Given two contexts Γ and Δ we can take their union Γ ∪ Δ to make a new context. The notation is a bit cumbersome, so we write Γ,Δ instead. In particular, if φ ∈ Φ then Γ,φ is shorthand for Γ ∪ {φ}.

If we can show that a proposition φ is true whenever all the propositions in a context Γ are true, we write

Γ ⊢ φ

which reads gamma entails φ. Furthermore, if a proposition φ is tautology (meaning it is always true like p ↔ p) then it is true independent of any context. That is, the empty context entials any tautology. Thus, we write

⊢ φ

to mean ∅ ⊢ φ. We will define precisely what the entails relationship means next.

Rules of Inference

A rule of inference is set of premises and a conclusion that can be drawn from those premises. The propositional logic we define has only a handful of rules of inference from which all proofs can be constructed. They are presented with a name followed by what looks like a fraction with the premises listed on top and the conslusion on the bottom.

                Γ₁ ⊢ A    Γ₂ ⊢ B    Γ₃ ⊢ C
  RULE NAME    ————————————————————————————
                          Γ ⊢ D

In this schemantic, the rule has three premises, each of which describe an assumption that a particular context entails a particular proposition. And the rule has one conclusion, stating the entailment you are allowed to conclude. Usually, the contexts listed and the propositions are related in some way. - #

Axioms

The first rule has no premises and simply states that φ can be concluded from any context containing φ. Said constructively, if we have a proof of φ, then obviously we can construct a proof of φ.

  AX  ——————————
       Γ,φ ⊢ φ

Here is a simple proof that {hp:p} ⊢ p in Lean using the Axiom rule:

example (hp : p) : p :=
  hp

If you look at this proof in the infoview, putting your cursor at the beginning of the second like, you will see

hp : p
⊢ p

Which says, give we have a proof hp of p, we need show p. This is easy, we jsut use hp itself.

Implies Rules

We have two rules for the → connective:

              Γ,φ ⊢ ψ
  →-Intro   ————————————
             Γ ⊢ φ → ψ

            Γ ⊢ φ → ψ    Γ ⊢ φ
  →-Elim   —————————————————————
                 Γ ⊢ ψ

The Implies Introduction rule allows us to introduce φ → ψ whenever we have Γ and φ together entailing ψ. The Implies Elimination rule is also know as Modus Ponens. It states that if we know φ implies ψ and we know φ, then we know ψ.

Notice that implies is written with an arrow → just like function abstraction in the λ-calculus. This is because one way to think about a proof of φ→ψ is to require it to have the form of a function that converts proofs of φ into proofs of ψ. This suggests that the way to prove statements with implications is to use λ-calculus expressions. Here are a couple of examples.

First we show and example of →-Intro. The context includes a proof of p. Thus we can introduce q→p for any q. We do this with a lambda expression taking a proof of q (and in this case ignoring it) and returning the proof hp of p available in the context.

example {hp : p} : q → p :=
  λ hq => hp

Next, here is an example of →-elim. We have a context with a proof of p→q and a proof of p. We know the proof hp of p→q is a lambda abstraction. So we can apply it to a proof hp of p to get a proof of q.

example {hpq: p → q} {hp: p} :=
  hpq hp

A complete description of how →-introduction works works is in the chapter on the Curry-Howard Isomorphism

And Rules

Next we have three rules for the ∧ connective:

              Γ ⊢ φ   Γ ⊢ ψ
  ∧-Intro  ———————————————————
               Γ ⊢ φ ∧ ψ

                  Γ ⊢ φ ∧ ψ
  ∧-Elim-Left   ——————————————
                    Γ ⊢ φ

                  Γ ⊢ φ ∧ ψ
  ∧-Elim-Right  —————————————
                    Γ ⊢ ψ

Whenever we see "Intro" that means we are introducing a connective (in this case ∧) into our conclusion. Whenever we see "Elim" that means we are eliminating part of a compound statement in our conclusion. Here, the And Introduction rule shows that we can construct a proof of φ ∧ ψ whenever the context contains a proof of φ and a proof of ψ. The And Elimination rules allow us to "eliminate" half of the proposition φ ∧ ψ to conclude the weaker statement φ or to conclude the weaker statement ψ. Said differently, if we have a proof of φ∧ψ then we can construct a proof of φ by just eliminating the part of the proof of φ∧ψ that shows ψ.

Unlike the somewhat cryptic rules for implies, the And rules just have functions (like And.intro) already defined for them. Here are examples of all of these rules in Lean.

#check And.intro
#check And.left
#check And.right

example (hp : p) (hq : q) : p ∧ q :=
  And.intro hp hq

example (hpq : p ∧ q) : p :=
  And.left hpq

example (hpq : p ∧ q) : q :=
  And.right hpq

Or Rules

Then we have three rules for the ∨ connective:

                   Γ ⊢ φ
 ∨-Intro-Left   ———————————
                 Γ ⊢ φ ∨ ψ

                    Γ ⊢ ψ
 ∨-Intro-Right   ————————————
                  Γ ⊢ φ ∨ ψ

            Γ ⊢ φ ∨ ψ    Γ ⊢ φ → ρ    Γ ⊢ ψ → ρ
 ∨-Elim   ———————————————————————————————————————
                         Γ ⊢ ρ

The Or Introduction rules allow us to conclude φ ∨ ψ from one of its parts. The Or Elimination rule looks complicated, but it is straightforward. It says that if we know Γ ⊢ φ ∨ ψ then we know that Γ must entail either φ or ψ. If we also know that both φ and ψ separately entail ρ, then we know that Γ must entail ρ.

Here are examples of the OR rules in Lean.

#check Or.inl
#check Or.inr
#check Or.elim

example (hp : p) : p ∨ q :=
  Or.inl hp

example (hq : q) : p ∨ q :=
  Or.inr hq

example (hpq : p ∨ q) : q ∨ p :=
  Or.elim
    hpq
    (λ hp => Or.inr hp)
    (λ hq => Or.inl hq)

Ex Falso

Finally, we have the a rule for the ¬ connective:

                Γ ⊢ False
  False -Elim ————————————
                  Γ ⊢ φ

which states that you can conclude anything if you have a proof of ⊥. This rule is also know as ex falso sequitur quodlibet or just ex falso or the principle of explosion! Here's an example:

#check False.elim

example { hf : False } : p :=
  False.elim hf

Proofs

A proof that Γ ⊢ φ is sequence of statements of the form Γ' ⊢ φ' each of which is either (a) an axiom or (b) obtained from previous statements in the sequence by one of the inference rules.

Example 1

As an example, we will prove the statement

∅ ⊢ (p∧q)→p

Working backwards from this goal, we see that →-Intro can be applied to produce this statement where φ is p∧q and ψ is p. Thus, we get an instance of →-Intro of the form

  p∧q ⊢ p
———————————          (Instantiation of →-Intro)
 ⊢ (p∧q)→p

We have now a simpler problem, which is to show p∧q ⊢ p. The ∧-Elim-Left rule applies here with φ=p∧q, ψ=p, and Γ={p∧q} giving us the instance

  p∧q ⊢ p∧q
——————————————       (Instantiation of ∧-Elim-Left)
   p∧q ⊢ p

And now we have an even simpler problem, which is to show that p∧q ⊢ p∧q. But this matches the axiom rule with Γ={p∧q} and φ = p∧q. Putting all this together into a proof gives us the following:

  1) p∧q ⊢ p∧q          axiomatically
  2) p∧q ⊢ p            from (1) via ∧-Elim-Left
  3) ⊢ (p∧q)→p          from (2) via →-Intro

And that's it. Our first proof!

Here is the same proof in Lean:

example : p∧q → p :=
  λ hpq => And.left hpq

The lambda expression encodes →-Intro, and And.left encodes ∧-Left.

What you can take away from this is the idea that constructing this proof is a purely syntactic endeavor. One can easily imagine an algorithm that does this automatically by pattern matching a given sub-goal against the Γ, φ and ψ in the description of a inference rule. The challenge is, of course, as we introduce more expressibility into our logic, and more inference rules, finding the right rules to apply at the right time amounts to a brute force search of all possible inference rules and all possible ways of instantiating those inference rools.

The other thing to notice is that the proof itself looks a lot like a program. In Lean and similar construction-based theorem provers, this observation is made precise. And it will turn out that writing proofs and writing programs amount to the same thing!

Example 2

Here is a slightly more complicated example. Let's prove

⊢ ¬p→(p→q)

Recall ¬p is just shorthand for p→⊥. So we're actually trying to prove

⊢ (p→⊥)→(p→q)

Once again, working backwards, we can apply →-Intro to get

p→⊥ ⊢ p→q

and then apply →-Intro again to get

p→⊥,p ⊢ q

Our context now contains both ¬p and p. Using ⊥-elim we get

p→⊥,p ⊢ ⊥

This subgoal matches the form of →-Elim with φ=p and ψ=⊥. Using this rule, we get two further subgoals that are just axioms:

p→⊥,p ⊢ p→⊥      and      p→⊥,p ⊢ p

Putting this all together, we get the following proof:

  1) p→⊥,p ⊢ p→⊥        axiomatically
  2) p→⊥,p ⊢ p          axiomatically
  3) p→⊥,p ⊢ ⊥          from (1) and (2) via →-Elim
  4) p→⊥,p ⊢ q          from (3) via ⊥-elim
  5) p→⊥ ⊢ p→q          from (4) via →-Intro
  6) ⊢ (p→⊥)→(p→q)      from (5) via →-Intro

And we're done! This is complicated though. Clearly we need a proof assistant to help us! In Lean this proof looks like:

theorem t : ¬p→(p→q) :=
  λ hnp => λ hp => False.elim (hnp hp)

The Law of the Excluded Middle

As we said, the law of the excluded middle states that

⊢ φ ∨ ¬φ

for all propositions φ. However, this statement is not provable using the inference rules above. To prove this meta-mathematical observation is beyond the scope of this lecture and requires an argument about the formal semantics of intuitionist propositional logic. For now, accept the fact that φ ∨ ¬φ cannot be proved rom the inference rules given, despite its seeming obviousness.

For this reason, intutionistic logic is weaker than classical logic. However, we can obtain classical logic by adding the above as a new axiom. When we get to proving statements in Lean, we'll see that we can add this axiom into our proofs if we would like to, so it is not big problem. However, it is also remarkable how much of mathematics we can do without this axiom.

Exercises

1. Prove ∅ ⊢ p → (p ∨ q)
2. Prove ∅ ⊢ (p ∨ q) → (q ∨ p)

REFERENCES

Morten Heine Sørensen, Pawel Urzyczyn "Lectures on the Curry-Howard Isomorphism" Elsevier. 1st Edition, Volume 149 - July 4, 2006.

• Chapter 2 describes Intuitionistic Propositional Logic

UNDER CONSTRUCTION
Code for this chapter

The Curry-Howard Isomorphism

Much of this chapter is an adaptation of the section of the book Lectures on the Curry-Howard Isomorphism by Morten Heine Sørensen and Pawel Urzyczyn. In particular, Chapter 4 of that book describes Intuitionistic Propositional Logic.

Statements, Contexts, and Judgements

When we introduced the Simply Typed Lambda Calculus, we informally defined the type rules VAR, ABST and APPL. Here we define the typing system formally.

• A type statement is a pair x : σ where x is a type variable and σ is a type. We say "x is of type σ".

• A typing context Γ is a finite set of type state statements.

• A judgement is an expression of the form Γ ⊢ M : σ where Γ is a typing context, M is a simply typed λ-calculus statement, and σ is a type.

For example, here is a judgment that states: "When f is a function from α to β and x is of type α, then f x is of type β. "

  { f : α → β, x : α }  ⊢ f x : β

Typing Rules

Typing rules are written the same way as the inference rules in propositional logic.

  VAR   ————————————————
          Γ,x:τ ⊢ x:τ

               Γ,x:σ ⊢ M : τ
  ABST  ——————————————————————————
           Γ ⊢ (λ x:σ => M) : σ→τ

           Γ ⊢ M : σ→τ    Γ ⊢ N : σ
  APPL  ——————————————————————————————
                   M N : τ

The first rule says that if a context defines x to have type τ then (somewhat obviously) we can conclude x has type τ.

The second rule says that if our context defines x : σ and entails that M : τ, then we can form an abstraction from x and M that has type σ to τ.

The third rule says that if Γ entails both that M : σ→τ and N : σ, then the application of M to N has type τ.

Example

Q: Find the type of

λ x : A => x

A: Working backwards from this goal we use ABST with τ=A and M=x to get

x:A ⊢ x:A

Then we use VAR. So the expression has type A→A and a proof of this is:

1) x:A ⊢ x:A                  axiomatically
2) (λ x : A => x) : A→A       by ABST

As we have seen, Lean figures this out automatically.

#check λ x : _ => x

EXAMPLE

Q: Find the types of x and y in

λ x => λ y => x y

A: Using the ABST rule gives

x : B   ⊢  λ y => x y : A

for some types A and B. Using ABST again gives

x : B, y : C   ⊢  x y : A

for some type C. Next we use the APPL rule with M = x, N = y, σ = C, τ = A

x : B, y : C  ⊢  x : C → A
x : B, y : C  ⊢  y : C

These judgements would hold if B we equal to C→A. So we make that substitution so the above axioms hold to get:

λ x : C → A => λ y : C => x y

for some types C and A. Generally speaking, type inference involves applying typing rules, accumulating type equations, and then solving the equations, all of which is done very efficiently in Lean's kernel.

Example

Q: Find the overall type of the previous expression.

A: Following the derivation above in reverse gives the following type inference proof tree:

    ————————————————————————————— VAR    ————————————————————————————— VAR
     x : C → A, y : C  ⊢  x : C → A       x : C → A, y : C  ⊢  y : C
    ———————————————————————————————————————————————————————————————————— APPL
                      x : C → A, y : C   ⊢  x y : A
                 ————————————————————————————————————————— ABST
                    x : C → A  ⊢  λ y : C => x y : C → A
            ————————————————————————————————————————————————————— ABST
             ⊢  λ x : C → A => λ y : C => x y : (C → A) → C → A

Thus, the type of λ x => λ y => x y is (C → A) → C → A. Note that with a little help, Lean can figure this out for us, but we do need to tell it that x is a function type of some kind.

#check λ x : _ → _ => λ y : _ => x y

Curry-Howard Isomorphism Intuition

Consider the two types we just found:

A → A
(C → A) → C → A

The first one is the type of a function on. The second one is the type of a function that takes a function on C → A.

Wwe can also read these as propositional formulas which state

A implies A
(C implies A) implies C implies A

It is not a coincidence that these are both tautologies.

The Curry-Howard Isomorphism emerges from the observation that the λ expressions that have the above types look a lot like the proofs that the above implications are tautologies!

With this observation, the statement x : A reads "x is a proof of A".

λ x : A => x

is a method that takes a proof of A and returns a proof of A, proving the implication A → A.

Curry-Howard: Types → Propositions

To state the CHI exacly, we will restrict ourselves to showing that Propositional Logic with only implication (→) is isomorphic to the simply typed λ-calculus. We will need one definition.

Def: Given a context Γ = { x₁: φ₁, x₂ : φ₂, ..., xₙ : φₙ }, the range of Γ, denoted |Γ|, is { φ₁, φ₂, ..., φₙ }.

Theorem: If Γ ⊢ M : φ then |Γ| ⊢ φ.

Proof Sketch: We convert any type derivation tree into a propositional proof by replacing VAR with AX, ABST with →-Intro, and APPL with →-Elim. This is done by induction on the proof tree. Here we just show an example which should be easily generalized. The type proof tree in the previous section can be re-written be removing all "x : "

    ————————————————————— AX       ———————————————————— AX
     C → A, C  ⊢  C → A               C → A, C  ⊢  C
  ——————————————————————————————————————————————————————————— →Elim
                      C → A, C   ⊢  A
                    ——————————————————— →-Intro
                      C → A  ⊢  C → A
                   —————————————————————— →-Intro
                    ⊢  (C → A) → C → A

Curry-Howard: Propositions → Types

The opposite direction of the CHI is more technical. We have to show how to produce a λ-calculus term M from a proof of φ so that M : φ. For example, suppose we started with the propositional proof tree in the previous section. How would we produce the type derivation from it? Here we will outline how this is done in general.

First we need a way to produce a type context from a propositional context. Suppose that

Γ = { φ₁, φ₂, ..., φₙ }

and define

Δ = { x₁ : φ₁, x₂ : φ₂, ..., xₙ : φₙ }

where the xᵢ are introduced as new type variables. The object Δ is a function of Γ of course, but we just don't write it this way.

Theorem: If Γ ⊢ φ then there exists a λ-calculus term M such that ∆ ⊢ M:φ.

The proof of this theorem uses induction on the proof tree that shows Γ ⊢ φ. Since there are three rules (AX, →Intro, and →-Elim), we have three cases, which we handle one by one.

Case: The proof ends with Γ,φ ⊢ φ by the VAR rule

Subcase 1: If φ ∈ Γ then there is some type variable x such that x : φ ∈ Δ. By the VAR rule we can conclude

Δ  ⊢  x : φ

Subcase 2: If φ ∉ Γ then we introduce a new variable x such that x : φ. Once again by the VAR rule

Δ, x : φ  ⊢  x : φ

(Why do we need two sub-cases? It's because of how we defined Δ on the previous as related to Γ and not to Γ ∪ { x : φ }).

Case: The proof ends with →Elim

Suppose the proof that Γ ⊢ φ ends with

    Γ ⊢ ρ → φ      Γ ⊢ ρ
  ——————————————————————————
           Γ ⊢ φ

We need to find a λ-term that has type φ. Here the premises of the above rule instance allow us to assume the induction hypothesis that there exists M and N such that

Δ ⊢ M : ρ → φ
Δ ⊢ N : ρ

By the ABST rule, we can conclude

Δ ⊢ M N : φ

Case:: The proof ends with →Intro

Suppose the proposition φ has the form the ρ → ψ and the proof Γ ⊢ ρ → ψ ends with

     Γ, ρ ⊢ ψ
  ——————————————
    Γ ⊢ ρ → ψ

Subcase 1: ψ ∈ Γ. By the induction hypothesis, there is a term M such that Δ ⊢ M : ψ. Introduce a variable x (not used in Δ) such that x : ρ. Then we can conclude

Δ, x : ρ  ⊢  M : ψ

and by the ABST rule

Δ ⊢ λ x : ρ => M : ρ →  ψ

Subcase 2: ψ ∉ Γ. Then by the induction hypothesis, there is a term M such that

Δ, x : ρ ⊢ M : ψ

from which we may also conclude

Δ ⊢ λ x : ρ => M : ρ →  ψ

Propositions, Theorems, and Proofs in Lean

The Curry-Howard approach is exactly how proofs of theorems are done in Lean. We show that the proposition to be proved is inhabited. In the examples below, we use the type Prop, from Lean's standard library.

We will start by declaring two variables of type Prop. We use curly braces here instead of parentheses for reasons we will explain later.

variable { A C : Prop }

To prove a proposition like A → A, we define the identity function from A into A, showing the proposition considered as a type is occupied. We have called the bound variable in the lambda expression proof, but you could call the bound variable anything you like.

def my_theorem : A → A :=
  λ proof : A => proof

Lean provides the keyword theorem for definitions intended to be results, which is like def but does requires the type of the theorem being defined to be Prop. The theorem keyword also gives Lean and the user an indication of the intended use of the definition.

theorem my_lean_theorem : A → A :=
  λ proof : A => proof

APPLYING THEOREMS TO PROVE OTHER THEOREMS

As another example, we prove the other proposition we encountered above. Here we call the bound variables pca for "proof of c → a" and pc for "proof of c".

theorem another_theorem : (C → A) → C → A :=
  λ pca : C → A =>
  λ pc : C =>
  pca pc

Or even better, we can use our first theorem to prove the second theorem:

theorem another_theorem_v2 : (C → A) → C → A :=
  λ h : C → A => my_lean_theorem h

More Examples

theorem t1 : A → C → A :=
  λ pa : A =>
  λ pc : C =>                                -- Notice that pc is not used
  pa

theorem t2 : A → C → A :=
  λ pa pc  => pa                             -- We can use λ with two arguments

theorem t3 : A → C → A :=
  λ pa _ => pa                               -- We can tell Lean we know pc is not used

example : A → C → A :=                       -- We can state and prove an unnamed theorem
  λ pa _ => pa                               -- using the `example` keyword

NEGATION

There are, of course, only so many theorems we can state using only implication. In the next chapter we will show how the λ-calculus can be extended to include ∧, ∨, and False. To give a sense of how this looks, here is an example using ¬p, which as you will recall is the same as p → False.

variable (p q: Prop)

example : p → ¬p → q :=
  λ pa pna => absurd pa pna

example : (p → q) → (¬q → ¬p) :=
  fun hpq nq hp => absurd (hpq hp) nq

Here, absurd is a theorem from the Lean standard library that we will discuss when we get to Lean's inductive type system.

A Note About Variable Declarations

If we had used

variable (A C : Prop)

above, then my_lean_theorem would have (A : Prop) as a non-implicit argument, so it would have to be applied as

my_lean_theorem hca h

which is ugly.

The way Lean uses variables is by putting them silently into all definitions and theorems that use them. So my_theorem internally looks like:

theorem my_lean_theorem (A : Prop) : A → A :=
  λ proof : A => proof

On the other hand, if we use curly braces in the variable declaration, as we did in the previous examples, then we get

theorem my_lean_theorem {A : Prop} : A → A :=
  λ proof : A => proof

so that the type of A is an implicit argument to my_lean_theorem.

References

Morten Heine Sørensen, Pawel Urzyczyn "Lectures on the Curry-Howard Isomorphism" Elsevier. 1st Edition, Volume 149 - July 4, 2006.

• Chapter 4 describes Intuitionistic Propositional Logic

UNDER CONSTRUCTION
Code for this chapter

Inductive Types

As we saw in the chapter on the λ-Calculus, we can encode fairly sophisticated objects like the natural numbers using just abstractions and applications. However, such encodings are a best clunky and hard to read. Additionally, encoding complex data types as λ-Calculus expressions has other problems:

Noncanonical terms: The types of such encodings are not guaranteed to result in canonical terms. For example, Church numerals were defined to have type

def α := Type
def N := (α → α) → α → α

But we can define expressions that have this type but that do not correspond to natural numbers. For example,

def nc : N := λ (f : α  → α) (x : α) => x

It would be vastly preferable if (a) every object of a given type was a legitimate representative of that type and every object also had exactly one representative.

Pattern Matching and Induction: To prove properties above objects of a given type, it is useful to apply induction on the structure of the object. For example, a natural number is either zero, or it is the successor of some other natural number. To prove a statement about natural numbers one would like support for pattern matching on the way the number was constructed.

Termination: As we have seem, operations on terms of a given type in the pure lambda calculus are not guaranteed to terminate. However, we will see that all terms of a given inductive type support structural recursion: We can define functions on that break the term into smaller pieces which eventual lead to indivisible elements, at which point the function terminates.

Thus, Lean and other type theoretic languages include a way to define types inductively. One lists all the ways to construct objects of a given type. Lean then provides a powerful pattern matching capability that can be used in definitions and theorems when operating or reasoning on an object defined inductively.

Namespaces

In this chapter we will be redefining several fundamental types in Lean, such as the natural numbers ℕ and the propositional connectives And and Or. Since these are part of Lean's standard library (included by default), if we do not take appropriate measures, we will get naming collisions. The easiest way to avoid this is to open a temporary namespace.

namespace Temp

Now, when we define a new symbol, such as

def Thing := Type

we are actually defining Temp.Thing. If Thing is defined in some inluded library, our new definition will not collide with it.

Lean's Inductive Types

So far we have introduced only simple arrow types composed Lean's basic type (called Type) and functions from those types into types. We now introduce a powerful way to make new types, which covers almost all of mathematics, called inductive types.

An inductive type is generated by constructors that may refer to the type itself. They say how to make objects of the given type.

Example: A type with only two elements is defined by:

inductive Two where
  | a : Two
  | b : Two

#check Two.a
#check Two.b

def t := Two.a
#eval t

Example: The simplest inductive yype has no constructors, meaning it specifies the empty type.

inductive Empty

Constructors With Arguments

You can also have constructors that take arguments and transform them into objects of the given type.

Example: The type Nat of Natural Numbers is defined by two constructors:

inductive Nat where
  | zero : Nat
  | succ : Nat → Nat           -- succ stand for `successor`

open Nat
#check succ (succ (succ zero)) -- 3

All the constructors in an inductively defined type live in a namespace with the same name as the type. The open command allows us to write succ instead of Nat.succ. We can also write

#check zero.succ.succ.succ

using so-called dot-notation.

Objects of type Nat thus either have the form zero or they consist of some finite number of applications of succ to the element zero. With more types, we can define even more complicated objects.

Example: A simple model of arithmetic expressions can be defined by the type:

inductive Expr where
  | var : String → Expr
  | add : Expr → Expr → Expr
  | mul : Expr → Expr → Expr
  | neg : Expr → Expr

open Expr

Some example terms include

#check add (var "x") (var "y")                          -- x+y
#check add (var "x") (mul (neg (var "y")) (var "z"))    -- x-yz

Functions of Inductive Types

To work with objects of inductive types, we usually need to know how the object was constructed. Lean uses the keyword match for that.

Example: Toggling a Two

def Two.toggle ( x : Two ) := match x with
  | a => b
  | b => a

Lean also knows how to reduce expressions involving match.

open Two

#reduce toggle (toggle a)
#reduce a.toggle.toggle

Example: 1+1 = 2

def Nat.plus (n m : Nat) := match n with
  | zero => m
  | succ x => succ (plus x m)

open Nat

#reduce plus (succ zero) (succ zero)

Example: Swap Adds and Muls

def Expr.swap (e : Expr) := match e with
  | var s => var s
  | add x y => add y x
  | mul x y => mul y x
  | neg x => neg x


def e := add (var "x") (mul (neg (var "y")) (var "z"))

#reduce e.swap -- -zy+x

Inductive Types May Depend on Other Types

The types we have defined so far do not interact with other types. Here's an example that does: Lists of Nats.

inductive NatList where
  | empty : NatList
  | cons : Nat → NatList → NatList

namespace NatList

#check cons zero (cons zero empty)              -- [0, 0]
#check (empty.cons zero).cons zero              -- [0, 0]

end NatList

#check [1,2]

Or we can define a List of elements of any type. In the the next bit of code, we implicitly state (using curly braced instead of parens) that List depends on an arbitrary type α.

inductive List {α : Type} where
  | empty : List
  | cons : α → List → List

namespace List
#check cons "lean" (cons "is cool" empty)       -- ["lean", "is cool"]
#check cons 3.4 (cons 1.21 empty)       -- ["lean", "is cool"]

end List

UNDER CONSTRUCTION
Code for this chapter

Propositional Logic Connectives

One of the remarkable things about inductive types is that the capture all of propositional logic, first order logic, and more. Thus, instead of defining and, or and the other logical connectives as built-in operators in the Lean language, they are just defined in the standard library in terms of more primited inductive types.

namespace Temp

And is an Inductive Type

Recall the inference rule

                 Γ ⊢ φ   Γ ⊢ ψ
    ∧-Intro ———————————————————
                  Γ ⊢ φ ∧ ψ

It states that whenever we know propositions φ and ψ, then we know φ ∧ ψ. From the point of view of types, it says that if φ and ψ are of type Prop, then so is φ ∧ ψ. In Lean we can write this as an inductive type definition as follows.

inductive And (φ ψ : Prop) : Prop where
  | intro : φ → ψ → And φ ψ

You can think of h : And p q as

• h has type And p q
• h is evidence that the type And p q is not empty
• h is a proof of the proposition And p q.

A Proof of a Simple Proposition

Consider the proposition

p → q → And p q

As a type, this proposition is a function from p to q to And p q. Thus, we know that an element of this type has the form

λ hp => λ hq => sorry

For the body of this lambda abstraction, we need to introduce an And type, which requires proofs of p and q respectively. Using the inductive definition of And we get

λ hp hq => And.intro hp hq

def g (p q : Prop) : p → q → And p q :=
  λ hp => λ hq => And.intro hp hq

And Eliminiation

The elimination rules for And are

                Γ ⊢ φ ∧ ψ                          Γ ⊢ φ ∧ ψ
  ∧-Elim-Left ——————————————         ∧-Elim-Right —————————————
                  Γ ⊢ φ                              Γ ⊢ ψ

which we can write in Lean as

def And.left {p q : Prop} (hpq : And p q) :=
  match hpq with
  | And.intro hp _ => hp

def And.right {p q : Prop} (hpq : And p q) :=
  match hpq with
  | And.intro _ hq => hq

Proofs with And-Elimination

With these inference rules, we can do even more proofs:

example (p q : Prop) : (And p q) → p :=
  λ hpq => And.left hpq

example (p q : Prop) : (And p q) → (And q p) :=
  λ hpq => And.intro hpq.right hpq.left

Match is Enough

Note that the elimination rules above are a convenience we defined to make the proof look more like propositional logic. We could also just write:

example (p q : Prop) : (And p q) → p :=
  λ hpq => match hpq with
    | And.intro hp _ => hp

This pattern suggests that with inductive types, we can think of match as a generic elimination rule.

Or is Inductive

To introduce new OR propositions, we use the two introduction rules

                 Γ ⊢ φ                              Γ ⊢ ψ
 ∨-Intro-Left ———————————          ∨-Intro-Right ————————————
               Γ ⊢ φ ∨ ψ                          Γ ⊢ φ ∨ ψ

In Lean, we have

inductive Or (φ ψ : Prop) : Prop where
  | inl (h : φ) : Or φ ψ
  | inr (h : ψ) : Or φ ψ

And we can use this inference rule in proofs as well.

example (p q : Prop) : And p q → Or p q :=
  λ hpq => Or.inr hpq.right

Or Elimination

Recall the inference rule

           Γ,p ⊢ r    Γ,q ⊢ r    Γ ⊢ p ∨ q
  ∨-Elim ————————————————————————————————————
                       Γ ⊢ r

It allows us to prove r given proofs that p → r, q → r and p ∨ q. We can define this rule in Lean with:

def Or.elim {p q r : Prop} (hpq : Or p q) (hpr : p → r) (hqr : q → r) :=
  match hpq with
  | Or.inl hp => hpr hp
  | Or.inr hq => hqr hq

Example of and Or-Elim Proof

Here is an example proof using introduction and elimination.

example (p q : Prop): Or p q → Or q p :=
  λ hpq => Or.elim
    hpq                               -- p ∨ q
    (λ hp => Or.inr hp)               -- p → (q ∨ p)
    (λ hq => Or.inl hq)               -- q → (q ∨ p)

Once again, the elimination rule is just a convenience and the proof could be written with match.

False is Inductive

Finally, we have False, which has no introduction rule, kind of like Empty, except we add the requirement that False is also type of Prop.

inductive False : Prop

From False we get the Not connective, which is just "syntactic sugar".

def Not (p : Prop) : Prop := p → False

Here is an example proof:

example (p q : Prop): (p → q) → (Not q → Not p) :=
  λ hpq hq => λ hp => hq (hpq hp)

False Elimination

To define the elimination rule for false

           Γ ⊢ ⊥
  ⊥-Elim ——————————
           Γ ⊢ p

we take advantage of the fact that False was defined inductively.

def False.elim { p : Prop } (h : False) : p :=
  nomatch h

Here is an example proof that from False you can conclude anything:

example (p q : Prop): And p (Not p) → q :=
  λ h => False.elim (h.right h.left)

By the way, this is another way to prove the HW1 example:

example : False → True :=
  λ h => False.elim h

Notation

The main difference between what we have defined here and Lean is that Lean defines notation like ∨ and ∧. We won't redo that entire infrastructure here. But to give a sense of it, here is how Lean defines infix notation for Or and And and Not notation.

infixr:30 " ∨ "  => Temp.Or
infixr:35 " ∧ "   => Temp.And
notation:max "¬" p:40 => Temp.Not p

The numbers define the precedence of the operations. So v has lower precedence than ∧, which has lower precedence than -.

Now we can write

end Temp -- start using Lean's propositions

example (p q : Prop): (p ∧ (¬p)) → q :=
  λ h => False.elim (h.right h.left)

Examples

You should try to do as many of these as possible. These are borrowed from the Theorem Proving in Lean Book.

variable (p q r : Prop)

example (h : p ∨ q) : q ∨ p := sorry
example : p ∧ q ↔ q ∧ p := sorry
example : p ∨ q ↔ q ∨ p := sorry
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := sorry
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := sorry
example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := sorry
example : (p → (q → r)) ↔ (p ∧ q → r) := sorry
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := sorry
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := sorry
example : ¬p ∨ ¬q → ¬(p ∧ q) := sorry
example : ¬(p ∧ ¬p) := sorry
example : p ∧ ¬q → ¬(p → q) := sorry
example : ¬p → (p → q) := sorry
example : (¬p ∨ q) → (p → q) := sorry
example : p ∨ False ↔ p := sorry
example : p ∧ False ↔ False := sorry
example : (p → q) → (¬q → ¬p) := sorry
example : (p → q) → (¬q → ¬p) := sorry

References

• https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html

• Homotypy Type Theory Book https://homotopytypetheory.org/book/ Chapter 5 covers inductive types

UNDER CONSTRUCTION
Code for this chapter

First Order Logic

Limitations of Propositional Logic

The main thing missing from propositional logic is objects. For example, suppose we wanted reason about statements like:

• Every person who lives in Seattle lives in Washington.
• There exists a person who does not live in Seattle.

These statements would be difficult in propositional logic, although given that there are only a finite number of people in the world we could say things like:

• lives_in_seattle_eric → lives_in_washington_eric
• lives_in_seattle_fred → lives_in_washington_fred
• ...

where we create new propositions for every person and every statement we would like to say about that person. However, what if we wanted to reason about an infinite domain like ℕ and say things like the following?

• every natural number is either odd or even

Since there are an infinite number of natural numbers, we need an infinite number of propositions

• odd_0, even_0, odd_1, even_1, ...

First Order Logic

First order logic (FOL) enriches propositional logic with the following elements:

• Objects: such as numbers, names, people, places, etc.
• Functions: that transform objects into other objects -- See next set of notes
• Predicates: that relate objects to objects
• Quantifiers: ∀ and ∃ that allow us to say:
  • ∀: For all objects ___
  • ∃: There exists an object such that ___
• All the connectives we have encountered so far: ∨, ∧, →, ¬, ...
• Types: Traditional FOL does not have types, but we will use them anyway)

For example, in the following proposition built from these elements:

∀ x ∃ y , f x > y

is read "For all x, there exists a y such that f(x) is greater than y". In this example,

• The objects x and y are presumbly numbers
• The symbol f is a function that maps numbers to numbers
• The symbol > is predicate taking two arguments and return true or false

All of this can be done easily in Lean.

variable (f : Nat → Nat)
#check ∀ x : Nat , ∃ y : Nat , f x > y

Objects

Objects in FOL can come from any agreed upon universe. Since we will be using Lean to work with first order logic, you can just assume that objects are any basic terms: numbers, strings, lists, and so on. FOL does not allow us to quantify over functions and types, only basic objects.

Example: A Finite Universe of People

For example, suppose we wanted to reason about a finite number of people. In Lean we can enumerate them with a new type:

inductive Person where | mary | steve | ed | jolin

open Person

#check ed

Example : Natural Numbers, Strings, Booleans, etc

Lean has a number of built inn types we can use, such as numbers, strings, and Booleans.

#check 1234
#check "uwece"
#check true

Predicates

A predicate is a Prop valued function.

Example: A Predicate on People

A predicate on Person is a function from Person into Prop, such as one which might specify whether the person lives in Seattle:

def InSeattle (x : Person) : Prop := match x with
  | mary  | ed    => True
  | steve | jolin => False

#check InSeattle

example : InSeattle steve ∨ ¬InSeattle steve :=
  Or.inr (λ h => h)

Example: A Predicate on ℕ

Or we might define a predicate inductively on the natural numbers.

def is_zero(n : Nat) : Prop := match n with
  | Nat.zero => True
  | Nat.succ _ => False

#check is_zero

example : ¬is_zero 91 :=  -- is_zero 91 → False
  λ h => h

theorem t : is_zero 0 := True.intro

theorem t1 : True := True.intro

Predicates with Multiple Arguments

We may define predicates to take any number or arguments, including no arguments at all.

-- No argument predicates are just normal propositions
variable (P : Prop)
#check P

-- A one-argument predicate
variable (InWashington : Person → Prop)
#check InWashington steve

-- A two-argument predicate
variable (Age : Person → Nat → Prop)
#check Age jolin 27

Relations

A two-argument predicate is called a relation.

Example: We might define a predicate on pairs of people such as

def on_right (p q : Person) : Prop := match p with
  | mary => q = steve
  | steve => q = ed
  | ed => q = jolin
  | jolin => q = mary

We can define other predicates in terms of existing predicates.

def next_to (p q : Person) := on_right p q ∨ on_right q p

example : next_to mary steve :=
  Or.inl (Eq.refl steve)

Greater Than is a Relation

Relations are usually represented with infix notation, but they are still just predicates. For example, in Lean, the greater-than relation on natural numbers is:

#check @GT.gt Nat
#eval GT.gt 2 3

This doesn't look very nice, so Lean defines notation:

infix:50 " > " => GT.gt

and we can write:

#eval 2 > 3

Similarly, >=, <, <=, != are all relations available in Lean.

Universal Quantification

In FOL, we use the symbol ∀ to denote universal quantification. You can think of univeral quantifiaction like a potentially infinte AND:

∀ x P(x)   ≡    P(x₁) ∧ P(x₂) ∧ P(x₃) ∧ ...

Example: Here's how you say "All people who live in Seattle also live in Washington":

∀ x : Person , InSeattle(x) → InWashington(x)

Example: In Lean, let's say we wanted to prove that every person either lives in Seattle or does not live in Seattle. A proof of this fact has the form of a function that takes an arbtrary person x and returns a proof that that person either lives in Seattle or does not. Thus, we can say:

example : ∀ (x : Person) , (InSeattle x) ∨ ¬(InSeattle x) :=
  λ x => match x with
  | steve => Or.inr (λ h => h)
  | mary => sorry
  | ed => sorry
  | jolin => sorry

∀ is just syntactic sugar for polymorphism. The above FOL statement can be equally well written as:

#check (x : Person) → (InSeattle x) ∨ ¬(InSeattle x)

Which highlights why we can just use a lambda to dispatch a forall.

Forall Introduction and Elimination

The universal quantifer has the introduction rule:

                   Γ ⊢ P
  ∀-intro ————————————————————————
               Γ ⊢ ∀ x : α, P

Where x is not in the free variables of Γ. The rule states that if we can prove P in context Γ assuming x not mentioned elsewhere in Γ, then we can prove ∀ x : α, P.

We also have the elimination rule:

             Γ ⊢ ∀ x , P x
  ∃-elim ————————————————————————
                  P t

where t is any term. This rule states that if we know P x holds for every x, then it must hold for any particular t.

Proving Statements with ∀

The Curry-Howard Isomorphism works for universal quantification too. We could do as we did with proposotional logic and rewrite the FOL rules as type inference. However, here we just say what it means in Lean (which amounts to the same thing).

• ∀-intro: To prove ∀ x , P x we construction a function that takes any x and returns proof of P x. This is an extension of the λ-abstraction rule.

• ∀-elim: Given a proof h of ∀ x , P x (which we recall is a λ-abstractionn) and a particular y of type α, we can prove P y by simply applying h to y. This is an extension of the λ-application rule.

For example, here is a proof that uses both of these rules:

variable (α : Type) (P Q : α → Prop)

example : (∀ x : α, P x ∧ Q x) → ∀ y : α, P y :=
  λ h q => (h q).left

Exists

The ∃ quantifer is like an OR over a lot of propositions:

∃ x , P(x)  ≡   P(x₁) ∨ P(x₂) ∨ ....

and it has similar introduction and elimination rules:

             Γ ⊢ φ[x:=t]                Γ ⊢ ∃ x , φ     Γ, φ ⊢ ψ
  ∃-intro: ———————————————     ∃-elim: ———————————————————————————
             Γ ⊢ ∃ x, φ                        Γ ⊢ ψ

Constructively, the first rule says that if we have a proof of φ with x some term t substituted in for x, then we have a proof of ∃ x, φ.

The second says that if we have a proof of ∃ x, φ and also a proof of ψ assuming φ, then we have a proof of ψ.

Lean's Implementation of Exists

In FOL, ∃ is usally just an abbreviation for as ¬∀¬. However, from a constructive point of view:

knowing that it is not the case that every x satisfies¬p is not the same as having a particular x that satisfies p. (Lean manual)

So in Lean, ∃ is defined inductively and constructively:

namespace temp

inductive Exists {α : Type} (p : α → Prop) : Prop where
  | intro (x : α) (h : p x) : Exists p

end temp

All we need to introduce an existentially quantified statement with predicate P is an element and a proof that P holds for that element.

An example use of the introduction rule is the following. Note the assumption that α has at least one element q is necessary.

example (q : α) : (∀ x , P x) → (∃ x , P x) :=
  λ hp => Exists.intro q (hp q)

Exists Elimination

The ∃-elim rule is defined in Lean as follows:

namespace temp

theorem Exists.elim {α : Type} {P : α → Prop} {b : Prop}
   (h₁ : Exists (λ x => P x)) (h₂ : ∀ (a : α), P a → b) : b :=
  match h₁ with
  | intro a h => h₂ a h

end temp

In this rule

b is an arbitrary proposition h₁ is a proof of ∃ x , p x h₂ is a proof that ∀ a , p a → b

which allow us to conclude b

Exists Elimination Example

For example, in

example (h₁ : ∃ x, P x ∧ Q x) : ∃ x, Q x ∧ P x :=
  Exists.elim h₁
  (λ c h => Exists.intro c (And.intro h.right h.left))

Example Proofs

variable (p: Type → Prop)
variable (r : Prop)

example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
  Iff.intro
  (λ h => Exists.elim h (λ c h => And.intro (Exists.intro c h.left) h.right))
  (λ h => Exists.elim h.left (λ c h1 => Exists.intro c (And.intro h1 h.right)))

example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) :=
  Iff.intro
  (λ h x hp => h (Exists.intro x hp))
  (λ h he => Exists.elim he (λ y hy => h y hy))

example : ∀ (x : Person) , (InSeattle x) ∨ ¬(InSeattle x) :=
  λ x => match x with
    | mary  | ed    => Or.inl trivial
    | steve | jolin => Or.inr (λ h => False.elim h)

example : (∀ x : α, P x ∧ Q x) → ∀ y : α, P y :=
  λ h : ∀ x : α, P x ∧ Q x =>
  λ y : α =>
  (h y).left

example (q : α) : (∀ x , P x) → (∃ x , P x) :=
  λ h => Exists.intro q (h q)

example (h₁ : ∃ x, P x ∧ Q x) : ∃ x, Q x ∧ P x :=
  have h₂ := λ w : α =>                                            -- proof of ∀
             λ hpq : P w ∧ Q w  =>                                 -- proof of →
             (Exists.intro w (And.intro hpq.right hpq.left))
  Exists.elim h₁ h₂

UNDER CONSTRUCTION
Code for this chapter

Tactics

Tactic mode is entered in a proof using the keyword by

variable (p : Type → Prop)

example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) := by
  sorry

The intro Tactic

Introducion applies to implications and forall statements, introducing either a new hypothesis or a new object. It takes the place of λ h₁ h₂ ... => ...

Note also that by using . and indentation, you can visually break up your proof to it is more readable.

example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) := by
  apply Iff.intro
  . intro hnep x
    sorry
  . intro hanp
    sorry

The apply and exact Tactics

The apply tactic applies a function, forall statement, or another theorem. It looks for arguments that match its type signature in the context and automatically uses them if possible.

example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) := by
  apply Iff.intro
  . intro h x hp
    exact h (Exists.intro x hp)
  . intro h hepx
    apply Exists.elim hepx
    intro x hpa
    exact (h x) hpa

example (p : Nat → Prop) (h : ∀ (x : Nat) , p x) : p 14 := by
  apply h

theorem my_thm (q : Prop) : q → q := id

example (q : Nat → Prop) : (∀ x, q x) → ∀ x, q x := by
  apply my_thm

exact is a variant of apply that requires you to fill in the arguments you are using. It essentially pops you out of tactic mode. It is used at the end of proofs to make things more clear and robust to changes in how other tactics in the proof are applied.

example (p : Nat → Prop) (h : ∀ (x : Nat) , p x) : p 14 := by
  exact h 14

The assumption Tactic

This tactic looks through the context to find an assumption that applies, and applies it. It is like apply but where you don't even say what to apply.

example (c : Type) (h : p c) : ∃ x, p x := by
  apply Exists.intro c
  assumption

Structures

Structures in Lean are a way to package data. They are a kind of inductive type, but presented differently. For example,

structure Point where
  x : Int
  y : Int

You can make new points in a variety of ways

def p₁ := Point.mk 1 2
def p₂ : Point := { x := 1, y := 2 }
def p₃ : Point := ⟨ 1,2 ⟩

Packaging and Exists

In Lean, And is a structure (not a simple inductive type, like I originally described).

#print And

example (p : Prop): p → (p ∧ p) :=
  λ hp => ⟨ hp, hp ⟩

This notation also works with inductive types though, as with Exists.

#print Exists

example (p : Type → Prop) (c : Type) : (∀ x, p x) → ∃ x, p x :=
  λ h => ⟨ c, h c ⟩

example : ∃ (p : Point) , p.x = 0 :=  by
  exact ⟨ ⟨ 0, 0 ⟩, rfl ⟩

Tactics Produce Low Level Proofs

theorem t (p : Type → Prop) (c : Type) : (∀ x, p x) → ∃ x, p x := by
  intro h
  exact ⟨ c, h c ⟩

#print t

Pattern Matching

You can match constructors with intro to more easily break up expressions.

example (p q : Prop) : p ∧ q → q := by
  intro ⟨ _, hq ⟩
  exact hq

example : (∃ x , ¬p x) → ¬ ∀ x, p x := by
  intro ⟨ x, hnp ⟩ hnap
  exact hnp (hnap x)

example (P Q : Type → Prop): (∃ x, P x ∧ Q x) → ∃ x, Q x ∧ P x := by
  intro ⟨ x, ⟨ hp, hq ⟩ ⟩
  exact ⟨ x, ⟨ hq, hp ⟩ ⟩

Getting Help with Apply?

You can ask Lean to try to find someting to apply with apply?

example : (∃ x , ¬p x) → ¬ ∀ x, p x := by
  intro ⟨ x, hnp ⟩ hnap
  apply?

It doesn't always work though.

FOL Examples Revisited

Now that we can use tactics, our First Order Logic Proofs can be made to look a little cleaner, although one might argue the use of angled brackets is harder to read.

variable (p: Type → Prop)
variable (r : Prop)

theorem asd : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) := by
  apply Iff.intro
  . intro h x hp
    exact h (Exists.intro x hp)
  . intro hp ⟨ x, hnp ⟩
    exact hp x hnp

example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r := by
  apply Iff.intro
  . intro ⟨ x, ⟨ hx, hr ⟩ ⟩
    exact ⟨ ⟨ x, hx ⟩ , hr ⟩
  . intro ⟨ ⟨ x, hx ⟩ , hr ⟩
    exact ⟨ x, ⟨ hx, hr ⟩ ⟩

example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) := by
  apply Iff.intro
  . intro h x hp
    exact h ⟨ x, hp ⟩
  . intro h ⟨ x, hp ⟩
    exact h x hp

The have and let Tactics

You can use have to record intermediate results

example (p q : Prop) : p ∧ q → p ∨ q := by
  intro ⟨ h1, h2 ⟩
  have hp : p := h1
  exact Or.inl hp

If you need an intermediate value, you should use let.

example : ∃ n , n > 0 := by
  let m := 1
  exact ⟨ m, Nat.one_pos ⟩

Cases

The cases tactic wraps around Or.elim to make proofs easier to read.

example (p q : Prop) : (p ∨ q) → q ∨ p  := by
  intro h
  cases h with
  | inl hp => exact Or.inr hp
  | inr hq => exact Or.symm (Or.inr hq)

-- Cases doesn't always buy you much. You can just apply Or.elim.
example (p q : Prop) : (p ∨ q) → q ∨ p  := by
  intro h
  apply Or.elim h
  . intro hp
    exact Or.symm h
  . intro hq
    exact Or.symm h

Cases Works With any Inductive Ttype

Here's are some somewhat longwinded ways to prove some simple results

variable (P Q : Type → Prop)

example : (∃ x, P x ∧ Q x) → ∃ x, Q x ∧ P x := by
  intro h
  cases h with
  | intro x h => exact ⟨ x, And.symm h ⟩

example (p q : Prop) : (p ∧ q) → (p ∨ q) :=  by
  intro h
  cases h with
  | intro hp hq => exact Or.inl hp

The by_cases Tactic

The cases tactic is not to be confused with the by_cases tactic, which uses classical reasoning.

example (p : Prop): p ∨ ¬p := by
  by_cases h : p
  . exact Classical.em p -- assuming h : p
  . exact Classical.em p -- assuming h : ¬p

The induction Tactic

Proof by induction works for all inductive types. It is similar to using cases, but it adds an inductive hypothesis where needed.

As an example, consider the natural numbers and suppose P : Nat → Prop is a property. To prove P with induction, you do :

• BASE CASE: P(0)
• INDUCTIVE STEP: ∀ n, P(n) → P(n+1)

def E (n : Nat) : Prop := match n with
  | Nat.zero => True
  | Nat.succ x => ¬E x

example : ∀ n : Nat, E n ∨ E n.succ := by
  intro n
  induction n with
  | zero => exact Or.inl trivial
  | succ k ih =>
    apply Or.elim ih
    . intro h1
      exact Or.inr (by exact fun a ↦ a h1)
    . intro h3
      exact Or.inl h3

Tactic Documentation

There are a lot of tactics:

https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md

UNDER CONSTRUCTION
Code for this chapter

Objects, Functions and Equality

In this chapter we extend the first order logic discussed in the last chapter to deal with functions of objects in our universe. On one of the critical components is a notion of equality between objects. Astonishingly, Lean's equality is not a built in type, but is defined in the standard library. Once we have equality, we can start working with statements about functions and their relationships in earnest.

Equality is a Binary Relation Defined Inductively

universe u

inductive MyEq {α : Sort u} : α → α → Prop where
  | refl a : MyEq a a

#check MyEq 1 2

example : MyEq 1 1 :=
  MyEq.refl 1

We can define some notation

infix:50 " ~ "  => MyEq

#check 1 ~ 1

Refl is Powerful

In Lean, terms that are beta-reducable to each other are considered definitionally equal. You can show a lot of equalities automatically

example : 1 ~ 1 :=
  MyEq.refl 1

example : 2 ~ (1+1) := by
  apply MyEq.refl

example : 9 ~ (3*(2+1)) := by
  apply MyEq.refl

Substitution

Substition is the second most critical property of the equality. It allows us to conclude, for example, that if x = y then p x is equal to p y.

theorem MyEq.subst {α : Sort u} {P : α → Prop} {a b : α}
                   (h₁ : a ~ b) (h₂ : P a) : P b := by
  cases h₁ with
  | refl => exact h₂

You can use this theorem to show the standard properties we know and love about equality.

theorem my_symmetry (a b : Type): a ~ b → b ~ a := by
  intro h
  apply MyEq.subst h
  exact MyEq.refl a

theorem my_transitivity (a b c : Type) : a ~ b → b ~ c → a ~ c := by
  intro hab hbc
  exact MyEq.subst hbc hab

theorem my_congr_arg (a b : Type) (f : Type → Type) : a ~ b → f a ~ f b := by
  intro hab
  apply MyEq.subst hab
  exact MyEq.refl (f a)

Lean's Equality

Lean's equality relation is called Eq and its notation is =, as we have been using. Lean also defines rfl to be Eq.refl _

#print rfl
example : 9 = 3*(2+1) := Eq.refl 9
example : 9 = 3*(2+1) := rfl

Lean provides a long list of theorems about equality, such as

#check Eq.symm
#check Eq.subst
#check Eq.substr
#check Eq.trans
#check Eq.to_iff
#check Eq.mp
#check Eq.mpr

#check congrArg
#check congrFun
#check congr

Tactics for Equality

rw[h]: Rewrites the current goal using the equality h.

theorem t1 (a b : Nat) : a = b → a + 1 = b + 1 := by
  intro hab
  rw[hab]

#print t1

To use an equality backwards, use ← (written \left)

theorem t2 (a b c : Nat) : a = b ∧ a = c → b + 1 = c + 1 := by
  intro ⟨ h1, h2 ⟩
  rw[←h1, ←h2]

#print t2

You can also rewrite assumptions using at.

example (a b c : Nat) : a = b ∧ a = c → b + 1 = c + 1 := by
  intro ⟨ h1, h2 ⟩
  rw[h1] at h2
  rw[h2]

The Simplifier

The simplifier uses equations and lemmas to simplify expressions

theorem t3 (a b : Nat) : a = b → a + 1 = b + 1 := by
  simp

#print t3

Sometimes you have to tell the simplifer what equations to use.

theorem t4 (a b c d e : Nat)
 (h1 : a = b)
 (h2 : b = c + 1)
 (h3 : c = d)
 (h4 : e = 1 + d)
 : a = e := by
   simp only[h1,h2,h3,h4,Nat.add_comm]


#check Nat.add_comm

#print t4

The linarith Tactic

By importing Mathlib.Tactic.Linarith (see top of this file), you get an even more powerful simplifier.

example (a b c d e : Nat)
 (h1 : a = b)
 (h2 : b = c + 1)
 (h3 : c = d)
 (h4 : e = 1 + d)
 : a = e := by linarith

example (x y z : ℚ)
 (h1 : 2*x - y + 3*z = 9)
 (h2 : x - 3*y - 2*z = 0)
 (h3 : 3*x + 2*y -z = -1)
 : x = 1 ∧ y = -1 ∧ z = 2 := by
 apply And.intro
 . linarith
 . apply And.intro
   . linarith
   . linarith

Example : Induction on Nat

As an example the brings many of these ideas together, consider the sum of the first n natural numbers, which is n(n+1)/2. A proof by induction would be:

• BASE CASE: 0 = 0*1/2
• NDUCTIVE STEP: ∀ k, Sum k = k(k+1)/2 → Sum (k+1) = (k+1)(k+2)/2

We can do this in lean with the induction tactic.

def S (n : Nat) : Nat := match n with
  | Nat.zero => 0
  | Nat.succ x => n + S x

#eval S 3

example : ∀ n, 2 * S n = n*(n+1) := by
  intro n
  induction n with
  | zero => simp[S]
  | succ k ih =>
    simp[S,ih]
    linarith

Inequality

Every inductive type comes with a theorem called noConfusion that states that different constructors give different objects.

inductive Person where | mary | steve | ed | jolin
open Person

example : mary ≠ steve := by
  intro h
  exact noConfusion h

inductive MyNat where
  | zero : MyNat
  | succ : MyNat → MyNat

example : MyNat.zero ≠ MyNat.zero.succ := by
  intro h
  exact MyNat.noConfusion h

Continuing the above example, suppose we want to specify who is on who's right side.

def on_right (p : Person) := match p with
  | mary => steve
  | steve => ed
  | ed => jolin
  | jolin => mary

def next_to (p q : Person) := on_right p = q ∨ on_right q = p

example : ¬next_to mary ed := by
  intro h
  cases h with
  | inl hme => exact noConfusion hme
  | inr hem => exact noConfusion hem

example : ∀ p , p ≠ on_right p := by
  sorry

Note: The trivial tactic actually figures out when to apply noConfusion

theorem t10 : ed ≠ steve := by
  intro h
  trivial

#print t10

#help tactic trivial

UNDER CONSTRUCTION
Code for this chapter

Relations

As described previously, a relation is a propositionally valued predicate of two arguments. Generally speaking, that is about all you can say about predicates. However, when we restrict our attention to predicates having specific properties, we can say much more.

In this chapter we will build up some of the theory behind relations and give several examples of each type of relation.

Note that Mathlib has many definitions involving relations. In particular, Rel is the general type of relations. We will not use that infrastructure in this chapter, as our goal is to build up the theory from scratch for the purposes of understanding it better, which in turn should make Mathlib more comprehensible.

Definitions

First, we define a general type for relations:

abbrev Relation (A : Type u) (B : Type v) := A → B → Prop

Types of Relation

abbrev Refl {A : Type u} (r : Relation A A) {x : A} := r x x
abbrev Symm {A : Type u} (r : Relation A A) {x y : A} := r x y → r y x
abbrev AntiSym {A : Type u} (r : Relation A A) {x y : A}:= r x y → r y x → x = y
abbrev Trans {A : Type u} (r : Relation A A) {x y z : A} := r x y → r y z → r x z

UNDER CONSTRUCTION
Code for this chapter

TODO

UNDER CONSTRUCTION
Code for this chapter

The Natural Numbers and Hierarchies

In the chapter on inductive types, we encountered the natural numbers. So to some extent, we are done defining them. But the natural numbers have many, many properties that are incredibly useful over a huge range of mathematics. In fact, defining them is the easy part. Understanding their structure is much more interesting.

In this chapter, we will define the natural numbers and develop some of their algebraic and ordering structure. Along the way, we show how Lean's hierarchy system works. Hierarchies are useful for proving general theorems about algebreic structures that can be reused in specific instances. For example, consider associative property: (x+y)+z = x+(y+z). This property holds for natural numbers, integers, rationals, reals, matrices, polynomials, and many more objects. And it leads to many auxilliary theorems, such as (w+x)+(y+z) = (w+(x+y))+z and so on. Rather than proving all all these theorems for a new type, we just prove a few basic theorems, like associativity and a few others, and then do some book-keeping to connect our new type to the hige list of theorems that hold for similar objects.

The Inductive Definition of the Natural Numbers

As we've seen, the Natural Numbers are defined inductively. We open the a temporary namespace, Temp to avoid naming conflicts with Lean's standard Nat type. So, in the below, every time you see Nat, it means Temp.Nat.

#check Nat.succ_add

theorem succ_add_eq_add_succ' (a b : Nat) : Nat.succ a + b = a + Nat.succ b := by
  apply Nat.succ_add

example (j k: Nat) : j.succ + k = j + k.succ := by exact Nat.succ_add_eq_add_succ j k

#check Nat.succ_add_eq_add_succ

namespace Temp

-- Definition
inductive Nat where
  | zero : Nat
  | succ : Nat → Nat

open Nat

Using this definition, it is straightfoward to define addition and multiplication.

def Nat.add (n m: Nat) : Nat := match m with
  | zero => n
  | succ k => succ (add n k)

-- def Nat.add (n m: Nat) : Nat := match n,m with
--   | a, Nat.zero   => a
--   | a, Nat.succ b => Nat.succ (Nat.add n m)

def Nat.mul (n m: Nat) : Nat := match n with
  | zero => zero
  | succ k => add (mul k m) m     -- (k+1)*m = k*m+m

First Use of Lean's Classes

If you have a type for which things like zero, one, addition, and multiplication are defined, it would be nice to use the notation 0, 1, + and *. Although you could use Lean's syntax and infix operators to define such notation, it is better practice to instantiate the classes that group all types that have zero, one, addition and multiplication. To do this, we use the instance keyword and various classes, such as Zero, One, Add and Mul defined in Lean's standard library or in Mathlib.

Here are several examples:

instance inst_zero : Zero Nat := ⟨ zero ⟩         -- Zero
instance inst_one : One Nat := ⟨ succ zero ⟩      -- One
instance inst_add : Add Nat := ⟨ add ⟩            -- Addition
instance inst_hadd : HAdd Nat Nat Nat := ⟨ add ⟩  -- Extra hints with addition
instance inst_mul : Mul Nat := ⟨ mul ⟩            -- Multiplication

Now we can do a few examples using the notation. Note that in these examples, we have to give Lean some hints that we are working with our Temp.Nat type. Otherwise it assumes numbers like 0 and 1 refer to the build in Nat type. We do this by coercing one of the terms in our expressions, as in (1:Nat).

example : (1:Nat) + 0 = 1 := rfl
example : (1:Nat) * 0 = 0 := rfl

Properties of Addition and Multiplication

With this notation, we can cleanly express some of the basic properties of the natural numbers and start working on proofs. These theorems may seem very basic, but together they form the basis of automated proof checking with the natural numbers, connecting results about, for example, cryptography, with the type-theoretic foundations of mathematics.

Most of these theorems can be found in Lean's standard library. But it is interesting to reproduce them here to understand how the theory is constructed.

#check AddSemiconjBy.eq
#check congrArg

theorem succ_add (n m : Nat) : (succ n) + m = succ (n + m) := by
  induction m with
  | zero => rfl
  | succ k ih => apply congrArg succ ih

theorem succ_add_eq_add_succ (a b : Nat) : succ a + b = a + succ b := by
  apply succ_add

theorem add_zero_zero_add {x: Nat} : 0+x=x+0 := by
  induction x with
    | zero => rfl
    | succ j ih =>
      apply congrArg succ ih

theorem zero_add {x : Nat} : 0+x = x := by
  induction x with
    | zero => rfl
    | succ j ih =>
      apply congrArg succ ih

theorem add_comm (x y : Nat) : x+y = y+x := by
  induction x with
  | zero => exact add_zero_zero_add
  | succ k ih =>
    have : y + k.succ = (y + k).succ := rfl
    rw[this,←ih]
    have : k + y.succ = (k+y).succ := rfl
    rw[←this]
    exact succ_add_eq_add_succ k y

theorem add_zero (x : Nat) : x+0 = x := by
  rw[add_comm,zero_add]

theorem succ_add_one (x : Nat) : x.succ = x + 1 := by
  induction x with
  | zero => rfl
  | succ k ih =>
    conv => lhs; rw[ih]
    rfl

theorem add_assoc (x y z : Nat) : x+y+z = (x+y)+z := sorry

Ordering Properties of Nat

def Nat.leb (x y : Nat) : Bool := match x,y with
  | zero,zero => true
  | succ _,zero => false
  | zero,succ _ => true
  | succ k, succ j => leb k j

def Nat.le (x y : Nat) : Prop := leb x y = true

instance inst_dec_le : DecidableRel le := by
  intro x y
  match x with
  | zero =>
    match y with
    | zero => exact isTrue rfl
    | succ k => exact isTrue rfl
  | succ k =>
    match y with
    | zero =>
      unfold le
      exact isFalse Bool.false_ne_true
    | succ j  =>
      unfold le
      exact (k.succ.leb j.succ).decEq true

def Nat.lt (x y: Nat) : Prop := le x y ∧ x ≠ y

instance inst_le : LE Nat  := ⟨ le ⟩

instance inst_lt : LT Nat  := ⟨ lt ⟩

#eval le (1:Nat) 0

def Nat.min (x y: Nat) : Nat := if le x y then x else y

instance inst_min : Min Nat  := ⟨ min ⟩

instance inst_max : Max Nat  := ⟨ sorry ⟩

instance inst_ord : Ord Nat  := ⟨ sorry ⟩

instance inst_preo : Preorder Nat  := ⟨ sorry, sorry, sorry ⟩

instance inst_po : PartialOrder Nat  := ⟨ sorry ⟩

instance inst_lo : LinearOrder Nat := ⟨
  sorry,
  by exact inst_dec_le,
  sorry,
  sorry,
  sorry,
  sorry,
  sorry ⟩

UNDER CONSTRUCTION
Code for this chapter

UNDER CONSTRUCTION
Code for this chapter

Integers via Quotients

Now that we have defined the natural numbers Nat, the next obvious step is to define the integers Int, which included positive _and_negative whole numbers. This can be done in several ways. For example, the Lean 4 standard library defines integers inductively saying that (a) any natural number is an integer, and (b) the negative successor of an integer is an integer.

Here, mainly to synergystically illustrate the use of quotients, we take a different approach, which is standard in foundational mathematics, although perhaps not as idiomatically type theoretic. We define pairs of natural numbers (p,q) and use the convention that if p>q then (p,q) represents the positive number p-q. Otherwise, it represents the non-positive number q-p.

This construction allows for multiple representatives of the same number. Therefore, we define an equivalence ≈ on pairs. We would like to write (p,q) ≈ (r,s) if and only if p-q=r-s, but since we are in the process of defining the integers, we do not yet have a notion of negative numbers. Some rearrangement leads to

(p,q) ≈ (r,s)  ↔   p+s=q+r

instead.

With this equivalence in place, we define an integer to be the equivalence class corresponding to a given difference. For example,

-2 ≡ { (0,2), (1,3), (2,4), ... }

Although we could define -2 to be the set of such pairs, Lean has a much more powerful tool for such constructions: the quotient. Taking the quotient of the set of pairs with respect to the equivalence relation we have defined allows us to use definitional equality on equivalence classes of pairs. This allows us, for example, to substitute an integer for an equivalent one in an algebreic expression.

UNDER CONSTRUCTION
Code for this chapter

From Pairs to Integers

As usual when defining a type with the same name as something in the standard library or in Mathlib, we open a namespace to avoid naming conflicts. The Int type we define in this section has the fully qualified name LeanBook.Int, and is a totally different type than Lean's Int type.

namespace LeanBook

Pairs of Natural Numbers

We first define pairs of natural numbers, recording the components of the pair in a simple structure. Then we define the notion of equivalence that will form the basis of the definition of an integer.

@[ext]
structure Pair where
  p : Nat
  q : Nat

def eq (x y: Pair) : Prop := x.p + y.q = x.q + y.p

Here are a few test cases.

example : eq ⟨1,2⟩ ⟨2,3⟩ := rfl
example : eq ⟨3,2⟩ ⟨20,19⟩ := rfl
example : ¬eq ⟨3,2⟩ ⟨20,23⟩ := by intro h; simp_all[eq]

Equivalence Relations

An equivalence relation ≈ is a relation that is

• reflexive: x ≈ x for all x
• symmetric: x ≈ y implies y ≈ x for all x and y
• transitive: x ≈ y and y ≈ z implies x ≈ z for all x, y and z

The relation eq defined above is such an equivalence relation. But we have to prove it. This is pretty easy, since it is just some basic arithmetic.

theorem eq_refl (u : Pair) : eq u u := by
  simp[eq]
  linarith

theorem eq_symm {v w: Pair} : eq v w → eq w v := by
  intro h
  simp_all[eq]
  linarith

theorem eq_trans {u v w: Pair} : eq u v → eq v w → eq u w := by
  intro h1 h2
  simp_all[eq]
  linarith

With these properties in hand, we can register an instance of Equivalence, a Lean 4 standard library class that stores the properties of the equivalence relation in one object, and enables us to easily use any theorems requiring our eq relation to have them.

instance eq_equiv : Equivalence eq := ⟨ eq_refl, eq_symm, eq_trans ⟩

We can also register eq with the HasEquiv class, which allows us to use the `≈' notation.

@[simp]
instance pre_int_has_equiv : HasEquiv Pair := ⟨ eq ⟩

Here is an example using the new notation.

def u : Pair := ⟨ 1,2 ⟩
def v : Pair := ⟨ 12,13 ⟩
#check u ≈ v

Finally, we register Pair and eq as a Setoid, which is a set and an equivalence relation on the set. It is needed for the definition of the quotient space later.

instance pre_int_setoid : Setoid Pair :=
  ⟨ eq, eq_equiv ⟩

This exact process should be followed whenever defining a new equivalence class in Lean.

Quotients

The equivalence class of x is defined to be the set of all pairs y such that x≈y. The set of all equivalence classes is called the quotient space, which we can form using Lean's Quotient:

def Int := Quotient pre_int_setoid

We can then construct elements of Int using Quotient.mk.

def mk (w : Pair) : Int := Quotient.mk pre_int_setoid w

#check mk ⟨ 1, 2 ⟩  -- 1
#check mk ⟨ 2, 1 ⟩  -- -1

A key aspect of the quotient space is that equality is extended to elements of the quotient space. Thus, we can write:

#check mk ⟨ 1, 2 ⟩ = mk ⟨ 2, 3 ⟩

instead of using ≈. As a result, we can us all the properties of equality we have become used to with basic types, such as definitional equality and substution.

We may now register a few more classes. The first defines zero, the second defines one, and the third defines a coercion from natural numbers to (non-negative) integers.

instance int_zero : Zero Int := ⟨ mk ⟨ 0,0 ⟩ ⟩
instance int_one : One Int := ⟨ mk ⟨ 1,0 ⟩ ⟩
instance int_of_nat {n: ℕ} :OfNat Int n := ⟨ mk ⟨ n, 0 ⟩ ⟩

#check (0:Int)
#check (1:Int)
#check (123:Int)

You may also encounter the notation ⟦⬝⟧ for equivalence classes. Since the notation does not know which equivalence relation you might be talking about, it is only useful in a context where the Type can be inferred.

-- Does not work:
#check_failure ⟦⟨1,2⟩⟧

-- Ok:
def my_int : Int := ⟦⟨1,2⟩⟧

Using Ints in Proofs

To prove theorems about negation we need some fundamental tools for proving properties of quotients:

• Quotient.exists_rep, which says ∃ a, ⟦a⟧ = q. This operator allows you to assert the existence of a representative of an equivalence class. Then, if you are trying to prove a result about the equivalence class, it amounts to proving it about the representative.

• Quotient.sound, which says a ≈ b → ⟦a⟧ = ⟦b⟧. Applying this operator allows you to replace a goal involving proving two equivalence classes are equal, with one showing that representatives of the respective equivalence classes are equivalent under the associated Setoid relation. In other words, we unlift the equality back to the underlying space.

Using these two operations, we do a simple proof in which, for illustrative purposes, we write out each step. It is instructive to open this proof in VS Code and examine the proof state before and after each step.

example : ∀ x : Int, x = x := by
  intro x
  obtain ⟨ ⟨ a, b ⟩, hd ⟩ := Quotient.exists_rep x
  rewrite[←hd]
  apply Quotient.sound
  simp only [pre_int_setoid,HasEquiv.Equiv,eq]
  exact Nat.add_comm a b

The proof can be made much simpler in this example, because definitional equality is all you need in this case.

example : ∀ x : Int, x = x := by
  intro x
  rfl

However, the use of Quotient.exists_rep and Quotient.sound in the more complicated proofs is often needed, and the above pattern will be applicable in many situations.

UNDER CONSTRUCTION
Code for this chapter

Lifting Operators

In this section we show how to lift an operation, such as negation or addition, from Pair to Int, and more generally from any type to a quotient on that type.

Lifting Negation

First, we define the meaning of negation for pairs, which is simply to switch the order of the pair's elements.

def pre_negate (x : Pair) : Pair := ⟨ x.q, x.p ⟩

We would like to lift the definition of negation to our new Int type. This means defining negation of an entire equivalence class, which would only work if our pre_negate function has the same result on all elements of an equivalence class, which fortunately it does! To capture this notion we define a respects theorem.

theorem pre_negate_respects (x y : Pair) :
  x ≈ y → mk (pre_negate x) = mk (pre_negate y) := by
  intro h
  simp_all[pre_int_setoid,eq]
  apply Quot.sound
  simp[pre_int_setoid,eq,pre_negate,h]

With this theorem, we may use Lean's Quotient.lift to define negate on Int.

def pre_negate' (x : Pair) : Int := mk (pre_negate x)

def negate (x : Int) : Int := Quotient.lift pre_negate' pre_negate_respects x

We may register our negation function wit the Neg class, allowing us to use the - notation for it, and to use any general theorems proved in Mathlib for types with negation.

instance int_negate : Neg Int := ⟨ negate ⟩

Now we can use negative integers.

#check -mk ⟨2,1⟩
#check -(1:Int)

Here is a simple theorem to test whether all of this is working.

theorem negate_negate { x : Int } : -(-x) = x := by
  let ⟨ u, hu ⟩ := Quotient.exists_rep x
  rw[←hu]
  apply Quot.sound
  simp[pre_int_setoid,pre_negate,eq]
  linarith

Lifing Addition

Just as we lifted negation, we can also define and lift addition. For pairs, addition is just componentwise addition.

def pre_add (x y : Pair) : Pair := ⟨ x.p + y.p, x.q + y.q ⟩

To do the lift, we need another respects theorey. This time, the theorem assumes multiple equivalences.

theorem pre_add_respects (w x y z : Pair)
  : w ≈ y → x ≈ z → mk (pre_add w x) = mk (pre_add y z) := by
  intro h1 h2
  apply Quot.sound
  simp_all[pre_int_setoid,eq,pre_add]
  linarith

With this theorem we can define addition on integers.

def pre_add' (x y : Pair) : Int := mk (pre_add x y)

def add (x y : Int) : Int := Quotient.lift₂ pre_add' pre_add_respects x y

And while we are at it, we can register addition with Mathlib's Add class so we can use +.

instance int_add : Add Int := ⟨ add ⟩

Here is an example. It is remarkable to see that the entire edifice we have built can interact so easily with rfl.

example : (1:Int) + 17 = 18 := rfl

A slightly more complicated example with addition and negation requires Quotient.sound since we have not yet lifted any theorems from Pair to Int.

example : (1:Int) + (-2) = -1 := by
  apply Quotient.sound
  rfl

UNDER CONSTRUCTION
Code for this chapter

Lifting Properties

In this section we show how to lift theorems from a type to a quotient on that type. Continuing with the Int example, we lift all the properties required to show that Int is an additive group. Then, using Lean's hierarchies, we formally instantiate Int as an additive group using these theorems and show how we can then use all of Mathlib's group infrastructure on our new Int type.

Lifting Theorems

There is no direct operator for lifting theorems, but doing so is straightforward. One typically defines a theorem on the base space and then uses it to prove the corresponding theorem on the quotient space. For example, here are several theorems defined on pairs.

theorem pre_add_com {x y: Pair} : eq (pre_add x y) (pre_add y x) := by
  simp[eq,pre_add]
  linarith

theorem pre_add_assoc {x y z: Pair}
  : eq (pre_add (pre_add x y) z) (pre_add x (pre_add y z))  := by
  simp[eq,pre_add]
  linarith

theorem pre_zero_add (x : Pair) : eq (pre_add ⟨0,0⟩ x) x := by
  simp[eq,pre_add]
  linarith

theorem pre_inv_add_cancel (x : Pair) : eq (pre_add (pre_negate x) x) ⟨0,0⟩ := by
  simp[eq,pre_negate,pre_add]
  linarith

To lift these theorems to Int, we apply essentially the same pattern to each. We assert the existence of Pairs that represent each of the intgers in the target theorem. We substitute those in for the integers. We use Quot.sound to restate the goal in terms of pairs. Finally we use the underlying theorem. Here are several examples:

theorem add_comm (x y: Int) : x+y = y+x := by
  have ⟨ u, hu ⟩ := Quotient.exists_rep x
  have ⟨ v, hv ⟩ := Quotient.exists_rep y
  rw[←hu,←hv]
  apply Quot.sound
  apply pre_add_com

theorem add_assoc (x y z: Int) : x+y+z = x+(y+z) := by
  have ⟨ u, hu ⟩ := Quotient.exists_rep x
  have ⟨ v, hv ⟩ := Quotient.exists_rep y
  have ⟨ w, hw ⟩ := Quotient.exists_rep z
  rw[←hu,←hv,←hw]
  apply Quot.sound
  apply pre_add_assoc

theorem zero_add (x : Int) : 0 + x = x := by
  have ⟨ u, hu ⟩ := Quotient.exists_rep x
  rw[←hu]
  apply Quot.sound
  apply pre_zero_add

theorem inv_add_cancel (x : Int) : -x + x = 0 := by
  have ⟨ u, hu ⟩ := Quotient.exists_rep x
  rw[←hu]
  apply Quot.sound
  apply pre_inv_add_cancel

Instantiating the Additive Group Structure on Int

The theorems above were chosen so that we could instantiate a everything we need to show that Int forms an additive, commutative group.

instance int_add_comm_magma : AddCommMagma Int := ⟨ add_comm ⟩

instance int_add_semi : AddSemigroup Int := ⟨ add_assoc ⟩

instance int_add_comm_semi : AddCommSemigroup Int := ⟨ add_comm ⟩

instance int_group : AddGroup Int :=
  AddGroup.ofLeftAxioms add_assoc zero_add inv_add_cancel

Now we get all the theorems and tactics about additive groups from Mathlib to apply to our Int type! For example,

example (x: Int) : x-x = 0 := by
  group

example (x y : Int) : x + y - y = x := by
  exact add_sub_cancel_right x y

example (x y z : Int) : x+y+z = x+z+y := by
  calc x+y+z
  _ = x+(y+z) := by rw[add_assoc]
  _ = x+(z+y) := by rw[add_comm y z]
  _ = x+z+y   := by rw[add_assoc]

Exercises

References

The construction here is defined in a number of Algebra textbooks. For an early example, see the Nicolas Bourbaki collective's book Algebra Part I, 1943. The English translation of that book from 1974 has the relevant material on page 20.

UNDER CONSTRUCTION
Code for this chapter

The Rational Numbers

The (pre) rational numbers are just pairs of an Int and a Nat. But we also have to keep track of whether the denomenator is non-zero. We do that be including in the structure definion the rationals a proof of that property. Thus, every rational number in Lean "knows" it is well-formed.

namespace LeanBook

structure PreRat where
  intro ::
  num : Int
  den : Nat
  dnz : den ≠ 0 := by decide -- works with constants

@[simp]
def eq (x y :PreRat) :=
  x.num * y.den = y.num * x.den

Pre-rational admits many representations of the same number.

def p12 : PreRat := PreRat.intro 1 2
def p48 : PreRat := PreRat.intro 4 8

example : eq p12 p48 := rfl

Of course, Lean would define notation for all of this.

Defining the Rationals

One way to define the Rationals from the Pre-Rationals is to form the set of all elements equivalent to a given Pre-Rational. Then that set is the rational.

For this to work, we have to show that the equality relation is an equivalence relation. This means it needs to be:

• reflexive: eq x x
• symmetric: eq x y → eq y x
• transitive: eq x y ∧ eq y z → eq x z

We define the equivalence class of x to be

[x] = { y | x = y }

In this case, it is the set of all rationals that reduce to the same number.

The following are equivalent statements

eq x y [x] = [y] [x] ∩ [y] = ∅

Equality is Reflexive and Symmetric

theorem eq_refl {x : PreRat} : eq x x := by
  rfl

theorem eq_symm {x y : PreRat} : eq x y → eq y x := by
  intro h
  simp[eq]
  rw[eq] at h
  apply Eq.symm
  exact h

Transitivity is More Challenging.

We want to show

x = y and y = z → x = z

Or

p m m a p a ——— = ——— and ——— = ——— → ——— = ——— q n q n q b

But we can't use fractions.

To show that x = z, which is equivalent to pb = aq.

We have

pbn = pnb = mqb = qmb = qan = aqn

Thus pb = aq since n ≠ 0

Source: https://math.stackexchange.com/questions/1316069/how-do-i-show-that-the-equivalence-relation-defining-the-rational-numbers-is-tra

Proof of Transitivity

theorem eq_trans {x y z : PreRat}
  : eq x y → eq y z → eq x z := by

  intro h1 h2
  let ⟨ p, q, _ ⟩   := x
  let ⟨ m, n, nnz ⟩ := y
  let ⟨ a, b, _ ⟩   := z

  have h : p * b * n = a * q * n := by
    calc p * b * n
    _  = p * ( b * n ) := by rw[Int.mul_assoc]
    _  = p * ( n * b ) := by simp[Int.mul_comm]
    _  = p * n * b     := by rw[Int.mul_assoc]
    _  = m * q * b     := by rw[h1]
    _  = q * m * b     := by simp[Int.mul_comm]
    _  = q * (m * b)   := by simp[Int.mul_assoc]
    _  = q * (a * n)   := by rw[h2]
    _  = q * a * n     := by simp[Int.mul_assoc]
    _  = a * q * n     := by simp[Int.mul_comm]

  simp at h
  apply Or.elim h
  . exact id
  . intro h
    exact False.elim (nnz h)

Building the Rationals

inductive Rat where
  | of_pre_rat : PreRat → Rat

open Rat

def P12 := of_pre_rat p12
def P48 := of_pre_rat p48

Lifting Equality to the Rationals

@[simp]
def LiftRel (r : PreRat → PreRat → Prop) (x y : Rat) : Prop :=
  match x, y with
  | of_pre_rat a, of_pre_rat b => r a b

@[simp]
def req := LiftRel eq

example : req P12 P48 := by
  simp[P12,P48,p12,p48]

Lifting Funtions

@[simp]
def pre_negate (x : PreRat) : PreRat := ⟨ -x.num, x.den, x.dnz ⟩

def Respects (f : PreRat → PreRat) := ∀ x y : PreRat, eq x y → eq (f x) (f y)

theorem negate_respects : Respects pre_negate := by
  intro h
  simp_all[pre_negate,eq]

@[simp]
def LiftFun (f : PreRat → PreRat) (x : Rat) : Rat := match x with
  | of_pre_rat a => of_pre_rat (f a)

@[simp]
def negate := LiftFun pre_negate

example : negate (negate P12) = P12 := by
  simp[P12]

UNDER CONSTRUCTION
Code for this chapter

Real Numbers

Having built ℕ inductively, ℤ from ℕ, and ℚ from ℕ and ℤ, we now turn to the real numbers ℝ. The key distinction between the ℚ and ℝ is that ℝ has the least upper bound property: every non-empty set of reals that is bounded from above has a least upper bound. The rationals ℚ do not have this property. For example, the set

{ q ∈ ℚ | q² < 2 }

has no least upper bound in ℚ, although in ℝ the least upper bound is √2 (for a Lean proof that the square root of 2 is no rational, see Chapter 5 of MIL.)

The usual way to construct ℝ, and the one taken by Mathlib, is to define Cauchy Sequences over ℚ that converge to irrational values. For example, the sequence

  4/1
  4/1 - 4/3
  4/1 - 4/3 + 4/5
  4/1 - 4/3 + 4/5 - 4/7
  4/1 - 4/3 + 4/5 - 4/7 + 4/9

Converges to π.

In this chapter, mainly as an exercise in formalization, we instead construct ℝ from Dedekind Cuts in which every real number is equated to the set of rational numbers less than it. We roughly follow the decription of this approach presented in Rudin's book Principles of Mathematical Analysis (which also, by the way, describes the Cauchy Sequence approach.)

Axioms of the Reals

To show that a set R is equivalent to the real numbers, we define the following relations and operations:

• Ordering relations: <, ≤, > and ≥
• Addition and subtraction: +, -
• Multiplication: *
• Division: /

and we require the following:

• R is totally ordered: ∀ x y ∈ R, x < y ∨ y < x ∨ x=y
• R is a field
  • Addition properties
    • Addition is commutative: x+y=y+x
    • Addition is associative: x+(y+z) = (x+y)+z
    • There is an additive identity 0 and x+0 = 0+x = x.
    • Each element x has an additive inverse -x such that x+(-x) = 0.
  • Multiplication properties
    • Multiplication is commutative: xy=yx
    • Multiplication is associative: x*(yz) = (xy)*z
    • There is a multiplicative identity 1 and x1 = 1x = x.
    • Each element x has a multiplicative inverse x⁻¹ such that xx⁻¹ = x⁻¹x = 1.
• R has the least upper bound property

Mathlib defines classes for all of these properties. Thus, as we prove them in Lean, we will register intances of these classes and more so that our construction works with all of the theorems and tactics that Mathlib provides for notation, ordering, groups, rings, and fields.

TODO: List the relevant Mathlib classes or insert a tree diagram of them.

References

A nice description of the Cauchy Completion: https://mathweb.ucsd.edu/~tkemp/140A/Construction.of.R.pdf

Rudin, W.: Principles of Mathematical Analysis. Third Edition. International Series in Pure and Applied Mathematics. McGraw-Hill Book Co., New York – Aukland – Dusseldorf, 1976.

A real analysis book in which ℝ is constructed from decimal expansions of the form f : ℕ → ℤ with f(0) being the integer part and f(n) ∈ {0, ..., 9} for n ≥ 1. Davidson and Donsig

UNDER CONSTRUCTION
Code for this chapter

The Dedekind Reals

Dedekind's representation of a real number r is as a pair (A,B) where A ⊆ ℚ is the set of all rational numbers less than r and B = ℚ \ A. The idea is that A approximates r from below and B approximates r from above. In the case that r ∈ ℚ, then A = (∞,r) and B = [r,∞). Since A completely determines the cut, we work mainly with it, only occasionally referring to B.

That this definition satisfies the properties of the real numbers needs to be proved, which is what this chapter is about. Specifically, we will prove that

• The set of cuts is totally ordered
• The set of cuts form a field
• Every bounded, non-empty set of cuts has a least upper bound

The last property distinguishes the real numbers from the rationals.

A standard reference for Dedekind cuts is Rudin's Principles of Mathematics. In the 3rd edition, cuts are defined on pages 17-21.

Definition

First, we define a structure to capture the precise definition of a cut A ⊆ ℚ. We require that A is nonempty, that it is not ℚ, that it is downward closed, and that is an open interval.

@[ext]
structure DCut where
  A : Set ℚ
  ne : ∃ q, q ∈ A                   -- not empty
  nf : ∃ q, q ∉ A                   -- not ℚ
  dc : ∀ x y, x ≤ y ∧ y ∈ A → x ∈ A -- downward closed
  op : ∀ x ∈ A, ∃ y ∈ A, x < y      -- open

open DCut

def DCut.B (c : DCut) : Set ℚ := Set.univ \ c.A

theorem not_in_a_in_b {c :DCut} {q : ℚ} : q ∉ c.A → q ∈ c.B := by simp[B]

theorem ub_to_notin {y:ℚ} {A : Set ℚ}
  : (∀ x ∈ A, x < y) → y ∉ A := by
  intro h hy
  have := h y hy
  simp_all

The open property can be used extended.

theorem op2 {a : DCut} (q : ℚ) (hq : q ∈ a.A)
  : ∃ x, ∃ y, x ∈ a.A ∧ y ∈ a.A ∧ q < x ∧ x < y := by
  have ⟨s, ⟨ hs1, hs2 ⟩ ⟩ := a.op q hq
  have ⟨t, ⟨ ht1, ht2 ⟩ ⟩ := a.op s hs1
  use s, t

Making Rationals into Reals

All rational numbers are also real numbers via the map that identifies a rational q with the interval (∞,q) of all rationals less than q. We call this set odown q, where odown is meant to abbreviate open, downward closed.

def odown (q : ℚ) : Set ℚ := { y | y < q }

To prove that odown q is a Dedekind cut requires we show it is nonempty, not ℚ itself, downward closed, and open. For the first two theorems we use use the facts that q-1 ∈ (∞,q) and q+1 ∉ (∞,q).

theorem odown_ne {q : ℚ} : ∃ x, x ∈ odown q := by
  use q-1
  simp[odown]

theorem odown_nf {q : ℚ} : ∃ x, x ∉ odown q := by
  use q+1
  simp[odown]

That odown q is downward closed follows from the definitions.

theorem odown_dc {q : ℚ} : ∀ x y, x ≤ y ∧ y ∈ odown q → x ∈ odown q := by
  intro x y ⟨ hx, hy ⟩
  simp_all[odown]
  linarith

To prove odown q is open, we are given x ∈ odown and need to supply y ∈ odown q with x < y. Since q is the least upper bound of odown q, we choose (x+q)/2.

theorem odown_op {q : ℚ} : ∀ x ∈ odown q, ∃ y ∈ odown q, x < y:= by
  intro x hx
  use (x+q)/2
  simp_all[odown]
  apply And.intro
  repeat linarith

With these theorems we define the map ofRat : ℚ → DCut that embeds the rationals into the Dedekind cuts.

def ofRat (q : ℚ) : DCut :=
  ⟨ odown q, odown_ne, odown_nf, odown_dc, odown_op ⟩

instance rat_cast_inst : RatCast DCut := ⟨ λ x => ofRat x ⟩

instance nat_cast_inst : NatCast DCut := ⟨ λ x => ofRat x ⟩

instance int_cast_inst : IntCast DCut := ⟨ λ x => ofRat x ⟩

With this map we can define 0 and 1, as well as a couple of helper theorems we will later.

instance zero_inst : Zero DCut := ⟨ ofRat 0 ⟩
instance one_inst : One DCut := ⟨ ofRat 1 ⟩
instance inhabited_inst : Inhabited DCut := ⟨ 0 ⟩

theorem zero_rw : A 0 = odown 0 := by rfl
theorem one_rw : A 1 = odown 1 := by rfl

theorem zero_ne_one : (0:DCut) ≠ 1 := by
  intro h
  simp[DCut.ext_iff,zero_rw,one_rw,odown,Set.ext_iff] at h
  have h0 := h (1/2)
  have h1 : (1:ℚ)/2 < 1 := by linarith
  have h2 : ¬(1:ℚ)/2 < 0 := by linarith
  exact h2 (h0.mpr h1)

instance non_triv_inst : Nontrivial DCut := ⟨ ⟨ 0, 1, zero_ne_one ⟩ ⟩

Simple Properties of Cuts

Here we define some simple properties that wil make subsequent proofs less cumbersome. The first says for x in A and y in B, that x < y.

theorem b_gt_a {c : DCut} {x y : ℚ} : x ∈ c.A → y ∈ c.B → x < y := by
  intro hx hy
  simp[B] at hy
  by_contra h
  exact  hy (c.dc y x ⟨ Rat.not_lt.mp h, hx ⟩)

An alternative for of this same theorem, in which B is characterized as ℚ \ A is also useful.

theorem a_lt_b {c : DCut} {x y : ℚ }: x ∈ c.A → y ∉ c.A → x < y := by
  intro hx hy
  exact b_gt_a hx (not_in_a_in_b hy)

Since A is downward closed, one can easily show B is upward closed.

theorem b_up_closed {c : DCut} {a b: ℚ} : a ∉ c.A → a ≤ b → b ∉ c.A := by
  intro h1 h2 h3
  exact h1 (c.dc a b ⟨ h2, h3 ⟩)

Ordering

Next we show that cuts are totally ordered by the subset relation. First, we define and instantiate the less than and less than or equal relations on cuts.

instance lt_inst : LT DCut := ⟨ λ x y => x ≠ y ∧ x.A ⊆ y.A ⟩
instance le_inst : LE DCut := ⟨ λ x y => x.A ⊆ y.A ⟩

To check these definitions make sense, we verify them with rational numbers.

example {x y : ℚ} : x ≤ y → (ofRat x) ≤ (ofRat y) := by
  intro h q hq
  exact gt_of_ge_of_gt h hq

It is useful to be able to rewrite the less than relation < in terms of inequality and ≤, and to rewrite ≤ in terms of equality and <.

theorem DCut.lt_of_le {x y: DCut} : x < y ↔ x ≠ y ∧ x ≤ y := by
  exact Eq.to_iff rfl

theorem DCut.le_of_lt {x y: DCut} : x ≤ y ↔ x = y ∨ x < y := by
  simp_all[le_inst,lt_inst]
  constructor
  . intro h
    simp[h]
    exact Classical.em (x=y)
  . intro h
    cases h with
    | inl h1 => exact Eq.subset (congrArg A h1)
    | inr h1 => exact h1.right

We can easily prove that cuts form a partial order, which allows us to regiest DCut with Mathlib's PartialOrder class.

theorem refl {a: DCut} : a ≤ a := by
  intro q hq
  exact hq

theorem anti_symm {a b: DCut} : a ≤ b → b ≤ a → a = b := by
  intro hab hba
  ext q
  constructor
  . intro hq
    exact hab (hba (hab hq))
  . intro hq
    exact hba (hab (hba hq))

theorem trans {a b c: DCut} : a ≤ b → b ≤ c → a ≤ c := by
  intro hab hbc q hq
  exact hbc (hab hq)

theorem lt_iff_le_not_le {a b : DCut} : a < b ↔ a ≤ b ∧ ¬b ≤ a := by
  constructor
  . intro h
    rw[lt_of_le] at h
    have ⟨ h1, h2 ⟩ := h
    constructor
    . exact h.right
    . intro h3
      exact h1 (anti_symm h.right h3)
  . intro ⟨ h1, h2 ⟩
    rw[le_of_lt] at h1
    apply Or.elim h1
    . intro h
      rw[h] at h2
      exact False.elim (h2 refl)
    . intro h
      exact h

instance pre_order_inst : Preorder DCut :=
  ⟨ @refl, @trans, @lt_iff_le_not_le ⟩

instance poset_inst : PartialOrder DCut :=
  ⟨ @anti_symm ⟩

Next we prove that cuts form a total order, and instantiate this fact with the TotalOrder class from Mathlib.

theorem total {x y : DCut} : x ≤ y ∨ y ≤ x := by
  by_cases h : x ≤ y
  . exact Or.inl h
  . apply Or.inr
    simp_all[le_inst]
    intro b hb
    rw[Set.subset_def] at h
    simp at h
    obtain ⟨ a, ⟨ ha1, ha2 ⟩ ⟩ := h
    exact x.dc b a ⟨ le_of_lt (a_lt_b hb ha2), ha1 ⟩

instance total_inst : IsTotal DCut (· ≤ ·) := ⟨ @total ⟩

The total order property allows crisply define positive and negative numbers.

def isPos (x : DCut) : Prop := 0 < x
def isNeg (x : DCut) : Prop := x < 0

We can also use the total order property to prove that DCut is Trichotomous, that is, that for all x and y, either x ≤ y, y ≤ x, or x=y.

theorem trichotomy (x y: DCut) : x ≤ y ∨ x = y ∨ y ≤ x := by
  apply Or.elim (@total x y)
  . intro h
    exact Or.symm (Or.inr h)
  . intro h
    exact Or.inr (Or.inr h)

theorem trichotomy_lt (x y: DCut) : x < y ∨ x = y ∨ y < x := by
  have := trichotomy x y
  simp[le_of_lt] at this
  aesop

instance trichotomous_inst : IsTrichotomous DCut (· ≤ ·) := ⟨ trichotomy ⟩

instance trichotomous_inst' : IsTrichotomous DCut (· < ·) := ⟨ trichotomy_lt ⟩

Theorems About Zero and One

theorem zero_in_pos {a : DCut} (ha : 0 < a) : 0 ∈ a.A := by
  obtain ⟨ h1, h2 ⟩ := ha
  simp at h1
  rw[DCut.ext_iff] at h1
  have h21 := Set.ssubset_iff_subset_ne.mpr ⟨h2, h1⟩
  have ⟨ x, ⟨ hx1, hx2 ⟩ ⟩ := (Set.ssubset_iff_of_subset h2).mp h21
  simp[zero_rw,odown] at hx2
  exact a.dc 0 x ⟨ hx2, hx1 ⟩

theorem pos_has_zero {a : DCut} : 0 < a ↔ 0 ∈ a.A := by
  constructor
  . intro h
    exact zero_in_pos h
  . simp[lt_inst,DCut.ext_iff]
    intro h
    constructor
    . intro h1
      rw[←h1] at h
      simp[zero_rw,odown] at h
    . intro q hq
      simp[zero_rw,odown] at hq
      apply a.dc q 0
      exact ⟨ by exact _root_.le_of_lt hq, h ⟩


theorem non_neg_in_pos {a : DCut} (ha : 0 < a) : ∃ x ∈ a.A, 0 < x := by
  have h0 := zero_in_pos ha
  exact a.op 0 h0

theorem zero_notin_neg {a : DCut} (ha : a < 0) : 0 ∉ a.A := by
  intro h
  simp[lt_inst] at ha
  have ⟨ h1, h2 ⟩ := ha
  have : 0 ∈ A 0 := h2 h
  simp[zero_rw,odown] at this

@[simp]
theorem zero_lt_one : (0:DCut) < 1 := by
  simp[lt_inst]
  apply And.intro
  . intro h
    simp[DCut.ext_iff,zero_rw,one_rw,odown,Set.ext_iff] at h
    have := h 0
    simp_all
  . intro q hq
    simp_all[zero_rw,one_rw,odown]
    linarith

@[simp]
theorem zero_le_one : (0:DCut) ≤ 1 := by
  simp[le_inst]
  intro q hq
  simp_all[zero_rw,one_rw,odown]
  linarith

theorem not_gt_to_le {a : DCut} : ¬ 0 < a ↔ a ≤ 0 := by
  constructor
  . have := trichotomy_lt 0 a
    apply Or.elim this
    . intro h1 h2
      simp_all
    . intro h1 h2
      simp_all
      apply le_of_lt.mpr
      rw[Eq.comm]
      exact h1
  . intro h1 h2
    apply le_of_lt.mp at h1
    simp_all[DCut.ext_iff,lt_inst]
    have ⟨ h3, h4 ⟩ := h2
    simp_all
    apply Or.elim h1
    . intro h
      exact h3 (id (Eq.symm h))
    . intro ⟨ h5, h6 ⟩
      have : A 0 = a.A := by exact Set.Subset.antisymm h4 h6
      exact h3 this

theorem has_ub (a : DCut) : ∃ x, x ∉ a.A ∧ ∀ y ∈ a.A, y < x := by
  obtain ⟨ x, hx ⟩ := a.nf
  use! x, hx
  intro y hy
  exact a_lt_b hy hx

theorem in_down {p q:ℚ} (h : p < q) : p ∈ odown q := by
  simp[odown]
  exact h

theorem in_zero {q:ℚ} (h: q<0) : q ∈ A 0 := by
  simp[zero_rw]
  exact in_down h

theorem in_one {q:ℚ} (h: q<1) : q ∈ A 1 := by
  simp[one_rw]
  exact in_down h

Supporting Reasoning by Cases

Later, in the chapter on multiplication, it will be useful to reason about combinations of non-negative and negative cuts. With one cut a, there are two possibilities: 0 ≤ a and a < 0. For two cuts there are four possibilities, and for three cuts, there are eight possibilities.

The following two definitions list all possible cases for two and three cuts respectively.

def two_ineq_list (a b : DCut) :=
  (0 ≤ a ∧ 0 ≤ b) ∨
  (a < 0 ∧ 0 ≤ b) ∨
  (0 ≤ a ∧ b < 0) ∨
  (a < 0 ∧ b < 0)

def two_ineq_nn_list (a b: DCut) :=
  (0 < a ∧ 0 < b) ∨ a = 0 ∨ b = 0

def three_ineq_list (a b c : DCut) :=
  (0 ≤ a ∧ 0 ≤ b ∧ 0 ≤ c) ∨
  (a < 0 ∧ 0 ≤ b ∧ 0 ≤ c) ∨
  (0 ≤ a ∧ b < 0 ∧ 0 ≤ c) ∨
  (0 ≤ a ∧ 0 ≤ b ∧ c < 0) ∨
  (a < 0 ∧ b < 0 ∧ 0 ≤ c) ∨
  (a < 0 ∧ 0 ≤ b ∧ c < 0) ∨
  (0 ≤ a ∧ b < 0 ∧ c < 0) ∨
  (a < 0 ∧ b < 0 ∧ c < 0)

def three_ineq_nn_list (a b c : DCut) :=
  (0 < a ∧ 0 < b ∧ 0 < c) ∨ a = 0 ∨ b = 0 ∨ c = 0

Next we show that these statements are tautologies. The goal is to be able to use the definitions in tactic mode, as in:

rcases @two_ineqs a b with ⟨ ha, hb ⟩ | ⟨ ha, hb ⟩ | ⟨ ha, hb ⟩ | ⟨ ha, hb ⟩
repeat
simp

We start with a theorem that can be used to rewrite x<0 as ¬0≤x.

theorem neg_t {x : DCut} : x < 0 ↔ ¬0 ≤ x := by
  have := trichotomy_lt 0 x
  simp_all[le_of_lt]
  constructor
  . intro h
    exact ⟨ ne_of_gt h, not_lt_of_gt h ⟩
  . tauto

Then the proofs are straightforward. To see how these are used later, see the proofs of commutativity and associativity of multiplication.

theorem lt_imp_le {x y : DCut} : x < y → x ≤ y := by simp[lt_of_le]

theorem two_ineqs (a b : DCut) : two_ineq_list a b := by
  simp[two_ineq_list,neg_t]
  tauto

theorem three_ineqs (a b c : DCut) : three_ineq_list a b c := by
  simp[three_ineq_list,neg_t]
  tauto

theorem two_nn_ineqs {a b : DCut} (ha : 0 ≤ a) (hb : 0 ≤ b)
  : two_ineq_nn_list a b := by
  simp[two_ineq_nn_list,neg_t]
  simp[le_of_lt] at ha hb
  tauto

theorem three_nn_ineqs {a b c : DCut} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c)
  : three_ineq_nn_list a b c := by
  simp[three_ineq_nn_list,neg_t]
  simp[le_of_lt] at ha hb hc
  tauto

Exercise: Show that ofRat is indeed an order embedding, that is x ≤ y → ofRat x ≤ ofRat y for all rational numbers x and y.

UNDER CONSTRUCTION
Code for this chapter

Addition

def presum (a b : DCut) :=  { z | ∃ x ∈ a.A, ∃ y ∈ b.A, x+y=z }

theorem presum_ne {a b : DCut} :  ∃ q, q ∈ presum a b := by
  obtain ⟨ x, hx ⟩ := a.ne
  obtain ⟨ y, hy ⟩ := b.ne
  exact ⟨ x+y, ⟨ x, ⟨ hx, ⟨ y, ⟨ hy, by linarith ⟩ ⟩ ⟩ ⟩ ⟩

theorem presum_nf {a b : DCut} : ∃ q, q ∉ presum a b := by
    obtain ⟨ x, hx ⟩ := a.nf
    obtain ⟨ y, hy ⟩ := b.nf
    use x+y
    intro h
    obtain ⟨ s, ⟨ hs, ⟨ t, ⟨ ht, hst ⟩ ⟩ ⟩ ⟩ := h
    have hs' := b_gt_a hs (not_in_a_in_b hx)
    have ht' := b_gt_a ht (not_in_a_in_b hy)
    linarith

theorem presum_op {a b : DCut}
  : ∀ x ∈ presum a b, ∃ y ∈ presum a b, x < y := by
  intro c hc
  simp_all[presum]
  obtain ⟨ x, ⟨ hx, ⟨ y, ⟨ hy, h ⟩ ⟩ ⟩ ⟩ := hc
  have hao := a.op
  have hbo := b.op
  obtain ⟨ x', hx', hxx' ⟩ := hao x hx
  obtain ⟨ y', hy', hyy' ⟩ := hbo y hy
  use x'
  apply And.intro
  . exact hx'
  . use y'
    apply And.intro
    . exact hy'
    . linarith

theorem presum_dc {a b : DCut }
  : ∀ (x y : ℚ), x ≤ y ∧ y ∈ presum a b → x ∈ presum a b := by
  intro s t ⟨ h1, h2 ⟩
  simp_all[presum]
  obtain ⟨ x, ⟨ hx, ⟨ y, ⟨ hy, h ⟩ ⟩ ⟩ ⟩ := h2

  have hyts : y - (t - s) ∈ b.A := by
    have h3 : 0 ≤ t-s := by linarith
    have h4 : y - (t-s) ≤ y := by linarith
    exact b.dc (y-(t-s)) y ⟨h4,hy⟩

  exact ⟨ x, ⟨ hx, ⟨ y - (t-s), ⟨ hyts, by linarith ⟩ ⟩ ⟩ ⟩

def sum (a b : DCut) : DCut :=
  ⟨ presum a b, presum_ne, presum_nf, presum_dc, presum_op ⟩

instance hadd_inst : HAdd DCut DCut DCut:= ⟨ sum ⟩

instance add_inst : Add DCut := ⟨ sum ⟩

theorem add_rats {x y: ℚ} : ofRat (x+y) = ofRat x + ofRat y := by

  simp[ofRat,hadd_inst,sum,presum,odown]
  ext q
  constructor

  . intro hq
    let ε := x+y - q
    have hε : q = x+y-ε := by
      simp[ε]
    simp_all
    exact ⟨ x-ε/2, ⟨ by linarith, ⟨ y-ε/2, ⟨ by linarith, by linarith ⟩ ⟩ ⟩ ⟩

  . intro ⟨ a, ⟨ ha, ⟨ b, ⟨ hb1, hb2 ⟩ ⟩ ⟩ ⟩
    simp_all
    linarith

The Associative Property Of Addition

theorem sum_assoc {a b c : DCut} : (a+b)+c = a + (b+c) := by
  simp[hadd_inst,sum]
  ext q
  constructor
  . intro hq
    simp_all[presum]
    obtain ⟨ x, ⟨ hx, ⟨ y, ⟨ hy, ⟨ z, ⟨ hz, hsum ⟩ ⟩ ⟩ ⟩ ⟩ ⟩ := hq
    exact ⟨ x, ⟨ hx, ⟨ y, ⟨ hy, ⟨ z, ⟨ hz, by linarith ⟩ ⟩ ⟩ ⟩ ⟩ ⟩
  . intro hq
    simp_all[presum]
    obtain ⟨ x, ⟨ hx, ⟨ y, ⟨ hy, ⟨ z, ⟨ hz, hsum ⟩ ⟩ ⟩ ⟩ ⟩ ⟩ := hq
    exact ⟨ x, ⟨ hx, ⟨ y, ⟨ hy, ⟨ z, ⟨ hz, by linarith ⟩ ⟩ ⟩ ⟩ ⟩ ⟩

instance addsemigroup_inst : AddSemigroup DCut := ⟨ @sum_assoc ⟩

Commutativity of Addition

theorem sum_comm {a b : DCut} : a + b = b + a := by
  simp[hadd_inst,sum]
  ext q
  constructor
  repeat
  . intro ⟨ x, ⟨ hx, ⟨ y, ⟨ hy, h ⟩ ⟩ ⟩ ⟩
    exact ⟨ y, ⟨ hy, ⟨ x, ⟨ hx, by linarith ⟩ ⟩ ⟩ ⟩

instance addcommsemigroup_inst : AddCommSemigroup DCut := ⟨ @sum_comm ⟩

Adding Zero

theorem sum_zero_left {a : DCut} : 0 + a = a := by
  ext c
  simp[hadd_inst,sum,zero_inst]
  constructor
  . intro ⟨ x, ⟨ hx, ⟨ y, ⟨ hy, h ⟩ ⟩ ⟩ ⟩
    have : x < 0 := hx
    apply a.dc c y
    apply And.intro
    . linarith
    . exact hy
  . intro h
    obtain ⟨ x, ⟨ hx1, hx2 ⟩ ⟩ := a.op c h
    have h1 : c-x < 0 := by linarith
    exact ⟨ c-x, ⟨ h1, ⟨ x, ⟨ hx1, by linarith ⟩ ⟩ ⟩ ⟩

theorem sum_zero_right {a : DCut} : a + 0 = a := by
  rw[sum_comm,sum_zero_left]

instance add_zero_inst : AddZeroClass DCut :=
  ⟨ @sum_zero_left, @sum_zero_right ⟩

UNDER CONSTRUCTION
Code for this chapter

Negation

def preneg (c : DCut) : Set ℚ := { x | ∃ a < 0, ∃ b ∉ c.A, x = a-b }

theorem preneg_rat {p : ℚ} : preneg (ofRat p) = (ofRat (-p)).A := by
  simp[preneg,ofRat,odown]
  ext q
  constructor
  . simp_all
    intro a ha x hx hq
    linarith
  . simp_all
    intro hq
    exact ⟨ q+p, ⟨ by linarith, ⟨ p, ⟨ by linarith, by linarith ⟩ ⟩ ⟩ ⟩

theorem predeg_ne {c : DCut} : ∃ q, q ∈ preneg c := by
  simp[preneg]
  have ⟨ q, hq ⟩ := c.nf
  use -q-2
  have h1 : q + 1 ∉ c.A := by
    apply b_up_closed hq
    linarith
  exact  ⟨ -1, ⟨ by linarith, ⟨ q+1, ⟨ h1, by linarith ⟩ ⟩ ⟩ ⟩

theorem predeg_nf {c : DCut} : ∃ q, q ∉ preneg c := by
  simp[preneg]
  have ⟨ q, hq ⟩ := c.ne
  use -q
  intro x hx y hy h
  have h2 : y ≤ q := by linarith
  have h3 : q ∉ c.A := by
    intro h1
    exact b_up_closed hy h2 hq
  exact h3 hq

theorem predeg_dc {c : DCut}
  : ∀ (x y : ℚ), x ≤ y ∧ y ∈ preneg c → x ∈ preneg c := by
  intro x y ⟨ hxy, ⟨ a, ⟨ ha, ⟨ b, ⟨ hb, h ⟩ ⟩ ⟩ ⟩ ⟩
  exact ⟨ a - (y-x), ⟨ by linarith, ⟨ b, ⟨ hb, by linarith ⟩ ⟩ ⟩ ⟩

theorem predeg_op {c : DCut}
  : ∀ x ∈ preneg c, ∃ y ∈ preneg c, x < y := by
  simp[preneg]
  intro q x hx y hy hxy
  have := c.op
  use q-x/2
  apply And.intro
  . simp[hxy]
    exact ⟨ x/2, ⟨ by linarith, ⟨ y, ⟨ hy, by linarith ⟩ ⟩ ⟩ ⟩
  . linarith

def neg (c : DCut) : DCut :=
  ⟨ preneg c, predeg_ne, predeg_nf, predeg_dc, predeg_op ⟩

instance neg_inst : Neg DCut := ⟨ neg ⟩

theorem neg_rat {p : ℚ} : -ofRat p = ofRat (-p) := by
  simp[neg_inst,neg]
  apply DCut.ext
  simp
  rw[preneg_rat]

Subtraction

def sub (a b : DCut) : DCut := a + (-b)

instance hsub_inst : HSub DCut DCut DCut := ⟨ sub ⟩

instance sub_inst : Sub DCut := ⟨ sub ⟩

theorem add_neg (a b : DCut) : a + -b = a - b := by
  simp[hsub_inst,sub]

Let's check this definition works for the simple example 1-1=0. The forward direction is easy. For the reverse direction, we need to choose x and y so that

• x < 1
• y < -1
• x + y = q

Since q < 0, we know q-1 < -1. For y, we take the point halfway between q-1 and -1, which is y = (q-2)/2.

example : ofRat 1 - ofRat 1 = ofRat 0 := by
  simp[hsub_inst,sub,neg_rat]
  ext q
  simp[hadd_inst,sum,ofRat,presum,odown]
  constructor
  . intro ⟨ x, ⟨ hx, ⟨ y, ⟨ hy, h ⟩ ⟩ ⟩ ⟩
    linarith
  . intro hq
    exact ⟨ (q+2)/2, ⟨ by linarith, ⟨ (q-2)/2, ⟨ by linarith, by linarith ⟩ ⟩ ⟩ ⟩

More challenging is to show for any cut c that c-c=0. We are given q<0. Since c.A is not ℚ, we can choose an element t ∉ c.A. We then want to find a ∈ -c.A and b ∈ c.A so that a+b=q. Using the Archimedean property of the rational numbers, we can find n such that t + (n+1)q ∈ c.A and t + nq ∉ c.A.

These values do not work directly because of the edge case where c is a principal cut (representing a rational number). For example, the situation could look like the diagram below.

                -c.A                        b      c.A    -a
       -t - nq             q       0   t + (n+1)q       t + nq
  ←———————+———————)————————+———————+———————+————————)—————+————————————→
                 -2       -1             4-3=1      2   4-2=2

But because c.A is open, we can find z greater than t + (n+1)q and which is still in c.A.

        -c.A                                              c.A
                      q          0    t + (n+1)q                  t + nq
  ←———————)———————————+——————————+————————+————————+———————)————————+————————————→
                                                   z

And then take ε = z - (t + (n+1)q) to get the following situation, where a is completly inside -c.A.

          a    -c.A                        b          c.A
  ←———————+———————)———————+———————+————————+———————————)———————+————————————→
   -t - nq - ε            q       0    t + (n+1)q + ε       t + nq + ε

This proof outline takes some work to get done in Lean. First we need a result showing that given t ∉ c.A we can find an n so that t + n s ∈ c.A.

theorem cut_element (c : DCut) (s t : ℚ) (hs : s < 0)
  : ∃ n : ℕ, t + n * s ∈ c.A := by
  obtain ⟨q, hq⟩ := c.ne
  let n := ⌈(q-t)/s⌉₊
  use n
  have hdiv : (q-t)/s ≤ n := Nat.le_ceil ((q - t) / s)
  have hcalc : t + n * s ≤ q := by
    have : (q-t) ≥ n * s := (div_le_iff_of_neg hs).mp hdiv
    simp_all
    linarith
  exact c.dc _ q ⟨hcalc, hq⟩

We then define the set of all n such that t + ns ∈ c.A. For subsequent steps to work, we need to instantiate this set as decidable. This can be done using Classical logic, in which propositions are considered decidable by default.

def Svals (c : DCut) (s t : ℚ) : Set ℕ := {n : ℕ | t + n * s ∈ c.A}

noncomputable
instance s_dec {c : DCut} {s t : ℚ}  : DecidablePred (· ∈ Svals c s t) := by
    intro n
    apply Classical.propDecidable

With Svals decidiable and nonempty, we can use Nat.find to show it has a minimal element. Note that Nat.find uses the Axiom of Choice.

theorem min_element (S : Set ℕ) [DecidablePred (· ∈ S)] (h : ∃ x, x ∈ S)
  : ∃ m, m ∈ S ∧ (∀ k < m, k ∉ S) := by
  have hsne : S.Nonempty := h
  let m := Nat.find hsne
  have hm : m ∈ S := Nat.find_spec hsne
  have hm_min : ∀ k < m, k ∉ S := λ k => Nat.find_min hsne
  exact ⟨ m, hm, hm_min ⟩

We use the minimal element to find n so that t + (n+1)q ∈ c.A and t + nq ∉ c.A. as desired.

theorem archimedean {c : DCut} {s t : ℚ} (ht : t ∉ c.A) (hs : s < 0)
  : ∃ n : ℤ, t+n*s ∉ c.A ∧ t+(n+1)*s ∈ c.A := by

  let S := Svals c s t
  have ⟨ m, hm, hm_min ⟩ := min_element S (cut_element c s t hs)

  by_cases h : m = 0

  · simp [h, S, Svals] at hm
    contradiction

  · use m - 1
    have hm' : m > 0 := Nat.zero_lt_of_ne_zero h

    apply And.intro
    · have := hm_min (m-1) (Nat.sub_one_lt_of_lt hm')
      simp_all[S,Svals]
    · simp
      assumption

Finally, we prove the desired theorem.

theorem neg_add_cancel_right {c : DCut} : c - c = 0 := by

  ext q
  constructor

  . simp[hsub_inst,neg_inst,neg,sub,hadd_inst,sum,preneg]
    intro ⟨ x, ⟨ hx, ⟨ y, ⟨ hy, hxy ⟩ ⟩ ⟩ ⟩
    obtain ⟨ a, ⟨ ha, ⟨ b, ⟨ hb, hab ⟩ ⟩ ⟩ ⟩ := hy
    have h1 : q ∈ A 0 ↔ q < 0 := Set.mem_def
    simp[h1]
    have h2 := a_lt_b hx hb
    linarith

  . intro hq
    have hq : q < 0 := hq
    obtain ⟨ t, ht ⟩ := c.nf
    obtain ⟨ n, ⟨ hn1, hn2 ⟩ ⟩ := archimedean ht hq

    let b' := t + (n+1)*q
    let a' := -n*q-t

    obtain ⟨ z, ⟨ hz, hbz ⟩ ⟩ := c.op b' hn2
    let ε := z - b'
    have hε : 0 < ε := by simp[ε]; linarith

    let b := z
    let a := -n*q-t-ε

    have hab : z+a = q := by
      simp[a,a',b,b',ε]
      linarith

    have ha : a ∈ (-c).A := by
      use -ε
      apply And.intro
      . linarith
      . use -a-ε
        apply And.intro
        . simp[a]
          exact hn1
        . linarith

    exact ⟨ z, ⟨ hz, ⟨ a, ⟨ ha, hab ⟩ ⟩ ⟩ ⟩

And by commutativity:

theorem neg_add_cancel_left {c : DCut} : -c + c = 0 := by
  rw[sum_comm,add_neg,neg_add_cancel_right]

Additive Group Structure

instance add_group_inst : AddGroup DCut :=
  AddGroup.ofLeftAxioms add_assoc @sum_zero_left @neg_add_cancel_left

instance add_comm_group_inst : AddCommGroup DCut := ⟨ @sum_comm ⟩

example (x y z : DCut) : x - y + z = z + x - y := by abel

instance add_monoid_wo_inst : AddMonoidWithOne DCut := ⟨
    by
      ext q
      exact ⟨ id, id ⟩,
    by
      intro n
      ext q
      constructor
      repeat
      . intro hq
        simp_all[add_rats,nat_cast_inst]
        exact hq
  ⟩

UNDER CONSTRUCTION
Code for this chapter

The Maximum Operator

theorem neg_gt_zero {a : DCut} (ha : a < 0) : 0 < -a := by

  simp[lt_inst]
  apply And.intro

  . intro h
    obtain ⟨ h1, h2 ⟩ := ha
    exact h1 h

  . intro q hq
    simp[zero_rw,odown] at hq
    simp[neg_inst,neg,preneg]
    obtain ⟨ b, hb ⟩ := a.nf
    exact ⟨ q, ⟨ hq, ⟨ 0, ⟨ zero_notin_neg ha, Eq.symm (sub_zero q) ⟩ ⟩ ⟩ ⟩

theorem maximum_ne {a b : DCut} : ∃ q, q ∈ a.A ∪ b.A := by
  obtain ⟨ x, hx ⟩ := a.ne
  use x
  exact Set.mem_union_left b.A hx

theorem maximum_nf {a b : DCut} : ∃ q, q ∉ a.A ∪ b.A := by
  obtain ⟨ x, hx ⟩ := a.nf
  obtain ⟨ y, hy ⟩ := b.nf
  apply Or.elim (trichotomy a b)
  . intro h
    simp_all
    use y
    apply And.intro
    . intro h1
      exact hy (h h1)
    . exact hy
  . intro h
    apply Or.elim h
    . intro h1
      simp[h1]
      use y
    . intro h1
      simp[h1]
      use x
      exact ⟨ hx, fun a ↦ hx (h1 a) ⟩

theorem maximum_dc {a b : DCut} : ∀ (x y : ℚ), x ≤ y ∧ y ∈ a.A ∪ b.A → x ∈ a.A ∪ b.A := by
  intro x y ⟨ hx, hy ⟩
  apply Or.elim hy
  . intro h
    simp[h]
    exact Or.inl (a.dc x y ⟨ hx, h ⟩)
  . intro h
    simp[h]
    exact Or.inr (b.dc x y ⟨ hx, h ⟩)

theorem maximum_op {a b : DCut} : ∀ x ∈ a.A ∪ b.A, ∃ y ∈ a.A ∪ b.A, x < y:= by
  intro x hx
  apply Or.elim hx
  . intro h
    obtain ⟨ q, ⟨ hq1, hq2 ⟩ ⟩ := a.op x h
    exact ⟨ q, ⟨ Set.mem_union_left b.A hq1, hq2 ⟩ ⟩
  . intro h
    obtain ⟨ q, ⟨ hq1, hq2 ⟩ ⟩ := b.op x h
    exact ⟨ q, ⟨ Set.mem_union_right a.A hq1, hq2 ⟩ ⟩

def maximum (a b : DCut) : DCut :=
 ⟨ a.A ∪ b.A, maximum_ne, maximum_nf, maximum_dc, maximum_op ⟩

instance max_inst : Max DCut := ⟨ maximum ⟩

theorem max_gz (a: DCut) : 0 ≤ maximum 0 a := by
  simp_all[le_inst,zero_rw,odown,maximum]

theorem max_sym {a b : DCut} : maximum a b = maximum b a := by
  simp[maximum,Set.union_comm]

@[simp]
theorem max_pos {a : DCut} : 0 ≤ a → maximum 0 a = a := by
  simp[maximum,le_inst,DCut.ext_iff]

@[simp]
theorem max_neg {a : DCut} : a ≤ 0 → maximum 0 a = 0 := by
  simp[maximum,le_inst,DCut.ext_iff]

@[simp]
theorem max_pos_lt {a : DCut} : 0 < a → maximum 0 a = a := by
   simp[maximum,lt_inst,DCut.ext_iff]

@[simp]
theorem max_neg_lt {a : DCut} : a < 0 → maximum 0 a = 0 := by
   simp[maximum,lt_inst,DCut.ext_iff]

@[simp]
theorem max_self {a : DCut} : maximum a a = a := by
   simp[maximum,lt_inst,DCut.ext_iff]

@[simp]
theorem max_pos_to_neg {a: DCut} (ha : 0 < a) : maximum 0 (-a) = 0 := by
  simp[maximum,lt_inst,DCut.ext_iff,neg_inst,neg,preneg,zero_rw,odown]
  intro x y hy z hz hxyz
  have ⟨ q, ⟨ hq1, hq2 ⟩ ⟩ := non_neg_in_pos ha
  have := a_lt_b hq1 hz
  linarith

theorem neg_lt {a : DCut}: 0 < a ↔ -a < 0 := by
  constructor
  . simp_all[lt_inst]
    intro h1 h2
    apply And.intro
    . intro h
      exact h1 (Eq.symm h)
    . intro x ⟨ q, ⟨ hq, ⟨ r, ⟨ hr, hqr ⟩ ⟩ ⟩ ⟩
      have h4 := a_lt_b (h2 hq) hr
      simp[zero_rw,odown]
      linarith
  . intro ⟨ h1, h2 ⟩
    apply And.intro
    . exact id (Ne.symm (neg_ne_zero.mp h1))
    . by_contra h
      have ⟨ z, ⟨ hz1, hz2 ⟩ ⟩ := Set.not_subset.mp h
      simp[neg_inst,neg,preneg,zero_rw,odown] at h2
      have := h2 0 z hz1 z hz2 (by linarith)
      simp at this

theorem neg_le {a : DCut} : 0 ≤ a ↔ -a ≤ 0 := by
  simp[le_of_lt,@neg_lt a,eq_comm]

theorem neg_lt' {a : DCut} : a < 0 ↔ 0 < -a := by

  constructor
  . intro ⟨ h1, h2 ⟩
    apply And.intro
    . simp[DCut.ext_iff] at h1 ⊢
      exact h1
    . intro q hq
      simp[neg_inst,neg,preneg]
      simp[zero_rw,odown] at hq
      have : 0 ∉ a.A := by
        intro h
        have := h2 h
        simp[zero_rw,odown] at this
      exact ⟨ q, ⟨ hq, ⟨ 0, ⟨ this, by linarith ⟩ ⟩ ⟩ ⟩
  . simp[lt_inst]
    intro ha h
    apply And.intro
    . exact ha
    . by_contra hnq
      have ⟨ z, ⟨ hz1, hz2 ⟩ ⟩ := Set.not_subset.mp hnq
      simp[neg_inst,neg,preneg,zero_rw,odown] at h hz2
      have ⟨ s, ⟨ hs1, hs2 ⟩ ⟩ := a.op z hz1
      have ⟨ q, ⟨ hq, ⟨ r, ⟨ hr1, hr2 ⟩ ⟩ ⟩ ⟩ := h (-s) (by linarith)
      have : s < r := by exact a_lt_b hs1 hr1
      linarith

theorem neg_le' {a : DCut} : a ≤ 0 ↔ 0 ≤ -a := by
  simp[le_of_lt,@neg_lt' a,eq_comm]

theorem pos_neg_sum {a : DCut} : a = maximum 0 a - maximum 0 (-a) := by
  by_cases h : 0 < a
  . rw[max_pos h.right]
    rw[max_neg (neg_le.mp h.right)]
    exact Eq.symm (sub_zero a)
  . have := trichotomy_lt 0 a
    simp[not_gt_to_le] at h
    apply Or.elim this
    . intro h'
      rw[max_pos_lt h']
      have := neg_lt.mp h'
      rw[max_neg_lt this]
      simp
    . intro h'
      rw[max_neg h]
      have := neg_le'.mp h
      rw[max_pos this]
      simp

@[simp]
theorem neg_max_zero_neg {a : DCut} (ha : a ≤ 0) : -maximum 0 (-a) = a := by
   have : 0 ≤ -a := by
     rw[neg_le'] at ha
     exact ha
   simp[max_pos,this]

UNDER CONSTRUCTION
Code for this chapter

Multiplication

Multiplication of Dedekind cuts is straightfoward, but also fairly involved, or as Rudin says: "bothersome". The issue is dealing with both positive and negative cuts. Following Rudin, the development of the definitions proceeds as follows:

• Define multiplication on positive cuts.
• Extend multiplciation on positive cuts to non-negative cuts, building on the previous step by handling the cases in which either or both of the cuts is zero.
• Extend multiplication on non-negative cuts to all cuts.

For each of the above definitions of multiplication, we also prove the properties required to show that multiplication forms a commutiative group on cuts:

• 0 is an identity: 0*x = 0
• Multiplication is commutative: x*y = y*x
• Associativity: x*(y*z) = (x*y)*z The last property is particularly challenging, because to relate arbitary reals with positive reals, one has to deal with an abundance of cases, preferably gracefully. Thus, along the way we will prove several intermediate results which allow us to make the proof more concise.

Definitions

Multiplication of Positive Cuts

Given two positive cuts 0 < a and 0 < b, their product is the set of points z such that for some x ∈ a and y ∈ b, z < x*y. This basic definition underlies the entire framework for multiplication, after which we simply have to deal with various combinations of non-negative and negative numbers.

def pre_mul (a b : DCut) :=
  { z | ∃ x ∈ a.A, ∃ y ∈ b.A, 0 < x ∧ 0 < y ∧ z < x*y }

To make some proofs more readable, it is useful to characterize pre_mul the following sufficient condition.

theorem pre_mul_suffice {a b : DCut} {x y z : ℚ}
  : x ∈ a.A → y ∈ b.A → 0 < x → 0 < y → z < x*y → z ∈ pre_mul a b := by
  intro hx hy _ _ _
  use x, hx, y, hy

To prove that this definition results in a cut, we need to prove as usual that it is non-empty, not equal to ℚ, downward closed, and open.

First, we show pre_mul a b is non-empty, by showing that it contains 0. Since a and b are positive, they contain 0. By the op property, a and b must also contain values x and y larger than zero. Then 0 < x*y as well, satisfying the definition.

theorem pre_mul_ne {a b : DCut} (ha : 0 < a) (hb : 0 < b) : ∃ q, q ∈ pre_mul a b := by

  have ⟨ x, ⟨ hx1, hx2 ⟩ ⟩ : ∃ x ∈ a.A, 0 < x := a.op 0 (zero_in_pos ha)
  have ⟨ y, ⟨ hy1, hy2 ⟩ ⟩ : ∃ y ∈ b.A, 0 < y := b.op 0 (zero_in_pos hb)
  use 0
  apply pre_mul_suffice hx1 hy1 hx2 hy2
  nlinarith

To show pre_mul a b is not ℚ, we choose x and y not in a and b respectively and show that x*yis bigger than every value in in pre_mul a b. Although this proof does not require that a and b are positive, we include these conditions anyway for consistency.

theorem pre_mul_nf {a b : DCut} (_ : 0 < a) (_ : 0 < b)
  : ∃ q, q ∉ pre_mul a b := by
  obtain ⟨ x, ⟨ hx, hx' ⟩ ⟩ := has_ub a
  obtain ⟨ y, ⟨ hy, hy' ⟩ ⟩ := has_ub b
  use x*y
  apply ub_to_notin
  intro q hq
  choose s hs t ht hs0 ht0 hqst using hq
  nlinarith[hx' s hs, hy' t ht]

That pre_mul a b is downward closed is results from a straightforward unpacking of the definitions.

theorem pre_mul_dc {a b : DCut}
  : ∀ x y, x ≤ y ∧ y ∈ (pre_mul a b) → x ∈ (pre_mul a b) := by
  intro x y ⟨ hxy, hy ⟩
  obtain ⟨ s, ⟨ hs, ⟨ t, ⟨ ht, ⟨ hsp, ⟨ htp, hyst ⟩ ⟩ ⟩ ⟩ ⟩ ⟩ := hy
  exact pre_mul_suffice hs ht hsp htp (lt_of_le_of_lt hxy hyst)

To show pre_mul a b is open, we start with values s and t in a and b respectively. Since a and b are open, we obtain values s' and t' in that are greater that s and t and still in a and b. Then s*t < s'*t' as required.

theorem pre_mul_op {a b : DCut}
  : ∀ x ∈ (pre_mul a b), ∃ y ∈ (pre_mul a b), x < y := by
  intro x ⟨ s, ⟨ hs, ⟨ t, ⟨ ht, ⟨ hsp, ⟨ htp, hyst ⟩ ⟩ ⟩ ⟩ ⟩ ⟩
  have ⟨ s', ⟨ hs', hss' ⟩ ⟩ := a.op s hs
  have ⟨ t', ⟨ ht', htt' ⟩ ⟩ := b.op t ht
  have h: s*t < s'*t' := by nlinarith
  use! s*t, s', hs', t', ht'
  split_ands
  repeat
  linarith

Grouping these properties together we have a proof that this definition of multiplication results in a proper cut.

def mul_pos (a b : DCut) (ha : 0 < a) (hb : 0 < b) : DCut :=
  ⟨ pre_mul a b, pre_mul_ne ha hb, pre_mul_nf ha hb, pre_mul_dc, pre_mul_op ⟩

We will need the following property to extend multiplication from positive numbers to non-negative numbers stating that the product of two positive numbers is again positive. Thus, the definition pre_mul operates exclusively on the positive reals.

theorem zero_in_pre_mul  {a b : DCut} (ha : 0 < a) (hb : 0 < b)
  : 0 ∈ pre_mul a b  := by
  have ⟨ x, ⟨ hx1, hx2 ⟩ ⟩ := non_neg_in_pos ha
  have ⟨ y, ⟨ hy1, hy2 ⟩ ⟩ := non_neg_in_pos hb
  use! x, hx1, y, hy1, hx2, hy2
  nlinarith

theorem mul_is_pos {a b : DCut} (ha : 0 < a) (hb : 0 < b)
  : 0 < mul_pos a b ha hb := by
  apply pos_has_zero.mpr
  exact zero_in_pre_mul ha hb

Multiplication on Non-negative Cuts

We now extend the definition to non-negative reals, essentially dealing with the cases in which either cut is zero, in which case the resulting product is zero. Indeed, if one of a and b is zero, then pre_mul a b = ∅.

example {A : Set ℕ}: A ⊆ ∅ ↔ A = ∅ := by exact Set.subset_empty_iff

@[simp]
theorem zero_mul_empty {a b : DCut} (h : 0 = a ∨ 0 = b) : pre_mul a b = ∅ := by
  rcases h with h | h
  repeat
  . simp[pre_mul,←h,zero_rw,odown]
    ext
    simp
    intros
    linarith

Since ∅ is not a valid cut, we use pre_mul a b ∪ odown 0 to represent the product of two non-negative cuts. Of course, if a and b are positive cuts, then pre_mul a b is downward closed, so the union with odown 0 is not needed.

@[simp]
theorem non_zero_mul_subsume {a b : DCut} (ha : 0 < a) (hb : 0 < b)
  : pre_mul a b ∪ odown 0 = pre_mul a b := by
  simp_all[lt_inst]
  exact lt_imp_le (mul_is_pos ha hb)

The usual theorems are required to show that the product is a cut. We simply have to deal with the possible cases.

theorem mul_nneg_ne {a b : DCut}
  : ∃ q, q ∈ pre_mul a b ∪ odown 0 := by
  use -1
  apply Or.inr
  simp[odown]

theorem mul_nneg_nf {a b : DCut} (ha : 0 ≤ a) (hb : 0 ≤ b)
  : ∃ q, q ∉ pre_mul a b ∪ odown 0 := by
  rcases two_nn_ineqs ha hb with ⟨ ha, hb ⟩ | h | h
  . simp[pre_mul_nf,ha,hb]
  repeat
  . simp[h,odown]
    exact ⟨ 1, rfl ⟩

theorem mul_nneg_dc {a b : DCut} {x y : ℚ}
  : x ≤ y ∧ y ∈ pre_mul a b ∪ odown 0 → x ∈ pre_mul a b ∪ odown 0 := by
  intro ⟨ h1, h2 ⟩
  apply Or.elim h2
  . intro hy
    apply Or.inl
    exact pre_mul_dc x y ⟨ h1, hy ⟩
  . intro hy
    apply Or.inr
    exact odown_dc x y ⟨ h1, hy ⟩

theorem mul_nneg_op {a b : DCut} (x : ℚ) :
  x ∈ pre_mul a b ∪ odown 0 → ∃ y ∈ pre_mul a b ∪ odown 0, x < y := by
  intro h
  apply Or.elim h
  . intro hx
    have ⟨ q, ⟨ hq1, hq2 ⟩ ⟩ := pre_mul_op x hx
    use q
    exact ⟨ Or.inl hq1, hq2 ⟩
  . intro hx
    use x/2
    simp_all[odown]
    exact ⟨ Or.inr (by linarith), by linarith ⟩

def mul_nneg (a b : DCut) (ha : 0 ≤ a) (hb : 0 ≤ b) : DCut :=
  ⟨ pre_mul a b ∪ odown 0,
    mul_nneg_ne,
    mul_nneg_nf ha hb,
    @mul_nneg_dc a b,
    @mul_nneg_op a b ⟩

We note that when a and b are positive cuts, that mul_nneg agrees with mul_pos.

theorem nneg_eq_pos {a b : DCut} (ha : 0 < a) (hb : 0 < b)
  : mul_nneg a b (lt_imp_le ha) (lt_imp_le hb) = mul_pos a b ha hb := by
  simp_all[mul_is_pos,ha,hb,mul_nneg,mul_pos]

Mulitiplication on Arbitrary Cuts

Finally, we extend multiiplcation to arbitrary cuts. This step uses the fact that every cut a can be written as the difference max 0 a - max 0 (-a). If 0 ≤ a then

max 0 a - max 0 (-a) = a + 0

and if a < 0 then

max 0 a - max 0 (-a) = 0 + -a

both of which are non-negative, and we can therefore use the previous definition of multiplication on non-negative cuts.

def mul (a b : DCut) : DCut :=
  let ap := maximum 0 a
  let an := maximum 0 (-a)
  let bp := maximum 0 b
  let bn := maximum 0 (-b)
  (mul_nneg ap bp (max_gz _) (max_gz _)) +
  (mul_nneg an bn (max_gz _) (max_gz _)) -
  (mul_nneg ap bn (max_gz _) (max_gz _)) -
  (mul_nneg an bp (max_gz _) (max_gz _))

We may now instantiate the notation classes for multiplcation.

instance hmul_inst : HMul DCut DCut DCut := ⟨ mul ⟩
instance mul_inst : Mul DCut := ⟨ mul ⟩

example : (1:DCut) * 0 = 0 := by
  simp[hmul_inst,mul]

Multiplication by 0

For non-negative cuts, it is useful to know that 0*a = 0 and a*0 = 0, as these properties allow us to reason about the zero cases in the non-negative commutativity proof. These properties also allow us to show that 0 is the multiplicative identity, which is needed for proving cuts with multiplication form a group.

@[simp]
theorem mul_nneg_zero_left {a : DCut} (ha: 0 ≤ a)
  : mul_nneg 0 a (λ _ a => a) ha = 0 := by
  simp[mul_nneg,DCut.ext_iff,zero_rw]

@[simp]
theorem mul_nneg_zero_right {a : DCut} (ha: 0 ≤ a)
  : mul_nneg a 0 ha (λ _ a => a) = 0 := by
  simp[mul_nneg,DCut.ext_iff,zero_rw]

These two theorems allow us to prove that the multiple of two non-negative cuts is again non-negative.

@[simp]
theorem mul_is_nneg {a b : DCut} (ha : 0 ≤ a) (hb : 0 ≤ b)
  : 0 ≤ mul_nneg a b ha hb := by
  rcases two_nn_ineqs ha hb with ⟨ ha, hb ⟩ | h | h
  . rw[nneg_eq_pos ha hb]
    exact lt_imp_le (mul_is_pos ha hb)
  repeat
  . simp[←h]
    simp_all[lt_of_le]

We can extend these properties to arbitrary cuts.

@[simp]
theorem mul_zero_left {a : DCut} : 0 * a = 0 := by
  simp[hmul_inst,mul]

@[simp]
theorem mul_zero_right {a : DCut} : a * 0 = 0 := by
  simp[hmul_inst,mul]

instance mul_zero_inst : MulZeroClass DCut := ⟨
    @mul_zero_left,
    @mul_zero_right
  ⟩

Commutativity

For positive cuts, commutativity is straightfoward, as it simply amounts to reordering x and y in the definition of pre_mul.

theorem mul_pos_comm {a b : DCut} (ha : 0 < a) (hb : 0 < b)
  : mul_pos a b ha hb = mul_pos b a hb ha  := by
  ext q
  constructor
  repeat
  . intro ⟨ x, ⟨ hx, ⟨ y, ⟨ hy, ⟨ h1, ⟨ h2, h3 ⟩ ⟩ ⟩ ⟩ ⟩ ⟩
    exact ⟨ y, ⟨ hy, ⟨ x, ⟨ hx, ⟨ h2, ⟨ h1, by linarith ⟩ ⟩ ⟩ ⟩ ⟩ ⟩

Proving commutativity for non-negative cuts amounts to three cases, where a and b are both positive and where one or the other is negative.

theorem mul_nneg_comm {a b : DCut} (ha : 0 ≤ a) (hb : 0 ≤ b)
  : mul_nneg a b ha hb = mul_nneg b a hb ha := by

  rcases two_nn_ineqs ha hb with ⟨ ha, hb ⟩ | h | h
  . simp[mul_nneg]
    have := mul_pos_comm ha hb
    simp_all[mul_pos]
  repeat
  . simp[h]

The proof of commutativity for arbitrary cuts requires us to reason about every possible combination of non-negative and negative cuts. We do this with the theorem two_ineqs_true which enuerates all four cases. For each case, the same simplificiation works.

theorem mul_comm {a b : DCut}: a*b = b*a := by
  rcases two_ineqs a b with ⟨ ha, hb ⟩ | ⟨ ha, hb ⟩ | ⟨ ha, hb ⟩ | ⟨ ha, hb ⟩
  repeat
  simp[ha,hb,hmul_inst,mul,mul_nneg_comm,neg_le.mp]

Multiplication by 1

The proof that 1*x=x is split into three main steps for positive, non-negative, and arbitary cuts. For positive cuts, the proof is split into two parts that show 1*a ≤ a and a*1 ≤ 1 respectively. The first direction is straightforward, and uses the fact that a is downward closed.

theorem mul_pos_id_left_1 {a : DCut} (ha: 0 < a)
  : mul_pos 1 a zero_lt_one ha ≤ a := by
  intro q ⟨ x, ⟨ hx, ⟨ y, ⟨ hy, ⟨ hx0, ⟨ hy0, hqxy ⟩ ⟩ ⟩ ⟩ ⟩ ⟩
  apply a.dc q (x*y)
  split_ands
  . linarith
  . have hxy : x*y < y := mul_lt_of_lt_one_left hy0 hx
    exact a.dc (x*y) y ⟨ by linarith, hy ⟩

For the other direction, we assume we have q ∈ a.A and need to show q is in mul_pos 1 a. This is done differently depending on whether q is positive or non-negative. For the first case, we use the fact that a.A is open to find s and t in a.A with q < s < t. Then q < s*t as required. For q non-negative, we use the fact that 0 ∈ a.A and find s ∈ a.A with 0<s. We also have 1/2 ∈ odown 1. Then q < s*(1/2) as required.

theorem mul_pos_id_left_2 {a : DCut} (ha: 0 < a)
  : a ≤ mul_pos 1 a zero_lt_one ha := by
  intro q hq
  simp[mul_pos]
  by_cases h : 0 < q
  . have ⟨ s, ⟨ t, ⟨ hx, ⟨ ht1, ⟨ hsq, st ⟩ ⟩ ⟩ ⟩ ⟩ := op2 q hq
    have hs3 : 0 < s := by linarith
    refine pre_mul_suffice ?_ ht1 (div_pos h hs3) ?_ ?_
    . apply in_one
      exact Bound.div_lt_one_of_pos_of_lt hs3 (by linarith)
    . linarith
    . have hts : t/s > 1 := (one_lt_div hs3).mpr (by linarith)
      have hqts : q*(t/s) = q / s * t := Eq.symm (mul_comm_div q s t)
      nlinarith
  . have ⟨s, ⟨ hs1, hs2 ⟩ ⟩ := a.op 0 (zero_in_pos ha)
    refine pre_mul_suffice ?_ hs1 one_half_pos hs2 ?_
    . apply in_one
      linarith
    . linarith

Combining the above inequalities gives the main result for positive cuts.

@[simp]
theorem mul_pos_id_left {a : DCut} (ha: 0 < a)
  : mul_pos 1 a zero_lt_one ha = a := by
  apply PartialOrder.le_antisymm
  . exact mul_pos_id_left_1 ha
  . exact mul_pos_id_left_2 ha

For non-negative cuts, we consider the cases where 0 = a and 0 < a separately.

@[simp]
theorem mul_nneg_id_left {a : DCut} (ha: 0 ≤ a)
  : mul_nneg 1 a zero_le_one ha = a := by
    rw[le_of_lt] at ha
    rcases ha with h1 | h2
    . simp[←h1]
    . have := mul_pos_id_left h2
      simp_all[mul_pos,DCut.ext_iff,mul_nneg,DCut.ext_iff]
      exact ha

Commutativity makes it easy to prove similar versions of theorems for which one side has already been established. For example:

@[simp]
theorem mul_nneg_id_right {a : DCut} (ha: 0 ≤ a)
  : mul_nneg a 1 ha zero_le_one = a := by
  rw[mul_nneg_comm,mul_nneg_id_left]

And similarly,

@[simp]
theorem mul_id_right {a : DCut} : a * 1 = a := by
  simp only[hmul_inst,mul]
  by_cases ha : 0 < a
  . simp[ha]
  . simp
    rw[not_gt_to_le] at ha
    simp[ha]

@[simp]
theorem mul_id_left {a : DCut} : 1 * a = a := by
  simp[mul_comm]

Mathlib includes a class that keeps track of these properties.

instance mul_one_inst : MulOneClass DCut := ⟨
  @mul_id_left,
  @mul_id_right
⟩

Associativity

The proof that mul is associatve amounts to a lot of book-keeping around some simple observations. We start with a proof that mul_pos is associatve, which has two directions to prove. Each uses the fact that the cuts are open.

theorem mul_pos_assoc {a b c : DCut} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
  : mul_pos a (mul_pos b c hb hc) ha (mul_is_pos hb hc) =
    mul_pos (mul_pos a b ha hb) c (mul_is_pos ha hb) hc  := by

  ext q
  constructor

  . choose x hx yz h' hx0 hyz0 hq
    choose y hy z hz hy0 hz0 hyz' using h'
    obtain ⟨ x', ⟨ hx', hxx' ⟩ ⟩ : ∃ x' ∈ a.A, x < x' := a.op x hx
    use x*y
    constructor
    . use! x', hx', y
      simp_all
      nlinarith
    . use z
      simp_all
      nlinarith

  . choose xy h' z hz hxy hx0 hq
    choose x hx y hy hz0 hy0 hxy' using h'
    have ⟨ z', ⟨ hz', hzz' ⟩ ⟩ : ∃ z' ∈ c.A, z <z' := c.op z hz
    use! x, hx, y*z
    constructor
    . use y, hy, z'
      simp_all
      nlinarith
    . simp_all
      nlinarith

Extending this result to non-negative cuts requires reasoning about four cases, convenienly available through the three_nn_ineqs theorem.

@[simp]
theorem mul_nneg_assoc {a b c : DCut} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c)
  : mul_nneg a (mul_nneg b c hb hc) ha (mul_is_nneg hb hc) =
    mul_nneg (mul_nneg a b ha hb) c (mul_is_nneg ha hb) hc := by

  rcases three_nn_ineqs ha hb hc with ⟨ ha', hb', hc' ⟩ | h | h | h

  . simp[mul_nneg]
    congr -- removes `∪ odown 0`
    simpa[mul_pos,ha',hb',hc'] using mul_pos_assoc ha' hb' hc'

  repeat
  . simp[h]

To prove associativity in general, it is tempting to look at 27 possible cases in which each of three cuts are positive, zero or negative. However, we can take advantage of some basic algebra to reduce the number of cases to eight. To proceed, note that when a ≤ 0 while 0 ≤ b and 0 ≤ c, then

(a*b)*c = a*(b*c)

becomes

-((-a)*b)*c = -((-a)*(b*c))

and then use mul_assoc_all_nn. Similarly, we can do all the other cases this way.

@[simp]
theorem mul_neg_dist_left {a b : DCut} : a*(-b) = -(a*b) := by
  simp[hmul_inst,mul]
  rcases two_ineqs a b with ⟨ ha, hb ⟩ | ⟨ ha, hb ⟩ | ⟨ ha, hb ⟩ | ⟨ ha, hb ⟩
  repeat
  simp[ha,hb,neg_le.mp]

@[simp]
theorem mul_neg_dist_right {a b : DCut} : (-a)*b = -(a*b) := by
  simp only[hmul_inst,mul]
  rcases two_ineqs a b with ⟨ ha, hb ⟩ | ⟨ ha, hb ⟩ | ⟨ ha, hb ⟩ | ⟨ ha, hb ⟩
  repeat
  simp[ha,hb,neg_le.mp]

To make the proof more readable, we rewrite the theorem for non-negative cuts in terms of arbitrary cuts.

theorem mul_assoc_all_nn {a b c : DCut} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c)
  : a * (b * c) = (a * b) * c := by
  simp[hmul_inst,mul]
  simp[ha,hb,hc,neg_le.mp] -- uses mul_nneg_assoc

And we prove a simple theorem that allows us to flip the direction of an inequality involving a negative cut.

theorem flip {a : DCut} (ha: a < 0) : 0 ≤ -a := neg_le'.mp (lt_imp_le ha)

Finally, combining the above, we can use the simplifier, flip and mul_assoc_all_nn to prove associativity for arbitrary cuts.

theorem mul_assoc {a b c : DCut} : a * (b * c) = (a * b) * c := by
  rcases three_ineqs a b c with ⟨ ha, hb, hc ⟩ | ⟨ ha, hb, hc ⟩ |
                                ⟨ ha, hb, hc ⟩ | ⟨ ha, hb, hc ⟩ |
                                ⟨ ha, hb, hc ⟩ | ⟨ ha, hb, hc ⟩ |
                                ⟨ ha, hb, hc ⟩ | ⟨ ha, hb, hc ⟩
  . exact mul_assoc_all_nn ha hb hc
  . simpa using mul_assoc_all_nn (flip ha) hb hc
  . simpa using mul_assoc_all_nn ha (flip hb) hc
  . simpa using mul_assoc_all_nn ha hb (flip hc)
  . simpa using mul_assoc_all_nn (flip ha) (flip hb) hc
  . simpa using mul_assoc_all_nn (flip ha) hb (flip hc)
  . simpa using mul_assoc_all_nn ha (flip hb) (flip hc)
  . simpa using mul_assoc_all_nn (flip ha) (flip hb) (flip hc)

Instantiating Multiplication Classes

With associatively and commutivity proved, we can show that multiplication forms a semigroup and a commutative magma.

instance semigroup_inst : Semigroup DCut := ⟨
  λ x y z => Eq.symm (@mul_assoc x y z)
⟩

instance semigroup_w_zero_inst : SemigroupWithZero DCut := ⟨
  @mul_zero_left,
  @mul_zero_right
⟩

instance mul_zo_inst : MulZeroOneClass DCut := ⟨
  @mul_zero_left,
  @mul_zero_right
⟩

instance comm_magma_inst : CommMagma DCut := ⟨ @mul_comm ⟩

instance comm_semigroup_inst : CommSemigroup DCut := ⟨ @mul_comm ⟩

Natural Powers and Monoid Instance

Mathlib's class structure that leads to instantiating a type as a field includes showing the type is a Monoid, which includes a method for raising a cut x to a natural numbered power, as in x^n. We define that method here.

def npow (n: ℕ) (x : DCut) : DCut := match n with
  | Nat.zero => 1
  | Nat.succ k => x * (npow k x)

And show to obvious statements about such powers.

theorem npow_zero {x : DCut} : npow 0 x = 1 := by rfl

theorem npow_succ {n : ℕ} {x : DCut} : npow (n+1) x = npow n x * x := by
  simp[npow,mul_comm]

Together these properties allow us to instante DCut as a Monoid, a Commutative Monoind, and a Commutative Monoid with zero.

instance monoid_inst : Monoid DCut := ⟨
  @mul_id_left,
  @mul_id_right, -- why does this need to be here if this is already a MulOneClass?
  npow,
  @npow_zero,
  @npow_succ
⟩

instance com_monoid_inst : CommMonoid DCut := ⟨
  @mul_comm
⟩

instance monoid_wz_inst : MonoidWithZero DCut := ⟨
  @mul_zero_left,
  @mul_zero_right
⟩

instance comm_monoid_wz_inst : CommMonoidWithZero DCut := ⟨
  @mul_zero_left,
  @mul_zero_right
⟩

Here is a simple example that uses theorems about monoids from Mathlib.

example (x : DCut) : x^2 = x*x := by
  exact pow_two x

UNDER CONSTRUCTION
Code for this chapter

Overview

An order relation on a set A is a predicate A → A → Prop that captures some notion of order. A familiar example is the the less than relation on the natural numbers:

#check 1 ≤ 2

where < is shorthand for

#check Nat.le       -- ℕ → ℕ → Prop

Nat.le is an example of a total order on a set, meaning any two elements x and y are related (i.e. x≤y or y≤x). This need not be the case in general. For example, the subset relation ⊆ on sets is only a partial order, because one can find sets A and B for which neither A ⊆ B or B ⊆ A.

namespace Temp

def A : Set ℕ := {1,2}
def B : Set ℕ := {3,4}

example : ¬A ⊆ B ∧ ¬B ⊆ A := by
  apply And.intro
  . intro h
    have h1a: 1 ∈ A := by simp[A]
    have h1b := h h1a
    simp[B] at h1b
  . intro h
    have h3b: 3 ∈ B := by simp[B]
    have h3a := h h3b
    simp[A] at h3a

end Temp

You will encounter many other examples of orderings besides these two, some of which we will get to in later sections. For now, we aim like to define a hierarchy of types of orders that capture their similarities and differences, defining a general theory of orders. A side goal here is to show how Lean's heirachy machinery works from the point of view of defining a new hierarchy instead of using someone else's hierarchy.

Most of this material comes from the book Introduction to Lattices and Order by Davey and Priestly.

Partial Orders

A partially ordered set or poset is a set and a less-than ordering relation on the set that requires pretty much the minimum one might expect from a binary relation for it to be called an ordering: the relation needs to be reflexive, anti-symmetric, and transitive (see Relations). Using a new Lean class, we define a class of types that have a less-than relation with these three properties.

class Poset (α : Type u) where
  le : α → α → Prop
  refl : ∀ x, le x x
  anti_sym : ∀ x y, le x y → le y x → x = y
  trans : ∀ x y z, le x y → le y z → le x z

Example : The Natural Numbers

Lean's standard library has all of these properties defined for natural numbers. Therefore, we can assert that ℕ is a poset by instantiating the Poset class as follows.

instance : Poset ℕ := ⟨ Nat.le, @Nat.le.refl, @Nat.le_antisymm, @Nat.le_trans⟩

Example : Sets

Lean's standard library also has all of these properties defined for sets.

instance {A: Type u} : Poset (Set A) := ⟨
  Set.Subset,
  Set.Subset.refl,
  λ _ _ h1 h2 => Set.Subset.antisymm h1 h2,
  λ _ _ _ h1 h2 => Set.Subset.trans h1 h2
⟩

Poset Notation

Simply having the Poset class defined does not give us much, however. Thus, the main goal of this section is to develop theorems that, for example, apply to any Poset, define specific kinds of Poset, or that relate Posets to each other.

To state these theorems cleaning, we first register some notation with Lean. Instantiating the LE and LT classes in Lean's standard library allow us to use ≤, ≥, <, and ge on elements of our Poset type. Notice how these instances are declared. We have to supply a Type A, and require that it has been instantiated as a Poset.

instance le_inst {A : Type u} [Poset A] : LE A := ⟨ Poset.le ⟩
instance lt_inst {A : Type u} [Poset A] : LT A := ⟨ λ x y => x ≤ y ∧ x ≠ y ⟩

example {A : Type u} [Poset A] (x:A) := x ≥ x

Total Orders

A total order is a Poset with the added requirement that any two elements are comparable.

def Comparable {P : Type u} [Poset P] (x y: P) := x ≤ y ∨ y ≤ x

class TotalOrder (T: Type u) extends Poset T where
  comp: ∀ x y : T, Comparable x y

The natural numbers are a total order, which is shown via a theorem in Lean's standard library. :

instance nat_total_order : TotalOrder ℕ :=
  ⟨ Nat.le_total ⟩

Sets are not a total order, however.

example : ∃ x y : Set ℕ, ¬Comparable x y := by
  apply Exists.intro {1}
  apply Exists.intro {2}
  simp[Comparable]

(Meet) Semilattices

A Semilattice is a Poset for which there exists a greatest lower bound function, usually called meet, for every pair of points x and y. Then we extend the hierarchy with a new class of orders.

class Semilattice (L : Type u) extends Poset L where
  meet : L → L → L
  lb : ∀ x y, meet x y ≤ x ∧ meet x y ≤ y
  greatest : ∀ x y w, w ≤ x → w ≤ y → w ≤ meet x y

For example, the natural numbers form a semilattice. So do sets.

instance nat_semi_lattice : Semilattice ℕ :=
  ⟨
    Nat.min,
    by
      intro x y
      exact ⟨ Nat.min_le_left x y, Nat.min_le_right x y⟩,
    by
      intro x y _ h1 h2
      exact Nat.le_min_of_le_of_le h1 h2
  ⟩

instance set_semi_lattice {α : Type u}: Semilattice (Set α) :=
  ⟨
    Set.inter,
    by
      intro A B
      apply And.intro
      . intro x hx
        exact Set.mem_of_mem_inter_left hx
      . intro x hx
        exact Set.mem_of_mem_inter_right hx,
    by
      intro A B _ h1 h2 _ hc
      exact ⟨ h1 hc, h2 hc ⟩
  ⟩

Lattices

If all pairs of elements also have a least upper bound, then the Poset is called a Lattice. The least upper bound function is called the join.

class Lattice (L : Type u) extends Semilattice L where
  join : L → L → L
  ub : ∀ x y, (x ≤ join x y ∧ y ≤ join x y)
  least : ∀ x y w, x ≤ w → y ≤ w → join x y ≤ w

Both ℕ and Sets are Lattices as well. The joing for ℕ is Nat.max and the join for sets is Set.union.

instance nat_lattice : Lattice ℕ :=
  ⟨
    Nat.max,
    by
      intro x y
      exact ⟨ Nat.le_max_left x y, Nat.le_max_right x y ⟩,
    by
      intro x y _ h1 h2
      exact Nat.max_le_of_le_of_le h1 h2
  ⟩

instance set_lattice {α : Type u}: Lattice (Set α) :=
  ⟨
    Set.union,
    by
      intro A B
      . exact Set.union_subset_iff.mp (λ  _ a => a),
    by
      intro A B C h1 h2 c hc
      apply Or.elim hc
      . exact λ h3 => h1 h3
      . exact λ h3 => h2 h3
  ⟩

As an example of a semilattice that is not a lattice is the so-called information ordering on partial functions, decribed in a separate chapter.

Notation for Lattices

The meet and join of two elements x and y of a poset are denonted x ⊓ y and x sup y. The notation classes for these operations are called Min and Max, even though you do not have to use them for actual mins and maxes.

instance Semilattice.and_inst {L : Type u} [Semilattice L] : Min L :=
  ⟨ meet ⟩

instance Lattice.or_inst {L : Type u} [Lattice L] : Max L :=
  ⟨ join ⟩

Meet and Join Example Theorems

Here are two straightforward theorems about meets and joins that test out the definitions and notation. They follow from the definitions of greatest lower bound, least upper bound, anti-symmetry, and reflexivity.

theorem Semilattice.meet_idempotent {L : Type u} [Semilattice L] (x : L) : x ⊓ x = x := by
  have ⟨ h1, h2 ⟩ := lb x x
  have h4 := greatest x x x (Poset.refl x) (Poset.refl x)
  exact Poset.anti_sym (x ⊓ x) x h1 h4

theorem Lattice.join_idempotent {L : Type u} [Lattice L] (x : L) : x ⊔ x = x := by
  have ⟨ h1, h2 ⟩ := ub x x
  have h4 := least x x x (Poset.refl x) (Poset.refl x)
  apply Poset.anti_sym (x ⊔ x) x h4 h1

Complete Lattices

Lattices require that every pair of elements have a greatest lower bound and leaset upper bound. A Complete Lattice requires that every set have such bounds. An example of a Complete Lattice is Set A, which we show after defining Complete Lattices.

def IsLB {P : Type u} [Poset P] (S : Set P) (lb : P) := ∀ x ∈ S, lb ≤ x

class CompleteSemilattice (L : Type u) extends Poset L where
  inf : Set L → L
  lb : ∀ S, IsLB S (inf S)
  greatest : ∀ S w, (IsLB S w) → w ≤ inf S

def IsUB {P : Type u} [Poset P] (S : Set P) (ub : P) := ∀ x, x ∈ S → x ≤ ub

class CompleteLattice (L : Type u) extends CompleteSemilattice L where
  sup : Set L → L
  ub : ∀ S, IsUB S (sup S)
  least : ∀ S, ∀ w, (IsUB S w) → sup S ≤ w

Example: The set of subsets of a given set A is a complete lattice, which we show in two steps using straighforward proofs.

instance set_csl {A : Type u}: CompleteSemilattice (Set A) :=
  ⟨
    λ S => { x | ∀ T ∈ S, x ∈ T },
    by
      intro S T h x hx
      dsimp at hx
      exact hx T h,
    by
      intro S T h x hx R hR
      exact h R hR hx
  ⟩

instance set_cl {A : Type u}: CompleteLattice (Set A) :=
  ⟨
    λ S => { x | ∃ T ∈ S, x ∈ T },
    by
      intro S T h x hx
      apply Exists.intro T
      exact ⟨h, hx⟩,
    by
      intro S T h x hx
      dsimp at hx
      obtain ⟨ R, ⟨ h1, h2 ⟩ ⟩ := hx
      exact h R h1 h2
  ⟩

Complete Lattices are Bounded

Notice that in the definition of inf the condition (IsLB S w) in (IsLB S w)→ w ≤ inf S is trivially satisfied if S = ∅. Therefore, w ≤ inf ∅ for all w, meaning that inf ∅ is a top element. Similarly, sup ∅ is a bottom element. We can conclude that every Complete Lattice is bounded, as shown by the next two theorems.

@[simp]
def CompleteLattice.bot {L : Type u} [CompleteLattice L] : L :=
  sup (∅:Set L)

@[simp]
def CompleteLattice.top {L : Type u} [CompleteLattice L] : L :=
  CompleteSemilattice.inf (∅:Set L)

theorem CompleteLattice.is_bot {L : Type u} [CompleteLattice L]
  : ∀ x : L, bot ≤ x := by
  intro x
  apply CompleteLattice.least ∅ x
  simp[IsUB]

theorem CompleteLattice.is_top {L : Type u} [CompleteLattice L]
  : ∀ x : L, x ≤ top := by
  intro x
  apply CompleteSemilattice.greatest ∅ x
  simp[IsLB]

Complete Lattices are Lattices

We can also show that a complete lattice is a lattice by restricting inf and sup to act on sets of size two.

instance CompleteSemilattice.inst_sl {L : Type u} [CompleteSemilattice L]
  : Semilattice L := ⟨
    λ x y => inf {x,y},
    by
      intro x y
      apply And.intro <;>
      apply lb <;>
      simp,
    by
      intro x u z h1 h2
      apply greatest
      simp[IsLB, h1, h2]
  ⟩

instance CompleteLattice.inst_l {L : Type u} [CompleteLattice L]
  : Lattice L := ⟨
    λ x y => sup {x,y},
    by
      intro x y
      apply And.intro <;>
      apply ub <;>
      simp,
    by
      intro x u z h1 h2
      apply least
      simp[IsUB, h1, h2]
  ⟩

Hierarchy

     Lattice     CL
        |         |
    Semilattice  CSL   Total Order
             \    |    /
                Poset

UNDER CONSTRUCTION
Code for this chapter

Simple Properties

theorem eq_to_le {P : Type u} [Poset P] {x y : P} : x = y → x ≤ y := by
  intro h
  rw[h]
  exact refl y

Up Sets and Down Sets

The set of all elements above (below) a given element x:P is called the up (down) set of x.

def up {P : Type u} [Poset P] (x : P) : Set P := { y | x ≤ y }
def down {P : Type u} [Poset P] (x : P) : Set P := { y | y ≤ x }

A set that is upwardly (downwardly) closed is called an Up (Down) set. We define predicates on subsets of a Poset to capture these properties. These are a bit tricky to read. The first one says that if x is any element and there is a y in some upward closed set S that is less than or equal to it, then x must also be in S. The second statement about downward closed sets is similar.

def UpSet {P : Type u} [Poset P] (S : Set P) := ∀ x, (∃ y ∈ S, y ≤ x) → x ∈ S
def DownSet {P : Type u} [Poset P] (S : Set P) := ∀ x, (∃ y ∈ S, x ≤ y) → x ∈ S

Simple theorems relating these definitions can now be proved. The next two, for example, show that up (down) sets are upwardly (downwardly) closed.

theorem up_is_up {P : Type u} [Poset P] (x : P) : UpSet (up x) := by
  intro z ⟨ y, ⟨ h1, h2 ⟩  ⟩
  simp_all[Set.mem_def,up]
  exact trans x y z h1 h2

theorem down_is_down {P : Type u} [Poset P] (x : P) : DownSet (down x) := by
  intro z ⟨ y, ⟨ h1, h2 ⟩  ⟩
  simp_all[Set.mem_def,down]
  apply trans z y x h2 h1

Upward closed sets are not just those built from a single element. For example, the union of two upwardly closed sets is also upwardly closed.

theorem up_union {P : Type u} [Poset P] (x y: P) : UpSet ((up x) ∪ (up y)) := by
  intro w ⟨ z, ⟨ h1, h2 ⟩ ⟩
  apply Or.elim h1
  . intro h3
    exact Or.inl (trans x z w h3 h2)
  . intro h3
    apply Or.inr (trans y z w h3 h2)

Lower and Upper Sets

def upper {P : Type u} [Poset P] (A : Set P) : Set P :=
 { x | ∀ a ∈ A, a ≤ x }

def lower {P : Type u} [Poset P] (A : Set P) : Set P :=
 { x | ∀ a ∈ A, x ≤ a }

-- 1
theorem sub_ul {P : Type u} [Poset P] (A : Set P)
  : A ⊆ upper (lower A) := by
  intro x hx a ha
  exact ha x hx

theorem sub_lu {P : Type u} [Poset P] (A : Set P)
  : A ⊆ lower (upper A) := by
  intro x hx a ha
  exact ha x hx

theorem eq_to_sub {P : Type u} [Poset P] (A : Set P)
  : lower (upper A) ⊆ A → lower (upper A) = A := by
  intro h
  exact Set.eq_of_subset_of_subset h (sub_lu A)

-- 2
theorem sub_up {P : Type u} [Poset P] {A B : Set P}
  : A ⊆ B → upper B ⊆ upper A := by
  intro h b hb a ha
  exact hb a (h ha)

-- 3
theorem sub_low {P : Type u} [Poset P] {A B : Set P}
  : A ⊆ B → lower B ⊆ lower A := by
  intro h b hb a ha
  exact hb a (h ha)

-- 4
theorem up_ulu {P : Type u} [Poset P] {A : Set P}
 : upper A = upper (lower (upper A)) := by
 apply Set.eq_of_subset_of_subset
 . intro a ha b hb
   exact hb a ha
 . intro a ha b hb
   exact ha b fun a a ↦ a b hb

-- 5
theorem low_lul {P : Type u} [Poset P] {A : Set P}
 : lower A = lower (upper (lower A)) := by
 apply Set.eq_of_subset_of_subset
 . intro a ha b hb
   exact hb a ha
 . intro a ha b hb
   exact ha b fun a a ↦ a b hb

Minimal and Maximal Elements

A minimal element of a set S ⊆ P is one for which no other elements of S are smaller.

def Minimal {P : Type u} [Poset P] (S : Set P) (m : P) := ∀ x ∈ S, x ≤ m → x = m

Minimal elements are not necessarily unique. The following example shows that when x and y are unrelated, either one of them is minimal.

example {P : Type u} [Poset P] (x y: P) : (¬x≤y ∧ ¬y≤x) → Minimal {x,y} x := by
  intro ⟨h1, h2⟩ z h3 h4
  apply Or.elim h3
  . exact id
  . intro h5
    rw[h5] at h4
    exact False.elim (h2 h4)

On the other hand, a minimum element is a unique minimal element.

def Minimum {P : Type u} [Poset P] (S : Set P) (m : P) := ∀ x ∈ S, m ≤ x

The most minimal element of a Poset is usually called bot.

def is_bot {P : Type u} [Poset P] (x : P) := ∀ y, x ≤ y

theorem bot_minimum {P : Type u} [Poset P] (m : P) : is_bot m → Minimum Set.univ m := by
  intro hb x hm
  simp_all[is_bot]

These definitions apply to maxima as well.

def Maximal {P : Type u} [Poset P] (S : Set P) (m : P) := ∀ x ∈ S , m ≤ x → x = m
def Maximum {P : Type u} [Poset P] (S : Set P) (m : P) := ∀ x ∈ S, x ≤ m
def is_top {P : Type u} [Poset P] (x : P) := ∀ y, y ≤ x

Chains and Anti-Chains

A chain is a totally ordered subset of a poset.

def Chain {P : Type u} [Poset P] (S : Set P) := ∀ x ∈ S, ∀ y ∈ S, x ≤ y ∨ y ≤ x

For example, the upset of any natural number is a chain.

example {n : ℕ} : Chain (up n) := by
  intro x hx y hy
  exact Nat.le_total x y

An antichain is a set of uncomparable elements.

def AntiChain {P : Type u} [Poset P] (S : Set P) := ∀ x ∈ S, ∀ y ∈ S, x ≠ y → (¬x ≤ y ∧ ¬y ≤ x)

For example, the set of singletons each containing a different natural number is an anti-chain.

def my_anti_chain : Set (Set ℕ) := { {n} | n : ℕ }

example : AntiChain my_anti_chain := by
  simp[my_anti_chain]
  intro Sm ⟨ m, hsm ⟩ Sn ⟨ n, hsn ⟩ hmn
  simp[le_inst]
  apply And.intro
  . intro h
    rw[←hsm,←hsn] at h
    rw[←hsm,←hsn] at hmn
    exact hmn (congrArg singleton (h rfl))
  . intro h
    rw[←hsm,←hsn] at h
    rw[←hsm,←hsn] at hmn
    exact id (Ne.symm hmn) (congrArg singleton (h rfl))

Exercises

1. Show the rational numbers ℚ with the natural order ≤ form a Poset

instance : Poset ℚ := ⟨ λ x y => x ≤ y, sorry, sorry, sorry ⟩

2. Show the upper set (0,1) is [1,∞)

example : upper {x:ℚ | 0 < x ∧ x < 1} = { x | 1 ≤ x } := sorry

UNDER CONSTRUCTION
Code for this chapter

Maps Between Posets

def OrderPreserving {P Q : Type u} [Poset P] [Poset Q] (φ : P → Q) :=
  ∀ x y : P, x ≤ y → φ x ≤ φ y

def OrderEmbedding {P Q : Type u} [Poset P] [Poset Q] (φ : P → Q) :=
  ∀ x y : P, x ≤ y ↔ φ x ≤ φ y

def OneToOne {P Q : Type u} (φ : P → Q) :=
  ∀ x y , φ x = φ y → x = y

def Onto {P Q : Type u} (φ : P → Q) :=
  ∀ y , ∃ x , φ x = y

def OrderIsomorphism {P Q : Type u} [Poset P] [Poset Q] (φ : P → Q) :=
  Onto φ ∧ OrderEmbedding φ

theorem order_pres_comp {P Q R : Type u} [Poset P] [Poset Q] [Poset R] (φ : P → Q) (ψ : Q → R)
  : OrderPreserving φ → OrderPreserving ψ → OrderPreserving (ψ ∘ φ) := by
  intro h1 h2 x y hxy
  apply h2 (φ x) (φ y)
  apply h1 x y
  exact hxy

theorem order_embed_1to1 {P Q : Type u} [Poset P] [Poset Q] (φ : P → Q)
  : OrderEmbedding φ → OneToOne φ := by
  intro h x y hxy
  apply anti_sym
  . apply (h x y).mpr
    exact eq_to_le hxy
  . apply (h y x).mpr
    exact eq_to_le (Eq.symm hxy)

theorem order_iso_bijective {P Q : Type u} [Poset P] [Poset Q] (φ : P → Q)
  : OrderIsomorphism φ → (OneToOne φ ∧ Onto φ) := by
  intro ⟨ h1, h2 ⟩
  exact ⟨ order_embed_1to1 φ h2, h1 ⟩

Examples

example : OrderPreserving (λ _ : ℕ => 0) := by
  intro x y h
  dsimp
  rfl

def f (n:ℕ) : Set ℕ := { x | x ≤ n }

example : OrderEmbedding f := by
  intro x y
  constructor
  . intro h
    intro z hz
    exact trans z x y hz h
  . intro h
    simp[f] at h
    exact h x (Poset.refl x)

def g (x : ℕ) : ℕ := 2*x

example : OrderEmbedding g := by
  intro x y
  constructor
  . intro h
    simp[g]
    exact h
  . intro h
    simp[g] at h
    exact h

UNDER CONSTRUCTION
Code for this chapter

Strings

open List

Note that List already have an ordering on them, but it is not the prefix ordering. This creates issues because List.le and [LT (List A)] are already defined. We avoid this here by just not using the ≤ notation.

#check List.le
variable {A : Type u} (x : List A) [LT A]
#check [] ≤ x
#eval [1,2,3] ≤ [1,2,5]
example {A : Type u} [LT A] (x : List A) : [] ≤ x := by
  simp[List.instLE]

End Note

instance list_poset {A : Type u} : Poset (List A) :=
  ⟨
    IsPrefix,
    List.prefix_refl,
    by
      intro s t ⟨ x, h1 ⟩ ⟨ y, h2 ⟩
      aesop,
    by
      intro s t u
      exact List.IsPrefix.trans
  ⟩

example {A : Type u} (x : List A) : [] <+: x := by
  simp[list_poset]

def meet {A : Type u} [Poset (List A)] [DecidableEq A] (x y : List A) : List A :=
  match x,y with
  | [], [] => []
  | _, [] => []
  | [], _ => []
  | a::L, b::M => if a = b then a :: meet L M else []

theorem bot_le {A : Type u} [Poset (List A)] (x: List A) : [] <+: x := by
  exact nil_prefix

theorem meet_le {A : Type u} [Poset (List A)] [DecidableEq A] (x y : List A)
  : (meet x y) <+: x := by
  match x,y with
  | a::L, b::M =>
    simp[meet]
    split_ifs
    . have : IsPrefix (meet L M) L := by apply meet_le -- structural recursion!
      simp[this]
    . apply bot_le
  | [], [] => simp[meet]
  | a::L, [] => simp[meet]
  | [], b::M => simp[meet]

theorem meet_le' {A : Type u} [Poset (List A)] [DecidableEq A] (x y : List A)
  : (meet x y) <+: y := by
  match x,y with
  | a::L, b::M =>
    simp[meet]
    split_ifs
    . have : IsPrefix (meet L M) M := by apply meet_le' -- structural recursion!
      simp[this]
      assumption
    . apply bot_le
  | [], [] => simp[meet]
  | a::L, [] => simp[meet]
  | [], b::M => simp[meet]

theorem meet_great {A : Type u} [Poset (List A)] [DecidableEq A] (x y : List A)
  : ∀ w, w <+: x → w <+: y → w <+: (meet x y) := by
  intro w hwx hwy
  match x, y with
  | a::L, b::M =>
    simp[meet]
    split_ifs
    . rename_i hab
      simp_all[hab]
      by_cases hw : w = []
      . simp[hw]
      . obtain ⟨ c, ⟨ N, hcN ⟩ ⟩ := ne_nil_iff_exists_cons.mp hw
        simp_all[hcN]
        apply meet_great -- structural recursion!
        . exact hwx.right
        . exact hwy
    . rename_i hab
      have : w = [] := by
        by_cases h : w = []
        . exact h
        . have ⟨ c, ⟨ N, hN ⟩ ⟩ : ∃ c, ∃ N, w = c :: N := ne_nil_iff_exists_cons.mp h
          have h1 : c = a := by simp_all[hN]
          have h2 : c = b := by simp_all[hN]
          simp_all
      simp[this]
  | [], [] => simp[meet,hwx]
  | a::L, [] => simp[meet,hwy]
  | [], b::M => simp[meet,hwx]

instance info_semilattice {A : Type u} [DecidableEq A] : Semilattice (List A) :=
  ⟨
    meet,
    λ L M => by
      constructor
      . constructor
        . apply meet_le
        . apply meet_le'
      . apply meet_great
  ⟩

UNDER CONSTRUCTION
Code for this chapter

Information Ordering on Values

def PartialFunction (A : Type u) (B : Type v) := A → Option B

namespace PartialFunction

def val_le (B : Type u) (u v : Option B) := u = none ∨ u = v

theorem val_le_refl {B : Type u} : Refl (val_le B) := by
  simp[Refl,val_le]

theorem val_le_anti_sym {B : Type u} : AntiSym (val_le B) := by
  intro x y h1 h2
  simp_all[val_le]
  aesop

theorem val_le_trans {B : Type u} : Trans (val_le B) := by
  intro x y z h1 h2
  simp_all[val_le]
  aesop

@[simp]
instance poset_val_le {B : Type u} : Poset (Option B) :=
  ⟨ val_le B, val_le_refl, val_le_anti_sym, val_le_trans ⟩

theorem none_val_le {B : Type u} : ∀ x : Option B, none ≤ x := by
  intro x
  have : val_le B none x := by simp[val_le]
  simp[Poset.le_inst,val_le]

def Dom {A : Type u} {B : Type v} (f: PartialFunction A B) : Set A := λ a => f a ≠ none

def le {A : Type u} {B : Type v} : Relation (PartialFunction A B) (PartialFunction A B) :=
  λ f g => ∀ x, (f x) ≤ (g x)


def bot {A : Type u} {B : Type v} : PartialFunction A B := λ _ => none

theorem le_refl {A : Type u} {B : Type v} : Refl (@le A B) := by
  intro x h
  apply val_le_refl

theorem le_anti_sym {A : Type u} {B : Type v} : AntiSym (@le A B) := by
  simp[AntiSym]
  intro f g hf hg
  funext x
  apply val_le_anti_sym
  . exact hf x
  . exact hg x

theorem le_trans {A : Type u} {B : Type v} : Trans (@le A B) := by
  simp[Trans]
  intro f g h hf hg
  simp[le]
  intro x
  apply val_le_trans
  . exact hf x
  . exact hg x

instance poset_le (A : Type u) (B : Type v): Poset (PartialFunction A B) :=
  ⟨ le, le_refl, le_anti_sym, le_trans ⟩

theorem le_def {A : Type u} {B : Type v} (f g: PartialFunction A B)
  : f ≤ g ↔ ∀ x, f x ≤ g x := by
  simp[le_inst, Poset.le, le, val_le]

theorem le_total_def {A : Type u} {B : Type v} (f g: PartialFunction A B)
  : f ≤ g ↔ ∀ x, f x = none ∨ f x = g x := by
  simp[le_inst, Poset.le, le, val_le]

theorem bot_le_all {A : Type u} {B : Type v} (f: PartialFunction A B) : bot ≤ f := by
  intro x
  simp[val_le,bot,Poset.le_inst]

theorem le_dom {A : Type u} {B : Type v} {f g : PartialFunction A B} :
  f ≤ g ↔ (Dom f ⊆ Dom g ∧ ∀ x ∈ Dom f, f x = g x):= by
  constructor
  . intro h
    constructor
    . intro a ha
      have := h a
      simp_all[Set.mem_def,Dom,val_le,Poset.le_inst]
    . intro a ha
      have := h a
      simp_all[Set.mem_def,Dom,Poset.le,val_le,le,Poset.le_inst]
  . intro ⟨ h1, h2 ⟩
    intro a
    have := h2 a
    simp_all[Set.mem_def,Dom,Poset.le,val_le,le]
    by_cases h3 : f a = none
    . exact Or.inl h3
    . apply Or.inr
      exact this h3

example (A : Type u) (B : Type v) (f : PartialFunction A B) : f ≤ f := by apply Poset.refl

Total Information Elements

def Total {A : Type u} {B : Type v} (f : PartialFunction A B) := ∀ x, f x ≠ none

theorem total_le {A : Type u} {B : Type v} {f g : PartialFunction A B}
  : Total f → Poset.le f g → f = g := by
  simp[Total,Poset.le]
  intro h hfg
  funext x
  have h1 := h x
  have h2 := hfg x
  simp_all[val_le,Poset.le,Poset.le_inst]

Information Ordering is a Lattice

def meet {A : Type u} {B : Type v} [DecidableEq B] (f g : PartialFunction A B) :=
  λ a => if f a = g a then f a else none

theorem meet_symm {A : Type u} {B : Type v} [DecidableEq B] {f g : PartialFunction A B}
  : meet f g = meet g f := by
  unfold meet
  aesop

theorem pf_meet_le {A : Type u} {B : Type v} [DecidableEq B] {f g : PartialFunction A B} :
  (meet f g) ≤ f := by
  intro a
  simp[meet]
  split_ifs <;>
  simp[val_le,Poset.le_inst]

theorem pf_meet_le' {A : Type u} {B : Type v} [DecidableEq B] {f g : PartialFunction A B} :
  le (meet f g) g := by
  rw[meet_symm]
  exact pf_meet_le

theorem pf_meet_greater {A : Type u} {B : Type v} [DecidableEq B] {f g : PartialFunction A B} :
  ∀ w, le w f → le w g → le w (meet f g) := by
  intro w h1 h2 a
  simp[meet,val_le]
  split_ifs
  . exact h1 a
  . simp[Poset.le_inst,Poset.le,val_le,Poset.le_inst]
    apply Or.elim (h2 a)
    . exact id
    . intro h3
      cases h1 a with
      | inl h => simp_all
      | inr h => simp_all

instance info_semilattice {A : Type u} {B : Type v} [DecidableEq B] : Semilattice (PartialFunction A B) :=
  ⟨
    meet,
    λ _ _ => ⟨ ⟨ pf_meet_le, pf_meet_le' ⟩, pf_meet_greater ⟩
  ⟩

end PartialFunction

UNDER CONSTRUCTION
Code for this chapter

The Dedekind-MacNeille Completion

A completion is an embedding of a partially ordered set into a complete lattice. It allows one to "fill in the gaps" in an ordered set so that, for example, limit points exist. The real numbers, for example, are the completion of the rational numbers.

In this chapter we describe the the Dedekind-MacNeille (DM) Completion, which is a generalization of the Dedekind cuts method of constructing the reals to the case of any ordered set. In particular, we define DM P for any poset P. If P=ℚ, the result is isomorphic to the reals with -∞ and ∞, but the approach works for any poset.

Formally, the Dedekind-MacNeille completion DM P is defined to be the family of subsets of S ⊆ P that are closed with respect to the closure operator λ P ↦ lower (upper P).

@[ext]
structure DM (P : Type u) [Poset P] where
  val : Set P
  h : lower (upper val) = val

Our goal is to show that DM P is a complete lattice for any P. We can easily show that DM P is a poset under the usual ⊆ ordering.

instance DM.poset {P : Type u} [Poset P] : Poset (DM P) :=
  ⟨
    λ ⟨ A, hA ⟩ ⟨ B, hB ⟩ => A ⊆ B,
    by
      intro ⟨ A, _ ⟩
      exact Set.Subset.refl A,
    by
      intro ⟨ A, hA ⟩ ⟨ B, hB ⟩ h1 h2
      simp_all
      exact Set.Subset.antisymm h1 h2,
    by
      intro ⟨ A, hA ⟩ ⟨ B, hB ⟩ ⟨ C, hC ⟩ h1 h2
      exact Set.Subset.trans h1 h2
  ⟩

In fact, the DM structure forms what Davey and Priestly call a topped intersection structure, which we will show is a Complete Lattice with a particular definition for the meet and join that we define next.

The Meet

We define a meet for DM P, which is just set-intersection taken over a subset of DM P.

$$ \mathrm{meet}(S) = \bigcap_{A ∈ S} A. $$

To prove this definition of meet gives DM P a semilattice structure, we have to show the result of such an intersection satisfies the upper-lower condition. First we define the intersection of a subset of DM P (i.e. of a set of sets taken from DM P).

def DM.inter {P : Type u} [Poset P] (S : Set (DM P)) := { x | ∀ T ∈ S, x ∈ T.val }

We will need to use the simple fact that the interection of a family ot sets is a subset of every member of the family.

theorem DM.inter_sub {P : Type u} [Poset P] {S : Set (DM P)}
  : ∀ T ∈ S, inter S ⊆ T.val := by
  intro T hT x hx
  exact hx T hT

Using this fact, we can show the intersection preserves the lower-upper property required of elements of DM P.

theorem DM.inter_in_dm {P : Type u} [Poset P] {S : Set (DM P)}
  : lower (upper (inter S)) = inter S := by
    apply Set.eq_of_subset_of_subset
    . intro x hx T hT
      rw[←T.h]
      exact sub_low (sub_up (inter_sub T hT)) hx
    . exact sub_lu (inter S)

And with this theorem we can finally define the meet as a function from Set (DM P) into DM P. Recall, that to do so we need to not only supply the operation inter on S, but also proof that inter S is in DM P.

def DM.meet {P : Type u} [Poset P] (S : Set (DM P)) : DM P :=
  ⟨ inter S, inter_in_dm ⟩

To show that DM P is a Complete Semilattice, we need to show that this definition of meet is indeed a greatest lower bound. We do so in two steps, first showing the meet S is a lower bound of S and second showing it is a greatest lower bound of S.

theorem DM.meet_lb {P : Type u} [Poset P] :
  ∀ S : Set (DM P), IsLB S (meet S) := by
  intro S T hT
  apply DM.inter_sub
  exact hT

theorem DM.meet_greatest {P : Type u} [Poset P]
  : ∀ S : Set (DM P), ∀ w, (IsLB S w) → w ≤ meet S := by
  intro S W h
  intro x hx T hT
  exact h T hT hx

Now we have everything we need to instantiate the Complete Semilattice class.

instance DM.csl {P : Type u} [Poset P] : CompleteSemilattice (DM P) :=
  ⟨ meet, meet_lb, meet_greatest ⟩

The Join

Next we define a join. It would be nice to simply define the join of S to be the union of all sets in S, but the result would in general not be closed with respect to the lower-upper operator used to define DM P. To get around this, the join for DM P is defined to be the intersection of sets containing the union.

$$ \mathrm{join}(S) = \bigcap \left \{ B \in DM(P) \;|\; \bigcup_{A ∈ S} A \subseteq B \right \} $$

First we define the union.

def DM.union {P : Type u} [Poset P] (S : Set (DM P)) := { x | ∃ T ∈ S, x ∈ T.val }

We will need an intermediate theorem analogous to the intersection theorem proved for the meet. This one shows that the intersection of a set of sets is contained in each set.

theorem DM.inter_union_dm {P : Type u} [Poset P] {S : Set (DM P)}
  : ∀ C ∈ {C : DM P| union S ⊆ C.val}, inter {C | union S ⊆ C.val} ⊆ C.val := by
    intro C hC x hx
    exact hx C hC

We use this theorem to show the meet is closed.

theorem DM.union_in_dm {P : Type u} [Poset P] {S : Set (DM P)}
  : lower (upper (inter {C | union S ⊆ C.val})) = inter {C | union S ⊆ C.val} := by
  apply Set.eq_of_subset_of_subset
  . intro x hx T hT
    rw[←T.h]
    exact sub_low (sub_up (inter_union_dm T hT)) hx
  . apply sub_lu

The join operator is then be defined as follows.

def DM.join {P : Type u} [Poset P] (S : Set (DM P)) : DM P :=
  ⟨ inter { C | union S ⊆ C.val }, union_in_dm ⟩

To show DM P is a Complete Lattice, we need to show the join is a least upper bound, which we do in two steps.

theorem DM.join_ub {P : Type u} [Poset P] :
  ∀ S : Set (DM P), IsUB S (join S) := by
  intro S T hT x hx W hW
  simp[union,Set.subset_def] at hW
  exact hW x T hT hx

theorem DM.join_least {P : Type u} [Poset P]
  : ∀ S : Set (DM P), ∀ W, (IsUB S W) → join S ≤ W := by
  intro S W h x hx
  apply hx W
  intro y ⟨ Q, ⟨ h1, h2 ⟩ ⟩
  exact h Q h1 h2

Now we have everything we need to show DM P is a Complete Lattice.

instance DM.lattice {P : Type u} [Poset P] : CompleteLattice (DM P) :=
  ⟨ join, join_ub, join_least ⟩

Completion Map

The mapping from P into DM P is defined implicitly in the construction of DM P. Explicitly, the embedding is definition by the down operator. That is, the map λ x ↦ down x is the ordering embedding that wintesses the completion. To show this, we prove that down x is closed under the lower-upper closure operator.

theorem DM.down_is_dm {P : Type u} [Poset P] {x : P}
  : lower (upper (down x)) = down x :=
  by
    apply Set.eq_of_subset_of_subset
    . intro y hy
      exact hy x fun a a ↦ a
    . intro a ha
      simp_all[upper,lower]

This theorem then allows us to formally define the embedded. We call it make, because it allows us to make an element of DM P out of any element x ∈ P.

def DM.make {P : Type u} [Poset P] (x : P) : DM P := ⟨ down x, down_is_dm ⟩

Finally, we prove that make is an order embeddeding (as defined in Maps).

theorem DM.make_embed {P : Type u} [Poset P]
  : OrderEmbedding (make : P → DM P) := by
  intro x y
  constructor
  . intro h z hz
    exact Poset.trans z x y hz h
  . intro h
    simp[make,down,le_inst,Poset.le] at h
    exact h x (Poset.refl x)

Completion of a Total Order

If P is a totally ordered set, then its completion ought to be totally ordered as well. We show that here. We start with a useful theorem stating the fact that all elements of DM P are downward closed.

theorem dm_down_close {P : Type u} [Poset P] {X : DM P}
  : ∀ y, ∀ x ∈ X.val, y ≤ x → y ∈ X.val := by
  intro y x hx hyx
  rw[←X.h] at hx ⊢
  intro z hz
  apply Poset.trans y x z hyx (hx z hz)

Now we show the main result.

theorem dm_total_order {P : Type u} [TotalOrder P]
  : ∀ (x y : DM P), Comparable x y := by

  intro X Y
  by_cases h : X.val ⊆ Y.val

  . exact Or.inl h

  . -- Obtain an x in X - Y
    obtain ⟨ x, ⟨ hx, hxny ⟩ ⟩ := Set.not_subset.mp h

    -- Show y ≤ x using the fact that Y is closed
    rw[←Y.h] at hxny
    simp[lower] at hxny
    obtain ⟨ y, ⟨ hy, hcomp ⟩ ⟩ := hxny
    have hyx : y ≤ x := by
      apply Or.elim (TotalOrder.comp x y)
      . intro h
        exact False.elim (hcomp h)
      . exact id

    -- Show Y ⊆ down x using transitivity of ≤ in P
    have hYdx : Y.val ⊆ down x := by
      intro b hb
      exact Poset.trans b y x (hy b hb) hyx

    -- Show down x ⊆ X using the helper theorem above
    have hdxX: down x ⊆ X.val := by
      intro b hb
      exact dm_down_close b x hx hb

    -- Show Y ⊆ X using transitivity of ⊆
    apply Or.inr
    intro q hq
    exact hdxX (hYdx hq)

Using this theorem, we can instantiate the total order class for DM P for any totally ordered P.

instance {P : Type u} [TotalOrder P] : TotalOrder (DM P) := ⟨ dm_total_order ⟩

We can show a useful theorem stating that every element besides top has a principal upper bound.

theorem DM.not_top_is_bounded {P : Type u} [Poset P] {x : DM P}
  : x ≠ CompleteLattice.top → ∃ q : P, x ≤ DM.make q := by
  intro h

  have h1 : x.val ≠ Set.univ := by
    by_contra h2
    simp[CompleteLattice.top,CompleteSemilattice.inf,DM.meet,DM.inter,DM.ext] at h
    apply h (DM.ext h2)

  have ⟨ q, hq ⟩ : ∃ q, q ∈ Set.univ \ x.val := by
    by_contra h
    simp at h
    exact h1 (Set.eq_univ_iff_forall.mpr h)

  have h2 : ¬q ∈ x.val := by exact Set.not_mem_of_mem_diff hq

  rw[←x.h] at h2
  simp[upper,lower] at h2
  obtain ⟨ r, ⟨ hr, hrq ⟩ ⟩ := h2

  use r
  simp[DM.make,down,le_inst,Poset.le]

  intro y hy
  simp
  exact hr y hy

We can also show that every element besides bot is non-empty.

theorem DM.not_bot_to_exists {P : Type u} [Poset P] {x : DM P}
  : x ≠ CompleteLattice.bot → ∃ v, v ∈ x.val := by
  intro h
  apply Set.nonempty_iff_ne_empty.mpr
  intro hxb
  simp[CompleteLattice.bot,CompleteLattice.sup,DM.join,DM.inter,DM.union] at h
  have : {x | ∀ (T : DM P), x ∈ T.val} = ∅ := by
    ext q
    constructor
    . simp
      by_contra hn
      simp at hn
      have := hn x
      simp_all[Set.mem_empty_iff_false]
    . simp

  simp[this] at h
  exact h (DM.ext hxb)

Examples

A Finite Example

namespace Temp

inductive MyPoset where
  | a : MyPoset
  | b : MyPoset

open MyPoset

def myle (x y : MyPoset) := x = y

instance : Poset MyPoset :=
  ⟨ myle, by simp[myle], by simp[myle], by simp[myle] ⟩

theorem my_poset_all {x : MyPoset} : x ∈ ({a, b}: Set MyPoset) := by
  match x with
  | a => exact Set.mem_insert a {b}
  | b => exact Set.mem_insert_of_mem a rfl

def top : DM MyPoset := ⟨
  { a, b },
  by
    apply Set.eq_of_subset_of_subset
    . intro x h
      exact my_poset_all
    . intro x hx
      simp[lower,upper]
      intro y h1 h2
      match x with
      | a => exact h1
      | b => exact h2
  ⟩

def bot : DM MyPoset := ⟨
  ∅,
  by
    apply Set.eq_of_subset_of_subset
    . intro x hx
      simp[lower,upper] at hx
      have h1 := hx a
      have h2 := hx b
      rw[h1] at h2
      apply noConfusion h2
    . exact Set.empty_subset (lower (upper ∅))
⟩

example : ∃ b : DM MyPoset, ∀ x, b ≤ x := by
  use bot
  intro S y hy
  exact False.elim hy

end Temp

Exercises

1. Show DM ℕ is isomorphic to ℕ ∪ {∞} where x ≤ ∞ for all x.

UNDER CONSTRUCTION
Code for this chapter

Useful Theorems

theorem not_empty_to_exists {A : Type u} {S : Set A} : S ≠ ∅ → ∃ x, x ∈ S := by
   intro h
   by_contra h'
   simp at h'
   exact h (Set.eq_empty_iff_forall_not_mem.mpr h')

theorem not_full_to_not_exists {A : Type u} {S : Set A}
  : S ≠ Set.univ → ∃ x, x ∉ S := by
  intro h
  exact (Set.ne_univ_iff_exists_not_mem S).mp h

theorem not_empty_set_diff {A : Type u} {X Y : Set A} (h : ¬X ⊆ Y)
  : X \ Y ≠ ∅ := by
  simp[Set.instSDiff,Set.diff]
  by_contra hx
  simp at hx
  exact h hx

theorem remove_set_notation {T : Type*} (A : Set T) (f : T → Prop)
  : { x | f x } = A ↔ ∀ x, x ∈ A ↔ f x := by
  constructor
  . exact fun a x ↦ Iff.symm (Eq.to_iff (congrFun a x))
  . exact fun a ↦ Eq.symm (Set.ext a)