summaryrefslogtreecommitdiff
path: root/AvlVerification/Specifications.lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--AvlVerification/Specifications.lean55
1 files changed, 55 insertions, 0 deletions
diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean
new file mode 100644
index 0000000..0bf9ffb
--- /dev/null
+++ b/AvlVerification/Specifications.lean
@@ -0,0 +1,55 @@
+import «AvlVerification»
+
+namespace Primitives
+
+namespace Result
+
+def map {A B: Type} (x: Result A) (f: A -> B): Result B := match x with
+| .ret y => .ret (f y)
+| .fail e => .fail e
+| .div => .div
+
+end Result
+
+end Primitives
+
+namespace avl_verification
+
+def Ordering.toLeanOrdering (o: avl_verification.Ordering): _root_.Ordering := match o with
+| .Less => .lt
+| .Equal => .eq
+| .Greater => .gt
+
+end avl_verification
+
+namespace Specifications
+
+open Primitives
+open Result
+
+variable {T: Type}
+
+class OrdSpec (U: Type) where
+ cmp: U -> U -> Result Ordering
+ infallible: ∀ a b, ∃ o, cmp a b = .ret o
+
+instance: Coe (avl_verification.Ordering) (_root_.Ordering) where
+ coe a := a.toLeanOrdering
+
+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)
+ 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
+
+end Specifications