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, 22 insertions, 14 deletions

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