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/BinarySearchTree.lean | 37 +++++++++++++++
 AvlVerification/Insert.lean           | 87 +++++++++++++++++++++++++++++++++++
 AvlVerification/Specifications.lean   | 55 ++++++++++++++++++++++
 AvlVerification/Tree.lean             | 81 ++++++++++++++++++++++++++++++++
 4 files changed, 260 insertions(+)
 create mode 100644 AvlVerification/BinarySearchTree.lean
 create mode 100644 AvlVerification/Insert.lean
 create mode 100644 AvlVerification/Specifications.lean
 create mode 100644 AvlVerification/Tree.lean

(limited to 'AvlVerification')

diff --git a/AvlVerification/BinarySearchTree.lean b/AvlVerification/BinarySearchTree.lean
new file mode 100644
index 0000000..130fd73
--- /dev/null
+++ b/AvlVerification/BinarySearchTree.lean
@@ -0,0 +1,37 @@
+import AvlVerification.Tree
+
+namespace BST
+
+open Primitives (Result)
+open avl_verification (AVLNode Ordering)
+open Tree (AVLTree AVLNode.left AVLNode.right AVLNode.val)
+
+inductive ForallNode (p: T -> Prop): AVLTree T -> Prop
+| none : ForallNode p none
+| some (a: T) (left: AVLTree T) (right: AVLTree T) : ForallNode p left -> p a -> ForallNode p right -> ForallNode p (some (AVLNode.mk a left right))
+
+-- This is the binary search invariant.
+inductive BST [LT T]: AVLTree T -> Prop
+| none : BST none
+| some (a: T) (left: AVLTree T) (right: AVLTree T) : 
+  ForallNode (fun v => v < a) left -> ForallNode (fun v => a < v) right
+  -> BST left -> BST right -> BST (some (AVLNode.mk a left right))
+
+@[simp]
+theorem singleton_bst [LT T] {a: T}: BST (some (AVLNode.mk a none none)) := by
+  apply BST.some
+  all_goals simp [ForallNode.none, BST.none] 
+
+theorem left [LT T] {t: AVLTree T}: BST t -> BST t.left := by
+  intro H
+  induction H with 
+  | none => exact BST.none
+  | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.left]; assumption
+
+theorem right [LT T] {t: AVLTree T}: BST t -> BST t.right := by
+  intro H
+  induction H with 
+  | none => exact BST.none
+  | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.right]; assumption
+
+end BST
diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean
new file mode 100644
index 0000000..870e9c2
--- /dev/null
+++ b/AvlVerification/Insert.lean
@@ -0,0 +1,87 @@
+import AvlVerification.Tree
+import AvlVerification.BinarySearchTree
+import AvlVerification.Specifications
+
+namespace Implementation
+
+open Primitives
+open avl_verification
+open Tree (AVLTree)
+
+variable {T: Type}
+
+@[pspec]
+theorem AVLTreeSet.insert_loop_spec {H: avl_verification.Ord T} 
+  (a: T) (t: Option (AVLNode T))
+  [LT T]
+  (Hbs_search: BST.BST t)
+  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o):
+  ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ret ⟨ added, t_new ⟩
+--  ∧ AVLTree.set t'.2 = insert a (AVLTree.set t)
+  ∧ BST.BST t_new
+  := by match t with
+  | none =>
+    simp [AVLTreeSet.insert_loop, AVLTree.set, setOf, BST.BST]
+  | some (AVLNode.mk b left right) =>
+    rw [AVLTreeSet.insert_loop]
+    simp only []
+    progress keep Hordering as ⟨ ordering ⟩
+    cases ordering
+    all_goals simp only []
+    have Hbs_search_right: BST.BST right := BST.right Hbs_search
+    have Hbs_search_left: BST.BST left := BST.left Hbs_search
+    {
+      progress keep Htree as ⟨ added₁, right₁, Hbst ⟩
+      refine' ⟨ added₁, ⟨ some (AVLNode.mk b left right₁), _ ⟩ ⟩
+      simp only [true_and]
+      refine' (BST.BST.some b left right₁ _ _ Hbs_search_left Hbst)
+      cases' Hbs_search; assumption
+      induction right with
+      | none =>
+        simp [AVLTreeSet.insert_loop] at Htree
+        rw [← Htree.2]
+        refine' (BST.ForallNode.some _ _ _ BST.ForallNode.none _ BST.ForallNode.none)
+        sorry
+      | some node =>
+        -- clef: ∀ x ∈ node.right, b < x
+        -- de plus: b < a
+        -- or, right₁ = insert a node.right moralement
+        -- donc, il suffit de prouver que: ∀ x ∈ insert a node.right, b < x <-> b < a /\ ∀ x ∈ node.right, b < x
+        sorry
+    }
+    {
+      simp [Hbs_search]
+    }
+    {
+      -- Symmetric case of left.
+      sorry
+    }
+
+@[pspec]
+def AVLTreeSet.insert_spec 
+  {H: avl_verification.Ord T} 
+  -- TODO: this can be generalized into `H.cmp` must be an equivalence relation.
+  -- and insert works no longer on Sets but on set quotiented by this equivalence relation.
+  (Hcmp_eq: ∀ a b, H.cmp a b = Result.ret Ordering.Equal -> a = b)
+  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o)
+  (Hbs_search: @BSTree.searchInvariant _ H t)
+  (a: T) (t: AVLTreeSet T):
+  ∃ t', t.insert _ H a = Result.ret t' 
+  -- set of values *POST* insertion is {a} \cup set of values of the *PRE* tree.
+  ∧ AVLTree.setOf t'.2.root = insert a (AVLTree.setOf t.root) 
+  -- it's still a binary search tree.
+  ∧ @BSTree.searchInvariant _ H t'.2.root
+  -- TODO(reinforcement): (t'.1 is false <=> a \in AVLTree.setOf t.root)
+  := by
+  rw [AVLTreeSet.insert]
+  progress keep h as ⟨ t', Hset ⟩; simp
+  rw [Hset]
+  sorry
+
+
+-- insert is infaillible, right?
+-- instance [LT T] (o: avl_verification.Ord T): Insert T (AVLTreeSet T) where
+--   insert x tree := (AVLTreeSet.insert T o tree x).map (fun (added, tree) => tree)
+
+end Implementation
+
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
diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean
new file mode 100644
index 0000000..3316e9e
--- /dev/null
+++ b/AvlVerification/Tree.lean
@@ -0,0 +1,81 @@
+import «AvlVerification»
+
+namespace Tree
+
+variable {T: Type}
+
+open avl_verification
+
+-- Otherwise, Lean cannot prove termination by itself.
+@[reducible]
+def AVLTree (U: Type) := Option (AVLNode U)
+def AVLTree.nil: AVLTree T := none
+
+def AVLTree.val (t: AVLTree T): Option T := match t with
+| none => none
+| some (AVLNode.mk x _ _) => some x
+
+def AVLTree.left (t: AVLTree T): AVLTree T := match t with
+| none => none
+| some (AVLNode.mk _ left _) => left
+
+def AVLTree.right (t: AVLTree T): AVLTree T := match t with
+| none => none
+| some (AVLNode.mk _ _ right) => right
+
+def AVLNode.left (t: AVLNode T): AVLTree T := match t with
+| AVLNode.mk _ left _ => left
+
+def AVLNode.right (t: AVLNode T): AVLTree T := match t with
+| AVLNode.mk _ _ right => right
+
+def AVLNode.val (t: AVLNode T): T := match t with
+| AVLNode.mk x _ _ => x
+
+mutual
+def AVLTree.height_node (tree: AVLNode T): Nat := match tree with
+| AVLNode.mk y left right => 1 + AVLTree.height left + AVLTree.height right
+
+def AVLTree.height (tree: AVLTree T): Nat := match tree with 
+| none => 0
+| some n => 1 + AVLTree.height_node n
+end
+
+def AVLTreeSet.nil: AVLTreeSet T := { root := AVLTree.nil }
+
+-- Automatic synthesization of this seems possible at the Lean level?
+instance: Inhabited (AVLTree T) where
+  default := AVLTree.nil
+
+instance: Inhabited (AVLTreeSet T) where
+  default := AVLTreeSet.nil
+
+instance: Coe (Option (AVLNode T)) (AVLTree T) where
+  coe x := x
+
+-- TODO: ideally, it would be nice if we could generalize
+-- this to any `BinaryTree` typeclass.
+
+def AVLTree.mem (tree: AVLTree T) (x: T) :=
+  match tree with
+  | none => False
+  | some (AVLNode.mk y left right) => x = y ∨ AVLTree.mem left x ∨ AVLTree.mem right x
+
+@[simp]
+def AVLTree.mem_none: AVLTree.mem none = ({}: Set T) := rfl
+
+@[simp]
+def AVLTree.mem_some {x: T} {left right: AVLTree T}: AVLTree.mem (some (AVLNode.mk x left right)) = (({x}: Set T) ∪ AVLTree.mem left ∪ AVLTree.mem right) := by
+  ext y
+  rw [AVLTree.mem]
+  simp [Set.insert_union]
+  simp [Set.insert_def, Set.setOf_set, Set.mem_def, Set.union_def]
+
+-- TODO(reinforcement): ∪ is actually disjoint if we prove this is a binary search tree.
+
+def AVLTree.set (t: AVLTree T): Set T := _root_.setOf (AVLTree.mem t)
+
+def AVLTree.setOf_left_incl (t: AVLTree T): t.left.set ⊂ t.set := sorry
+def AVLTree.setOf_right_incl (t: AVLTree T): t.right.set ⊂ t.set := sorry
+
+end Tree
-- 
cgit v1.2.3


From 9da83df6319b806d584da9ae5c6da260fcae56a8 Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Thu, 4 Apr 2024 17:29:44 +0200
Subject: refactor: define some projectors for ForallNode

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

(limited to 'AvlVerification')

diff --git a/AvlVerification/BinarySearchTree.lean b/AvlVerification/BinarySearchTree.lean
index 130fd73..954f21f 100644
--- a/AvlVerification/BinarySearchTree.lean
+++ b/AvlVerification/BinarySearchTree.lean
@@ -10,6 +10,12 @@ inductive ForallNode (p: T -> Prop): AVLTree T -> Prop
 | none : ForallNode p none
 | some (a: T) (left: AVLTree T) (right: AVLTree T) : ForallNode p left -> p a -> ForallNode p right -> ForallNode p (some (AVLNode.mk a left right))
 
+theorem ForallNode.left {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.left := sorry
+
+theorem ForallNode.right {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.right := sorry
+
+theorem ForallNode.label {a: T} {p: T -> Prop} {left right: AVLTree T}: ForallNode p (AVLNode.mk a left right) -> p a := sorry
+
 -- This is the binary search invariant.
 inductive BST [LT T]: AVLTree T -> Prop
 | none : BST none
-- 
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')

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 22a499f5d4d231bef3193405983f9ade6da116db Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Thu, 4 Apr 2024 17:30:46 +0200
Subject: feat: close key theorem for any result on binary search trees

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
---
 AvlVerification/Insert.lean | 51 +++++++++++++++++++++++----------------------
 1 file changed, 26 insertions(+), 25 deletions(-)

(limited to 'AvlVerification')

diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean
index 870e9c2..92691b2 100644
--- a/AvlVerification/Insert.lean
+++ b/AvlVerification/Insert.lean
@@ -11,49 +11,50 @@ open Tree (AVLTree)
 variable {T: Type}
 
 @[pspec]
-theorem AVLTreeSet.insert_loop_spec {H: avl_verification.Ord T} 
-  (a: T) (t: Option (AVLNode T))
-  [LT T]
-  (Hbs_search: BST.BST t)
-  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o):
+theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop)
+  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o)
+  (a: T) (t: Option (AVLNode T)):
   ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ret ⟨ added, t_new ⟩
 --  ∧ AVLTree.set t'.2 = insert a (AVLTree.set t)
-  ∧ BST.BST t_new
+  ∧ (BST.ForallNode p t -> p a -> BST.ForallNode p t_new)
   := by match t with
   | none =>
-    simp [AVLTreeSet.insert_loop, AVLTree.set, setOf, BST.BST]
+    simp [AVLTreeSet.insert_loop, AVLTree.set, setOf]
+    intros _ Hpa
+    constructor; all_goals try simp [BST.ForallNode.none]
+    exact Hpa
   | some (AVLNode.mk b left right) =>
     rw [AVLTreeSet.insert_loop]
     simp only []
     progress keep Hordering as ⟨ ordering ⟩
     cases ordering
     all_goals simp only []
-    have Hbs_search_right: BST.BST right := BST.right Hbs_search
-    have Hbs_search_left: BST.BST left := BST.left Hbs_search
     {
-      progress keep Htree as ⟨ added₁, right₁, Hbst ⟩
+      progress keep Htree as ⟨ added₁, right₁, Hnode ⟩
       refine' ⟨ added₁, ⟨ some (AVLNode.mk b left right₁), _ ⟩ ⟩
       simp only [true_and]
-      refine' (BST.BST.some b left right₁ _ _ Hbs_search_left Hbst)
-      cases' Hbs_search; assumption
-      induction right with
-      | none =>
-        simp [AVLTreeSet.insert_loop] at Htree
-        rw [← Htree.2]
-        refine' (BST.ForallNode.some _ _ _ BST.ForallNode.none _ BST.ForallNode.none)
-        sorry
-      | some node =>
-        -- clef: ∀ x ∈ node.right, b < x
-        -- de plus: b < a
-        -- or, right₁ = insert a node.right moralement
-        -- donc, il suffit de prouver que: ∀ x ∈ insert a node.right, b < x <-> b < a /\ ∀ x ∈ node.right, b < x
-        sorry
+      intros Hptree Hpa
+      constructor
+      exact Hptree.left
+      exact Hptree.label
+      exact Hnode Hptree.right Hpa
     }
     {
-      simp [Hbs_search]
+      simp; tauto
     }
     {
+      -- TODO: investigate wlog.
       -- Symmetric case of left.
+      progress keep Htree as ⟨ added₁, left₁, Hnode ⟩
+      refine' ⟨ added₁, ⟨ some (AVLNode.mk b left₁ right), _ ⟩ ⟩
+      simp only [true_and]
+      intros Hptree Hpa
+      constructor
+      exact Hnode Hptree.left Hpa
+      exact Hptree.label
+      exact Hptree.right
+    }
+
       sorry
     }
 
-- 
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/Insert.lean         | 51 ++++++++++++++++++++++++++++++++++++-
 AvlVerification/Specifications.lean | 10 ++++++++
 2 files changed, 60 insertions(+), 1 deletion(-)

(limited to 'AvlVerification')

diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean
index 92691b2..3c2b8b3 100644
--- a/AvlVerification/Insert.lean
+++ b/AvlVerification/Insert.lean
@@ -7,8 +7,16 @@ namespace Implementation
 open Primitives
 open avl_verification
 open Tree (AVLTree)
+open Specifications (OrdSpec ordSpecOfInfaillible ordOfOrdSpec ltOfRustOrder)
 
-variable {T: Type}
+-- TODO: OSpec should be proven.
+variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpec T H)
+
+instance rustOrder {U: Type} {O: avl_verification.Ord U} (OSpec: OrdSpec O): _root_.Ord U := ordOfOrdSpec O OSpec
+-- Why the TC fails if I don't specify the previous instance explicitly?
+instance rustLt {U: Type} {O: avl_verification.Ord U} (OSpec: OrdSpec O): LT U := @ltOfOrd _ (ordOfOrdSpec O OSpec)
+
+instance rustLt' : LT T := rustLt Ospec
 
 @[pspec]
 theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop)
@@ -55,6 +63,47 @@ theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop)
       exact Hptree.right
     }
 
+@[pspec]
+lemma AVLTreeSet.insert_loop_spec_global
+  (a: T) (t: Option (AVLNode T))
+  :
+  haveI : LT T := (rustLt Ospec)
+  BST.BST t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ret ⟨ added, t_new ⟩
+  ∧ BST.BST t_new := by 
+  intro Hbst
+  letI instOrd : _root_.Ord T := (rustOrder Ospec)
+  letI instLt : LT T := (rustLt Ospec)
+  match t with
+  | none => simp [AVLTreeSet.insert_loop]
+  | some (AVLNode.mk b left right) =>
+    rw [AVLTreeSet.insert_loop]
+    simp only []
+    have := Ospec.infallible; simp at this
+    -- TODO: unbundle `this`...
+    have : ∀ a b, ∃ o, H.cmp a b = .ret o := sorry
+    progress keep Hordering as ⟨ ordering ⟩
+    cases ordering
+    all_goals simp only []
+    {
+      have ⟨ added₂, right₂, ⟨ H_result, H_bst ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a right (BST.right Hbst)
+      progress keep Htree with AVLTreeSet.insert_loop_spec_local as ⟨ added₁, right₁, Hnode ⟩
+      exact (fun x => b < x)
+      rewrite [Htree] at H_result; simp at H_result
+      refine' ⟨ added₁, ⟨ some (AVLNode.mk b left right₁), _ ⟩ ⟩
+      simp only [true_and]
+      cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right
+      constructor
+      exact H_forall_left
+      apply Hnode; exact H_forall_right
+      exact (ltOfRustOrder H b a Hordering)
+      exact H_bst_left
+      convert H_bst
+      exact H_result.2
+    }
+    {
+      simp; tauto
+    }
+    {
       sorry
     }
 
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/BinarySearchTree.lean | 41 +++++++++------
 AvlVerification/Insert.lean           | 95 ++++++++++++++++++++++++-----------
 AvlVerification/Specifications.lean   | 62 ++++++++++++++---------
 AvlVerification/Tree.lean             |  3 --
 4 files changed, 129 insertions(+), 72 deletions(-)

(limited to 'AvlVerification')

diff --git a/AvlVerification/BinarySearchTree.lean b/AvlVerification/BinarySearchTree.lean
index 954f21f..2b17d52 100644
--- a/AvlVerification/BinarySearchTree.lean
+++ b/AvlVerification/BinarySearchTree.lean
@@ -10,34 +10,45 @@ inductive ForallNode (p: T -> Prop): AVLTree T -> Prop
 | none : ForallNode p none
 | some (a: T) (left: AVLTree T) (right: AVLTree T) : ForallNode p left -> p a -> ForallNode p right -> ForallNode p (some (AVLNode.mk a left right))
 
-theorem ForallNode.left {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.left := sorry
-
-theorem ForallNode.right {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.right := sorry
-
-theorem ForallNode.label {a: T} {p: T -> Prop} {left right: AVLTree T}: ForallNode p (AVLNode.mk a left right) -> p a := sorry
+theorem ForallNode.left {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.left := by
+  intro Hpt
+  cases Hpt with 
+  | none => simp [AVLTree.left, ForallNode.none]
+  | some a left right f_pleft f_pa f_pright => simp [AVLTree.left, f_pleft]
+
+theorem ForallNode.right {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.right := by
+  intro Hpt
+  cases Hpt with 
+  | none => simp [AVLTree.right, ForallNode.none]
+  | some a left right f_pleft f_pa f_pright => simp [AVLTree.right, f_pright]
+
+theorem ForallNode.label {a: T} {p: T -> Prop} {left right: AVLTree T}: ForallNode p (AVLNode.mk a left right) -> p a := by
+  intro Hpt
+  cases Hpt with 
+  | some a left right f_pleft f_pa f_pright => exact f_pa
 
 -- This is the binary search invariant.
-inductive BST [LT T]: AVLTree T -> Prop
-| none : BST none
+inductive Invariant [LT T]: AVLTree T -> Prop
+| none : Invariant none
 | some (a: T) (left: AVLTree T) (right: AVLTree T) : 
   ForallNode (fun v => v < a) left -> ForallNode (fun v => a < v) right
-  -> BST left -> BST right -> BST (some (AVLNode.mk a left right))
+  -> Invariant left -> Invariant right -> Invariant (some (AVLNode.mk a left right))
 
 @[simp]
-theorem singleton_bst [LT T] {a: T}: BST (some (AVLNode.mk a none none)) := by
-  apply BST.some
-  all_goals simp [ForallNode.none, BST.none] 
+theorem singleton_bst [LT T] {a: T}: Invariant (some (AVLNode.mk a none none)) := by
+  apply Invariant.some
+  all_goals simp [ForallNode.none, Invariant.none] 
 
-theorem left [LT T] {t: AVLTree T}: BST t -> BST t.left := by
+theorem left [LT T] {t: AVLTree T}: Invariant t -> Invariant t.left := by
   intro H
   induction H with 
-  | none => exact BST.none
+  | none => exact Invariant.none
   | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.left]; assumption
 
-theorem right [LT T] {t: AVLTree T}: BST t -> BST t.right := by
+theorem right [LT T] {t: AVLTree T}: Invariant t -> Invariant t.right := by
   intro H
   induction H with 
-  | none => exact BST.none
+  | none => exact Invariant.none
   | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.right]; assumption
 
 end BST
diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean
index 3c2b8b3..baf3441 100644
--- a/AvlVerification/Insert.lean
+++ b/AvlVerification/Insert.lean
@@ -7,9 +7,47 @@ namespace Implementation
 open Primitives
 open avl_verification
 open Tree (AVLTree)
-open Specifications (OrdSpec ordSpecOfInfaillible ordOfOrdSpec ltOfRustOrder)
+open Specifications (OrdSpec ordSpecOfTotalityAndDuality ordOfOrdSpec ltOfRustOrder gtOfRustOrder)
+
+example: OrdSpec OrdU32 := ordSpecOfTotalityAndDuality _ 
+  (by 
+  -- Totality
+  intro a b
+  unfold Ord.cmp
+  unfold OrdU32
+  unfold OrdU32.cmp
+  if hlt : a < b then 
+    use .Less
+    simp [hlt]
+  else
+    if heq: a = b
+    then
+    use .Equal
+    simp [hlt]
+    rw [heq]
+    -- TODO: simp [hlt, heq] breaks everything???
+    else
+      use .Greater
+      simp [hlt, heq]
+  ) (by 
+  -- Duality
+  intro a b Hgt
+  if hlt : b < a then
+    unfold Ord.cmp
+    unfold OrdU32
+    unfold OrdU32.cmp
+    simp [hlt]
+  else
+    unfold Ord.cmp at Hgt
+    unfold OrdU32 at Hgt
+    unfold OrdU32.cmp at Hgt
+    have hnlt : ¬ (a < b) := sorry
+    have hneq : ¬ (a = b) := sorry
+    exfalso
+    apply hlt
+    -- I need a Preorder on U32 now.
+    sorry)
 
--- TODO: OSpec should be proven.
 variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpec T H)
 
 instance rustOrder {U: Type} {O: avl_verification.Ord U} (OSpec: OrdSpec O): _root_.Ord U := ordOfOrdSpec O OSpec
@@ -20,9 +58,9 @@ instance rustLt' : LT T := rustLt Ospec
 
 @[pspec]
 theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop)
-  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o)
+  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ok o)
   (a: T) (t: Option (AVLNode T)):
-  ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ret ⟨ added, t_new ⟩
+  ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩
 --  ∧ AVLTree.set t'.2 = insert a (AVLTree.set t)
   ∧ (BST.ForallNode p t -> p a -> BST.ForallNode p t_new)
   := by match t with
@@ -68,8 +106,8 @@ lemma AVLTreeSet.insert_loop_spec_global
   (a: T) (t: Option (AVLNode T))
   :
   haveI : LT T := (rustLt Ospec)
-  BST.BST t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ret ⟨ added, t_new ⟩
-  ∧ BST.BST t_new := by 
+  BST.Invariant t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩
+  ∧ BST.Invariant t_new := by 
   intro Hbst
   letI instOrd : _root_.Ord T := (rustOrder Ospec)
   letI instLt : LT T := (rustLt Ospec)
@@ -78,9 +116,7 @@ lemma AVLTreeSet.insert_loop_spec_global
   | some (AVLNode.mk b left right) =>
     rw [AVLTreeSet.insert_loop]
     simp only []
-    have := Ospec.infallible; simp at this
-    -- TODO: unbundle `this`...
-    have : ∀ a b, ∃ o, H.cmp a b = .ret o := sorry
+    have : ∀ a b, ∃ o, H.cmp a b = .ok o := Ospec.infallible
     progress keep Hordering as ⟨ ordering ⟩
     cases ordering
     all_goals simp only []
@@ -104,34 +140,33 @@ lemma AVLTreeSet.insert_loop_spec_global
       simp; tauto
     }
     {
-      sorry
+      have ⟨ added₂, left₂, ⟨ H_result, H_bst ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a left (BST.left Hbst)
+      progress keep Htree with AVLTreeSet.insert_loop_spec_local as ⟨ added₁, left₁, Hnode ⟩
+      exact (fun x => x < b)
+      rewrite [Htree] at H_result; simp at H_result
+      refine' ⟨ added₁, ⟨ some (AVLNode.mk b left₁ right), _ ⟩ ⟩
+      simp only [true_and]
+      cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right
+      constructor
+      apply Hnode; exact H_forall_left
+      exact (gtOfRustOrder H b a Hordering)
+      exact H_forall_right
+      convert H_bst
+      exact H_result.2
+      exact H_bst_right
     }
 
 @[pspec]
 def AVLTreeSet.insert_spec 
-  {H: avl_verification.Ord T} 
-  -- TODO: this can be generalized into `H.cmp` must be an equivalence relation.
-  -- and insert works no longer on Sets but on set quotiented by this equivalence relation.
-  (Hcmp_eq: ∀ a b, H.cmp a b = Result.ret Ordering.Equal -> a = b)
-  (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o)
-  (Hbs_search: @BSTree.searchInvariant _ H t)
   (a: T) (t: AVLTreeSet T):
-  ∃ t', t.insert _ H a = Result.ret t' 
-  -- set of values *POST* insertion is {a} \cup set of values of the *PRE* tree.
-  ∧ AVLTree.setOf t'.2.root = insert a (AVLTree.setOf t.root) 
+  haveI : LT T := (rustLt Ospec)
+  BST.Invariant t.root -> (∃ t' added,t.insert _ H a = Result.ok (added, t')
   -- it's still a binary search tree.
-  ∧ @BSTree.searchInvariant _ H t'.2.root
-  -- TODO(reinforcement): (t'.1 is false <=> a \in AVLTree.setOf t.root)
+  ∧ BST.Invariant t'.root)
   := by
-  rw [AVLTreeSet.insert]
-  progress keep h as ⟨ t', Hset ⟩; simp
-  rw [Hset]
-  sorry
-
-
--- insert is infaillible, right?
--- instance [LT T] (o: avl_verification.Ord T): Insert T (AVLTreeSet T) where
---   insert x tree := (AVLTreeSet.insert T o tree x).map (fun (added, tree) => tree)
+  rw [AVLTreeSet.insert]; intro Hbst
+  progress keep h as ⟨ t', Hset ⟩; 
+  simp; assumption
 
 end Implementation
 
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
diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean
index 3316e9e..fdd4b78 100644
--- a/AvlVerification/Tree.lean
+++ b/AvlVerification/Tree.lean
@@ -75,7 +75,4 @@ def AVLTree.mem_some {x: T} {left right: AVLTree T}: AVLTree.mem (some (AVLNode.
 
 def AVLTree.set (t: AVLTree T): Set T := _root_.setOf (AVLTree.mem t)
 
-def AVLTree.setOf_left_incl (t: AVLTree T): t.left.set ⊂ t.set := sorry
-def AVLTree.setOf_right_incl (t: AVLTree T): t.right.set ⊂ t.set := sorry
-
 end Tree
-- 
cgit v1.2.3