5 files changed, 11 insertions, 200 deletions
diff --git a/AvlVerification.lean b/AvlVerification.lean
index 9380768..fee58d5 100644
--- a/AvlVerification.lean
+++ b/AvlVerification.lean
@@ -1,6 +1,7 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [avl_verification]
 import Base
+
 open Primitives
 
 namespace avl_verification
@@ -93,8 +94,8 @@ def AVLTreeSet.insert
   Result (Bool × (AVLTreeSet T))
   :=
   do
-  let (b, as) ← AVLTreeSet.insert_loop T OrdInst value self.root
-  Result.ok (b, { root := as })
+  let (b, u) ← AVLTreeSet.insert_loop T OrdInst value self.root
+  Result.ok (b, { root := u })
 
 /- [avl_verification::{(avl_verification::Ord for u32)#1}::cmp]:
    Source: 'src/main.rs', lines 65:4-65:43 -/
diff --git a/AvlVerification/BinarySearchTree.lean b/AvlVerification/BinarySearchTree.lean
deleted file mode 100644
index 2b17d52..0000000
--- a/AvlVerification/BinarySearchTree.lean
+++ /dev/null
@@ -1,54 +0,0 @@
-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))
-
-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 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
-  -> Invariant left -> Invariant right -> Invariant (some (AVLNode.mk a left right))
-
-@[simp]
-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}: Invariant t -> Invariant t.left := by
-  intro H
-  induction H with 
-  | none => exact Invariant.none
-  | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.left]; assumption
-
-theorem right [LT T] {t: AVLTree T}: Invariant t -> Invariant t.right := by
-  intro H
-  induction H with 
-  | none => exact Invariant.none
-  | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.right]; assumption
-
-end BST
diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean
deleted file mode 100644
index ac2d056..0000000
--- a/AvlVerification/Specifications.lean
+++ /dev/null
@@ -1,98 +0,0 @@
-import «AvlVerification»
-
-namespace Primitives
-
-namespace Result
-
-def map {A B: Type} (x: Result A) (f: A -> B): Result B := match x with
-| .ok y => .ok (f y)
-| .fail e => .fail e
-| .div => .div
-
-@[inline]
-def isok {A: Type} : Result A -> Bool
-| .ok _ => true
-| .fail _ => false
-| .div => false
-
-@[inline]
-def get? {A: Type}: (r: Result A) -> isok r -> A
-| .ok x, _ => x
-
-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
-
-def Ordering.ofLeanOrdering (o: _root_.Ordering): avl_verification.Ordering := match o with
-| .lt => .Less
-| .eq => .Equal
-| .gt => .Greater
-
-end avl_verification
-
-namespace Specifications
-
-open Primitives
-open Result
-
-variable {T: Type} (H: outParam (avl_verification.Ord T))
-
--- TODO: reason about raw bundling vs. refined bundling.
--- 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
-
-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, OrdSpecRel H Eq
-
-instance: Coe (avl_verification.Ordering) (_root_.Ordering) where
-  coe a := a.toLeanOrdering
-
-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
-  )
-
-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
-  intros a b
-  intro Hcmp
-  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: 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
-  intro Hcmp
-  apply ltOfRustOrder
-  exact (Spec.duality _ _ Hcmp)
-
-
-end Specifications
diff --git a/AvlVerification/Insert.lean b/Verification/Insert.lean
index f5b7958..260eaa1 100644
--- a/AvlVerification/Insert.lean
+++ b/Verification/Insert.lean
@@ -1,54 +1,15 @@
-import AvlVerification.Tree
-import AvlVerification.BinarySearchTree
-import AvlVerification.Specifications
+import Verification.Tree
+import Verification.BinarySearchTree
+import Verification.Specifications
 
 namespace Implementation
 
 open Primitives
 open avl_verification
 open Tree (AVLTree AVLTree.set)
-open Specifications (OrdSpecDualityEq ordOfOrdSpec ltOfRustOrder gtOfRustOrder)
+open Specifications (OrdSpecLinearOrderEq infallible 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)
-
-variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpecDualityEq T H)
+variable (T: Type) (H: avl_verification.Ord T) [LinearOrder T] (Ospec: OrdSpecLinearOrderEq H)
 
 @[pspec]
 theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop)
@@ -107,7 +68,7 @@ lemma AVLTreeSet.insert_loop_spec_global
   | some (AVLNode.mk b left right) =>
     rw [AVLTreeSet.insert_loop]
     simp only []
-    have : ∀ a b, ∃ o, H.cmp a b = .ok o := Ospec.infallible
+    have : ∀ a b, ∃ o, H.cmp a b = .ok o := infallible H
     progress keep Hordering as ⟨ ordering ⟩
     cases ordering
     all_goals simp only []
diff --git a/AvlVerification/Tree.lean b/Verification/Tree.lean
index 8a043a1..d6a4f80 100644
--- a/AvlVerification/Tree.lean
+++ b/Verification/Tree.lean
@@ -76,6 +76,7 @@ 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)
 
 @[simp]
-def AVLTree.set_some {x: T} {left right: AVLTree T}: AVLTree.set (some (AVLNode.mk x left right)) = {x} ∪ AVLTree.set left ∪ AVLTree.set right := sorry
+def AVLTree.set_some {x: T} {left right: AVLTree T}: AVLTree.set (some (AVLNode.mk x left right)) = {x} ∪ AVLTree.set left ∪ AVLTree.set right := by 
+  simp [set, setOf]
 
 end Tree