1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
import «AvlVerification»
namespace Primitives
namespace Result
def map {A B: Type} (x: Result A) (f: A -> B): Result B := match x with
| .ok y => .ok (f y)
| .fail e => .fail e
| .div => .div
@[inline]
def isok {A: Type} : Result A -> Bool
| .ok _ => true
| .fail _ => false
| .div => false
@[inline]
def get? {A: Type}: (r: Result A) -> isok r -> A
| .ok x, _ => x
end Result
end Primitives
namespace avl_verification
def Ordering.toLeanOrdering (o: avl_verification.Ordering): _root_.Ordering := match o with
| .Less => .lt
| .Equal => .eq
| .Greater => .gt
def Ordering.ofLeanOrdering (o: _root_.Ordering): avl_verification.Ordering := match o with
| .lt => .Less
| .eq => .Equal
| .gt => .Greater
end avl_verification
namespace Specifications
open Primitives
open Result
variable {T: Type} (H: outParam (avl_verification.Ord T))
-- TODO: reason about raw bundling vs. refined bundling.
-- raw bundling: hypothesis with Rust extracted objects.
-- refined bundling: lifted hypothesis with Lean native objects.
class OrdSpecInfaillible where
infallible: ∀ a b, ∃ (o: avl_verification.Ordering), H.cmp a b = .ok o
class OrdSpecDuality extends OrdSpecInfaillible H where
duality: ∀ a b, H.cmp a b = .ok .Greater -> H.cmp b a = .ok .Less
-- TODO: OrdSpecEq := OrdSpecRel (R := Eq).
class OrdSpecEq extends OrdSpecInfaillible H where
equality: ∀ a b, H.cmp a b = .ok .Equal -> a = b
class OrdSpecRel (R: outParam (T -> T -> Prop)) extends OrdSpecInfaillible H where
equivalence: ∀ a b, H.cmp a b = .ok .Equal -> R a b
class OrdSpecDualityEq extends OrdSpecDuality H, OrdSpecEq H
instance: Coe (avl_verification.Ordering) (_root_.Ordering) where
coe a := a.toLeanOrdering
def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpecInfaillible H): Ord T where
compare x y := (H.cmp x y).get? (by
cases' (spec.infallible x y) with o Hcmp
rewrite [isok, Hcmp]
simp only
)
instance [spec: OrdSpecInfaillible H]: Ord T := ordOfOrdSpec H spec
instance [OrdSpecInfaillible H]: LT T := ltOfOrd
theorem ltOfRustOrder {Spec: OrdSpecInfaillible H}:
haveI O := ordOfOrdSpec H Spec
haveI := @ltOfOrd _ O
∀ a b, H.cmp a b = .ok .Less -> a < b := by
intros a b
intro Hcmp
rw [LT.lt]
simp [ltOfOrd]
rw [compare]
simp [ordOfOrdSpec]
-- https://proofassistants.stackexchange.com/questions/1062/what-does-the-motive-is-not-type-correct-error-mean-in-lean
simp_rw [Hcmp, get?, avl_verification.Ordering.toLeanOrdering]
rfl
theorem gtOfRustOrder {Spec: OrdSpecDuality H}:
haveI O := ordOfOrdSpec H Spec.toOrdSpecInfaillible
haveI := @ltOfOrd _ O
∀ a b, H.cmp a b = .ok .Greater -> b < a := by
intros a b
intro Hcmp
apply ltOfRustOrder
exact (Spec.duality _ _ Hcmp)
end Specifications
|
