From dc142cff1316f8d9f151ef79f79262ff8b8df846 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 18 Jan 2021 17:21:03 -0800
Subject: [PATCH] test: `sizeOf` experiments

---
 tests/playground/sizeof1.lean | 210 ++++++++++++++++++++++++++++++++++
 tests/playground/sizeof2.lean |  60 ++++++++++
 tests/playground/sizeof3.lean | 132 +++++++++++++++++++++
 3 files changed, 402 insertions(+)
 create mode 100644 tests/playground/sizeof1.lean
 create mode 100644 tests/playground/sizeof2.lean
 create mode 100644 tests/playground/sizeof3.lean

diff --git a/tests/playground/sizeof1.lean b/tests/playground/sizeof1.lean
new file mode 100644
index 0000000000..23ff335fd2
--- /dev/null
+++ b/tests/playground/sizeof1.lean
@@ -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
diff --git a/tests/playground/sizeof2.lean b/tests/playground/sizeof2.lean
new file mode 100644
index 0000000000..c19778d383
--- /dev/null
+++ b/tests/playground/sizeof2.lean
@@ -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
diff --git a/tests/playground/sizeof3.lean b/tests/playground/sizeof3.lean
new file mode 100644
index 0000000000..128c3cb9f5
--- /dev/null
+++ b/tests/playground/sizeof3.lean
@@ -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