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>

6 files changed, 95 insertions, 86 deletions

diff --git a/AvlVerification.lean b/AvlVerification.lean
index b90680c..f9e6830 100644
--- a/AvlVerification.lean
+++ b/AvlVerification.lean
@@ -32,16 +32,8 @@ structure AVLTreeSet (T : Type) where
 def AVLTreeSet.new (T : Type) (OrdInst : Ord T) : Result (AVLTreeSet T) :=
   Result.ok { root := none }
 
-/- [avl_verification::{avl_verification::AVLTreeSet<T>}::find]:
-   Source: 'src/main.rs', lines 30:4-30:39 -/
-def AVLTreeSet.find
-  (T : Type) (OrdInst : Ord T) (self : AVLTreeSet T) (value : T) :
-  Result Bool
-  :=
-  sorry
-
 /- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]: loop 0:
-   Source: 'src/main.rs', lines 63:4-81:5 -/
+   Source: 'src/main.rs', lines 43:4-61:5 -/
 divergent def AVLTreeSet.insert_loop
   (T : Type) (OrdInst : Ord T) (value : T) (current_tree : Option (AVLNode T))
   :
@@ -69,17 +61,17 @@ divergent def AVLTreeSet.insert_loop
       Result.ok (b, some (AVLNode.mk t current_tree3 current_tree2))
 
 /- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]:
-   Source: 'src/main.rs', lines 63:4-63:46 -/
+   Source: 'src/main.rs', lines 43:4-43:46 -/
 def AVLTreeSet.insert
   (T : Type) (OrdInst : Ord T) (self : AVLTreeSet T) (value : T) :
   Result (Bool × (AVLTreeSet T))
   :=
   do
-  let (b, as) ← AVLTreeSet.insert_loop T OrdInst value self.root
-  Result.ok (b, { root := as })
+  let (b, u) ← AVLTreeSet.insert_loop T OrdInst value self.root
+  Result.ok (b, { root := u })
 
 /- [avl_verification::{(avl_verification::Ord for u32)#1}::cmp]:
-   Source: 'src/main.rs', lines 85:4-85:43 -/
+   Source: 'src/main.rs', lines 65:4-65:43 -/
 def OrdU32.cmp (self : U32) (other : U32) : Result Ordering :=
   if self < other
   then Result.ok Ordering.Less
@@ -89,7 +81,7 @@ def OrdU32.cmp (self : U32) (other : U32) : Result Ordering :=
     else Result.ok Ordering.Greater
 
 /- Trait implementation: [avl_verification::{(avl_verification::Ord for u32)#1}]
-   Source: 'src/main.rs', lines 84:0-84:16 -/
+   Source: 'src/main.rs', lines 64:0-64:16 -/
 def OrdU32 : Ord U32 := {
   cmp := OrdU32.cmp
 }
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 ⟩; 
diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean
index 958a3e7..0694df3 100644
--- a/AvlVerification/Specifications.lean
+++ b/AvlVerification/Specifications.lean
@@ -42,32 +42,40 @@ namespace Specifications
 open Primitives
 open Result
 
-variable {T: Type} (H: avl_verification.Ord T)
+variable {T: Type} (H: outParam (avl_verification.Ord T))
 
 -- TODO: reason about raw bundling vs. refined bundling.
-class OrdSpec where
+-- raw bundling: hypothesis with Rust extracted objects.
+-- refined bundling: lifted hypothesis with Lean native objects.
+class OrdSpecInfaillible where
   infallible: ∀ a b, ∃ (o: avl_verification.Ordering), H.cmp a b = .ok o
+
+class OrdSpecDuality extends OrdSpecInfaillible H where
   duality: ∀ a b, H.cmp a b = .ok .Greater -> H.cmp b a = .ok .Less
 
+-- TODO: OrdSpecEq := OrdSpecRel (R := Eq).
+class OrdSpecEq extends OrdSpecInfaillible H where
+  equality: ∀ a b, H.cmp a b = .ok .Equal -> a = b
+
+class OrdSpecRel (R: outParam (T -> T -> Prop)) extends OrdSpecInfaillible H where
+  equivalence: ∀ a b, H.cmp a b = .ok .Equal -> R a b
+
+class OrdSpecDualityEq extends OrdSpecDuality H, OrdSpecEq H
+
 instance: Coe (avl_verification.Ordering) (_root_.Ordering) where
   coe a := a.toLeanOrdering
 
-def ordSpecOfTotalityAndDuality
-  (H: avl_verification.Ord T)
-  (Hresult: ∀ a b, ∃ o, H.cmp a b = Primitives.Result.ok o)
-  (Hduality: ∀ a b, H.cmp a b = .ok .Greater -> H.cmp b a = .ok .Less)
-  : OrdSpec H where
-  infallible := Hresult
-  duality := Hduality
-
-def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpec H): Ord T where
+def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpecInfaillible H): Ord T where
   compare x y := (H.cmp x y).get? (by
     cases' (spec.infallible x y) with o Hcmp
     rewrite [isok, Hcmp]
     simp only
   )
 
-theorem ltOfRustOrder {Spec: OrdSpec H}: 
+instance [spec: OrdSpecInfaillible H]: Ord T := ordOfOrdSpec H spec
+instance [OrdSpecInfaillible H]: LT T := ltOfOrd
+
+theorem ltOfRustOrder {Spec: OrdSpecInfaillible H}: 
   haveI O := ordOfOrdSpec H Spec
   haveI := @ltOfOrd _ O
   ∀ a b, H.cmp a b = .ok .Less -> a < b := by
@@ -81,8 +89,8 @@ theorem ltOfRustOrder {Spec: OrdSpec H}:
   simp_rw [Hcmp, get?, avl_verification.Ordering.toLeanOrdering]
   rfl
 
-theorem gtOfRustOrder {Spec: OrdSpec H}: 
-  haveI O := ordOfOrdSpec H Spec
+theorem gtOfRustOrder {Spec: OrdSpecDuality H}: 
+  haveI O := ordOfOrdSpec H Spec.toOrdSpecInfaillible
   haveI := @ltOfOrd _ O
   ∀ a b, H.cmp a b = .ok .Greater -> b < a := by
   intros a b
diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean
index fdd4b78..8a043a1 100644
--- a/AvlVerification/Tree.lean
+++ b/AvlVerification/Tree.lean
@@ -75,4 +75,7 @@ def AVLTree.mem_some {x: T} {left right: AVLTree T}: AVLTree.mem (some (AVLNode.
 
 def AVLTree.set (t: AVLTree T): Set T := _root_.setOf (AVLTree.mem t)
 
+@[simp]
+def AVLTree.set_some {x: T} {left right: AVLTree T}: AVLTree.set (some (AVLNode.mk x left right)) = {x} ∪ AVLTree.set left ∪ AVLTree.set right := sorry
+
 end Tree
diff --git a/lake-manifest.json b/lake-manifest.json
index 3e20e73..3c33932 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -67,7 +67,7 @@
   {"url": "https://github.com/AeneasVerif/aeneas",
    "type": "git",
    "subDir": "backends/lean",
-   "rev": "03a175b423c9ccff2160300c4d349978f9b1aeb9",
+   "rev": "23da71768c03d955c916635bfc5c9d5806a80187",
    "name": "base",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/notes.md b/notes.md
index 53b3256..942e1ca 100644
--- a/notes.md
+++ b/notes.md
@@ -123,3 +123,8 @@ Source: 'src/main.rs', lines 132:4-158:5
 [Error] There should be no bottoms in the value
 Source: 'src/main.rs', lines 175:52-181:9
 ```
+
+## Réunion
+
+- Prédicat avec `setOf`: OK.
+- `ForallNode` négatif pour exclure l'appartenance d'un élément à l'arbre