Theorem Proving in Lean. Part of exercises 8.
parent
9558ea4e52
commit
e726572c38
|
@ -1,2 +1,4 @@
|
||||||
/build
|
/build
|
||||||
/lake-packages/*
|
/lake-packages/*
|
||||||
|
/_target
|
||||||
|
/leanpkg.path
|
||||||
|
|
|
@ -183,11 +183,11 @@ end ex2
|
||||||
-- assignment of values to the variables.
|
-- assignment of values to the variables.
|
||||||
namespace ex3
|
namespace ex3
|
||||||
|
|
||||||
inductive foo : Type _
|
inductive Foo : Type _
|
||||||
| const : Nat → foo
|
| const : Nat → Foo
|
||||||
| var : Nat → foo
|
| var : Nat → Foo
|
||||||
| plus : foo → foo → foo
|
| plus : Foo → Foo → Foo
|
||||||
| times : foo → foo → foo
|
| times : Foo → Foo → Foo
|
||||||
|
|
||||||
def value_at : Nat → List Nat → Nat
|
def value_at : Nat → List Nat → Nat
|
||||||
| _, [] => default
|
| _, [] => default
|
||||||
|
@ -195,10 +195,10 @@ def value_at : Nat → List Nat → Nat
|
||||||
| (i + 1), vs => value_at i (List.tail! vs)
|
| (i + 1), vs => value_at i (List.tail! vs)
|
||||||
|
|
||||||
-- The provided "variables" are supplied in a 0-indexed list.
|
-- The provided "variables" are supplied in a 0-indexed list.
|
||||||
def eval_foo : foo → List Nat → Nat
|
def eval_foo : Foo → List Nat → Nat
|
||||||
| (foo.const n) , _ => n
|
| (Foo.const n) , _ => n
|
||||||
| (foo.var n) , vs => value_at n vs
|
| (Foo.var n) , vs => value_at n vs
|
||||||
| (foo.plus m n) , vs => eval_foo m vs + eval_foo n vs
|
| (Foo.plus m n) , vs => eval_foo m vs + eval_foo n vs
|
||||||
| (foo.times m n), vs => eval_foo m vs * eval_foo n vs
|
| (Foo.times m n), vs => eval_foo m vs * eval_foo n vs
|
||||||
|
|
||||||
end ex3
|
end ex3
|
||||||
|
|
|
@ -0,0 +1,138 @@
|
||||||
|
/- Exercises 8
|
||||||
|
-
|
||||||
|
- Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
|
||||||
|
-/
|
||||||
|
|
||||||
|
-- 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
|
||||||
|
|
||||||
|
-- What does it mean to "derecurse" a function? A recursive function can be written iteratively.
|
||||||
|
-- What class of recursive functions can be written iteratively? Primitive recursive functions.
|
||||||
|
|
||||||
|
-- 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
|
||||||
|
|
||||||
|
-- TODO: Answer this.
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
def append (v₁ : Vector α m) (v₂ : Vector α n) : Vector α (m + n) := sorry
|
||||||
|
|
||||||
|
-- TODO: Answer this.
|
||||||
|
|
||||||
|
end Vector
|
||||||
|
|
||||||
|
end ex4
|
||||||
|
|
||||||
|
-- Exercise 5
|
||||||
|
--
|
||||||
|
-- Consider the following type of arithmetic expressions. The idea is that
|
||||||
|
-- `var n` is a variable, `vₙ`, and `const n` is the constant whose value is
|
||||||
|
-- `n`.
|
||||||
|
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 => sorry
|
||||||
|
| var n => v n
|
||||||
|
| plus e₁ e₂ => sorry
|
||||||
|
| times e₁ e₂ => sorry
|
||||||
|
|
||||||
|
def sampleVal : Nat → Nat
|
||||||
|
| 0 => 5
|
||||||
|
| 1 => 6
|
||||||
|
| _ => 0
|
||||||
|
|
||||||
|
-- Try it out. You should get 47 here.
|
||||||
|
-- #eval eval sampleVal sampleExpr
|
||||||
|
|
||||||
|
-- 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 := sorry
|
||||||
|
|
||||||
|
theorem simpConst_eq (v : Nat → Nat)
|
||||||
|
: ∀ e : Expr, eval v (simpConst e) = eval v e :=
|
||||||
|
sorry
|
||||||
|
|
||||||
|
theorem fuse_eq (v : Nat → Nat)
|
||||||
|
: ∀ e : Expr, eval v (fuse e) = eval v e :=
|
||||||
|
sorry
|
||||||
|
|
||||||
|
-- The last two theorems show that the definitions preserve the value.
|
||||||
|
|
||||||
|
end ex5
|
Loading…
Reference in New Issue