210 lines
5.3 KiB
Plaintext
210 lines
5.3 KiB
Plaintext
/-! # Avigad.Chapter8
|
||
|
||
Induction and Recursion
|
||
-/
|
||
|
||
namespace Avigad.Chapter8
|
||
|
||
/-! ### 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.
|
||
-/
|
||
|
||
namespace ex1
|
||
|
||
def add : Nat → Nat → Nat
|
||
| m, Nat.zero => m
|
||
| m, Nat.succ n => Nat.succ (add m n)
|
||
|
||
def mul : Nat → Nat → Nat
|
||
| _, Nat.zero => 0
|
||
| m, Nat.succ n => add m (mul m n)
|
||
|
||
def exp : Nat → Nat → Nat
|
||
| _, Nat.zero => 1
|
||
| m, Nat.succ n => mul m (exp m n)
|
||
|
||
end ex1
|
||
|
||
/-! ### 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`).
|
||
-/
|
||
|
||
namespace ex2
|
||
|
||
variable {α : Type _}
|
||
|
||
def reverse : List α → List α
|
||
| [] => []
|
||
| (head :: tail) => reverse tail ++ [head]
|
||
|
||
-- Proof of `reverse (reverse xs) = xs` shown in previous exercise.
|
||
|
||
end ex2
|
||
|
||
/-! ### 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.
|
||
-/
|
||
|
||
namespace ex3
|
||
|
||
def below {motive : Nat → Sort u} (t : Nat) : Sort (max 1 u) :=
|
||
Nat.recOn t
|
||
(zero := PUnit)
|
||
(succ := fun n ih => PProd (PProd (motive n) ih) (PUnit : Sort (max 1 u)))
|
||
|
||
/--
|
||
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
|
||
-/
|
||
noncomputable def brecOn {motive : Nat → Sort u}
|
||
(t : Nat) (F : (t : Nat) → @below motive t → motive t) : motive t :=
|
||
(Nat.recOn t
|
||
(motive := fun n => PProd
|
||
(motive n)
|
||
(Nat.recOn n PUnit fun n ih => PProd (PProd (motive n) ih) PUnit))
|
||
(zero := { fst := F Nat.zero PUnit.unit, snd := PUnit.unit })
|
||
(succ := fun n ih => {
|
||
fst := F (Nat.succ n) { fst := ih, snd := PUnit.unit },
|
||
snd := { fst := ih, snd := PUnit.unit }
|
||
})).1
|
||
|
||
#check WellFounded.fix
|
||
|
||
end ex3
|
||
|
||
/-! ### 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.
|
||
-/
|
||
|
||
namespace ex4
|
||
|
||
inductive Vector (α : Type u) : Nat → Type u
|
||
| nil : Vector α 0
|
||
| cons : α → {n : Nat} → Vector α n → Vector α (n + 1)
|
||
|
||
namespace Vector
|
||
|
||
/--
|
||
As long we flip the indices in our type signature in the resulting summation,
|
||
there is no need for an auxiliary function.
|
||
-/
|
||
def append : Vector α m → Vector α n → Vector α (n + m)
|
||
| nil, bs => bs
|
||
| cons a as, bs => cons a (append as bs)
|
||
|
||
end Vector
|
||
|
||
end ex4
|
||
|
||
/-! ### Exercise 5
|
||
|
||
Consider the following type of arithmetic expressions.
|
||
-/
|
||
|
||
namespace ex5
|
||
|
||
inductive Expr where
|
||
| const : Nat → Expr
|
||
| var : Nat → Expr
|
||
| plus : Expr → Expr → Expr
|
||
| times : Expr → Expr → Expr
|
||
deriving Repr
|
||
|
||
open Expr
|
||
|
||
def sampleExpr : Expr :=
|
||
plus (times (var 0) (const 7)) (times (const 2) (var 1))
|
||
|
||
-- Here `sampleExpr` represents `(v₀ * 7) + (2 * v₁)`. Write a function that
|
||
-- evaluates such an expression, evaluating each `var n` to `v n`.
|
||
|
||
def eval (v : Nat → Nat) : Expr → Nat
|
||
| const n => n
|
||
| var n => v n
|
||
| plus e₁ e₂ => eval v e₁ + eval v e₂
|
||
| times e₁ e₂ => eval v e₁ * eval v e₂
|
||
|
||
def sampleVal : Nat → Nat
|
||
| 0 => 5
|
||
| 1 => 6
|
||
| _ => 0
|
||
|
||
-- Try it out. You should get 47 here.
|
||
#eval eval sampleVal sampleExpr
|
||
|
||
/-! ### 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 simpConst : Expr → Expr
|
||
| plus (const n₁) (const n₂) => const (n₁ + n₂)
|
||
| times (const n₁) (const n₂) => const (n₁ * n₂)
|
||
| e => e
|
||
|
||
def fuse : Expr → Expr
|
||
| plus e₁ e₂ => simpConst $ plus (fuse e₁) (fuse e₂)
|
||
| times e₁ e₂ => simpConst $ times (fuse e₁) (fuse e₂)
|
||
| e => e
|
||
|
||
theorem simpConst_eq (v : Nat → Nat)
|
||
: ∀ e : Expr, eval v (simpConst e) = eval v e := by
|
||
intro e
|
||
unfold simpConst
|
||
repeat { unfold eval }
|
||
match h : e with
|
||
| const n
|
||
| var n
|
||
| plus (const _) (const _)
|
||
| plus (var _) _
|
||
| plus (plus _ _) _
|
||
| plus (times _ _) _
|
||
| times (const _) (const _)
|
||
| times (var _) _
|
||
| times (plus _ _) _
|
||
| times (times _ _) _ => rfl
|
||
| plus _ (var _)
|
||
| plus _ (plus _ _)
|
||
| plus _ (times _ _)
|
||
| times _ (var _)
|
||
| times _ (plus _ _)
|
||
| times _ (times _ _) => simp only
|
||
|
||
|
||
theorem fuse_eq (v : Nat → Nat)
|
||
: ∀ e : Expr, eval v (fuse e) = eval v e := by
|
||
intro e
|
||
induction e with
|
||
| const n | var n => unfold fuse; rfl
|
||
| plus e₁ e₂ he₁ he₂ | times e₁ e₂ he₁ he₂ =>
|
||
unfold fuse
|
||
rw [simpConst_eq]
|
||
unfold eval
|
||
rw [he₁, he₂]
|
||
|
||
-- The last two theorems show that the definitions preserve the value.
|
||
|
||
end ex5
|
||
|
||
end Avigad.Chapter8
|