From b650710ad3f8c14b713bdf52f684f472115dce2f Mon Sep 17 00:00:00 2001 From: Raito Bezarius Date: Tue, 23 Apr 2024 14:24:04 +0200 Subject: 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 --- AvlVerification/Find.lean | 42 ------------------------------------------ 1 file changed, 42 deletions(-) delete mode 100644 AvlVerification/Find.lean (limited to 'AvlVerification/Find.lean') diff --git a/AvlVerification/Find.lean b/AvlVerification/Find.lean deleted file mode 100644 index b729dab..0000000 --- a/AvlVerification/Find.lean +++ /dev/null @@ -1,42 +0,0 @@ -import AvlVerification.Tree -import AvlVerification.BinarySearchTree -import AvlVerification.Specifications - -namespace Implementation - -open Primitives -open avl_verification -open Tree (AVLTree AVLTree.set) -open Specifications (OrdSpecDualityEq ordOfOrdSpec ltOfRustOrder gtOfRustOrder) - -variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpecDualityEq T H) - -@[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 - match t with - | none => trivial - | some (AVLNode.mk b left right) => - rw [AVLTreeSet.find_loop] - dsimp only - have : ∀ a b, ∃ o, H.cmp a b = .ok o := Ospec.infallible - 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 - -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 - -end Implementation - -- cgit v1.2.3