From 69e7653d313773304939de58c575595ece3aa034 Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Tue, 23 Apr 2024 16:34:06 +0200
Subject: 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>
---
 Verification.lean      |  1 +
 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
 
-- 
cgit v1.2.3