refactor: generalize the theory and perform some lifts

Move forward the "HSpec" idea, move around files, construct the hierarchy of trees, etc.

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

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