feat: add functional correctness of elements contained in the resulting tree

We revamp the typeclass mechanisms and we add an equality hypothesis
now.

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

1 files changed, 58 insertions, 57 deletions

diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean
index baf3441..16e740f 100644
--- a/AvlVerification/Insert.lean
+++ b/AvlVerification/Insert.lean
@@ -6,55 +6,49 @@ namespace Implementation
 
 open Primitives
 open avl_verification
-open Tree (AVLTree)
-open Specifications (OrdSpec ordSpecOfTotalityAndDuality ordOfOrdSpec ltOfRustOrder gtOfRustOrder)
+open Tree (AVLTree AVLTree.set)
+open Specifications (OrdSpecDualityEq 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)
+-- 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)
 
-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
--- Why the TC fails if I don't specify the previous instance explicitly?
-instance rustLt {U: Type} {O: avl_verification.Ord U} (OSpec: OrdSpec O): LT U := @ltOfOrd _ (ordOfOrdSpec O OSpec)
-
-instance rustLt' : LT T := rustLt Ospec
+variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpecDualityEq T H)
 
 @[pspec]
 theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop)
@@ -105,14 +99,11 @@ theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop)
 lemma AVLTreeSet.insert_loop_spec_global
   (a: T) (t: Option (AVLNode T))
   :
-  haveI : LT T := (rustLt Ospec)
   BST.Invariant t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩
-  ∧ BST.Invariant t_new := by 
+  ∧ BST.Invariant t_new ∧ AVLTree.set t_new = {a} ∪ AVLTree.set t := by 
   intro Hbst
-  letI instOrd : _root_.Ord T := (rustOrder Ospec)
-  letI instLt : LT T := (rustLt Ospec)
   match t with
-  | none => simp [AVLTreeSet.insert_loop]
+  | none => simp [AVLTreeSet.insert_loop, AVLTree.set, setOf]
   | some (AVLNode.mk b left right) =>
     rw [AVLTreeSet.insert_loop]
     simp only []
@@ -121,12 +112,13 @@ lemma AVLTreeSet.insert_loop_spec_global
     cases ordering
     all_goals simp only []
     {
-      have ⟨ added₂, right₂, ⟨ H_result, H_bst ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a right (BST.right Hbst)
+      have ⟨ added₂, right₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a right (BST.right Hbst)
       progress keep Htree with AVLTreeSet.insert_loop_spec_local as ⟨ added₁, right₁, Hnode ⟩
       exact (fun x => b < x)
       rewrite [Htree] at H_result; simp at H_result
       refine' ⟨ added₁, ⟨ some (AVLNode.mk b left right₁), _ ⟩ ⟩
       simp only [true_and]
+      split_conjs
       cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right
       constructor
       exact H_forall_left
@@ -135,17 +127,23 @@ lemma AVLTreeSet.insert_loop_spec_global
       exact H_bst_left
       convert H_bst
       exact H_result.2
+      simp [AVLTree.set_some]
+      rewrite [H_result.2, H_set]
+      simp
     }
     {
-      simp; tauto
+      simp; split_conjs
+      . tauto
+      . simp [Ospec.equality _ _ Hordering]
     }
     {
-      have ⟨ added₂, left₂, ⟨ H_result, H_bst ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a left (BST.left Hbst)
+      have ⟨ added₂, left₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := 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]
+      split_conjs
       cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right
       constructor
       apply Hnode; exact H_forall_left
@@ -154,15 +152,18 @@ lemma AVLTreeSet.insert_loop_spec_global
       convert H_bst
       exact H_result.2
       exact H_bst_right
+      simp [AVLTree.set_some]
+      rewrite [H_result.2, H_set]
+      simp [Set.singleton_union, Set.insert_comm, Set.insert_union]
     }
 
 @[pspec]
 def AVLTreeSet.insert_spec 
   (a: T) (t: AVLTreeSet T):
-  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.
-  ∧ BST.Invariant t'.root)
+  ∧ BST.Invariant t'.root
+  ∧ AVLTree.set t'.root = {a} ∪ AVLTree.set t.root)
   := by
   rw [AVLTreeSet.insert]; intro Hbst
   progress keep h as ⟨ t', Hset ⟩;