diff options
| author | Raito Bezarius | 2024-04-23 14:24:04 +0200 |
|---|---|---|
| committer | Raito Bezarius | 2024-04-23 14:24:04 +0200 |
| commit | b650710ad3f8c14b713bdf52f684f472115dce2f (patch) | |
| tree | d9da70f7564ea73ceacf880b78473c89f617bba7 /AvlVerification/Find.lean | |
| parent | 2ff68510aabc63e250f98264e0642557015de4e2 (diff) | |
feat: close `find` / `insert` proofs
After a complete 180 with the Order theory, we close the goals of find
and insert and we give an example of U32 order that we will upstream to
Aeneas directly.
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
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): |