refactor: generalize the theory and perform some lifts

Move forward the "HSpec" idea, move around files, construct the hierarchy of trees, etc.

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>

6 files changed, 286 insertions, 107 deletions

diff --git a/AvlVerification/BinarySearchTree.lean b/AvlVerification/BinarySearchTree.lean
new file mode 100644
index 0000000..130fd73
--- /dev/null
+++ b/AvlVerification/BinarySearchTree.lean
@@ -0,0 +1,37 @@
+import AvlVerification.Tree
+
+namespace BST
+
+open Primitives (Result)
+open avl_verification (AVLNode Ordering)
+open Tree (AVLTree AVLNode.left AVLNode.right AVLNode.val)
+
+inductive ForallNode (p: T -> Prop): AVLTree T -> Prop
+| none : ForallNode p none
+| some (a: T) (left: AVLTree T) (right: AVLTree T) : ForallNode p left -> p a -> ForallNode p right -> ForallNode p (some (AVLNode.mk a left right))
+
+-- This is the binary search invariant.
+inductive BST [LT T]: AVLTree T -> Prop
+| none : BST none
+| some (a: T) (left: AVLTree T) (right: AVLTree T) : 
+  ForallNode (fun v => v < a) left -> ForallNode (fun v => a < v) right
+  -> BST left -> BST right -> BST (some (AVLNode.mk a left right))
+
+@[simp]
+theorem singleton_bst [LT T] {a: T}: BST (some (AVLNode.mk a none none)) := by
+  apply BST.some
+  all_goals simp [ForallNode.none, BST.none] 
+
+theorem left [LT T] {t: AVLTree T}: BST t -> BST t.left := by
+  intro H
+  induction H with 
+  | none => exact BST.none
+  | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.left]; assumption
+
+theorem right [LT T] {t: AVLTree T}: BST t -> BST t.right := by
+  intro H
+  induction H with 
+  | none => exact BST.none
+  | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.right]; assumption
+
+end BST
diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean
new file mode 100644
index 0000000..870e9c2
--- /dev/null
+++ b/AvlVerification/Insert.lean
@@ -0,0 +1,87 @@
+import AvlVerification.Tree
+import AvlVerification.BinarySearchTree
+import AvlVerification.Specifications
+
+namespace Implementation
+
+open Primitives
+open avl_verification
+open Tree (AVLTree)
+
+variable {T: Type}
+
+@[pspec]
+theorem AVLTreeSet.insert_loop_spec {H: avl_verification.Ord T} 
+  (a: T) (t: Option (AVLNode T))
+  [LT T]
+  (Hbs_search: BST.BST t)
+  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o):
+  ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ret ⟨ added, t_new ⟩
+--  ∧ AVLTree.set t'.2 = insert a (AVLTree.set t)
+  ∧ BST.BST t_new
+  := by match t with
+  | none =>
+    simp [AVLTreeSet.insert_loop, AVLTree.set, setOf, BST.BST]
+  | some (AVLNode.mk b left right) =>
+    rw [AVLTreeSet.insert_loop]
+    simp only []
+    progress keep Hordering as ⟨ ordering ⟩
+    cases ordering
+    all_goals simp only []
+    have Hbs_search_right: BST.BST right := BST.right Hbs_search
+    have Hbs_search_left: BST.BST left := BST.left Hbs_search
+    {
+      progress keep Htree as ⟨ added₁, right₁, Hbst ⟩
+      refine' ⟨ added₁, ⟨ some (AVLNode.mk b left right₁), _ ⟩ ⟩
+      simp only [true_and]
+      refine' (BST.BST.some b left right₁ _ _ Hbs_search_left Hbst)
+      cases' Hbs_search; assumption
+      induction right with
+      | none =>
+        simp [AVLTreeSet.insert_loop] at Htree
+        rw [← Htree.2]
+        refine' (BST.ForallNode.some _ _ _ BST.ForallNode.none _ BST.ForallNode.none)
+        sorry
+      | some node =>
+        -- clef: ∀ x ∈ node.right, b < x
+        -- de plus: b < a
+        -- or, right₁ = insert a node.right moralement
+        -- donc, il suffit de prouver que: ∀ x ∈ insert a node.right, b < x <-> b < a /\ ∀ x ∈ node.right, b < x
+        sorry
+    }
+    {
+      simp [Hbs_search]
+    }
+    {
+      -- Symmetric case of left.
+      sorry
+    }
+
+@[pspec]
+def AVLTreeSet.insert_spec 
+  {H: avl_verification.Ord T} 
+  -- TODO: this can be generalized into `H.cmp` must be an equivalence relation.
+  -- and insert works no longer on Sets but on set quotiented by this equivalence relation.
+  (Hcmp_eq: ∀ a b, H.cmp a b = Result.ret Ordering.Equal -> a = b)
+  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o)
+  (Hbs_search: @BSTree.searchInvariant _ H t)
+  (a: T) (t: AVLTreeSet T):
+  ∃ t', t.insert _ H a = Result.ret t' 
+  -- set of values *POST* insertion is {a} \cup set of values of the *PRE* tree.
+  ∧ AVLTree.setOf t'.2.root = insert a (AVLTree.setOf t.root) 
+  -- it's still a binary search tree.
+  ∧ @BSTree.searchInvariant _ H t'.2.root
+  -- TODO(reinforcement): (t'.1 is false <=> a \in AVLTree.setOf t.root)
+  := by
+  rw [AVLTreeSet.insert]
+  progress keep h as ⟨ t', Hset ⟩; simp
+  rw [Hset]
+  sorry
+
+
+-- insert is infaillible, right?
+-- instance [LT T] (o: avl_verification.Ord T): Insert T (AVLTreeSet T) where
+--   insert x tree := (AVLTreeSet.insert T o tree x).map (fun (added, tree) => tree)
+
+end Implementation
+
diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean
new file mode 100644
index 0000000..0bf9ffb
--- /dev/null
+++ b/AvlVerification/Specifications.lean
@@ -0,0 +1,55 @@
+import «AvlVerification»
+
+namespace Primitives
+
+namespace Result
+
+def map {A B: Type} (x: Result A) (f: A -> B): Result B := match x with
+| .ret y => .ret (f y)
+| .fail e => .fail e
+| .div => .div
+
+end Result
+
+end Primitives
+
+namespace avl_verification
+
+def Ordering.toLeanOrdering (o: avl_verification.Ordering): _root_.Ordering := match o with 
+| .Less => .lt
+| .Equal => .eq
+| .Greater => .gt
+
+end avl_verification
+
+namespace Specifications
+
+open Primitives
+open Result
+
+variable {T: Type}
+
+class OrdSpec (U: Type) where
+  cmp: U -> U -> Result Ordering
+  infallible: ∀ a b, ∃ o, cmp a b = .ret o
+
+instance: Coe (avl_verification.Ordering) (_root_.Ordering) where
+  coe a := a.toLeanOrdering
+
+def ordSpecOfInfaillible
+  (H: avl_verification.Ord T)
+  (Hresult: ∀ a b, ∃ o, H.cmp a b = Primitives.Result.ret o)
+  : OrdSpec T where
+  cmp x y := (H.cmp x y).map (fun z => z.toLeanOrdering)
+  infallible := by
+    intros a b
+     -- TODO: transform the "raw" hypothesis into the "nice" hypothesis.
+    sorry
+
+instance [OrdSpec T]: Ord T where
+  compare x y := match (OrdSpec.cmp x y) with 
+  | .ret z => z
+  | .fail _ => by sorry
+  | .div => by sorry
+
+end Specifications
diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean
new file mode 100644
index 0000000..3316e9e
--- /dev/null
+++ b/AvlVerification/Tree.lean
@@ -0,0 +1,81 @@
+import «AvlVerification»
+
+namespace Tree
+
+variable {T: Type}
+
+open avl_verification
+
+-- Otherwise, Lean cannot prove termination by itself.
+@[reducible]
+def AVLTree (U: Type) := Option (AVLNode U)
+def AVLTree.nil: AVLTree T := none
+
+def AVLTree.val (t: AVLTree T): Option T := match t with
+| none => none
+| some (AVLNode.mk x _ _) => some x
+
+def AVLTree.left (t: AVLTree T): AVLTree T := match t with
+| none => none
+| some (AVLNode.mk _ left _) => left
+
+def AVLTree.right (t: AVLTree T): AVLTree T := match t with
+| none => none
+| some (AVLNode.mk _ _ right) => right
+
+def AVLNode.left (t: AVLNode T): AVLTree T := match t with
+| AVLNode.mk _ left _ => left
+
+def AVLNode.right (t: AVLNode T): AVLTree T := match t with
+| AVLNode.mk _ _ right => right
+
+def AVLNode.val (t: AVLNode T): T := match t with
+| AVLNode.mk x _ _ => x
+
+mutual
+def AVLTree.height_node (tree: AVLNode T): Nat := match tree with
+| AVLNode.mk y left right => 1 + AVLTree.height left + AVLTree.height right
+
+def AVLTree.height (tree: AVLTree T): Nat := match tree with 
+| none => 0
+| some n => 1 + AVLTree.height_node n
+end
+
+def AVLTreeSet.nil: AVLTreeSet T := { root := AVLTree.nil }
+
+-- Automatic synthesization of this seems possible at the Lean level?
+instance: Inhabited (AVLTree T) where
+  default := AVLTree.nil
+
+instance: Inhabited (AVLTreeSet T) where
+  default := AVLTreeSet.nil
+
+instance: Coe (Option (AVLNode T)) (AVLTree T) where
+  coe x := x
+
+-- TODO: ideally, it would be nice if we could generalize
+-- this to any `BinaryTree` typeclass.
+
+def AVLTree.mem (tree: AVLTree T) (x: T) :=
+  match tree with
+  | none => False
+  | some (AVLNode.mk y left right) => x = y ∨ AVLTree.mem left x ∨ AVLTree.mem right x
+
+@[simp]
+def AVLTree.mem_none: AVLTree.mem none = ({}: Set T) := rfl
+
+@[simp]
+def AVLTree.mem_some {x: T} {left right: AVLTree T}: AVLTree.mem (some (AVLNode.mk x left right)) = (({x}: Set T) ∪ AVLTree.mem left ∪ AVLTree.mem right) := by
+  ext y
+  rw [AVLTree.mem]
+  simp [Set.insert_union]
+  simp [Set.insert_def, Set.setOf_set, Set.mem_def, Set.union_def]
+
+-- TODO(reinforcement): ∪ is actually disjoint if we prove this is a binary search tree.
+
+def AVLTree.set (t: AVLTree T): Set T := _root_.setOf (AVLTree.mem t)
+
+def AVLTree.setOf_left_incl (t: AVLTree T): t.left.set ⊂ t.set := sorry
+def AVLTree.setOf_right_incl (t: AVLTree T): t.right.set ⊂ t.set := sorry
+
+end Tree
diff --git a/Main.lean b/Main.lean
index c96af67..6010d26 100644
--- a/Main.lean
+++ b/Main.lean
@@ -10,119 +10,27 @@ namespace Avl
 open avl_verification
 variable {T: Type}
 
-def AVL.nil: AVLTreeSet T := { root := none }
+-- instance {H: avl_verification.Ord T}: LT T := {
+--  lt := λ x y => H.cmp x y = Result.ret Ordering.Less
+-- }
 
+-- This is the binary search invariant.
+def BSTree.searchInvariant {H: avl_verification.Ord T} (t: AVLTree T) := match t with
+| none => True
+| some (AVLNode.mk y u v) => ∀ x ∈ AVLTree.setOf (u : AVLTree T), H.cmp y x = Result.ret Ordering.Less ∧ ∀ x ∈ AVLTree.setOf (v : AVLTree T), H.cmp y x = Result.ret Ordering.Greater
 
--- TODO: AVLTree T ou AVLNode T?
-noncomputable def AVL.height' (tree: AVLNode T): Nat := AVLNode.rec tree
-  (mk := fun _ _ _ ihl ihr => 1 + ihl + ihr)
-  (none := 0)
-  (some := fun _ ih => 1 + ih)
+-- Prove that:
+-- searchInvariant t <-> searchInvariant t.left /\ searchInvariant t.right /\ something about t.val
+-- searchInvariant t -> searchInvariant t.left /\ searchInvariant t.right by weakening.
 
--- Otherwise, Lean cannot prove termination by itself.
-@[reducible]
-def AVLTree (U: Type) := Option (AVLNode U)
+def BSTree.nil_has_searchInvariant {H: avl_verification.Ord T}: @BSTree.searchInvariant _ H AVL.nil.root := by trivial
 
-mutual
-def AVL.height'' (tree: AVLNode T): Nat := match tree with
-| AVLNode.mk y left right => 1 +  AVL.height left + AVL.height right
+theorem BSTree.searchInvariant_children {H: avl_verification.Ord T} (t: AVLTree T): @searchInvariant _ H t -> @searchInvariant _ H t.left ∧ @searchInvariant _ H t.right := sorry
 
-def AVL.height (tree: AVLTree T): Nat := match tree with 
-| none => 0
-| some node => 1 + AVL.height'' node
-end
-
-
-@[reducible]
-def AVLTree.mem (tree: AVLTree T) (x: T) :=
-  match tree with
-  | none => False
-  | some (AVLNode.mk y left right) => x = y ∨ AVLTree.mem left x ∨ AVLTree.mem right x
-
-@[simp]
-def AVLTree.mem_none: AVLTree.mem none = ({}: Set T) := rfl
-
--- TODO: why the explicit type annotation is required here?
--- TODO(reinforcement): ∪ is actually disjoint.
-@[simp]
-def AVLTree.mem_some {x: T} {left right: AVLTree T}: AVLTree.mem (some (AVLNode.mk x left right)) = (({x}: Set T) ∪ AVLTree.mem left ∪ AVLTree.mem right) := by
-  ext y
-  rw [AVLTree.mem]
-  simp [Set.insert_union]
-  simp [Set.insert_def, Set.setOf_set, Set.mem_def, Set.union_def]
-
-
-def AVLTree.setOf: AVLTree T -> Set T := AVLTree.mem
-def AVLTree.val (t: AVLTree T): Option T := match t with
-| none => none
-| some (AVLNode.mk x _ _) => some x
-def AVLTree.left (t: AVLTree T): AVLTree T := match t with
-| none => none
-| some (AVLNode.mk _ left _) => left
-def AVLTree.right (t: AVLTree T): AVLTree T := match t with
-| none => none
-| some (AVLNode.mk _ _ right) => right
+def AVLTree.height (t: AVLTree T) := AVL.height t
+def AVLTree.balanceFactor (t: AVLTree T): Int := t.right.height - t.left.height
+def AVLTree.balanceInvariant (t: AVLTree T) := t.balanceFactor = -1 ∨ t.balanceFactor = 0 ∨ t.balanceFactor = 1
 
 def AVLTree.mem_eq_setOf (t: AVLTree T): AVLTree.mem t = t.setOf := rfl
 
--- TODO: {t.val} = {} if t.val is none else {t.val.get!} otherwise.
--- @[simp]
--- def AVLTree.setOf_eq_union (t: AVLTree T): t.setOf = {t.val} ∪ t.left.setOf ∪ t.right.setOf := sorry
-
--- Note: we would like to have a theorem that says something like
--- t.setOf = {t.val} ∪ t.left.setOf ∪ t.right.setOf
--- but it's not doable because Aeneas does not generate a `structure` but an inductive type with one constructor.
-
-#check AVL.nil
-#check U32.ofInt 0
-#check 0#u32
--- TODO: créer une instance OfNat pour les Uxyz.
--- TODO: générer {} adéquatement... ?
--- TODO: derive from Ord an Lean Order instance.
--- TODO: oh no, H.cmp returns a Result!
-
-@[pspec]
-theorem AVLTreeSet.insert_loop_spec {H: avl_verification.Ord T} 
-  (a: T) (t: Option (AVLNode T))
-  (Hcmp_eq: ∀ a b, H.cmp a b = Result.ret Ordering.Equal -> a = b)
-  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o):
-  ∃ t', AVLTreeSet.insert_loop T H a t = Result.ret t' 
-  ∧ AVLTree.setOf t'.2 = insert a (AVLTree.setOf t) := by match t with
-  | none =>
-    simp [AVLTreeSet.insert_loop, AVLTree.setOf]
-  | some (AVLNode.mk b left right) =>
-    rw [AVLTreeSet.insert_loop]
-    simp only []
-    progress keep Hordering as ⟨ ordering ⟩
-    cases ordering
-    all_goals {
-      -- TODO: oof.
-      -- We are trying to tackle all goals at the same time.
-      -- Refactor this to make it only one simp ideally without even `try`.
-      simp only []
-      try progress keep H as ⟨ t'', Hset ⟩
-      simp [AVLTree.setOf]
-      try simp [AVLTree.setOf] at Hset
-      try simp [Hset]
-      try rw [Set.insert_comm, Set.insert_union]
-      try simp [Hcmp_eq _ _ Hordering]
-    }
-
-@[pspec]
-def AVLTreeSet.insert_spec 
-  {H: avl_verification.Ord T} 
-  -- TODO: this can be generalized into `H.cmp` must be an equivalence relation.
-  -- and insert works no longer on Sets but on set quotiented by this equivalence relation.
-  (Hcmp_eq: ∀ a b, H.cmp a b = Result.ret Ordering.Equal -> a = b)
-  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o)
-  (a: T) (t: AVLTreeSet T):
-  ∃ t', t.insert _ H a = Result.ret t' 
-  -- set of values *POST* insertion is {a} \cup set of values of the *PRE* tree.
-  ∧ AVLTree.setOf t'.2.root = insert a (AVLTree.setOf t.root) 
-  -- TODO(reinforcement): (t'.1 is false <=> a \in AVLTree.setOf t.root)
-  := by
-  rw [AVLTreeSet.insert]
-  progress keep h as ⟨ t', Hset ⟩; simp
-  rw [Hset]
-
 end Avl
diff --git a/notes.md b/notes.md
new file mode 100644
index 0000000..cd82dd3
--- /dev/null
+++ b/notes.md
@@ -0,0 +1,11 @@
+# Formalization notes
+
+- Inhabited is not synthesized systematically for any type.
+- Synthesize type aliases (?): requires to obtain this information before MIR.
+
+## Bundle of specifications
+
+Most of the time, we have naked types which does not exhibit their "expected" specification,
+e.g. an `Ord` trait which does not prove that it's an order.
+
+Ideally, we need to be able to build trait specifications and find a way to unbundle them and use them in the different tactics.