summaryrefslogtreecommitdiff
path: root/AvlVerification/Specifications.lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--AvlVerification/Specifications.lean36
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