/
binnat.ctt
226 lines (173 loc) · 7.94 KB
/
binnat.ctt
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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
-- This file defines binary natural numbers are prove that they are
-- isomorphic to unary natural numbers and by univalence we get a path
-- in the universe between these two types.
--
-- We then define a "doubling structure" with an operation for
-- computing 2*x and prove that the doubling structure for binary
-- numbers is isomorphic to the one for unary. This is then used to
-- transport a proof that 2^20 * 1024 = 2^5 * 2^15 * 1024 from binary
-- to unary numbers. This computation is instant for binary numbers
-- but impossible for unary, hence this illustrates how univalence can
-- be used to do program and data refinements.
--
module binnat where
import nat
-- Positive binary numbers like in Coq
data pos = pos1
| x0 (p : pos)
| x1 (p : pos)
sucPos : pos -> pos = split
pos1 -> x0 pos1
x0 p -> x1 p
x1 p -> x0 (sucPos p)
doubleN : nat -> nat = split
zero -> zero
suc n -> suc (suc (doubleN n))
PosToN : pos -> nat = split
pos1 -> suc zero
x0 p -> doubleN (PosToN p)
x1 p -> suc (doubleN (PosToN p))
posInd (P : pos -> U) (h1 : P pos1) (hS : (p : pos) -> P p -> P (sucPos p)) (p : pos) : P p =
let H (p : pos) (hx0p : P (x0 p)) : P (x0 (sucPos p)) = hS (x1 p) (hS (x0 p) hx0p)
f : (p : pos) -> P p = split
pos1 -> h1
x0 p -> posInd (\(p : pos) -> P (x0 p)) (hS pos1 h1) H p
x1 p -> hS (x0 p) (posInd (\(p : pos) -> P (x0 p)) (hS pos1 h1) H p)
in f p
sucPosSuc : (p : pos) -> Path nat (PosToN (sucPos p)) (suc (PosToN p)) = split
pos1 -> <_> suc (suc zero)
x0 p -> <_> suc (doubleN (PosToN p))
x1 p -> <i> doubleN (sucPosSuc p @ i)
zeronPosToN (p : pos) : neg (Path nat zero (PosToN p)) =
posInd (\(p : pos) -> neg (Path nat zero (PosToN p))) (\(prf : Path nat zero one) -> znots zero prf) hS p
where
hS (p : pos) (_ : neg (Path nat zero (PosToN p))) (prf : Path nat zero (PosToN (sucPos p))) : N0 =
znots (PosToN p) (<i> comp (<j> nat) (prf @ i) [ (i=0) -> <_> zero, (i = 1) -> sucPosSuc p ])
-- Inverse of PosToN:
NtoPos' : nat -> pos = split
zero -> pos1
suc n -> sucPos (NtoPos' n)
NtoPos : nat -> pos = split
zero -> pos1
suc n -> NtoPos' n
PosToNK : (n : nat) -> Path nat (PosToN (NtoPos (suc n))) (suc n) = split
zero -> <_> (suc zero)
suc n ->
let ih : Path nat (suc (PosToN (NtoPos' n))) (suc (suc n)) = <i> suc (PosToNK n @ i)
in compPath nat (PosToN (NtoPos (suc (suc n)))) (suc (PosToN (NtoPos' n)))
(suc (suc n)) (sucPosSuc (NtoPos' n)) ih
NtoPosSuc : (n : nat) -> neg (Path nat zero n) -> Path pos (NtoPos (suc n)) (sucPos (NtoPos n)) = split
zero -> \(p : neg (Path nat zero zero)) -> efq (Path pos (NtoPos (suc zero)) (sucPos (NtoPos zero))) (p (<_> zero))
suc n -> \(_ : neg (Path nat zero (suc n))) -> <_> (sucPos (NtoPos' n))
NtoPosK (p:pos) : Path pos (NtoPos (PosToN p)) p
= posInd (\(p:pos) -> Path pos (NtoPos (PosToN p)) p) (refl pos pos1) hS p
where
hS (p : pos) (hp: Path pos (NtoPos (PosToN p)) p) : Path pos (NtoPos (PosToN (sucPos p))) (sucPos p)
=
let H1 : Path pos (NtoPos (PosToN (sucPos p))) (NtoPos (suc (PosToN p)))
= mapOnPath nat pos NtoPos (PosToN (sucPos p)) (suc (PosToN p)) (sucPosSuc p)
H2 : Path pos (NtoPos (suc (PosToN p))) (sucPos (NtoPos (PosToN p)))
= NtoPosSuc (PosToN p) (zeronPosToN p)
H3 : Path pos (sucPos (NtoPos (PosToN p))) (sucPos p)
= mapOnPath pos pos sucPos (NtoPos (PosToN p)) p hp
in compPath pos (NtoPos (PosToN (sucPos p))) (sucPos (NtoPos (PosToN p))) (sucPos p)
(compPath pos (NtoPos (PosToN (sucPos p))) (NtoPos (suc (PosToN p))) (sucPos (NtoPos (PosToN p))) H1 H2)
H3
posToNinj : injective pos nat PosToN
= \ (p0 p1:pos) (h:Path nat (PosToN p0) (PosToN p1)) ->
<i> comp (<_>pos) (NtoPos (h@i)) [(i=0) -> NtoPosK p0,(i=1) -> NtoPosK p1]
-- Binary natural numbers
data binN = binN0 | binNpos (p : pos)
NtoBinN : nat -> binN = split
zero -> binN0
suc n -> binNpos (NtoPos (suc n))
BinNtoN : binN -> nat = split
binN0 -> zero
binNpos p -> PosToN p
NtoBinNK : (n:nat) -> Path nat (BinNtoN (NtoBinN n)) n = split
zero -> <_> zero
suc n -> PosToNK n
rem (p : pos) : Path binN (NtoBinN (PosToN (sucPos p))) (binNpos (sucPos p)) =
compPath binN (NtoBinN (PosToN (sucPos p))) (binNpos (NtoPos (suc (PosToN p))))
(binNpos (sucPos p)) rem1 rem2
where
rem1 : Path binN (NtoBinN (PosToN (sucPos p))) (binNpos (NtoPos (suc (PosToN p))))
= mapOnPath nat binN NtoBinN (PosToN (sucPos p)) (suc (PosToN p)) (sucPosSuc p)
rem2 : Path binN (binNpos (NtoPos (suc (PosToN p)))) (binNpos (sucPos p))
= <i>binNpos
(compPath pos (NtoPos (suc (PosToN p))) (sucPos (NtoPos (PosToN p))) (sucPos p)
(NtoPosSuc (PosToN p) (zeronPosToN p))
(mapOnPath pos pos sucPos (NtoPos (PosToN p)) p (NtoPosK p))@i)
lem1 (p : pos) : Path binN (NtoBinN (PosToN p)) (binNpos p)
= posInd (\ (p:pos) -> Path binN (NtoBinN (PosToN p)) (binNpos p)) (refl binN (binNpos pos1))
(\ (p:pos) (_:Path binN (NtoBinN (PosToN p)) (binNpos p)) -> rem p) p
BinNtoNK : (b:binN) -> Path binN (NtoBinN (BinNtoN b)) b = split
binN0 -> <_> binN0
binNpos p -> lem1 p
PathbinNN : Path U binN nat
= isoPath binN nat BinNtoN NtoBinN NtoBinNK BinNtoNK
-- Doubling
-- doublesN n m = 2^n * m
doublesN : nat -> nat -> nat = split
zero -> \(m:nat) -> m
suc n -> \(m:nat) -> doublesN n (doubleN m)
-- 1024 = 2^8 * 2^2 = 2^10
n1024 : nat = doublesN (add four four) four
doubleBinN : binN -> binN = split
binN0 -> binN0
binNpos p -> binNpos (x0 p)
doublesBinN : nat -> binN -> binN = split
zero -> \(m:binN) -> m
suc n -> \(m:binN) -> doublesBinN n (doubleBinN m)
-- Doubling structure
data Double =
D (A : U) -- carrier
(double : A -> A) -- doubling function computing 2 * x
(elt : A) -- element to double
carrier : Double -> U = split D c _ _ -> c
double : (D : Double) -> (carrier D -> carrier D)
= split D _ op _ -> op
elt : (D : Double) -> carrier D = split D _ _ e -> e
DoubleN : Double = D nat doubleN n1024
bin1024 : binN = binNpos (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 pos1))))))))))
DoubleBinN : Double = D binN doubleBinN bin1024
-- iterate
iter (A : U) : nat -> (A -> A) -> A -> A = split
zero -> \(f:A->A) (z:A) -> z
suc n -> \(f:A->A) (z:A) -> f (iter A n f z)
-- Compute: 2^n * x
doubles (D : Double) (n : nat) (x : carrier D) : carrier D =
iter (carrier D) n (double D) x
-- 2^20 * e = 2^5 * (2^15 * e)
propDouble (D : Double) : U
= Path (carrier D) (doubles D n20 (elt D))
(doubles D n5 (doubles D n15 (elt D)))
-- The property we want to prove that takes long to typecheck:
-- 2^10 * 1024 = 2^5 * (2^5 * 1024)
-- propN : propDouble DoubleN = refl nat (doublesN n20 n1024)
-- With binary numbers it is instant
propBin : propDouble DoubleBinN = <_> doublesBinN n20 (elt DoubleBinN)
-- Define intermediate structure:
doubleBinN' (b:binN) : binN = NtoBinN (doubleN (BinNtoN b))
DoubleBinN' : Double = D binN doubleBinN' (NtoBinN n1024)
eqDouble1 : Path Double DoubleN DoubleBinN'
= elimIsIso nat (\(B : U) (f : nat -> B) (g : B -> nat) -> Path Double DoubleN (D B (\(b : B) -> f (doubleN (g b))) (f n1024)))
(<_> DoubleN) binN NtoBinN BinNtoN BinNtoNK NtoBinNK
eqDouble2 : Path Double DoubleBinN' DoubleBinN
= mapOnPath (binN -> binN) Double F doubleBinN' doubleBinN rem
where
F (d:binN -> binN) : Double = D binN d (NtoBinN n1024)
rem : Path (binN -> binN) doubleBinN' doubleBinN
= <i> \(x : binN) -> rem1 x @ i
where
rem1 : (n : binN) -> Path binN (doubleBinN' n) (doubleBinN n)
= split
binN0 -> <_> binN0
binNpos p -> lem1 (x0 p)
eqDouble : Path Double DoubleN DoubleBinN =
compPath Double DoubleN DoubleBinN' DoubleBinN eqDouble1 eqDouble2
opaque doubleN
propDoubleImpl : propDouble DoubleBinN -> propDouble DoubleN =
substInv Double propDouble DoubleN DoubleBinN eqDouble
goal : propDouble DoubleN = propDoubleImpl propBin
transparent_all