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.
229 lines
5.4 KiB
Text
229 lines
5.4 KiB
Text
set_option linter.unusedVariables false
|
||
|
||
inductive PList (α : Type) : Prop
|
||
| nil
|
||
| cons : α → PList α → PList α
|
||
|
||
infixr:67 " ::: " => PList.cons
|
||
|
||
def map {α β} (f : α → β) : List α → List β
|
||
| [] => []
|
||
| a::as => f a :: map f as
|
||
|
||
def pmap {α β} (f : α → β) : PList α → PList β
|
||
| PList.nil => PList.nil
|
||
| a:::as => f a ::: pmap f as
|
||
|
||
theorem ex1 : map Nat.succ [1] = [2] :=
|
||
rfl
|
||
|
||
theorem ex2 : map Nat.succ [] = [] :=
|
||
rfl
|
||
|
||
theorem ex3 (a : Nat) : map Nat.succ [a] = [Nat.succ a] :=
|
||
rfl
|
||
|
||
theorem ex4 {α β} (f : α → β) (a : α) (as : List α) : map f (a::as) = (f a) :: map f as :=
|
||
rfl
|
||
|
||
theorem ex5 {α β} (f : α → β) : map f [] = [] :=
|
||
rfl
|
||
|
||
def map2 {α β} (f : α → β) (as : List α) : List β :=
|
||
let rec loop : List α → List β
|
||
| [] => []
|
||
| a::as => f a :: loop as;
|
||
loop as
|
||
|
||
def pmap2 {α β} (f : α → β) (as : PList α) : PList β :=
|
||
let rec loop : PList α → PList β
|
||
| PList.nil => PList.nil
|
||
| a:::as => f a ::: loop as;
|
||
loop as
|
||
|
||
|
||
theorem ex6 {α β} (f : α → β) (a : α) (as : List α) : map2 f (a::as) = (f a) :: map2 f as :=
|
||
rfl
|
||
|
||
def foo (xs : List Nat) : List Nat :=
|
||
match xs with
|
||
| [] => []
|
||
| x::xs =>
|
||
let y := 2 * x;
|
||
match xs with
|
||
| [] => []
|
||
| x::xs => (y + x) :: foo xs
|
||
|
||
def pfoo (xs : PList Nat) : PList Nat :=
|
||
match xs with
|
||
| PList.nil => PList.nil
|
||
| x:::xs =>
|
||
let y := 2 * x;
|
||
match xs with
|
||
| PList.nil => PList.nil
|
||
| x:::xs => (y + x) ::: pfoo xs
|
||
|
||
#guard foo [1, 2, 3, 4] == [4, 10]
|
||
|
||
theorem fooEq (x y : Nat) (xs : List Nat) : foo (x::y::xs) = (2*x + y) :: foo xs :=
|
||
rfl
|
||
|
||
def bla (x : Nat) (ys : List Nat) : List Nat :=
|
||
if x % 2 == 0 then
|
||
match ys with
|
||
| [] => []
|
||
| y::ys => (y + x/2) :: bla (x/2) ys
|
||
else
|
||
match ys with
|
||
| [] => []
|
||
| y::ys => (y + x/2 + 1) :: bla (x/2) ys
|
||
|
||
def pbla (x : Nat) (ys : PList Nat) : PList Nat :=
|
||
if x % 2 == 0 then
|
||
match ys with
|
||
| PList.nil => PList.nil
|
||
| y:::ys => (y + x/2) ::: pbla (x/2) ys
|
||
else
|
||
match ys with
|
||
| PList.nil => PList.nil
|
||
| y:::ys => (y + x/2 + 1) ::: pbla (x/2) ys
|
||
termination_by structural ys
|
||
|
||
theorem blaEq (y : Nat) (ys : List Nat) : bla 4 (y::ys) = (y+2) :: bla 2 ys :=
|
||
rfl
|
||
|
||
inductive PNat : Prop
|
||
| zero
|
||
| succ : PNat → PNat
|
||
|
||
def f : Nat → Nat → Nat
|
||
| 0, y => y
|
||
| x+1, y =>
|
||
match f x y with
|
||
| 0 => f x y
|
||
| v => f x v + 1
|
||
|
||
def pf : PNat → PNat → PNat
|
||
| PNat.zero, y => y
|
||
| PNat.succ x, y =>
|
||
match pf x y with
|
||
| PNat.zero => pf x y
|
||
| v => PNat.succ $ pf x v
|
||
|
||
def g (xs : List Nat) : Nat :=
|
||
match xs with
|
||
| [] => 0
|
||
| y::ys =>
|
||
match ys with
|
||
| [] => 1
|
||
| _ => g ys + 1
|
||
|
||
def pg (xs : PList Nat) : True :=
|
||
match xs with
|
||
| PList.nil => True.intro
|
||
| y:::ys =>
|
||
match ys with
|
||
| PList.nil => True.intro
|
||
| _ => pg ys
|
||
|
||
def aux : Nat → Nat → Nat
|
||
| 0, y => y
|
||
| x+1, y =>
|
||
match f x y with
|
||
| 0 => f x y
|
||
| v => f x v + 1
|
||
|
||
def paux : PNat → PNat → PNat
|
||
| PNat.zero, y => y
|
||
| PNat.succ x, y =>
|
||
match pf x y with
|
||
| PNat.zero => pf x y
|
||
| v => PNat.succ (pf x v)
|
||
|
||
theorem ex (x y : Nat) : f x y = aux x y := by
|
||
cases x
|
||
rfl
|
||
rfl
|
||
|
||
axiom F : Nat → Nat
|
||
|
||
inductive is_nat : Nat -> Prop
|
||
| Z : is_nat 0
|
||
| S {n} : is_nat n → is_nat (F n)
|
||
|
||
inductive is_nat_T : Nat -> Type
|
||
| Z : is_nat_T 0
|
||
| S {n} : is_nat_T n → is_nat_T (F n)
|
||
|
||
axiom P : Nat → Prop
|
||
axiom F0 : P 0
|
||
axiom F1 : P (F 0)
|
||
axiom FS {n : Nat} : P n → P (F (F n))
|
||
|
||
axiom T : Nat → Prop
|
||
axiom TF0 : T 0
|
||
axiom TF1 : T (F 0)
|
||
axiom TFS {n : Nat} : T n → T (F (F n))
|
||
|
||
-- set_option trace.Elab.definition.structural true in
|
||
theorem «nested recursion» : ∀ {n}, is_nat n → P n
|
||
| _, is_nat.Z => F0
|
||
| _, is_nat.S is_nat.Z => F1
|
||
| _, is_nat.S (is_nat.S h) => FS («nested recursion» h)
|
||
|
||
/-- forbidding this, because it shouldn't exist in the first place.
|
||
We don't expect this kind of inconsistent inaccessible patterns. -/
|
||
-- theorem «nested recursion, inaccessible» : ∀ {n}, is_nat n → P n
|
||
-- | _, .(is_nat.Z) => F0
|
||
-- | _, is_nat.S .(is_nat.Z) => F1
|
||
-- | _, is_nat.S (is_nat.S h) => FS («nested recursion, inaccessible» h)
|
||
|
||
theorem «reordered discriminants, type» : ∀ n, is_nat_T n → Nat → T n := fun n hn m =>
|
||
match n, m, hn with
|
||
| _, _, is_nat_T.Z => TF0
|
||
| _, _, is_nat_T.S is_nat_T.Z => TF1
|
||
| _, m, is_nat_T.S (is_nat_T.S h) => TFS («reordered discriminants, type» _ h m)
|
||
|
||
|
||
theorem «reordered discriminants» : ∀ n, is_nat n → Nat → P n := fun n hn m =>
|
||
match n, m, hn with
|
||
| _, _, is_nat.Z => F0
|
||
| _, _, is_nat.S is_nat.Z => F1
|
||
| _, m, is_nat.S (is_nat.S h) => FS («reordered discriminants» _ h m)
|
||
termination_by structural _ n => n
|
||
|
||
/- known unsupported case for types, just here for reference. -/
|
||
-- def «unsupported nesting» (xs : List Nat) : True :=
|
||
-- match xs with
|
||
-- | List.nil => True.intro
|
||
-- | y::ys =>
|
||
-- match ys with
|
||
-- | List.nil => True.intro
|
||
-- | _::_::zs => «unsupported nesting» zs
|
||
-- | zs => «unsupported nesting» ys
|
||
|
||
def «unsupported nesting, predicate» (xs : PList Nat) : True :=
|
||
match xs with
|
||
| PList.nil => True.intro
|
||
| y:::ys =>
|
||
match ys with
|
||
| PList.nil => True.intro
|
||
| _:::_:::zs => «unsupported nesting, predicate» zs
|
||
| zs => «unsupported nesting, predicate» ys
|
||
|
||
|
||
def f1 (xs : List Nat) : Nat :=
|
||
match xs with
|
||
| [] => 0
|
||
| x::xs =>
|
||
match xs with
|
||
| [] => 0
|
||
| _ => f1 xs + 1
|
||
|
||
def pf1 (xs : PList Nat) : True :=
|
||
match xs with
|
||
| PList.nil => True.intro
|
||
| x:::xs =>
|
||
match xs with
|
||
| PList.nil => True.intro
|
||
| _ => pf1 xs
|