-- Ignore the next line if this is the first time you learn Lean.

import LeanFoundations._MyTactics

In this file, we basically have two things: formal Lean code and comments. Lean code is just what it is called and comments are lines of natural language encompassed in /- -/

Though to write a Lean program only requires Lean code, sometimes it is helpful to explain them in natural language. In fact, this file is written as it is a book, where most lines are comments with relatively less Lean code.

Besides, /-! -/ is used for markdown display, i.e., we can have headers(#), citations(>), etc. And /-- -/ is used for DocString (you will figure it out later by hovering the cursor on some term). Another variant of comment is -- followed by a newline. For example

-- this is a comment.

Functional Programming in Lean #

The core of modern computer proof assistants is type theory (λ-calculus), i.e. functional programming. This chapter is intended to introduce some basics about functional programming in Lean. In (dependent) type theory, we give a lot of rules to determine valid judgements term: type. Functions are just a special rule to form a certain type, and proofs are just the judgement proof: proposition, as is the Curry-Howard correspondence. This chapter will show you (some of) those rules, and you will learn more of them gradually later in the following chapters. You will find that programming languages based on type theory have only a few core features (axioms in meta language). All you need for logic can be built from scratch within these features.

Enumerated Types #

Our first example is to define a finite type. Just like defining a finite set, you can define a type by enumerating all possible members. The keyword to define a type is inductive. (You can tell why it is called inductive if you have learned some type theory; otherwise, just accept that as a name.)

The following says we are going to define a new type Day with members Sunday: Day, Monday: Day, etc. You may think of this as Sunday, Monady, ... ∈ Day just like a set.

inductive Day where
  | Monday: Day
  | Tuesday: Day
  | Wednesday: Day
  | Thursday -- the `: Day` can be omitted since it can be infered from the context
  | Friday
  | Saturday | Sunday -- you can write these constructors in one line

As in set theory, things we concern are approximately series of judgements e1 ∈ S1, e2 ∈ S2, ... Each of them is either an allowed construstion (axiom) or the consequence of some logical inference. In type theory, the judgements are of the form t: A, and inductive is one way to extend the judgement rules. : can be considered as the relation on terms and types freely generated by those rules. In this case, the relation : Day is freely generated by constructors Monday, Tuesday, Wednesday, etc.

We are then able to check the newly defined type by

#check Day.Sunday
#eval Day.Sunday

If you then run command lake build, you can see the following output.

info: ././././LeanFoundations/Logic/Basic.lean:line_number1:0: Day.Sunday : Day
info: ././././LeanFoundations/Logic/Basic.lean:line_number2:0: Day.Sunday

Namespaces #

You may have noticed that we have actually defined Day.Sunday: Day. To access the term Sunday, we have to write Day.Sunday. This Day acts as a namespace so that if we have another type with the same constructor names, we won't fall into a name conflict.

inductive Weekend: Type where
  | Sunday
  | Saturday


#check Weekend.Sunday

If you want to use those names in a namespace directly, you can open it

open Weekend

#check Sunday

Namespaces can also be defined manually. This is helpful if you want to define something with existing names. For example, Lean has provided the type Bool with constructors true and false. To show you how to define it from scratch, I have to define my own Bool using a different name MyBool, or I can use a namespace to avoid it.

inductive MyBool where
  | true
  | false

namespace scratch
inductive Bool where
  | true | false

end scratch

Another application is to define the classical logic. As you may have known, Curry-Howard correspondence is proved for intuitionistic logic. But you may want to use law of excluded middle since we have the double negation monad (Glivenko's theorem) embedding classical logic in intuitionistic logc. We can put those classical axioms in a namespace to use them if necessary.

Lean also provides such a namespace called Classical, and Lean is classical by default, even if you don't open the Classical namespace.

namespace classical
axiom em: forall (p: Prop), p ∨ ¬ p

end classical

Section #

After you open a namespace, you are unable to close it. To limit the side effect of an open, you can put it inside a section.

section

open scratch

-- do something with scratch

#check Bool
end

You can also give a name to a section

section WeNeedScratchHere

open scratch

-- do something with scratch

#check Bool
end WeNeedScratchHere

Define functions by case analysis #

Now we know how to define a type by enumerating. Then a natural way to define a function out of an enumerated type is to define a value for each case of it. This is known as case analysis (proof by cases).

We want to define a funciton next_weekday : Day -> Day. Apparently, we want to map Day.Monday to Day.Tuesday, Day.Tuesday to Day.Wednesday, etc. We have to notice two things here:

1. how to define a function;
2. how to do case analysis.

In type theory, to define a function, we use the λ-abstraction. For example, to define a quadratic function \(f: \mathbb{R} \to \mathbb{R}\), we may write \(f(x) = x^2\). Here, \(f\) is itself a function, which does not depend on the name of the dummy variable \(x\), e.g., \(f(y)=y^2\) is the same function. So, a better way to think of it is \(f := x \mapsto x ^ 2\). The := is to emphasize this is a definition. Later, this was written as \(\hat{x}.x^2\) by Whitehead and Russell, and Church chose \(\lambda x. x^2\) as the final notation. This way to define a function is called λ-abstraction.

In Lean, we also define functions in this style. Besides, you also specify the type for each term. In the above example, \(\mathbb{R}\) is the type of real numbers with rules \(0,1,2:\mathbb{R}\), and given \(x: \mathbb{R}\), \(x^2: \mathbb{R}\). Then, \(λx.x^2: \mathbb{R} \to \mathbb{R}\) is the rule to construct a function as well as its type.

So, the next_weekday is some λ (w: Day). if w matches Monday, then Tuesday; ... In Lean, we write it as follows.

def next_day: Day -> Day := λ (w: Day) =>
  match w with
  | Day.Sunday => Day.Monday
  | Day.Monday => Day.Tuesday
  | .Tuesday => .Wednesday  -- we can omit Day.
  | .Wednesday => .Thursday
  | .Thursday => .Friday
  | .Friday => .Saturday
  | .Saturday => .Sunday

λ-abstraction is defined using λ variable => term unlike the usual λ x . M as in many text books.

To type the λ in the text editor VSCode, type \lambda and it will change that to λ. If you don't remember this, then hover your cursor over the λ and VSCode will tell you how to type it.

Or if you don't like non-ASCII characters, use fun variable => term instead.

def next_day_using_func: Day -> Day := fun (w: Day) =>
  match w with
  | Day.Sunday => Day.Monday
  | Day.Monday => Day.Tuesday
  | .Tuesday => .Wednesday  -- we can omit Day.
  | .Wednesday => .Thursday
  | .Thursday => .Friday
  | .Friday => .Saturday
  | .Saturday => .Sunday

If you want to apply the function to some term, just type fun term. For example, To test the function next_day,

#eval (next_day Day.Sunday)

Currying #

The above function is defined only for one variable. In set theory, a function for two variables is defined as \(f: A \times B \to C\). This can also be interpreted by the exponential rule: for each \(a \in A\), \(f(a)\) is a function \(B \to C\), i.e., we many instead define \(f: A \to (B \to C)\). This behavior is called currying, which is adopted by type theory as the definition of multi-variable functions.

If we make the convention that \(\to\) is right associative, we can simply write it as \(f: A \to B \to C\). For example, we can check whether two days of a week are equal.

def day_eq_b: Day -> Day -> Bool := fun d1 =>
  match d1 with
  | .Monday => fun d2 =>
    match d2 with
    | .Monday => true
    | _ => false  -- `_` is for the wildcard case, i.e., all other than `.Monday`
  | .Tuesday => fun d2 =>
    match d2 with
    | .Tuesday => true
    | _ => false
  | .Wednesday => fun d2 =>
     match d2 with
    | .Wednesday => true
    | _ => false
  | .Thursday => fun d2 =>
    match d2 with
    | .Thursday => true
    | _ => false
  | .Friday => fun d2 =>
    match d2 with
    | .Friday => true
    | _ => false
  | .Saturday => fun d2 =>
    match d2 with
    | .Saturday => true
    | _ => false
  | .Sunday => fun d2 =>
    match d2 with
    | .Sunday => true
    | _ => false

#eval ((day_eq_b .Friday) .Friday)
#eval ((day_eq_b .Sunday) .Saturday)

Some other examples.

def ABA: Day -> Bool -> Day := λ a => λ _b => a

def ABB: Day -> Bool -> Bool := λ _a => λ b => b

You could write λ a => λ b => a, but Lean will complain that b is not used. To satisfy Lean, we put an underscore _ before b to indicate that it is an unused variable.

Since we define \(\to\) to be right-associative, the application should then be left-associative, so we can save parentheses.

#eval day_eq_b .Friday .Friday
#eval day_eq_b .Sunday .Saturday

This also suggests a simpler way to define curried functions. (Note that day_eq_b' is slightly different from day_eq_b.)

def ABA': Day -> Bool -> Day := λ a _b => a

def ABB': Day -> Bool -> Bool := λ _a b => b

def day_eq_b': Day -> Day -> Bool := fun d1 d2 =>
  match d1 with
  | .Monday =>
    match d2 with
    | .Monday => true
    | _ => false  -- `_` is for the wildcard case, i.e., all other than `.monday`
  | .Tuesday =>
    match d2 with
    | .Tuesday => true
    | _ => false
  | .Wednesday =>
     match d2 with
    | .Wednesday => true
    | _ => false
  | .Thursday =>
    match d2 with
    | .Thursday => true
    | _ => false
  | .Friday =>
    match d2 with
    | .Friday => true
    | _ => false
  | .Saturday =>
    match d2 with
    | .Saturday => true
    | _ => false
  | .Sunday =>
    match d2 with
    | .Sunday => true
    | _ => false

Syntactic Sugar #

The above might be thought as the standard way to define a function by λ-abstraction. However, it may not be the most convenient way to define a function. For example, the semantics of the above next_day can be interpreted as: for every w: Day, we want to find a term of type Day for the application next_day w, i.e., the following. This sweeter way to write down the same thing with a different syntax is called a syntactic sugar. (Note the prime ' after the name. In Lean, we are unable to change a defined name.)

def next_day' (w: Day): Day := match w with
  | Day.Sunday => Day.Monday
  | Day.Monday => Day.Tuesday
  | .Tuesday => .Wednesday  -- we can omit Day.
  | .Wednesday => .Thursday
  | .Thursday => .Friday
  | .Friday => .Saturday
  | .Saturday => .Sunday

Moreover, we have an even simpler syntax sugar for match.

def next_day'': Day -> Day
  | Day.Sunday => Day.Monday
  | Day.Monday => Day.Tuesday
  | .Tuesday => .Wednesday  -- we can omit Day.
  | .Wednesday => .Thursday
  | .Thursday => .Friday
  | .Friday => .Saturday
  | .Saturday => .Sunday

This is especially useful when you are defining a curried function.

def day_eq_b'': Day -> Day -> Bool
  | .Monday, .Monday => true  -- we use `,` to separate them
  | .Tuesday, .Tuesday => true
  | .Wednesday, .Wednesday => true
  | .Thursday, .Thursday => true
  | .Friday, .Friday => true
  | .Sunday, .Sunday => true
  | .Saturday, .Saturday => true
  | _, _ => false

For the builtin type Bool, you can also use an if ... then ... else ... notation instead of matching a true/false

def my_not (x: Bool): Bool := if x then false else true

#eval my_not false

You can also define the next_day in the namespace Day. This time, let's call it Day.next. But to use it, you have to spell the full name: Day.next .Wednesday. The good part of that is you can use w.next for some w: Day.

def Day.next: Day -> Day := next_day -- certainly, you can use your own definitions here

#eval Day.next .Wednesday
#eval Day.Wednesday.next

Booleans #

We next focus on booleans. As shown above, booleans are simply enumerated by true and false.

inductive Bool where
  | true
  | false

In Lean, booleans are built-in, so we don't redefine them, we just use them directly. Lean also provides many other useful facts about booleans, under the namespace Bool. Since we are going to build up everything from scratch, we don't use them and will define them on our own.

We first define some functions on Bool, then prove some facts about it.

namespace scratch
def Bool.not (b : Bool) : Bool :=
  match b with
  | .true => .false
  | .false => .true

def Bool.and (b1 b2 : Bool) : Bool :=
  match b1 with
  | .true => b2
  | .false => .false

def Bool.or (b1 b2 : Bool) : Bool :=
  match b1 with
  | .true => .true
  | .false => b2

end scratch

Now, let's have our first theorem, i.e., some proposition we can prove. Usually, propositions begin with the keyword theorem and are proved by the tactics after keyword by.

The reader may be familiar with Curry-Howard correspondence or other proof assistants, and thus expect to prove a theorem with def and := directly. Certainly, this is accepted in Lean. For beginners, I suggest tactics because it is easier to read/write them.

If you are using VSCode, the by will activate our goal in the InfoView of Lean. Interactively, after we type some tactic, the goal will then be changed. We repeat this process until the goal can be solved by some tactic. You can set your cursor at certain tactic to check the goal after it.

namespace scratch
theorem not_false_is_true : Bool.not .false = .true := by -- To use tactics, we begin with keyword `by`
  compute [Bool.not] -- This is not a standard Lean tactic. I just want to show some intermediate steps
  eq_refl -- The only way to prove equality is reflexivity.
  -- There's no further gaols. We have proved that.

The proof here says that

1. we first compute the negb function, which turns the goal to true = true;
2. then, we use the reflexivity of equality to finish the proof.

The compute is not a standard Lean tactic. It is made just to perform the β-reduction so that you can you can observe the result of computation. Unfortunately, there is not such a tactic in Lean itself. We will soon see some other tactic that always try compute and eq_refl at one step, so you don't have to worry about this non-standard tactic.

If you don't want to always come up with a name, then use the example keyword.

example: (Bool.or .true .false) = .true := by
  compute [Bool.or]
  eq_refl
example: (Bool.and .false .true) = .false := by
  compute [Bool.and]
  eq_refl

In fact, Lean provides the simp tactic, so you can finish this by only one line.

simp is a very complicated tactic. It does not only apply the eq_refl, but also tries many other automations, like Classical.choice

example (p: Prop): ¬¬p -> p := by
simp

example: Bool.not .true = .false := by
  simp [Bool.not]
end scratch

Natural Numbers #

Our next example is natural numbers \(\mathbb{N}\). Intuitively, natural numbers are how we count things. We begin with zero: ℕ, and to count one more, we use a successor function succ: ℕ → ℕ. Set-theoretically, we use the empty set ∅ for zero, and define the successor as \(S(n)=n\cup\{n\}\). They are both well defined as sets in ZFC (axioms of separation, pairing and union). Then, the axiom of infinity tells us that we can define ℕ.

In type theory, we do not introduce an axiom like this. Rather, we define a new symbol ℕ and setup rules on t: ℕ for some term t. For natural numbers, we define two constructors:

• zero: ℕ;
• succ: ℕ -> ℕ.

This means exactly that there are two ways to write down a natural number, either a zero, or a succ of another natural numbers. For example, zero: ℕ, succ (succ (succ zero)): ℕ.

As before, Lean provides its own built-in natural numbers, so we put our definition into the scratch namespace and explain how it works. Later, we will use the built-in Nat type.

namespace scratch
inductive Nat where
  | zero: Nat
  | succ: Nat -> Nat


#check Nat.zero.succ
#check Nat.succ (Nat.zero)


open Nat

#check zero
#check succ
#check zero.succ.succ

After we define the type Nat, we know how to construct terms of this type. Then, how can we get some data out of a term of type Nat? Still, we do the enumeration by match, while we can capture an extra number in the case of succ. Let's take the following example of the predecessor function.

def Nat.pred (n : Nat) : Nat :=
  match n with
  | .zero => .zero
  | .succ n' => n'


#eval zero.pred  -- zero

#eval zero.succ.succ.pred  -- zero.succ

For each natural number n: Nat, either it is a Nat.zero, or it is a Nat.succ n'. For the former case, we just use Nat.zero as the predecessor; for the latter, the predecessor is exactly n'.

Simillarly, we define the predecessor of predecessor as follows.

def Nat.pred2 (n : Nat) : Nat :=
  match n with
  | .zero => .zero
  | .succ n' => match n' with
    | .zero => .zero
    | .succ n'' => n''

This is a bit cumbersome, since if you have to match many cases, you have to write a very deep match structure. Lean allows us to do the pattern match in non-constructor forms.

def Nat.pred2' (n : Nat) : Nat :=
  match n with
  | .zero => .zero
  | .succ .zero => .zero
  | .succ (.succ n') => n'


#eval zero.succ.pred2'  -- zero

#eval zero.succ.succ.succ.succ.pred2'  -- zero.succ.succ

Recursively defined functions #

We now have a type Bool and a type Nat. It's natural to think about the function beven: Nat → Bool that determines the evenness of a number. What we have now is only pattern match, i.e. defining function by cases. Naively, you may want to define the evenness function like

def Nat.beven (n: Nat): Bool :=
  match n with
  | .zero => true
  | .succ .zero => false
  | .succ (.succ n') => match n' with
    | .zero => true
    | .succ .zero => false
    | .succ (.succ n'') => match n'' with
      | .zero => true
      | .succ .zero => false
      | .succ (.succ n''') =>
        ...

Apparently, we have to repeat this forever in order to enumerate all cases. However, in Lean, this is not allowed. Each definable term in Lean must be described by finite words. This is because Lean require every funciton to be total, i.e., as a function beven: Nat → Boot, beven is defined on each t: Nat. If the function is defined with infinite words, it will take Lean infinite seconds to check whether this function is total or not.

Then, how could we define it? We want some technique to encode the above infinite process into a finite one. For example, from the above, we can see some obviously repeated pattern like

match n with
  | .zero => true
  | .succ .zero => true
  | .succ (.succ n') => ...

So, the function is repeating itself, i.e., we have the following recursive rule:

• beven .zero := true
• beven (.succ .zero) := false
• beven (.succ (.succ n)) := beven n

In Lean, we simply write it as

def Nat.beven: Nat -> Bool
  | .zero => .true
  | .succ .zero => .false
  | .succ (.succ n) => Nat.beven n

Or we can simplify our recursive rules:

• beven .zero := true
• beven (.succ n) := not (beven n)

def Nat.beven': Nat -> Bool
  | .zero => .true
  | .succ n => n.beven'.not  -- Bool.not (Nat.beven' n)

Great! Lean accepts them as a well-defined functions. But, are we allowed to repeat whatever we want? For example, we can change the recursive rules to

• beven .zero := true
• beven (.succ .zero) := false
• beven n := beven (.succ (.succ n))

Mathematically, this is absolutely correct, but Lean will certainly refuse it because when we want to compute beven (.succ (.succ .zero)), from the rules, we will then have to compute beven (.succ (.succ (.succ (.succ .zero)))). Repeating this process many times, we never stop, which breaks the totality of Lean functions, since the value of beven is not defined in this cases as it does not terminate.

You can try typing this in Lean.

def Nat.beven2: Nat -> Bool
  | .zero => true
  | .succ .zero => false
  | n => Nat.beven2 n.succ.succ

Lean will then complain fail to show termination.

The idea behind this is quite simple: you have to reduce the complexity in a good way, so that the function is computable, or otherwise, we could just define any term of any type abusing recursion.

In fact, the above relies on a subtle observation that the structure of recursive function on Nat follows the structure of the term of type Nat. To explain this, let's look at the recursive rules for beven' again.

• beven .zero := true
• beven (.succ n) := not (beven n)

They stipulate a value true: Bool on .zero, and a function not: Bool → Bool on .succ. If you want to compute the value on .succ (.succ .zero), you just replace .zero with true and .succ with not. Then, we compute the replaced expression as is already well-defined.

In other words, to define a function f: Nat -> A for some type A, you specify an a: A and an s: A -> A. Then, f is computed by replacing .zero, .succ with a, s respectively. This is known as catamorphism.

The case for beven is a bit complicated. We leave it to the reader to find its definition in terms of catamorphism.

The real situation in Lean is more complicated, see here for more infomation.

Finally, let's define some arithmetic functions on Nat.

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


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


def Nat.sub: Nat -> Nat -> Nat
  | .zero, _ => .zero
  | m, .zero => m
  | .succ m, .succ n => m.sub n


def Nat.beq: Nat -> Nat -> Bool
  | .zero, .zero => .true
  | .succ m, .succ n => Nat.beq m n
  | _, _ => .false


def Nat.ble: Nat -> Nat -> Bool
  | .zero, _ => .true
  | .succ _, .zero => .false
  | .succ m, .succ n => Nat.ble m n

Exercise: 1 star, standard (ltb) #

Define the ltb function that tests natural numbers for less-than, yielding a boolean.

Hint: You can use pattern matching on both arguments at once.

def blt: Nat -> Nat -> Bool := sorry

Exercise: 1 star, standard (factorial) #

The factorial function is defined with the following recursive rules:

• factorial 0 := 1
• factorial (n+1) := (n+1) * factorial n

def Nat.factorial: Nat -> Nat := sorry

end scratch

Proofs #

namespace scratch

Now, we have known some basic data type and functions on them, and have seen some kind of facts (theorem + proof) about them. We are going to introduce more proof techniques. Up to now, we only have the intuitive equality predicate = and the only way to prove it is through the reflexivity. Generally speaking, we prove it by first simplifying all computable expression, then concluding with eq_refl.

Universal Quantifiers #

This alone is not powerful enough for us to prove more things. For example, we know false and false is false and false and true is false, i.e., forall b: Bool, we shall have false and b is false. In Lean, we use keyword forall or ∀ (\forall) for universal Quantifiers:

forall (b: Bool), Bool.and .false b = .false

But, how can we prove a theorem (proposition) with universal quantifiers? We introduce a new technique called intro, which will bring the premises into current context. Generally speaking, a context is a list of facts you know, with each entry in the list given a name. To understand that, we have to look at Lean's structure of a definition. In Lean, after each def or theorem, you specify some name for the thing you want to define/prove with a desired type (proposition). This type is then called the goal in the interactive infomation view.

Use VSCode to show the infomation view by Shift+Ctrl(Cmd)+Enter.

To fulfill the goal, you have to provide some suitable term/tactics under certain context. For example, to define the function \(x\mapsto x^2\), you first assume some \(x: \mathbb{R}\), and under this assumption, we can find \(x^2: \mathbb{R}\). In this case, the assumption \(x:\mathbb{R}\) is the context, and the \(x^2: \mathbb{R}\) is how we fulfill the goal. After that, we will make the \(x: \mathbb{R}\) into the premise by making the abstraction \(\lambda x. x^2: \mathbb{R} \to \mathbb{R}\).

In other words, to find a term for the goal \(\mathbb{R} \to \mathbb{R}\), we first bring the premise, i.e., the first \(\mathbb{R}\), into the context by giving it a name \(x: \mathbb{R}\), turning the goal into \(\mathbb{R}\), and then find a term \(x^2: \mathbb{R}\) to fulfill the goal under this context. Hence, by making the abstraction, we can conclude a term \(\lambda x. x^2:\mathbb{R} -> \mathbb{R}\). In Lean, we only have to use the intro tactic to bring in premises, indicating that we want to show an equivalent way to define.

theorem Bool.false_and: forall (b: Bool), Bool.and .false b = .false := by
  -- The gaol is `∀ (b : Bool), false.and b = false`.
  intro b  -- Then, it turns into `false.and b = false`.
  compute [Bool.and]  -- We are able to do the computation then.
  eq_refl  -- Finally, conclude it by reflexivity.

Here's another example.

theorem Nat.add_zero: forall (n: Nat), Nat.add .zero n = n := by
  intro n
  compute [Nat.add]
  eq_refl

Or, you can just use simp

theorem Nat.one_add: forall (n: Nat), Nat.zero.succ.add n = n.succ := by
  simp [Nat.add]

Exercise: 1 star, standard (mul_zero) #

theorem Nat.zero_mul: forall (n: Nat), Nat.mul .zero n = .zero := by
  sorry

You can also prefix the universal quantifier twice, e.g.,

theorem Bool.false_and_and: forall (b1: Bool),
  (forall (b2: Bool), (Bool.false.and b1).and b2 = .false)
:= by
  intro b1  -- you can `intro` many premises at one time.
  intro b2
  simp [Bool.and]

We also have some syntactic sugar for this case. First, you can save the forall and parentheses.

theorem Bool.false_and_and': forall (b1 b2: Bool),
  (Bool.false.and b1).and b2 = .false
:= by
  intro b1 b2
  simp [Bool.and]

theorem Bool.false_and_and'': forall b1 b2: Bool,
  (Bool.false.and b1).and b2 = .false
:= by
  intro b1 b2
  simp [Bool.and]

But for variables of different types, you have to add the parentheses.

forall (b: Bool) (n: Nat), something_about_b_and_n

For functions, we don't have to always write the λ-abstractions. We can do the same for theorems too. This is equivalent to say that we bring variables into context directly.

theorem Bool.false_and_and''' (b1: Bool): forall b2: Bool,
  (Bool.false.and b1).and b2 = .false
:= by
  intro b2
  simp [Bool.and]

theorem Bool.false_and_and'''' (b1 b2: Bool):
  (Bool.false.and b1).and b2 = .false
:= by
  simp [Bool.and]

Case Analysis #

We next think about the fact that forall b: Bool, b.not.not = b. This is apparently true because either b is true or false, b.not.not will be itself. However, if you try to compute b.not.not by

theorem Bool.not_not: forall (b: Bool), b.not.not = b := by
  intro b
  compute [Bool.not]

, Lean will expand it into

match
  (match b with
  | true => false
  | false => true) with
| true => false
| false => true

and then get stuck. This is because Lean can only compute a concrete term. In the previous examples, you know how to do the computation for zero.add n because it is literally in the definition of Nat.add. Now, we want to match b: Bool, which is an arbitrary term. Lean gets lost here. Luckily, we can solve this by assuming b: Bool is either true: Bool or false: Bool. In either case, Lean can figure out how to do the computation.

theorem Bool.not_not: forall (b: Bool), b.not.not = b := by
  intro b  -- Bring `b` into context.
  -- Do the case analysis.
  cases b with
  | true =>
    -- You can observe that the `b` is replaced by `true`.
    compute [Bool.not]  -- So, we can compute it.
    eq_refl
  | false => simp [Bool.not] -- or simply use a `simp`

Let's try some other example. We want to show the commutativity of Bool.and, where we use case analysis twice.

theorem Bool.and_comm: forall (b1 b2: Bool), b1.and b2 = b2.and b1 := by
  intro b1 b2
  cases b1 with
  | true => match b2 with
    | true => eq_refl
    | false => simp [Bool.and]
  | false => match b2 with
    | true => simp [Bool.and]
    | false => eq_refl

Exercise: 1 star, standard (or_comm) #

theorem Bool.or_comm: forall (b1 b2: Bool), b1.or b2 = b2.or b1 := by
  sorry

Implication #

We have learned the most basic predicate = and we can prefix an equality with universal quantifiers. What if we want add other conditions? For example, if m n: Nat are even numbers, then so is m.add n. Using context, we encode this proposition as a goal (m.add n).beven = true under the context that m n: Nat and H1: m.beven = true, H2: n.beven = true.

H means hypothesis, which is the conventional variable name for propositions in a context.

However, in Lean, we cannot write a context directly. Just like universal quantifiers, we prefix the goal with premises by -> or → (\to):

example: forall m n: Nat,
  m.beven = .true ->
  n.beven = .true ->
  (m.add n).beven = .true
:= ...

To prove such a theorem, we still use the intro tactic to turn the goal into the equivalent context-wise form. After that, we can make use of such a variable in the context. We then give a simple case that when the goal is in the context, we can fulfill it by the exact tactic. We will learn some more complication usage (apply) in the future chapters.

theorem imp_example: forall n: Nat, n = n -> n = n := by
  intro n
  intro H
  exact H

Rewriting #

We have seen how to prove an equality, but how can we make use of it? The answer is the rewrite tactic. If you have E: a = b in your context, you can rewrite all the occurences of a into b (or the converse).

example: forall m n: Nat, m = n -> m.add m = n.add n := by
  intro m n  -- Intro m n as usual.
  intro E  -- For implication.
  -- Our goal is `m.add m = n.add n`.
  rewrite [E]  -- This turns it into `n.add n = n.add n`.
  eq_refl  -- Finally, reflexivity.

This example rewrites m into n by using the left to right direction of E. Since equalities are symmetric, we can certainly use the other direction by typing a <- or ← (<-) to specifiy.

You can use rw as an abbreviation of rewrite, while it will also try some cheap tactics to close the goal.

example: forall m n: Nat, m = n -> m.add m = n.add n := by
  intro m n  -- Intro m n as usual.
  intro E  -- For implication.
  -- Our goal is `m.add m = n.add n`.
  rewrite [<-E]  -- This turns it into `m.add m = m.add m`.
  eq_refl  -- Finally, reflexivity.

For a proved theorem/premise prefixed with universal quantifiers, we can directly rewrite it, and Lean will try to figure out the suitable term after quantifiers. In the following example, Lean will try to unify the b.not.not in Bool.not_not, and it finally determins that b.not can be the quantified b and simplify our goal (certainly b and b.not.not also works).

This is one way to make use of a universally-quantified proposition. Lean implicitly adds some syntactic sugar here (type-inference). Later, we will explain it in details.

example: forall b: Bool, b.not.not.not.not = b := by
  intro b
  rewrite [Bool.not_not]
  rewrite [Bool.not_not]
  eq_refl

Symmetry #

A direct result of the rewrite tactic is the symmetry of equality.

example: forall m n: Nat, m = n -> n = m := by
  intro m n H
  rewrite [H]
  eq_refl

This shows that to prove n = m, you can change the goal to m = n. Lean provides a tactic symm for this purpose.

example: 3 = 4 -> 4 = 3 := by
  intro H
  symm
  exact H

And it can also be used to switch the sides of an equality

example: 3 = 4 -> 4 = 3 := by
  intro H
  symm at H  -- This changes 3 = 4 to 4 = 3
  exact H
end scratch

Now, we step out of the namespace scratch. In fact, Lean have already provided those theorems for us. We will gradually move to the Nat and Bool defined by Lean as we learn more. For pedagogical purpose, we put our own definitions in the namespace scratch. You can check those in Lean prelude by #check. For example

#check Nat.zero_add
#check Bool.and_assoc

namespace scratch
theorem Nat.zero_add (n : Nat) :  Nat.zero.add n = n := by
  induction n with
  | zero => rfl
  | succ n' ih =>
    compute [Nat.add]
    eq_refl

theorem plus_succ_n (n m : Nat) : n.succ.add m = (n.add m).succ := by
  induction n with
  | zero =>
    compute [Nat.add]
    eq_refl
  | succ n' ih =>
    compute [Nat.add]
    eq_refl

end scratch

More Exercises #

The following exercises are translated from Software Foundations. Try to solve them yourself! Each exercise is marked with its difficulty level.

Tips for solving exercises:

1. Start by understanding the type of the function/theorem
2. Use pattern matching for function definitions
3. Use induction for proofs about natural numbers
4. Use case analysis for proofs about booleans
5. Use rewriting for proofs about equality
6. Use simplification for proofs about arithmetic

namespace scratch

Exercise: 1 star, standard (nandb) #

Define the function nand (negated-and) that returns true if either or both of its inputs are false.

Hint: You can use pattern matching on both arguments at once using a comma.

def Bool.nand (b1 b2 : Bool) : Bool := sorry

Exercise: 1 star, standard (andb3) #

Define the function andb3 that returns true when all of its inputs are true, and false otherwise.

Hint: You can use pattern matching on all three arguments at once.

def Bool.and3 (b1 b2 b3 : Bool) : Bool := sorry

Exercise: 1 star, standard (identity_fn_applied_twice) #

Prove the following theorem about boolean functions.

Hint: You'll need to use case analysis on the boolean argument.

theorem identity_fn_applied_twice :
  ∀ (f : Bool → Bool),
  (∀ (x : Bool), f x = x) →
  ∀ (b : Bool), f (f b) = b
:= by
  sorry

Exercise: 1 star, standard (negation_fn_applied_twice) #

State and prove a theorem negation_fn_applied_twice similar to the previous one but where the second hypothesis says that the function f has the property that f x = negb x.

Hint: This is similar to the previous exercise, but you'll need to use the negb function.

theorem negation_fn_applied_twice :
  ∀ (f : Bool → Bool),
  (∀ (x : Bool), f x = x.not) →
  ∀ (b : Bool), f (f b) = b
:= by
  sorry

Exercise: 3 stars, standard (andb_eq_orb) #

Prove the following theorem.

Hint: You'll need to use case analysis on both boolean arguments.

theorem andb_eq_orb :
  ∀ (b c : Bool),
  (b.and c = b.or c) →
  b = c
:= by
  sorry

Exercise: 3 stars, standard (binary) #

We can generalize our unary representation of natural numbers to the more efficient binary representation by treating a binary number as a sequence of constructors B0 and B1 (representing 0s and 1s), terminated by a Z.

Hint: You'll need to use pattern matching and recursion.

inductive Bin where
  | Z
  | B0 (n : Bin)
  | B1 (n : Bin)

def incr (b : Bin) : Bin :=
  match b with
  | .Z => .B1 .Z
  | .B0 b' => .B1 b'
  | .B1 b' => .B0 (incr b')

def bin_to_nat (b : Bin) : Nat :=
  match b with
  | .Z => .zero
  | .B0 b' => Nat.add (bin_to_nat b') (bin_to_nat b')
  | .B1 b' => Nat.succ (Nat.add (bin_to_nat b') (bin_to_nat b'))

end scratch