test: sizeOf experiments
This commit is contained in:
Leonardo de Moura
parent
f1ed13efff
commit
dc142cff13
3 changed files with 402 additions and 0 deletions
210
tests/playground/sizeof1.lean
Normal file
210
tests/playground/sizeof1.lean
Normal file
|
|
@ -0,0 +1,210 @@
|
|||
mutual
|
||||
|
||||
inductive TreePos (α : Type u) (β : Type v) where
|
||||
| leaf (a : α)
|
||||
| node (children : List (List (TreeNeg α β)))
|
||||
|
||||
inductive TreeNeg (α : Type u) (β : Type v) where
|
||||
| leaf (a : β)
|
||||
| node (children : List (List (TreePos α β)))
|
||||
|
||||
end
|
||||
|
||||
#check @TreePos.rec
|
||||
#check @TreePos.rec_1
|
||||
#check @TreePos.rec_2
|
||||
#check @TreePos.rec_3
|
||||
#check @TreePos.rec_4
|
||||
#check @TreeNeg.rec
|
||||
|
||||
noncomputable def sizeof_1 [SizeOf α] [SizeOf β] (x : TreePos α β) : Nat :=
|
||||
@TreePos.rec α β (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat)
|
||||
(fun a => 1 + sizeOf a)
|
||||
(fun _ ih => 1 + ih)
|
||||
(fun b => 1 + sizeOf b)
|
||||
(fun _ ih => 1 + ih)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
x
|
||||
|
||||
noncomputable def sizeof_2 [SizeOf α] [SizeOf β] (x : TreeNeg α β) : Nat :=
|
||||
@TreeNeg.rec α β (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat)
|
||||
(fun a => 1 + sizeOf a)
|
||||
(fun _ ih => 1 + ih)
|
||||
(fun b => 1 + sizeOf b)
|
||||
(fun _ ih => 1 + ih)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
x
|
||||
|
||||
noncomputable def sizeof_3 [SizeOf α] [SizeOf β] (x : List (List (TreeNeg α β))) : Nat :=
|
||||
@TreePos.rec_1 α β (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat)
|
||||
(fun a => 1 + sizeOf a)
|
||||
(fun _ ih => 1 + ih)
|
||||
(fun b => 1 + sizeOf b)
|
||||
(fun _ ih => 1 + ih)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
x
|
||||
|
||||
noncomputable def sizeof_4 [SizeOf α] [SizeOf β] (x : List (List (TreePos α β))) : Nat :=
|
||||
@TreePos.rec_2 α β (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat)
|
||||
(fun a => 1 + sizeOf a)
|
||||
(fun _ ih => 1 + ih)
|
||||
(fun b => 1 + sizeOf b)
|
||||
(fun _ ih => 1 + ih)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
x
|
||||
|
||||
noncomputable def sizeof_5 [SizeOf α] [SizeOf β] (x : List (TreeNeg α β)) : Nat :=
|
||||
@TreePos.rec_3 α β (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat)
|
||||
(fun a => 1 + sizeOf a)
|
||||
(fun _ ih => 1 + ih)
|
||||
(fun b => 1 + sizeOf b)
|
||||
(fun _ ih => 1 + ih)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
x
|
||||
|
||||
noncomputable def sizeof_6 [SizeOf α] [SizeOf β] (x : List (TreePos α β)) : Nat :=
|
||||
@TreePos.rec_4 α β (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat)
|
||||
(fun a => 1 + sizeOf a)
|
||||
(fun _ ih => 1 + ih)
|
||||
(fun b => 1 + sizeOf b)
|
||||
(fun _ ih => 1 + ih)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
x
|
||||
|
||||
noncomputable instance [SizeOf α] [SizeOf β] : SizeOf (TreePos α β) := ⟨sizeof_1⟩
|
||||
|
||||
noncomputable instance [SizeOf α] [SizeOf β] : SizeOf (TreeNeg α β) := ⟨sizeof_2⟩
|
||||
|
||||
theorem aux_1 [SizeOf α] [SizeOf β] (cs : List (TreePos α β)) : sizeof_6 cs = sizeOf cs :=
|
||||
@TreePos.rec_4 α β (fun _ => True) (fun _ => True) (fun _ => True) (fun _ => True) (fun _ => True) (fun cs => sizeof_6 cs = sizeOf cs)
|
||||
(fun a => trivial)
|
||||
(fun _ ih => trivial)
|
||||
(fun b => trivial)
|
||||
(fun _ ih => trivial)
|
||||
trivial
|
||||
(fun _ _ ih₁ ih₂ => trivial)
|
||||
trivial
|
||||
(fun _ _ _ _ => trivial)
|
||||
trivial
|
||||
(fun _ _ ih₁ ih₂ => trivial)
|
||||
rfl
|
||||
(fun h t ih₁ ih₂ => by
|
||||
show 1 + sizeof_1 h + sizeof_6 t = 1 + sizeOf h + sizeOf t
|
||||
rw ih₂
|
||||
rfl)
|
||||
cs
|
||||
|
||||
theorem aux_2 [SizeOf α] [SizeOf β] (cs : List (List (TreePos α β))) : sizeof_4 cs = sizeOf cs :=
|
||||
@TreePos.rec_2 α β (fun _ => True) (fun _ => True) (fun _ => True) (fun cs => sizeof_4 cs = sizeOf cs) (fun _ => True) (fun _ => True)
|
||||
(fun a => trivial)
|
||||
(fun _ ih => trivial)
|
||||
(fun b => trivial)
|
||||
(fun _ ih => trivial)
|
||||
trivial
|
||||
(fun _ _ ih₁ ih₂ => trivial)
|
||||
rfl
|
||||
(fun h t ih₁ ih₂ => by
|
||||
show sizeof_4 (h::t) = sizeOf (h::t)
|
||||
show 1 + sizeof_6 h + sizeof_4 t = 1 + sizeOf h + sizeOf t
|
||||
rw ih₂
|
||||
rw aux_1)
|
||||
trivial
|
||||
(fun _ _ ih₁ ih₂ => trivial)
|
||||
trivial
|
||||
(fun _ _ ih₁ ih₂ => trivial)
|
||||
cs
|
||||
|
||||
theorem aux_3 [SizeOf α] [SizeOf β] (cs : List (TreeNeg α β)) : sizeof_5 cs = sizeOf cs :=
|
||||
@TreePos.rec_3 α β (fun _ => True) (fun _ => True) (fun _ => True) (fun _ => True) (fun cs => sizeof_5 cs = sizeOf cs) (fun _ => True)
|
||||
(fun a => trivial)
|
||||
(fun _ ih => trivial)
|
||||
(fun b => trivial)
|
||||
(fun _ ih => trivial)
|
||||
trivial
|
||||
(fun _ _ ih₁ ih₂ => trivial)
|
||||
trivial
|
||||
(fun _ _ _ _ => trivial)
|
||||
rfl
|
||||
(fun h t ih₁ ih₂ => by
|
||||
show 1 + sizeof_2 h + sizeof_5 t = 1 + sizeOf h + sizeOf t
|
||||
rw ih₂
|
||||
rfl)
|
||||
trivial
|
||||
(fun _ _ ih₁ ih₂ => trivial)
|
||||
cs
|
||||
|
||||
theorem aux_4 [SizeOf α] [SizeOf β] (cs : List (List (TreeNeg α β))) : sizeof_3 cs = sizeOf cs :=
|
||||
@TreePos.rec_1 α β (fun _ => True) (fun _ => True) (fun cs => sizeof_3 cs = sizeOf cs) (fun _ => True) (fun _ => True) (fun _ => True)
|
||||
(fun a => trivial)
|
||||
(fun _ ih => trivial)
|
||||
(fun b => trivial)
|
||||
(fun _ ih => trivial)
|
||||
rfl
|
||||
(fun h t ih₁ ih₂ => by
|
||||
show sizeof_3 (h::t) = sizeOf (h::t)
|
||||
show 1 + sizeof_5 h + sizeof_3 t = 1 + sizeOf h + sizeOf t
|
||||
rw ih₂
|
||||
rw aux_3)
|
||||
trivial
|
||||
(fun _ _ ih₁ ih₂ => trivial)
|
||||
trivial
|
||||
(fun _ _ ih₁ ih₂ => trivial)
|
||||
trivial
|
||||
(fun _ _ ih₁ ih₂ => trivial)
|
||||
cs
|
||||
|
||||
theorem TreePos.leaf.sizeOf_spec [SizeOf α] [SizeOf β] (a : α) : sizeOf (TreePos.leaf (β := β) a) = 1 + sizeOf a :=
|
||||
rfl
|
||||
|
||||
theorem TreePos.node.sizeOf_spec [SizeOf α] [SizeOf β] (cs : List (List (TreeNeg α β))) : sizeOf (TreePos.node cs) = 1 + sizeOf cs := by
|
||||
show 1 + sizeof_3 cs = 1 + sizeOf cs
|
||||
rw aux_4
|
||||
|
||||
theorem TreeNeg.leaf.sizeOf_spec [SizeOf α] [SizeOf β] (b : β) : sizeOf (TreeNeg.leaf (α := α) b) = 1 + sizeOf b :=
|
||||
rfl
|
||||
|
||||
theorem TreeNeg.node.sizeOf_spec [SizeOf α] [SizeOf β] (cs : List (List (TreePos α β))) : sizeOf (TreeNeg.node cs) = 1 + sizeOf cs := by
|
||||
show 1 + sizeof_4 cs = 1 + sizeOf cs
|
||||
rw aux_2
|
||||
60
tests/playground/sizeof2.lean
Normal file
60
tests/playground/sizeof2.lean
Normal file
|
|
@ -0,0 +1,60 @@
|
|||
mutual
|
||||
|
||||
inductive Arg (α : Type u) where
|
||||
| val (a : α)
|
||||
| expr (e : Expr α)
|
||||
|
||||
inductive Expr (α : Type u) where
|
||||
| app (f : String) (a : List (Arg α))
|
||||
|
||||
end
|
||||
|
||||
noncomputable def sizeof_1 [SizeOf α] (a : Arg α) :=
|
||||
@Arg.rec α (fun _ => Nat) (fun _ => Nat) (fun _ => Nat)
|
||||
(fun a => 1 + sizeOf a)
|
||||
(fun e ih => 1 + ih)
|
||||
(fun f _ ih => 1 + sizeOf f + ih)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
a
|
||||
|
||||
noncomputable def sizeof_2 [SizeOf α] (a : Expr α) :=
|
||||
@Expr.rec α (fun _ => Nat) (fun _ => Nat) (fun _ => Nat)
|
||||
(fun a => 1 + sizeOf a)
|
||||
(fun e ih => 1 + ih)
|
||||
(fun f _ ih => 1 + sizeOf f + ih)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
a
|
||||
|
||||
noncomputable def sizeof_3 [SizeOf α] (a : List (Arg α)) :=
|
||||
@Arg.rec_1 α (fun _ => Nat) (fun _ => Nat) (fun _ => Nat)
|
||||
(fun a => 1 + sizeOf a)
|
||||
(fun e ih => 1 + ih)
|
||||
(fun f _ ih => 1 + sizeOf f + ih)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
a
|
||||
|
||||
noncomputable instance [SizeOf α] : SizeOf (Arg α) := ⟨sizeof_1⟩
|
||||
|
||||
noncomputable instance [SizeOf α] : SizeOf (Expr α) := ⟨sizeof_2⟩
|
||||
|
||||
theorem aux_1 [SizeOf α] (a : List (Arg α)) : sizeof_3 a = sizeOf a := by
|
||||
induction a with
|
||||
| nil => rfl
|
||||
| cons h t ih =>
|
||||
show sizeof_3 (h :: t) = sizeOf (h :: t)
|
||||
show 1 + sizeof_1 h + sizeof_3 t = 1 + sizeOf h + sizeOf t
|
||||
rw ih
|
||||
rfl
|
||||
|
||||
theorem Arg.val.sizeOf_spec [SizeOf α] (a : α) : sizeOf (Arg.val a) = 1 + sizeOf a :=
|
||||
rfl
|
||||
|
||||
theorem Arg.expr.sizeOf_spec [SizeOf α] (e : Expr α) : sizeOf (Arg.expr e) = 1 + sizeOf e :=
|
||||
rfl
|
||||
|
||||
theorem Expr.app.sizeOf_spec [SizeOf α] (f : String) (args : List (Arg α)) : sizeOf (Expr.app f args) = 1 + sizeOf f + sizeOf args := by
|
||||
show 1 + sizeOf f + sizeof_3 args = 1 + sizeOf f + sizeOf args
|
||||
rw aux_1
|
||||
132
tests/playground/sizeof3.lean
Normal file
132
tests/playground/sizeof3.lean
Normal file
|
|
@ -0,0 +1,132 @@
|
|||
mutual
|
||||
inductive AList (α β : Type u)
|
||||
| nil
|
||||
| cons (a : α) (t : BList α β)
|
||||
|
||||
inductive BList (α β : Type u)
|
||||
| cons (b : β) (t : AList α β)
|
||||
end
|
||||
|
||||
namespace AList
|
||||
|
||||
noncomputable def sizeof_1 [SizeOf α] [SizeOf β] (a : AList α β) : Nat :=
|
||||
@AList.rec α β (fun _ => Nat) (fun _ => Nat)
|
||||
1
|
||||
(fun a _ ih => 1 + sizeOf a + ih)
|
||||
(fun b _ ih => 1 + sizeOf b + ih)
|
||||
a
|
||||
|
||||
noncomputable def sizeof_2 [SizeOf α] [SizeOf β] (a : BList α β) : Nat :=
|
||||
@BList.rec α β (fun _ => Nat) (fun _ => Nat)
|
||||
1
|
||||
(fun a _ ih => 1 + sizeOf a + ih)
|
||||
(fun b _ ih => 1 + sizeOf b + ih)
|
||||
a
|
||||
|
||||
noncomputable instance [SizeOf α] [SizeOf β] : SizeOf (AList α β) := ⟨sizeof_1⟩
|
||||
noncomputable instance [SizeOf α] [SizeOf β] : SizeOf (BList α β) := ⟨sizeof_2⟩
|
||||
|
||||
end AList
|
||||
|
||||
theorem AList.nil.sizeOf_spec [SizeOf α] [SizeOf β] : sizeOf (AList.nil : AList α β) = 1 :=
|
||||
rfl
|
||||
|
||||
theorem AList.cons.sizeOf_spec [SizeOf α] [SizeOf β] (a : α) (t : BList α β) : sizeOf (AList.cons a t) = 1 + sizeOf a + sizeOf t :=
|
||||
rfl
|
||||
|
||||
theorem BList.cons.sizeOf_spec [SizeOf α] [SizeOf β] (b : β) (t : AList α β) : sizeOf (BList.cons a t) = 1 + sizeOf a + sizeOf t :=
|
||||
rfl
|
||||
|
||||
mutual
|
||||
inductive Foo (α : Type u)
|
||||
| mk (cs : AList (Foo α) (Boo α))
|
||||
|
||||
inductive Boo (α : Type u)
|
||||
| mk (a : α) (cs : BList (Foo α) (Boo α))
|
||||
end
|
||||
|
||||
#check @Foo.rec
|
||||
#check @Foo.rec_1
|
||||
#check @Foo.rec_2
|
||||
#check @Boo.rec
|
||||
|
||||
namespace Foo
|
||||
|
||||
noncomputable def sizeof_1 [SizeOf α] (a : Foo α) : Nat :=
|
||||
@Foo.rec α (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat)
|
||||
(fun _ ih => 1 + ih)
|
||||
(fun a _ ih => 1 + sizeOf a + ih)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
a
|
||||
|
||||
noncomputable def sizeof_2 [SizeOf α] (a : Boo α) : Nat :=
|
||||
@Boo.rec α (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat)
|
||||
(fun _ ih => 1 + ih)
|
||||
(fun a _ ih => 1 + sizeOf a + ih)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
a
|
||||
|
||||
noncomputable def sizeof_3 [SizeOf α] (a : AList (Foo α) (Boo α)) : Nat :=
|
||||
@Foo.rec_1 α (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat)
|
||||
(fun _ ih => 1 + ih)
|
||||
(fun a _ ih => 1 + sizeOf a + ih)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
a
|
||||
|
||||
noncomputable def sizeof_4 [SizeOf α] (a : BList (Foo α) (Boo α)) : Nat :=
|
||||
@Foo.rec_2 α (fun _ => Nat) (fun _ => Nat) (fun _ => Nat) (fun _ => Nat)
|
||||
(fun _ ih => 1 + ih)
|
||||
(fun a _ ih => 1 + sizeOf a + ih)
|
||||
1
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
(fun _ _ ih₁ ih₂ => 1 + ih₁ + ih₂)
|
||||
a
|
||||
|
||||
noncomputable instance [SizeOf α] : SizeOf (Foo α) := ⟨sizeof_1⟩
|
||||
noncomputable instance [SizeOf α] : SizeOf (Boo α) := ⟨sizeof_2⟩
|
||||
|
||||
theorem aux_1 [SizeOf α] (a : AList (Foo α) (Boo α)) : sizeof_3 a = sizeOf a :=
|
||||
@AList.rec (Foo α) (Boo α) (fun a => sizeof_3 a = sizeOf a) (fun b => sizeof_4 b = sizeOf b)
|
||||
rfl
|
||||
(fun a t ih => by
|
||||
show sizeof_3 (AList.cons a t) = sizeOf (AList.cons a t)
|
||||
show 1 + sizeOf a + sizeof_4 t = sizeOf (AList.cons a t)
|
||||
rw ih
|
||||
rfl)
|
||||
(fun b t ih => by
|
||||
show sizeof_4 (BList.cons b t) = sizeOf (BList.cons b t)
|
||||
show 1 + sizeOf b + sizeof_3 t = sizeOf (BList.cons b t)
|
||||
rw ih
|
||||
rfl)
|
||||
a
|
||||
|
||||
theorem aux_2 [SizeOf α] (a : BList (Foo α) (Boo α)) : sizeof_4 a = sizeOf a :=
|
||||
@BList.rec (Foo α) (Boo α) (fun a => sizeof_3 a = sizeOf a) (fun b => sizeof_4 b = sizeOf b)
|
||||
rfl
|
||||
(fun a t ih => by
|
||||
show sizeof_3 (AList.cons a t) = sizeOf (AList.cons a t)
|
||||
show 1 + sizeOf a + sizeof_4 t = sizeOf (AList.cons a t)
|
||||
rw ih
|
||||
rfl)
|
||||
(fun b t ih => by
|
||||
show sizeof_4 (BList.cons b t) = sizeOf (BList.cons b t)
|
||||
show 1 + sizeOf b + sizeof_3 t = sizeOf (BList.cons b t)
|
||||
rw ih
|
||||
rfl)
|
||||
a
|
||||
|
||||
end Foo
|
||||
|
||||
theorem Foo.mk.sizeOf_spec [SizeOf α] (cs : AList (Foo α) (Boo α)) : sizeOf (Foo.mk cs) = 1 + sizeOf cs := by
|
||||
show 1 + Foo.sizeof_3 cs = 1 + sizeOf cs
|
||||
rw Foo.aux_1
|
||||
|
||||
theorem Boo.mk.sizeOf_spec [SizeOf α] (a : α) (cs : BList (Foo α) (Boo α)) : sizeOf (Boo.mk a cs) = 1 + sizeOf a + sizeOf cs := by
|
||||
show 1 + sizeOf a + Foo.sizeof_4 cs = 1 + sizeOf a + sizeOf cs
|
||||
rw Foo.aux_2
|
||||
Loading…
Add table
Reference in a new issue