08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
200 lines
7.3 KiB
Text
200 lines
7.3 KiB
Text
set_option guard_msgs.diff true
|
||
|
||
/-!
|
||
This module tests functional induction principles on *structurally* recursive functions.
|
||
-/
|
||
|
||
def fib : Nat → Nat
|
||
| 0 | 1 => 0
|
||
| n+2 => fib n + fib (n+1)
|
||
termination_by structural x => x
|
||
|
||
/--
|
||
info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
|
||
(case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) (a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check fib.induct
|
||
|
||
|
||
def binary : Nat → Nat → Nat
|
||
| 0, acc | 1, acc => 1 + acc
|
||
| n+2, acc => binary n (binary (n+1) acc)
|
||
termination_by structural x => x
|
||
|
||
/--
|
||
info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc) (case2 : ∀ (acc : Nat), motive 1 acc)
|
||
(case3 : ∀ (n acc : Nat), motive (n + 1) acc → motive n (binary (n + 1) acc) → motive n.succ.succ acc)
|
||
(a✝ a✝¹ : Nat) : motive a✝ a✝¹
|
||
-/
|
||
#guard_msgs in
|
||
#check binary.induct
|
||
|
||
|
||
-- Different parameter order
|
||
def binary' : Bool → Nat → Bool
|
||
| acc, 0 | acc , 1 => not acc
|
||
| acc, n+2 => binary' (binary' acc (n+1)) n
|
||
termination_by structural _ x => x
|
||
|
||
/--
|
||
info: binary'.induct (motive : Bool → Nat → Prop) (case1 : ∀ (acc : Bool), motive acc 0)
|
||
(case2 : ∀ (acc : Bool), motive acc 1)
|
||
(case3 : ∀ (acc : Bool) (n : Nat), motive acc (n + 1) → motive (binary' acc (n + 1)) n → motive acc n.succ.succ)
|
||
(a✝ : Bool) (a✝¹ : Nat) : motive a✝ a✝¹
|
||
-/
|
||
#guard_msgs in
|
||
#check binary'.induct
|
||
|
||
def zip {α β} : List α → List β → List (α × β)
|
||
| [], _ => []
|
||
| _, [] => []
|
||
| x::xs, y::ys => (x, y) :: zip xs ys
|
||
termination_by structural x => x
|
||
|
||
/--
|
||
info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop)
|
||
(case1 : ∀ (x : List β), motive [] x) (case2 : ∀ (t : List α), (t = [] → False) → motive t [])
|
||
(case3 : ∀ (x : α) (xs : List α) (y : β) (ys : List β), motive xs ys → motive (x :: xs) (y :: ys)) (a✝ : List α)
|
||
(a✝¹ : List β) : motive a✝ a✝¹
|
||
-/
|
||
#guard_msgs in
|
||
#check zip.induct
|
||
|
||
/-- Let's try to use it! -/
|
||
theorem zip_length {α β} (xs : List α) (ys : List β) :
|
||
(zip xs ys).length = xs.length.min ys.length := by
|
||
induction xs, ys using zip.induct
|
||
case case1 => simp [zip]
|
||
case case2 => simp [zip]
|
||
case case3 => simp [zip, *]
|
||
|
||
theorem zip_get? {i : Nat} {α β} (as : List α) (bs : List β) :
|
||
(List.zip as bs)[i]? = match as[i]?, bs[i]? with
|
||
| some a, some b => some (a, b)
|
||
| _, _ => none := by
|
||
induction as, bs using zip.induct generalizing i
|
||
<;> cases i <;> simp_all
|
||
|
||
-- Testing recursion on an indexed data type
|
||
inductive Finn : Nat → Type where
|
||
| fzero : {n : Nat} → Finn n
|
||
| fsucc : {n : Nat} → Finn n → Finn (n+1)
|
||
|
||
def Finn.min (x : Bool) {n : Nat} (m : Nat) : Finn n → (f : Finn n) → Finn n
|
||
| fzero, _ => fzero
|
||
| _, fzero => fzero
|
||
| fsucc i, fsucc j => fsucc (Finn.min (not x) (m + 1) i j)
|
||
termination_by structural n
|
||
|
||
/--
|
||
info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n → Prop)
|
||
(case1 : ∀ (x : Bool) (m n : Nat) (f : Finn n), motive x m Finn.fzero f)
|
||
(case2 : ∀ (x : Bool) (m n : Nat) (a : Finn n), (a = Finn.fzero → False) → motive x m a Finn.fzero)
|
||
(case3 : ∀ (x : Bool) (m n : Nat) (i j : Finn n), motive (!x) (m + 1) i j → motive x m i.fsucc j.fsucc) (x : Bool)
|
||
{n : Nat} (m : Nat) (a✝ f : Finn n) : motive x m a✝ f
|
||
-/
|
||
#guard_msgs in
|
||
#check Finn.min.induct
|
||
|
||
namespace TreeExample
|
||
|
||
inductive Tree (β : Type v) where
|
||
| leaf
|
||
| node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
|
||
|
||
def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β :=
|
||
match t with
|
||
| leaf => node leaf k v leaf
|
||
| node left key value right =>
|
||
if k < key then
|
||
node (left.insert k v) key value right
|
||
else if key < k then
|
||
node left key value (right.insert k v)
|
||
else
|
||
node left k v right
|
||
termination_by structural t
|
||
|
||
/--
|
||
info: TreeExample.Tree.insert.induct.{u_1} {β : Type u_1} (k : Nat) (motive : Tree β → Prop) (case1 : motive Tree.leaf)
|
||
(case2 :
|
||
∀ (left : Tree β) (key : Nat) (value : β) (right : Tree β),
|
||
k < key → motive left → motive (left.node key value right))
|
||
(case3 :
|
||
∀ (left : Tree β) (key : Nat) (value : β) (right : Tree β),
|
||
¬k < key → key < k → motive right → motive (left.node key value right))
|
||
(case4 :
|
||
∀ (left : Tree β) (key : Nat) (value : β) (right : Tree β),
|
||
¬k < key → ¬key < k → motive (left.node key value right))
|
||
(t : Tree β) : motive t
|
||
-/
|
||
#guard_msgs in
|
||
#check Tree.insert.induct
|
||
|
||
end TreeExample
|
||
|
||
namespace TermDenote
|
||
|
||
inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
|
||
| nil : HList β []
|
||
| cons : β i → HList β is → HList β (i::is)
|
||
|
||
inductive Member : α → List α → Type
|
||
| head : Member a (a::as)
|
||
| tail : Member a bs → Member a (b::bs)
|
||
|
||
def HList.get : HList β is → Member i is → β i
|
||
| .cons a as, .head => a
|
||
| .cons _ as, .tail h => as.get h
|
||
|
||
inductive Ty where
|
||
| nat
|
||
| fn : Ty → Ty → Ty
|
||
|
||
@[reducible] def Ty.denote : Ty → Type
|
||
| nat => Nat
|
||
| fn a b => a.denote → b.denote
|
||
|
||
inductive Term : List Ty → Ty → Type
|
||
| var : Member ty ctx → Term ctx ty
|
||
| const : Nat → Term ctx .nat
|
||
| plus : Term ctx .nat → Term ctx .nat → Term ctx .nat
|
||
| app : Term ctx (.fn dom ran) → Term ctx dom → Term ctx ran
|
||
| lam : Term (.cons dom ctx) ran → Term ctx (.fn dom ran)
|
||
| let : Term ctx ty₁ → Term (.cons ty₁ ctx) ty₂ → Term ctx ty₂
|
||
|
||
def Term.denote : Term ctx ty → HList Ty.denote ctx → ty.denote
|
||
| .var h, env => env.get h
|
||
| .const n, _ => n
|
||
| .plus a b, env => a.denote env + b.denote env
|
||
-- the following recursive call is interesting: Here the `ty.denote` for `f`'s type
|
||
-- becomes a function, and thus the recursive call takes an extra argument
|
||
-- But in the induction principle, we have `motive f` here, which does not
|
||
-- take an extra argument, so we have to be careful to not pass too many arguments to it
|
||
| .app f a, env => f.denote env (a.denote env)
|
||
| .lam b, env => fun x => b.denote (.cons x env)
|
||
| .let a b, env => b.denote (.cons (a.denote env) env)
|
||
termination_by structural x => x
|
||
|
||
/--
|
||
info: TermDenote.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Prop)
|
||
(case1 : ∀ (a : List Ty) (ty : Ty) (h : Member ty a) (env : HList Ty.denote a), motive (Term.var h) env)
|
||
(case2 : ∀ (a : List Ty) (n : Nat) (x : HList Ty.denote a), motive (Term.const n) x)
|
||
(case3 :
|
||
∀ (a : List Ty) (a_1 b : Term a Ty.nat) (env : HList Ty.denote a),
|
||
motive a_1 env → motive b env → motive (a_1.plus b) env)
|
||
(case4 :
|
||
∀ (a : List Ty) (ty dom : Ty) (f : Term a (dom.fn ty)) (a_1 : Term a dom) (env : HList Ty.denote a),
|
||
motive f env → motive a_1 env → motive (f.app a_1) env)
|
||
(case5 :
|
||
∀ (a : List Ty) (dom ran : Ty) (b : Term (dom :: a) ran) (env : HList Ty.denote a),
|
||
(∀ (x : dom.denote), motive b (HList.cons x env)) → motive b.lam env)
|
||
(case6 :
|
||
∀ (a : List Ty) (ty ty₁ : Ty) (a_1 : Term a ty₁) (b : Term (ty₁ :: a) ty) (env : HList Ty.denote a),
|
||
motive a_1 env → motive b (HList.cons (a_1.denote env) env) → motive (a_1.let b) env)
|
||
{ctx : List Ty} {ty : Ty} (a✝ : Term ctx ty) (a✝¹ : HList Ty.denote ctx) : motive a✝ a✝¹
|
||
-/
|
||
#guard_msgs in
|
||
#check TermDenote.Term.denote.induct
|
||
|
||
end TermDenote
|