diff options
| author | Raito Bezarius | 2024-04-23 16:34:06 +0200 |
|---|---|---|
| committer | Raito Bezarius | 2024-04-23 16:34:55 +0200 |
| commit | 69e7653d313773304939de58c575595ece3aa034 (patch) | |
| tree | c949a7274e113246816bb07110d02a2abb9d85a9 | |
| parent | d3ea366adcd71d0ef15ffbc5d35ca998aa53f19a (diff) | |
feat: make `find` a better specification
Previously, find := true was matching this spec.
It needed to be in PRE/POST style and be an equivalence wrt to the
location return value.
Alternatively, we import the Order.
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
| -rw-r--r-- | Verification.lean | 1 | ||||
| -rw-r--r-- | Verification/Find.lean | 28 |
2 files changed, 19 insertions, 10 deletions
diff --git a/Verification.lean b/Verification.lean index 31d8103..4a28407 100644 --- a/Verification.lean +++ b/Verification.lean @@ -1,2 +1,3 @@ import Verification.Insert import Verification.Find +import Verification.Order 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 |