Avigad.Chapter8

Induction and Recursion

Exercise 1

Open a namespace Hidden to avoid naming conflicts, and use the equation compiler to define addition, multiplication, and exponentiation on the natural numbers. Then use the equation compiler to derive some of their basic properties.

def Avigad.Chapter8.ex1.add : Nat → Nat → Nat

Equations

• Avigad.Chapter8.ex1.add x Nat.zero = x
• Avigad.Chapter8.ex1.add x (Nat.succ n) = Nat.succ (Avigad.Chapter8.ex1.add x n)

def Avigad.Chapter8.ex1.mul : Nat → Nat → Nat

Equations

• Avigad.Chapter8.ex1.mul x Nat.zero = 0
• Avigad.Chapter8.ex1.mul x (Nat.succ n) = Avigad.Chapter8.ex1.add x (Avigad.Chapter8.ex1.mul x n)

def Avigad.Chapter8.ex1.exp : Nat → Nat → Nat

Equations

• Avigad.Chapter8.ex1.exp x Nat.zero = 1
• Avigad.Chapter8.ex1.exp x (Nat.succ n) = Avigad.Chapter8.ex1.mul x (Avigad.Chapter8.ex1.exp x n)

Exercise 2

Similarly, use the equation compiler to define some basic operations on lists (like the reverse function) and prove theorems about lists by induction (such as the fact that reverse (reverse xs) = xs for any list xs).

def Avigad.Chapter8.ex2.reverse {α : Type u_1} : List α → List α

Equations

• Avigad.Chapter8.ex2.reverse [] = []
• Avigad.Chapter8.ex2.reverse (head :: tail) = Avigad.Chapter8.ex2.reverse tail ++ [head]

Exercise 3

Define your own function to carry out course-of-value recursion on the natural numbers. Similarly, see if you can figure out how to define WellFounded.fix on your own.

def Avigad.Chapter8.ex3.below {motive : Nat → Sort u} (t : Nat) : Sort (max 1 u)

Equations

• Avigad.Chapter8.ex3.below t = Nat.recOn t PUnit fun (n : Nat) (ih : Sort (max 1 u)) => PProd (PProd (motive n) ih) PUnit

noncomputable def Avigad.Chapter8.ex3.brecOn {motive : Nat → Sort u} (t : Nat) (F : (t : Nat) → Avigad.Chapter8.ex3.below t → motive t) : motive t

A copied implementation of Nat.brecOn with the motive properly supplied. Notice the noncomputable tag; the code generator does not support the recOn recursor yet, for reasons I haven't fully understood yet. This thread touches on the topic:

https://leanprover-community.github.io/archive/stream/270676-lean4/topic/code.20generator.20does.20not.20support.20recursor.html

Equations

• One or more equations did not get rendered due to their size.

Exercise 4

Following the examples in Section Dependent Pattern Matching, define a function that will append two vectors. This is tricky; you will have to define an auxiliary function.

inductive Avigad.Chapter8.ex4.Vector (α : Type u) : Nat → Type u

• nil: {α : Type u} → Avigad.Chapter8.ex4.Vector α 0
• cons: {α : Type u} → α → {n : Nat} → Avigad.Chapter8.ex4.Vector α n → Avigad.Chapter8.ex4.Vector α (n + 1)

def Avigad.Chapter8.ex4.Vector.append {α : Type u_1} {m : Nat} {n : Nat} : Avigad.Chapter8.ex4.Vector α m → Avigad.Chapter8.ex4.Vector α n → Avigad.Chapter8.ex4.Vector α (n + m)

As long we flip the indices in our type signature in the resulting summation, there is no need for an auxiliary function.

Equations

• Avigad.Chapter8.ex4.Vector.append Avigad.Chapter8.ex4.Vector.nil x = x
• Avigad.Chapter8.ex4.Vector.append (Avigad.Chapter8.ex4.Vector.cons a as) x = Avigad.Chapter8.ex4.Vector.cons a (Avigad.Chapter8.ex4.Vector.append as x)

Exercise 5

Consider the following type of arithmetic expressions.

inductive Avigad.Chapter8.ex5.Expr : Type

• const: Nat → Avigad.Chapter8.ex5.Expr
• var: Nat → Avigad.Chapter8.ex5.Expr
• plus: Avigad.Chapter8.ex5.Expr → Avigad.Chapter8.ex5.Expr → Avigad.Chapter8.ex5.Expr
• times: Avigad.Chapter8.ex5.Expr → Avigad.Chapter8.ex5.Expr → Avigad.Chapter8.ex5.Expr

instance Avigad.Chapter8.ex5.instReprExpr : Repr Avigad.Chapter8.ex5.Expr

Equations

• Avigad.Chapter8.ex5.instReprExpr = { reprPrec := Avigad.Chapter8.ex5.reprExpr✝ }

def Avigad.Chapter8.ex5.sampleExpr : Avigad.Chapter8.ex5.Expr

Equations

• One or more equations did not get rendered due to their size.

def Avigad.Chapter8.ex5.eval (v : Nat → Nat) : Avigad.Chapter8.ex5.Expr → Nat

Equations

• Avigad.Chapter8.ex5.eval v (Avigad.Chapter8.ex5.Expr.const a) = a
• Avigad.Chapter8.ex5.eval v (Avigad.Chapter8.ex5.Expr.var a) = v a
• Avigad.Chapter8.ex5.eval v (Avigad.Chapter8.ex5.Expr.plus a a_1) = Avigad.Chapter8.ex5.eval v a + Avigad.Chapter8.ex5.eval v a_1
• Avigad.Chapter8.ex5.eval v (Avigad.Chapter8.ex5.Expr.times a a_1) = Avigad.Chapter8.ex5.eval v a * Avigad.Chapter8.ex5.eval v a_1

def Avigad.Chapter8.ex5.sampleVal : Nat → Nat

Equations

• Avigad.Chapter8.ex5.sampleVal x = match x with | 0 => 5 | 1 => 6 | x => 0

Constant Fusion

Implement "constant fusion," a procedure that simplifies subterms like 5 + 7 to 12. Using the auxiliary function simpConst, define a function "fuse": to simplify a plus or a times, first simplify the arguments recursively, and then apply simpConst` to try to simplify the result.

def Avigad.Chapter8.ex5.simpConst : Avigad.Chapter8.ex5.Expr → Avigad.Chapter8.ex5.Expr

Equations

• One or more equations did not get rendered due to their size.

def Avigad.Chapter8.ex5.fuse : Avigad.Chapter8.ex5.Expr → Avigad.Chapter8.ex5.Expr

Equations

• Avigad.Chapter8.ex5.fuse (Avigad.Chapter8.ex5.Expr.plus e₁ e₂) = Avigad.Chapter8.ex5.simpConst (Avigad.Chapter8.ex5.Expr.plus (Avigad.Chapter8.ex5.fuse e₁) (Avigad.Chapter8.ex5.fuse e₂))
• Avigad.Chapter8.ex5.fuse (Avigad.Chapter8.ex5.Expr.times e₁ e₂) = Avigad.Chapter8.ex5.simpConst (Avigad.Chapter8.ex5.Expr.times (Avigad.Chapter8.ex5.fuse e₁) (Avigad.Chapter8.ex5.fuse e₂))
• Avigad.Chapter8.ex5.fuse x = x

theorem Avigad.Chapter8.ex5.simpConst_eq (v : Nat → Nat) (e : Avigad.Chapter8.ex5.Expr) : Avigad.Chapter8.ex5.eval v (Avigad.Chapter8.ex5.simpConst e) = Avigad.Chapter8.ex5.eval v e

theorem Avigad.Chapter8.ex5.fuse_eq (v : Nat → Nat) (e : Avigad.Chapter8.ex5.Expr) : Avigad.Chapter8.ex5.eval v (Avigad.Chapter8.ex5.fuse e) = Avigad.Chapter8.ex5.eval v e