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


From 7064a237805d5cac48d2f5aa7e4691ea7695b8af Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Thu, 4 Apr 2024 17:30:22 +0200
Subject: feat: lift Rust "totality" to total orders

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
---
 AvlVerification/Specifications.lean | 45 ++++++++++++++++++++++++-------------
 1 file changed, 30 insertions(+), 15 deletions(-)

(limited to 'AvlVerification/Specifications.lean')

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


From 50be416e22a39eaf59f7edba81b919e1f114a0ae Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Thu, 4 Apr 2024 17:31:19 +0200
Subject: feat: close the BST proof modulo unbundling

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
---
 AvlVerification/Specifications.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'AvlVerification/Specifications.lean')

diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean
index 94fdd5f..247fd00 100644
--- a/AvlVerification/Specifications.lean
+++ b/AvlVerification/Specifications.lean
@@ -67,4 +67,14 @@ def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpec H): Ord T where
     simp only
   )
 
+theorem ltOfRustOrder {Spec: OrdSpec H}: 
+  haveI O := ordOfOrdSpec H Spec
+  haveI := @ltOfOrd _ O
+  ∀ a b, H.cmp a b = .ret .Less -> a < b := by
+  intros a b
+  intro Hcmp
+  change ((Spec.cmp a b).get? _ == .lt)
+  simp [Hcmp, map, avl_verification.Ordering.toLeanOrdering]
+  simp [get?]
+  rfl
 end Specifications
-- 
cgit v1.2.3


From 3577c7dc9d3013d401c45a7628b0ff4b6fd0ec67 Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Fri, 12 Apr 2024 19:11:16 +0200
Subject: feat: upgrade and close all proofs except Preorder on U32

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
---
 AvlVerification/Specifications.lean | 62 +++++++++++++++++++++++--------------
 1 file changed, 38 insertions(+), 24 deletions(-)

(limited to 'AvlVerification/Specifications.lean')

diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean
index 247fd00..958a3e7 100644
--- a/AvlVerification/Specifications.lean
+++ b/AvlVerification/Specifications.lean
@@ -5,19 +5,19 @@ 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)
+| .ok y => .ok (f y)
 | .fail e => .fail e
 | .div => .div
 
 @[inline]
-def isRet {A: Type} : Result A -> Bool
-| .ret _ => true
+def isok {A: Type} : Result A -> Bool
+| .ok _ => true
 | .fail _ => false
 | .div => false
 
 @[inline]
-def get? {A: Type}: (r: Result A) -> isRet r -> A
-| .ret x, _ => x
+def get? {A: Type}: (r: Result A) -> isok r -> A
+| .ok x, _ => x
 
 end Result
 
@@ -30,6 +30,11 @@ def Ordering.toLeanOrdering (o: avl_verification.Ordering): _root_.Ordering := m
 | .Equal => .eq
 | .Greater => .gt
 
+def Ordering.ofLeanOrdering (o: _root_.Ordering): avl_verification.Ordering := match o with
+| .lt => .Less
+| .eq => .Equal
+| .gt => .Greater
+
 end avl_verification
 
 namespace Specifications
@@ -39,42 +44,51 @@ open Result
 
 variable {T: Type} (H: avl_verification.Ord T)
 
+-- TODO: reason about raw bundling vs. refined bundling.
 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
-
-@[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
+  infallible: ∀ a b, ∃ (o: avl_verification.Ordering), H.cmp a b = .ok o
+  duality: ∀ a b, H.cmp a b = .ok .Greater -> H.cmp b a = .ok .Less
 
 instance: Coe (avl_verification.Ordering) (_root_.Ordering) where
   coe a := a.toLeanOrdering
 
-def ordSpecOfInfaillible
+def ordSpecOfTotalityAndDuality
   (H: avl_verification.Ord T)
-  (Hresult: ∀ a b, ∃ o, H.cmp a b = Primitives.Result.ret o)
+  (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 := by
-    intros a b; cases' (Hresult a b) with o Hcmp; refine' ⟨ o.toLeanOrdering, _ ⟩
-    simp [Result.map, Hcmp]
+  infallible := Hresult
+  duality := Hduality
 
 def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpec H): Ord T where
-  compare x y := (spec.cmp x y).get? (by
+  compare x y := (H.cmp x y).get? (by
     cases' (spec.infallible x y) with o Hcmp
-    rewrite [isRet, Hcmp]
+    rewrite [isok, Hcmp]
     simp only
   )
 
 theorem ltOfRustOrder {Spec: OrdSpec H}: 
   haveI O := ordOfOrdSpec H Spec
   haveI := @ltOfOrd _ O
-  ∀ a b, H.cmp a b = .ret .Less -> a < b := by
+  ∀ a b, H.cmp a b = .ok .Less -> a < b := by
   intros a b
   intro Hcmp
-  change ((Spec.cmp a b).get? _ == .lt)
-  simp [Hcmp, map, avl_verification.Ordering.toLeanOrdering]
-  simp [get?]
+  rw [LT.lt]
+  simp [ltOfOrd]
+  rw [compare]
+  simp [ordOfOrdSpec]
+  -- https://proofassistants.stackexchange.com/questions/1062/what-does-the-motive-is-not-type-correct-error-mean-in-lean
+  simp_rw [Hcmp, get?, avl_verification.Ordering.toLeanOrdering]
   rfl
+
+theorem gtOfRustOrder {Spec: OrdSpec H}: 
+  haveI O := ordOfOrdSpec H Spec
+  haveI := @ltOfOrd _ O
+  ∀ a b, H.cmp a b = .ok .Greater -> b < a := by
+  intros a b
+  intro Hcmp
+  apply ltOfRustOrder
+  exact (Spec.duality _ _ Hcmp)
+
+
 end Specifications
-- 
cgit v1.2.3