From 5e35e3875884ca4be63f253d9e8d7f2fc71b3527 Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Thu, 28 Mar 2024 17:59:35 +0100
Subject: 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>
---
 AvlVerification/Specifications.lean | 55 +++++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100644 AvlVerification/Specifications.lean

(limited to 'AvlVerification/Specifications.lean')

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
-- 
cgit v1.2.3

