summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--AvlVerification.lean5
-rw-r--r--AvlVerification/BinarySearchTree.lean54
-rw-r--r--AvlVerification/Specifications.lean98
-rw-r--r--Verification.lean2
-rw-r--r--Verification/BinarySearchTree.lean114
-rw-r--r--Verification/Find.lean (renamed from AvlVerification/Find.lean)24
-rw-r--r--Verification/Insert.lean (renamed from AvlVerification/Insert.lean)51
-rw-r--r--Verification/Order.lean57
-rw-r--r--Verification/Specifications.lean150
-rw-r--r--Verification/Tree.lean (renamed from AvlVerification/Tree.lean)3
-rw-r--r--lakefile.lean4
11 files changed, 347 insertions, 215 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/Verification.lean b/Verification.lean
new file mode 100644
index 0000000..31d8103
--- /dev/null
+++ b/Verification.lean
@@ -0,0 +1,2 @@
+import Verification.Insert
+import Verification.Find
diff --git a/Verification/BinarySearchTree.lean b/Verification/BinarySearchTree.lean
new file mode 100644
index 0000000..a49be5e
--- /dev/null
+++ b/Verification/BinarySearchTree.lean
@@ -0,0 +1,114 @@
+import Verification.Tree
+import AvlVerification
+
+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
+
+theorem ForallNode.not_mem {a: T} (p: T -> Prop) (t: Option (AVLNode T)): ¬ p a -> ForallNode p t -> a ∉ AVLTree.set t := fun Hnpa Hpt => by
+ cases t with
+ | none => simp [AVLTree.set]; tauto
+ | some t =>
+ cases Hpt with
+ | some b left right f_pbleft f_pb f_pbright =>
+ simp [AVLTree.set_some]
+ push_neg
+ split_conjs
+ . by_contra hab; rw [hab] at Hnpa; exact Hnpa f_pb
+ . exact ForallNode.not_mem p left Hnpa f_pbleft
+ . exact ForallNode.not_mem p right Hnpa f_pbright
+
+theorem ForallNode.not_mem' {a: T} (p: T -> Prop) (t: Option (AVLNode T)): p a -> ForallNode (fun x => ¬p x) t -> a ∉ AVLTree.set t := fun Hpa Hnpt => by
+ refine' ForallNode.not_mem (fun x => ¬ p x) t _ _
+ simp [Hpa]
+ exact Hnpt
+
+theorem ForallNode.imp {p q: T -> Prop} {t: AVLTree T}: (∀ x, p x -> q x) -> ForallNode p t -> ForallNode q t := fun Himp Hpt => by
+ induction Hpt
+ . simp [ForallNode.none]
+ . constructor
+ . assumption
+ . apply Himp; assumption
+ . assumption
+
+-- This is the binary search invariant.
+variable [LinearOrder T]
+inductive Invariant: 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 {a: T}: Invariant (some (AVLNode.mk a none none)) := by
+ apply Invariant.some
+ all_goals simp [ForallNode.none, Invariant.none]
+
+theorem left {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 {t: AVLTree T}: Invariant t -> Invariant t.right := by
+ intro H
+ induction H with
+ | none => exact Invariant.none
+ | some _ _ _ _ _ _ _ _ _ => simp [AVLTree.right]; assumption
+
+-- TODO: ask at most for LT + Irreflexive (lt_irrefl) + Trichotomy (le_of_not_lt)?
+theorem left_pos {left right: Option (AVLNode T)} {a x: T}: BST.Invariant (some (AVLNode.mk a left right)) -> x ∈ AVLTree.set (AVLNode.mk a left right) -> x < a -> x ∈ AVLTree.set left := fun Hbst Hmem Hxa => by
+ simp [AVLTree.set_some] at Hmem
+ rcases Hmem with (Heq | Hleft) | Hright
+ . rewrite [Heq] at Hxa; exact absurd Hxa (lt_irrefl _)
+ . assumption
+ . exfalso
+
+ -- Hbst -> x ∈ right -> ForallNode (fun v => ¬ v < a)
+ refine' ForallNode.not_mem' (fun v => v < a) right Hxa _ _
+ simp [le_of_not_lt]
+ cases Hbst with
+ | some _ _ _ _ Hforall _ =>
+ refine' ForallNode.imp _ Hforall
+ exact fun x => le_of_lt
+ assumption
+
+theorem right_pos {left right: Option (AVLNode T)} {a x: T}: BST.Invariant (some (AVLNode.mk a left right)) -> x ∈ AVLTree.set (AVLNode.mk a left right) -> a < x -> x ∈ AVLTree.set right := fun Hbst Hmem Hax => by
+ simp [AVLTree.set_some] at Hmem
+ rcases Hmem with (Heq | Hleft) | Hright
+ . rewrite [Heq] at Hax; exact absurd Hax (lt_irrefl _)
+ . exfalso
+ refine' ForallNode.not_mem' (fun v => a < v) left Hax _ _
+ simp [le_of_not_lt]
+ cases Hbst with
+ | some _ _ _ Hforall _ _ =>
+ refine' ForallNode.imp _ Hforall
+ exact fun x => le_of_lt
+ assumption
+ . assumption
+
+
+end BST
diff --git a/AvlVerification/Find.lean b/Verification/Find.lean
index b729dab..764a685 100644
--- a/AvlVerification/Find.lean
+++ b/Verification/Find.lean
@@ -1,15 +1,16 @@
-import AvlVerification.Tree
-import AvlVerification.BinarySearchTree
-import AvlVerification.Specifications
+import Verification.Tree
+import Verification.BinarySearchTree
+import Verification.Specifications
+import AvlVerification
namespace Implementation
open Primitives
open avl_verification
open Tree (AVLTree AVLTree.set)
-open Specifications (OrdSpecDualityEq ordOfOrdSpec ltOfRustOrder gtOfRustOrder)
+open Specifications (OrdSpecLinearOrderEq infallible ltOfRustOrder gtOfRustOrder)
-variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpecDualityEq T H)
+variable (T: Type) (H: avl_verification.Ord T) [DecidableEq T] [LinearOrder T] (Ospec: OrdSpecLinearOrderEq H)
@[pspec]
def AVLTreeSet.find_loop_spec
@@ -20,17 +21,14 @@ def AVLTreeSet.find_loop_spec
| some (AVLNode.mk b left right) =>
rw [AVLTreeSet.find_loop]
dsimp 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 dsimp only
- . refine' AVLTreeSet.find_loop_spec a right (BST.right Hbst) _
- -- b < a
- -- Hbst fournit que a ∈ right
- sorry
- . refine' AVLTreeSet.find_loop_spec a left (BST.left Hbst) _
- -- symmétrie du précédent.
- sorry
+ . refine' AVLTreeSet.find_loop_spec a right (BST.right Hbst) (BST.right_pos Hbst Hmem _)
+ exact ltOfRustOrder _ _ _ Hordering
+ . refine' AVLTreeSet.find_loop_spec a left (BST.left Hbst) (BST.left_pos Hbst Hmem _)
+ exact gtOfRustOrder _ _ _ Hordering
def AVLTreeSet.find_spec
(a: T) (t: AVLTreeSet T):
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/Verification/Order.lean b/Verification/Order.lean
new file mode 100644
index 0000000..396a524
--- /dev/null
+++ b/Verification/Order.lean
@@ -0,0 +1,57 @@
+import Verification.Specifications
+
+namespace Implementation
+
+open Primitives
+open avl_verification
+open Specifications (OrdSpecLinearOrderEq ltOfRustOrder gtOfRustOrder)
+
+instance ScalarU32DecidableLE : DecidableRel (· ≤ · : U32 -> U32 -> Prop) := by
+ simp [instLEScalar]
+ -- Lift this to the decidability of the Int version.
+ infer_instance
+
+instance : LinearOrder (Scalar .U32) where
+ le_antisymm := fun a b Hab Hba => by
+ apply (Scalar.eq_equiv a b).2; exact (Int.le_antisymm ((Scalar.le_equiv _ _).1 Hab) ((Scalar.le_equiv _ _).1 Hba))
+ le_total := fun a b => by
+ rcases (Int.le_total a b) with H | H
+ left; exact (Scalar.le_equiv _ _).2 H
+ right; exact (Scalar.le_equiv _ _).2 H
+ decidableLE := ScalarU32DecidableLE
+
+instance : OrdSpecLinearOrderEq OrdU32 where
+ infallible := fun a b => by
+ unfold Ord.cmp
+ unfold OrdU32
+ unfold OrdU32.cmp
+ rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
+ 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]
+ symmetry := fun a b => by
+ rw [Ordering.toDualOrdering, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
+ rw [compare, Ord.opposite]
+ simp [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
+ split_ifs with hab hba hba' hab' hba'' _ hba₃ _ <;> tauto
+ exact lt_irrefl _ (lt_trans hab hba)
+ rw [hba'] at hab; exact lt_irrefl _ hab
+ rw [hab'] at hba''; exact lt_irrefl _ hba''
+ -- The order is total, therefore, we have at least one case where we are comparing something.
+ cases (lt_trichotomy a b) <;> tauto
+ equivalence := fun a b => by
+ unfold Ord.cmp
+ unfold OrdU32
+ unfold OrdU32.cmp
+ simp only []
+ split_ifs <;> simp only [Result.ok.injEq, not_false_eq_true, neq_imp, IsEmpty.forall_iff]; tauto; try assumption
diff --git a/Verification/Specifications.lean b/Verification/Specifications.lean
new file mode 100644
index 0000000..392c438
--- /dev/null
+++ b/Verification/Specifications.lean
@@ -0,0 +1,150 @@
+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
+
+@[simp]
+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
+
+@[simp]
+def Ordering.toDualOrdering (o: avl_verification.Ordering): avl_verification.Ordering := match o with
+| .Less => .Greater
+| .Equal => .Equal
+| .Greater => .Less
+
+@[simp]
+theorem Ordering.toLeanOrdering.injEq (x y: avl_verification.Ordering): (x.toLeanOrdering = y.toLeanOrdering) = (x = y) := by
+ apply propext
+ cases x <;> cases y <;> simp
+
+@[simp]
+theorem ite_eq_lt_distrib (c : Prop) [Decidable c] (a b : Ordering) :
+ ((if c then a else b) = .Less) = if c then a = .Less else b = .Less := by
+ by_cases c <;> simp [*]
+
+@[simp]
+theorem ite_eq_eq_distrib (c : Prop) [Decidable c] (a b : Ordering) :
+ ((if c then a else b) = .Equal) = if c then a = .Equal else b = .Equal := by
+ by_cases c <;> simp [*]
+
+@[simp]
+theorem ite_eq_gt_distrib (c : Prop) [Decidable c] (a b : Ordering) :
+ ((if c then a else b) = .Greater) = if c then a = .Greater else b = .Greater := by
+ by_cases c <;> simp [*]
+
+end avl_verification
+
+namespace Specifications
+
+open Primitives
+open Result
+
+variable {T: Type} (H: outParam (avl_verification.Ord T))
+
+@[simp]
+def _root_.Ordering.toDualOrdering (o: _root_.Ordering): _root_.Ordering := match o with
+| .lt => .gt
+| .eq => .eq
+| .gt => .lt
+
+
+@[simp]
+theorem toDualOrderingOfToLeanOrdering (o: avl_verification.Ordering): o.toDualOrdering.toLeanOrdering = o.toLeanOrdering.toDualOrdering := by
+ cases o <;> simp
+
+@[simp]
+theorem toDualOrderingIdempotency (o: _root_.Ordering): o.toDualOrdering.toDualOrdering = o := by
+ cases o <;> simp
+
+-- TODO: reason about raw bundling vs. refined bundling.
+-- raw bundling: hypothesis with Rust extracted objects.
+-- refined bundling: lifted hypothesis with Lean native objects.
+class OrdSpec [Ord T] where
+ infallible: ∀ a b, ∃ (o: avl_verification.Ordering), H.cmp a b = .ok o ∧ compare a b = o.toLeanOrdering
+
+class OrdSpecSymmetry [O: Ord T] extends OrdSpec H where
+ symmetry: ∀ a b, O.compare a b = (O.opposite.compare a b).toDualOrdering
+
+-- Must be R decidableRel and an equivalence relationship?
+class OrdSpecRel [O: Ord T] (R: outParam (T -> T -> Prop)) extends OrdSpec H where
+ equivalence: ∀ a b, H.cmp a b = .ok .Equal -> R a b
+
+class OrdSpecLinearOrderEq [O: Ord T] extends OrdSpecSymmetry H, OrdSpecRel H Eq
+
+theorem infallible [Ord T] [OrdSpec H]: ∀ a b, ∃ o, H.cmp a b = .ok o := fun a b => by
+ obtain ⟨ o, ⟨ H, _ ⟩ ⟩ := OrdSpec.infallible a b
+ exact ⟨ o, H ⟩
+
+instance: Coe (avl_verification.Ordering) (_root_.Ordering) where
+ coe a := a.toLeanOrdering
+
+theorem rustCmpEq [Ord T] [O: OrdSpec H]: H.cmp a b = .ok o <-> compare a b = o.toLeanOrdering := by
+ apply Iff.intro
+ . intro Hcmp
+ obtain ⟨ o', ⟨ Hcmp', Hcompare ⟩ ⟩ := O.infallible a b
+ rw [Hcmp', ok.injEq] at Hcmp
+ simp [Hcompare, Hcmp', Hcmp]
+ . intro Hcompare
+ obtain ⟨ o', ⟨ Hcmp', Hcompare' ⟩ ⟩ := O.infallible a b
+ rw [Hcompare', avl_verification.Ordering.toLeanOrdering.injEq] at Hcompare
+ simp [Hcompare.symm, Hcmp']
+
+
+theorem oppositeOfOpposite {x y: _root_.Ordering}: x.toDualOrdering = y ↔ x = y.toDualOrdering := by
+ cases x <;> cases y <;> simp
+theorem oppositeRustOrder [Ord T] [Spec: OrdSpecSymmetry H] {a b}: H.cmp b a = .ok o ↔ H.cmp a b = .ok o.toDualOrdering := by
+ rw [rustCmpEq, Spec.symmetry, compare, Ord.opposite, oppositeOfOpposite, rustCmpEq, toDualOrderingOfToLeanOrdering]
+
+theorem ltOfRustOrder
+ [LO: LinearOrder T]
+ [Spec: OrdSpec H]:
+ ∀ a b, H.cmp a b = .ok .Less -> a < b := by
+ intros a b
+ intro Hcmp
+ -- why the typeclass search doesn't work here?
+ refine' (@compare_lt_iff_lt T LO).1 _
+ obtain ⟨ o, ⟨ Hcmp', Hcompare ⟩ ⟩ := Spec.infallible a b
+ simp only [Hcmp', ok.injEq] at Hcmp
+ simp [Hcompare, Hcmp, avl_verification.Ordering.toLeanOrdering]
+
+theorem gtOfRustOrder
+ [LinearOrder T]
+ [Spec: OrdSpecSymmetry H]:
+ ∀ a b, H.cmp a b = .ok .Greater -> b < a := by
+ intros a b
+ intro Hcmp
+ refine' @ltOfRustOrder _ H _ Spec.toOrdSpec _ _ _
+ rewrite [oppositeRustOrder]
+ simp [Hcmp]
+
+end Specifications
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
diff --git a/lakefile.lean b/lakefile.lean
index ccc0a55..743a0db 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,9 +4,9 @@ open Lake DSL
require base from git
"https://github.com/AeneasVerif/aeneas"@"main"/"backends/lean"
-package «AvlVerification» where
+package «Verification» where
-- add package configuration options here
@[default_target]
-lean_lib «AvlVerification» where
+lean_lib «Verification» where
-- add library configuration options here