diff options
| author | Raito Bezarius | 2024-04-04 17:31:19 +0200 |
|---|---|---|
| committer | Raito Bezarius | 2024-04-05 18:33:47 +0200 |
| commit | 50be416e22a39eaf59f7edba81b919e1f114a0ae (patch) | |
| tree | 255447dcbbf7d26233b2caa092dc1af9ce188f2b /AvlVerification/Specifications.lean | |
| parent | 22a499f5d4d231bef3193405983f9ade6da116db (diff) | |
feat: close the BST proof modulo unbundling
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
Diffstat (limited to 'AvlVerification/Specifications.lean')
| -rw-r--r-- | AvlVerification/Specifications.lean | 10 |
1 files changed, 10 insertions, 0 deletions
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 |