diff options
Diffstat (limited to 'Verification')
| -rw-r--r-- | Verification/Find.lean | 28 |
1 files changed, 18 insertions, 10 deletions
diff --git a/Verification/Find.lean b/Verification/Find.lean index 764a685..9ff7f3d 100644 --- a/Verification/Find.lean +++ b/Verification/Find.lean @@ -15,26 +15,34 @@ variable (T: Type) (H: avl_verification.Ord T) [DecidableEq T] [LinearOrder T] ( @[pspec] def AVLTreeSet.find_loop_spec (a: T) (t: Option (AVLNode T)): - BST.Invariant t -> a ∈ AVLTree.set t -> AVLTreeSet.find_loop _ H a t = Result.ok true := fun Hbst Hmem => by + BST.Invariant t -> ∃ b, AVLTreeSet.find_loop _ H a t = Result.ok b ∧ (b ↔ a ∈ AVLTree.set t) := fun Hbst => by + rewrite [AVLTreeSet.find_loop] match t with - | none => trivial + | none => use false; simp [AVLTree.set]; tauto | some (AVLNode.mk b left right) => - rw [AVLTreeSet.find_loop] dsimp only 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) (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 + . convert (AVLTreeSet.find_loop_spec a right (BST.right Hbst)) using 4 + apply Iff.intro + -- We apply a localization theorem here. + . intro Hmem; exact (BST.right_pos Hbst Hmem (ltOfRustOrder _ _ _ Hordering)) + . intro Hmem; simp [AVLTree.set_some]; right; assumption + . simp [Ospec.equivalence _ _ Hordering] + . convert (AVLTreeSet.find_loop_spec a left (BST.left Hbst)) using 4 + apply Iff.intro + -- We apply a localization theorem here. + . intro Hmem; exact (BST.left_pos Hbst Hmem (gtOfRustOrder _ _ _ Hordering)) + . intro Hmem; simp [AVLTree.set_some]; left; right; assumption + def AVLTreeSet.find_spec (a: T) (t: AVLTreeSet T): - BST.Invariant t.root -> a ∈ AVLTree.set t.root -> - t.find _ H a = Result.ok true := fun Hbst Hmem => by - rw [AVLTreeSet.find]; progress + BST.Invariant t.root -> ∃ b, t.find _ H a = Result.ok b ∧ (b ↔ a ∈ AVLTree.set t.root) := fun Hbst => by + rw [AVLTreeSet.find] + progress; simp only [Result.ok.injEq, exists_eq_left']; assumption end Implementation |