diff options
Diffstat (limited to '')
| -rw-r--r-- | Verification/Find.lean (renamed from AvlVerification/Find.lean) | 24 |
1 files changed, 11 insertions, 13 deletions
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): |