feat: lift Rust "totality" to total orders

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

1 files changed, 30 insertions, 15 deletions

diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean
index 0bf9ffb..94fdd5f 100644
--- a/AvlVerification/Specifications.lean
+++ b/AvlVerification/Specifications.lean
@@ -9,6 +9,16 @@ def map {A B: Type} (x: Result A) (f: A -> B): Result B := match x with
 | .fail e => .fail e
 | .div => .div
 
+@[inline]
+def isRet {A: Type} : Result A -> Bool
+| .ret _ => true
+| .fail _ => false
+| .div => false
+
+@[inline]
+def get? {A: Type}: (r: Result A) -> isRet r -> A
+| .ret x, _ => x
+
 end Result
 
 end Primitives
@@ -27,11 +37,17 @@ namespace Specifications
 open Primitives
 open Result
 
-variable {T: Type}
+variable {T: Type} (H: avl_verification.Ord T)
+
+class OrdSpec where
+  cmp: T -> T -> Result Ordering := fun x y => (H.cmp x y).map (fun z => z.toLeanOrdering)
+  infallible: ∀ a b, ∃ (o: Ordering), cmp a b = .ret o
+
+@[simp]
+theorem OrdSpec.cmpEq {Spec: OrdSpec H}: ∀ x y, Spec.cmp x y = (H.cmp x y).map (fun z => z.toLeanOrdering) := sorry
 
-class OrdSpec (U: Type) where
-  cmp: U -> U -> Result Ordering
-  infallible: ∀ a b, ∃ o, cmp a b = .ret o
+@[simp]
+theorem OrdSpec.infallibleEq {Spec: OrdSpec H}: ∀ a b, ∃ (o: Ordering), Spec.cmp a b = .ret o <-> ∀ a b, ∃ (o: Ordering), (H.cmp a b).map (fun z => z.toLeanOrdering) = .ret o := sorry
 
 instance: Coe (avl_verification.Ordering) (_root_.Ordering) where
   coe a := a.toLeanOrdering
@@ -39,17 +55,16 @@ instance: Coe (avl_verification.Ordering) (_root_.Ordering) where
 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)
+  : OrdSpec H where
   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
+    intros a b; cases' (Hresult a b) with o Hcmp; refine' ⟨ o.toLeanOrdering, _ ⟩
+    simp [Result.map, Hcmp]
+
+def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpec H): Ord T where
+  compare x y := (spec.cmp x y).get? (by
+    cases' (spec.infallible x y) with o Hcmp
+    rewrite [isRet, Hcmp]
+    simp only
+  )
 
 end Specifications