diff options
Diffstat (limited to 'AvlVerification')
| -rw-r--r-- | AvlVerification/Insert.lean | 115 | ||||
| -rw-r--r-- | AvlVerification/Specifications.lean | 36 | ||||
| -rw-r--r-- | AvlVerification/Tree.lean | 3 |
3 files changed, 83 insertions, 71 deletions
diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean index baf3441..16e740f 100644 --- a/AvlVerification/Insert.lean +++ b/AvlVerification/Insert.lean @@ -6,55 +6,49 @@ namespace Implementation open Primitives open avl_verification -open Tree (AVLTree) -open Specifications (OrdSpec ordSpecOfTotalityAndDuality ordOfOrdSpec ltOfRustOrder gtOfRustOrder) +open Tree (AVLTree AVLTree.set) +open Specifications (OrdSpecDualityEq 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) +-- 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: @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 +variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpecDualityEq T H) @[pspec] theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop) @@ -105,14 +99,11 @@ theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop) lemma AVLTreeSet.insert_loop_spec_global (a: T) (t: Option (AVLNode T)) : - haveI : LT T := (rustLt Ospec) BST.Invariant t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩ - ∧ BST.Invariant t_new := by + ∧ BST.Invariant t_new ∧ AVLTree.set t_new = {a} ∪ AVLTree.set t := by intro Hbst - letI instOrd : _root_.Ord T := (rustOrder Ospec) - letI instLt : LT T := (rustLt Ospec) match t with - | none => simp [AVLTreeSet.insert_loop] + | none => simp [AVLTreeSet.insert_loop, AVLTree.set, setOf] | some (AVLNode.mk b left right) => rw [AVLTreeSet.insert_loop] simp only [] @@ -121,12 +112,13 @@ lemma AVLTreeSet.insert_loop_spec_global cases ordering all_goals simp only [] { - have ⟨ added₂, right₂, ⟨ H_result, H_bst ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a right (BST.right Hbst) + have ⟨ added₂, right₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := 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] + split_conjs cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right constructor exact H_forall_left @@ -135,17 +127,23 @@ lemma AVLTreeSet.insert_loop_spec_global exact H_bst_left convert H_bst exact H_result.2 + simp [AVLTree.set_some] + rewrite [H_result.2, H_set] + simp } { - simp; tauto + simp; split_conjs + . tauto + . simp [Ospec.equality _ _ Hordering] } { - have ⟨ added₂, left₂, ⟨ H_result, H_bst ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a left (BST.left Hbst) + have ⟨ added₂, left₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := 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] + split_conjs cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right constructor apply Hnode; exact H_forall_left @@ -154,15 +152,18 @@ lemma AVLTreeSet.insert_loop_spec_global convert H_bst exact H_result.2 exact H_bst_right + simp [AVLTree.set_some] + rewrite [H_result.2, H_set] + simp [Set.singleton_union, Set.insert_comm, Set.insert_union] } @[pspec] def AVLTreeSet.insert_spec (a: T) (t: AVLTreeSet T): - 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. - ∧ BST.Invariant t'.root) + ∧ BST.Invariant t'.root + ∧ AVLTree.set t'.root = {a} ∪ AVLTree.set t.root) := by rw [AVLTreeSet.insert]; intro Hbst progress keep h as ⟨ t', Hset ⟩; diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean index 958a3e7..0694df3 100644 --- a/AvlVerification/Specifications.lean +++ b/AvlVerification/Specifications.lean @@ -42,32 +42,40 @@ namespace Specifications open Primitives open Result -variable {T: Type} (H: avl_verification.Ord T) +variable {T: Type} (H: outParam (avl_verification.Ord T)) -- TODO: reason about raw bundling vs. refined bundling. -class OrdSpec where +-- 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 +-- TODO: OrdSpecEq := OrdSpecRel (R := Eq). +class OrdSpecEq extends OrdSpecInfaillible H where + equality: ∀ a b, H.cmp a b = .ok .Equal -> a = b + +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, OrdSpecEq H + instance: Coe (avl_verification.Ordering) (_root_.Ordering) where coe a := a.toLeanOrdering -def ordSpecOfTotalityAndDuality - (H: avl_verification.Ord T) - (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 := Hresult - duality := Hduality - -def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpec H): Ord T where +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 ) -theorem ltOfRustOrder {Spec: OrdSpec H}: +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 @@ -81,8 +89,8 @@ theorem ltOfRustOrder {Spec: OrdSpec H}: simp_rw [Hcmp, get?, avl_verification.Ordering.toLeanOrdering] rfl -theorem gtOfRustOrder {Spec: OrdSpec H}: - haveI O := ordOfOrdSpec H Spec +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 diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean index fdd4b78..8a043a1 100644 --- a/AvlVerification/Tree.lean +++ b/AvlVerification/Tree.lean @@ -75,4 +75,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 + end Tree |