1 files changed, 65 insertions, 30 deletions

diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean
index 3c2b8b3..baf3441 100644
--- a/AvlVerification/Insert.lean
+++ b/AvlVerification/Insert.lean
@@ -7,9 +7,47 @@ namespace Implementation
 open Primitives
 open avl_verification
 open Tree (AVLTree)
-open Specifications (OrdSpec ordSpecOfInfaillible ordOfOrdSpec ltOfRustOrder)
+open Specifications (OrdSpec ordSpecOfTotalityAndDuality ordOfOrdSpec ltOfRustOrder gtOfRustOrder)
+
+example: OrdSpec OrdU32 := ordSpecOfTotalityAndDuality _ 
+  (by 
+  -- Totality
+  intro a b
+  unfold Ord.cmp
+  unfold OrdU32
+  unfold OrdU32.cmp
+  if hlt : a < b then 
+    use .Less
+    simp [hlt]
+  else
+    if heq: a = b
+    then
+    use .Equal
+    simp [hlt]
+    rw [heq]
+    -- TODO: simp [hlt, heq] breaks everything???
+    else
+      use .Greater
+      simp [hlt, heq]
+  ) (by 
+  -- Duality
+  intro a b Hgt
+  if hlt : b < a then
+    unfold Ord.cmp
+    unfold OrdU32
+    unfold OrdU32.cmp
+    simp [hlt]
+  else
+    unfold Ord.cmp at Hgt
+    unfold OrdU32 at Hgt
+    unfold OrdU32.cmp at Hgt
+    have hnlt : ¬ (a < b) := sorry
+    have hneq : ¬ (a = b) := sorry
+    exfalso
+    apply hlt
+    -- I need a Preorder on U32 now.
+    sorry)
 
--- TODO: OSpec should be proven.
 variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpec T H)
 
 instance rustOrder {U: Type} {O: avl_verification.Ord U} (OSpec: OrdSpec O): _root_.Ord U := ordOfOrdSpec O OSpec
@@ -20,9 +58,9 @@ instance rustLt' : LT T := rustLt Ospec
 
 @[pspec]
 theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop)
-  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o)
+  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ok o)
   (a: T) (t: Option (AVLNode T)):
-  ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ret ⟨ added, t_new ⟩
+  ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩
 --  ∧ AVLTree.set t'.2 = insert a (AVLTree.set t)
   ∧ (BST.ForallNode p t -> p a -> BST.ForallNode p t_new)
   := by match t with
@@ -68,8 +106,8 @@ lemma AVLTreeSet.insert_loop_spec_global
   (a: T) (t: Option (AVLNode T))
   :
   haveI : LT T := (rustLt Ospec)
-  BST.BST t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ret ⟨ added, t_new ⟩
-  ∧ BST.BST t_new := by 
+  BST.Invariant t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩
+  ∧ BST.Invariant t_new := by 
   intro Hbst
   letI instOrd : _root_.Ord T := (rustOrder Ospec)
   letI instLt : LT T := (rustLt Ospec)
@@ -78,9 +116,7 @@ lemma AVLTreeSet.insert_loop_spec_global
   | some (AVLNode.mk b left right) =>
     rw [AVLTreeSet.insert_loop]
     simp only []
-    have := Ospec.infallible; simp at this
-    -- TODO: unbundle `this`...
-    have : ∀ a b, ∃ o, H.cmp a b = .ret o := sorry
+    have : ∀ a b, ∃ o, H.cmp a b = .ok o := Ospec.infallible
     progress keep Hordering as ⟨ ordering ⟩
     cases ordering
     all_goals simp only []
@@ -104,34 +140,33 @@ lemma AVLTreeSet.insert_loop_spec_global
       simp; tauto
     }
     {
-      sorry
+      have ⟨ added₂, left₂, ⟨ H_result, H_bst ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a left (BST.left Hbst)
+      progress keep Htree with AVLTreeSet.insert_loop_spec_local as ⟨ added₁, left₁, Hnode ⟩
+      exact (fun x => x < b)
+      rewrite [Htree] at H_result; simp at H_result
+      refine' ⟨ added₁, ⟨ some (AVLNode.mk b left₁ right), _ ⟩ ⟩
+      simp only [true_and]
+      cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right
+      constructor
+      apply Hnode; exact H_forall_left
+      exact (gtOfRustOrder H b a Hordering)
+      exact H_forall_right
+      convert H_bst
+      exact H_result.2
+      exact H_bst_right
     }
 
 @[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) 
+  haveI : LT T := (rustLt Ospec)
+  BST.Invariant t.root -> (∃ t' added,t.insert _ H a = Result.ok (added, t')
   -- 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)
+  ∧ BST.Invariant 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)
+  rw [AVLTreeSet.insert]; intro Hbst
+  progress keep h as ⟨ t', Hset ⟩; 
+  simp; assumption
 
 end Implementation