diff options
Diffstat (limited to '')
| -rw-r--r-- | Verification.lean | 2 | ||||
| -rw-r--r-- | Verification/BinarySearchTree.lean | 114 | ||||
| -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.lean | 57 | ||||
| -rw-r--r-- | Verification/Specifications.lean | 150 | ||||
| -rw-r--r-- | Verification/Tree.lean (renamed from AvlVerification/Tree.lean) | 3 |
7 files changed, 342 insertions, 59 deletions
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 |