From 50be416e22a39eaf59f7edba81b919e1f114a0ae Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Thu, 4 Apr 2024 17:31:19 +0200
Subject: feat: close the BST proof modulo unbundling

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
---
 AvlVerification/Specifications.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'AvlVerification/Specifications.lean')

diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean
index 94fdd5f..247fd00 100644
--- a/AvlVerification/Specifications.lean
+++ b/AvlVerification/Specifications.lean
@@ -67,4 +67,14 @@ def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpec H): Ord T where
     simp only
   )
 
+theorem ltOfRustOrder {Spec: OrdSpec H}: 
+  haveI O := ordOfOrdSpec H Spec
+  haveI := @ltOfOrd _ O
+  ∀ a b, H.cmp a b = .ret .Less -> a < b := by
+  intros a b
+  intro Hcmp
+  change ((Spec.cmp a b).get? _ == .lt)
+  simp [Hcmp, map, avl_verification.Ordering.toLeanOrdering]
+  simp [get?]
+  rfl
 end Specifications
-- 
cgit v1.2.3

