diff options
Diffstat (limited to 'AvlVerification/Insert.lean')
| -rw-r--r-- | AvlVerification/Insert.lean | 115 |
1 files changed, 58 insertions, 57 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 ⟩; |