diff options
| author | Ryan Lahfa | 2024-04-23 14:26:27 +0200 |
|---|---|---|
| committer | GitHub | 2024-04-23 14:26:27 +0200 |
| commit | d3ea366adcd71d0ef15ffbc5d35ca998aa53f19a (patch) | |
| tree | d9da70f7564ea73ceacf880b78473c89f617bba7 /Verification/Insert.lean | |
| parent | 0f49a61cc33bddf2cc69bc8915b95c915dc5f987 (diff) | |
| parent | b650710ad3f8c14b713bdf52f684f472115dce2f (diff) | |
Merge pull request #3 from RaitoBezarius/bst-find
feat: `find` and `insert` reinforced proofs
Diffstat (limited to '')
| -rw-r--r-- | Verification/Insert.lean (renamed from AvlVerification/Insert.lean) | 51 |
1 files changed, 6 insertions, 45 deletions
diff --git a/AvlVerification/Insert.lean b/Verification/Insert.lean index f5b7958..260eaa1 100644 --- a/AvlVerification/Insert.lean +++ b/Verification/Insert.lean @@ -1,54 +1,15 @@ -import AvlVerification.Tree -import AvlVerification.BinarySearchTree -import AvlVerification.Specifications +import Verification.Tree +import Verification.BinarySearchTree +import Verification.Specifications namespace Implementation open Primitives open avl_verification open Tree (AVLTree AVLTree.set) -open Specifications (OrdSpecDualityEq ordOfOrdSpec ltOfRustOrder gtOfRustOrder) +open Specifications (OrdSpecLinearOrderEq infallible 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) - -variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpecDualityEq T H) +variable (T: Type) (H: avl_verification.Ord T) [LinearOrder T] (Ospec: OrdSpecLinearOrderEq H) @[pspec] theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop) @@ -107,7 +68,7 @@ lemma AVLTreeSet.insert_loop_spec_global | some (AVLNode.mk b left right) => rw [AVLTreeSet.insert_loop] simp 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 simp only [] |