blob: 0bf9ffb3486d9da93641aca41ddbd25a5441624f (
plain)
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
|
import «AvlVerification»
namespace Primitives
namespace Result
def map {A B: Type} (x: Result A) (f: A -> B): Result B := match x with
| .ret y => .ret (f y)
| .fail e => .fail e
| .div => .div
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
end avl_verification
namespace Specifications
open Primitives
open Result
variable {T: Type}
class OrdSpec (U: Type) where
cmp: U -> U -> Result Ordering
infallible: ∀ a b, ∃ o, cmp a b = .ret o
instance: Coe (avl_verification.Ordering) (_root_.Ordering) where
coe a := a.toLeanOrdering
def ordSpecOfInfaillible
(H: avl_verification.Ord T)
(Hresult: ∀ a b, ∃ o, H.cmp a b = Primitives.Result.ret o)
: OrdSpec T where
cmp x y := (H.cmp x y).map (fun z => z.toLeanOrdering)
infallible := by
intros a b
-- TODO: transform the "raw" hypothesis into the "nice" hypothesis.
sorry
instance [OrdSpec T]: Ord T where
compare x y := match (OrdSpec.cmp x y) with
| .ret z => z
| .fail _ => by sorry
| .div => by sorry
end Specifications
|
