-
Notifications
You must be signed in to change notification settings - Fork 0
/
PositiveBHeap_withIs.ttw
92 lines (85 loc) · 2.05 KB
/
PositiveBHeap_withIs.ttw
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
codata BHeap (R : A -> A -> Prop) : Type
| E
| N of
& root of A
& l r of BHeap
& okl of l is N -> R root l.root
& okr of r is N -> R root r.root
// Axiom.
le-s-r : (n : Nat) -> n <= s n
nats : (n : Nat) -> BHeap (<=) := N
& root => n
& l => nats (s n)
& r => nats (s n)
& okl => fun _ : l is N => le-s-r n
& okr => fun _ : r is N => le-s-r n
map
#(A B : Type)
(R : A -> A -> Prop) (S : B -> B -> Prop)
(f : A -> B)
(pres : #(x y : A) -> R x y -> S (f x) (f y))
: (h : BHeap R) -> BHeap S
| E => E
| N => N
& root => f h.root
& l => map h.l
& r => map h.r
& okl with h.l
| E => fun e : map h.l is N => abort e
| N => fun _ : map h.l is N => pres (h.okl (_ : h.l is N))
& okr with h.r
| E => fun e : map h.r is N => abort e
| N => fun _ : map h.r is N => pres (h.okr (_ : h.r is N))
// Less bloated.
map
#(A B : Type)
(R : A -> A -> Prop) (S : B -> B -> Prop)
(f : A -> B)
(pres : #(x y : A) -> R x y -> S (f x) (f y))
: (h : BHeap R) -> BHeap S
| E => E
| N => N
& root => f h.root
& l => map h.l
& r => map h.r
& okl with h.l
| E => abort
| N => fun _ => pres (h.okl _)
& okr with h.r
| E => abort
| N => fun _ => pres (h.okr _)
zipWith
#(A B C : Type)
(RA : A -> A -> Prop)
(RB : B -> B -> Prop)
(RC : C -> C -> Prop)
(f : A -> B -> C)
(pres : #(a1 a2 : A, b1 b2 : B) ->
RA a1 a2 -> RB b1 b2 -> RC (f a1 b1) (f a2 b2))
: (ha : BHeap RA, hb : BHeap RB) -> BHeap RC
| E, _
| _, E => E
| N, N => N
& root => f ha.root hb.root
& l => zipWith ha.l hb.l
& r => zipWith ha.r hb.r
& okl with ha.l, hb.l
| E, _
| _, E => abort
| N, N => fun _ => pres (ha.okl _) (hb.okl _)
& okr with ha.r, hb.r
| E, _
| _, E => abort
| N, N => fun _ => pres (ha.okr _) (hb.okr _)
mirror : (h : BHeap R) -> BHeap R
| E => E
| N => N
& root => h.root
& l => mirror h.r
& r => mirror h.l
& okl => h.okr
& okr => h.okl
repeat (x : A) (refl : (x : A) -> R x x) : BHeap R := N
& root => x
& l & r => repeat
& okl & okr => refl x