CoderScript.sml

1(*===========================================================================*)
2(* Pairs of encoder/decoders.                                                *)
3(*===========================================================================*)
4
5(* Interactive mode
6app load
7["bossLib", "rich_listTheory", "EncodeTheory", "DecodeTheory", "normalForms",
8 "metisLib"];
9*)
10Theory Coder
11Ancestors
12  pair arithmetic list rich_list Encode Decode option combin
13Libs
14  pairTools metisLib normalForms
15
16
17val Suff = Q_TAC SUFF_TAC;
18val Know = Q_TAC KNOW_TAC;
19
20val REVERSE = Tactical.REVERSE;
21
22val TOP_CASE_TAC = BasicProvers.TOP_CASE_TAC;
23
24(*---------------------------------------------------------------------------
25     decode turns a decoding parser of type
26
27       bool list -> ('a # bool list) option
28
29     into a straight function of type
30
31       bool list -> 'a
32 ---------------------------------------------------------------------------*)
33
34Definition decode_def:
35   decode (p : 'a -> bool) (d : bool list -> ('a # bool list) option) l =
36   case d l of SOME (x, _) => x | NONE => @x. p x
37End
38
39(*---------------------------------------------------------------------------
40     Well-formed (predicate,encoder,decoder) triples.
41 ---------------------------------------------------------------------------*)
42
43Definition wf_coder_def:
44   wf_coder (p, e, d) <=> wf_pred p /\ wf_encoder p e /\ (d = enc2dec p e)
45End
46
47Definition domain_def:
48   domain
49   (p : 'a->bool, e : 'a->bool list, d : bool list->('a#bool list) option) = p
50End
51
52Definition encoder_def:
53   encoder
54   (p : 'a->bool, e : 'a->bool list, d : bool list->('a#bool list) option) = e
55End
56
57Definition decoder_def:
58   decoder
59   (p : 'a->bool, e : 'a->bool list, d : bool list->('a#bool list) option) =
60   decode p d
61End
62
63(*---------------------------------------------------------------------------
64     Well-formed coders have nice properties for boolification.
65 ---------------------------------------------------------------------------*)
66
67Theorem decode_encode:
68     !p e x. wf_encoder p e /\ p x ==> (decode p (enc2dec p e) (e x) = x)
69Proof
70   RW_TAC std_ss [] >>
71   Cases_on `enc2dec p e (e x)` >-
72   (POP_ASSUM MP_TAC >>
73    RW_TAC std_ss [enc2dec_none] >>
74    PROVE_TAC [APPEND_NIL]) >>
75   POP_ASSUM MP_TAC >>
76   Cases_on `x'` >>
77   SIMP_TAC std_ss [decode_def] >>
78   RW_TAC std_ss [enc2dec_some] >>
79   MP_TAC (Q.SPECL [`p`, `e`] wf_encoder_def) >>
80   RW_TAC std_ss [] >>
81   Suff `IS_PREFIX (e x) (e q)` >- PROVE_TAC [] >>
82   PROVE_TAC [IS_PREFIX_APPEND]
83QED
84
85Theorem wf_coder:
86     !c.
87       wf_coder c ==>
88       !x. domain c x ==> (decoder c (encoder c x) = x)
89Proof
90   Cases
91   >> Cases_on `r`
92   >> RW_TAC std_ss
93      [wf_coder_def, decode_encode, encoder_def, decoder_def, domain_def]
94QED
95
96Theorem wf_coder_closed:
97     !c. wf_coder c ==> !l. domain c (decoder c l)
98Proof
99   Cases
100   >> Cases_on `r`
101   >> RW_TAC std_ss
102      [wf_coder_def, domain_def, decoder_def, decode_def, wf_pred_def]
103   >> REPEAT TOP_CASE_TAC >- (HO_MATCH_MP_TAC SELECT_AX >> PROVE_TAC [])
104   >> POP_ASSUM MP_TAC
105   >> RW_TAC std_ss [enc2dec_some]
106QED
107
108Theorem wf_coder_op:
109     !p e f.
110       (?x. p x) /\ wf_encoder p e /\ (!x. p x ==> (e x = f x)) ==>
111       wf_coder (p, e, enc2dec p f)
112Proof
113   RW_TAC std_ss [wf_coder_def, wf_pred_def]
114   >> Q.UNDISCH_TAC `p x`
115   >> DISCH_THEN (K ALL_TAC)
116   >> MATCH_MP_TAC EQ_EXT
117   >> RW_TAC std_ss []
118   >> Know `wf_encoder p f` >- METIS_TAC [wf_encoder_eq]
119   >> STRIP_TAC
120   >> (Cases_on `enc2dec p e x`
121       >> Cases_on `enc2dec p f x`
122       >> POP_ASSUM MP_TAC
123       >> POP_ASSUM MP_TAC
124       >> RW_TAC std_ss [enc2dec_none, enc2dec_some_alt]) >|
125   [PROVE_TAC [],
126    PROVE_TAC [],
127    Cases_on `x'`
128    >> Cases_on `x''`
129    >> FULL_SIMP_TAC std_ss []
130    >> Suff `q = q'` >- PROVE_TAC [APPEND_11]
131    >> PROVE_TAC [wf_encoder_alt, biprefix_append, biprefix_refl]]
132QED
133
134(*---------------------------------------------------------------------------
135     Units
136 ---------------------------------------------------------------------------*)
137
138Definition unit_coder_def:   unit_coder p = (p, encode_unit, decode_unit p)
139End
140
141Theorem wf_coder_unit:
142     !p. wf_pred p ==> wf_coder (unit_coder p)
143Proof
144   RW_TAC std_ss
145   [unit_coder_def, wf_encode_unit, wf_coder_def, decode_unit_def]
146QED
147
148(*---------------------------------------------------------------------------
149     Booleans
150 ---------------------------------------------------------------------------*)
151
152Definition bool_coder_def:   bool_coder p = (p, encode_bool, decode_bool p)
153End
154
155Theorem wf_coder_bool:
156     !p. wf_pred p ==> wf_coder (bool_coder p)
157Proof
158   RW_TAC std_ss
159   [bool_coder_def, wf_encode_bool, decode_bool_def, wf_coder_def]
160QED
161
162(*---------------------------------------------------------------------------
163     Pairs
164 ---------------------------------------------------------------------------*)
165
166Definition prod_coder_def:
167   prod_coder (p1, e1, d1) (p2, e2, d2) =
168   (lift_prod p1 p2, encode_prod e1 e2, decode_prod (lift_prod p1 p2) d1 d2)
169End
170
171Theorem wf_coder_prod:
172     !c1 c2. wf_coder c1 /\ wf_coder c2 ==> wf_coder (prod_coder c1 c2)
173Proof
174   REPEAT GEN_TAC
175   >> Know `?p1 e1 d1. c1 = (p1, e1, d1)` >- PROVE_TAC [pairTheory.ABS_PAIR_THM]
176   >> Know `?p2 e2 d2. c2 = (p2, e2, d2)` >- PROVE_TAC [pairTheory.ABS_PAIR_THM]
177   >> RW_TAC std_ss []
178   >> RW_TAC std_ss [decode_prod_def, prod_coder_def]
179   >> MATCH_MP_TAC wf_coder_op
180   >> FULL_SIMP_TAC std_ss [wf_coder_def, wf_encode_prod, wf_pred_def]
181   >> CONJ_TAC >- (Q.EXISTS_TAC `(x, x')` >> RW_TAC std_ss [lift_prod_def])
182   >> Cases
183   >> RW_TAC std_ss [encode_prod_def, lift_prod_def, dec2enc_enc2dec]
184QED
185
186(*---------------------------------------------------------------------------
187     Sums
188 ---------------------------------------------------------------------------*)
189
190Definition sum_coder_def:
191   sum_coder (p1, e1, d1) (p2, e2, d2) =
192   (lift_sum p1 p2, encode_sum e1 e2, decode_sum (lift_sum p1 p2) d1 d2)
193End
194
195Theorem wf_coder_sum:
196     !c1 c2. wf_coder c1 /\ wf_coder c2 ==> wf_coder (sum_coder c1 c2)
197Proof
198   REPEAT GEN_TAC
199   >> Know `?p1 e1 d1. c1 = (p1, e1, d1)` >- PROVE_TAC [pairTheory.ABS_PAIR_THM]
200   >> Know `?p2 e2 d2. c2 = (p2, e2, d2)` >- PROVE_TAC [pairTheory.ABS_PAIR_THM]
201   >> RW_TAC std_ss []
202   >> RW_TAC std_ss [decode_sum_def, sum_coder_def]
203   >> MATCH_MP_TAC wf_coder_op
204   >> FULL_SIMP_TAC std_ss [wf_coder_def, wf_encode_sum, wf_pred_def]
205   >> CONJ_TAC >- (Q.EXISTS_TAC `INL x` >> RW_TAC std_ss [lift_sum_def])
206   >> Cases
207   >> RW_TAC std_ss [encode_sum_def, lift_sum_def, dec2enc_enc2dec]
208QED
209
210(*---------------------------------------------------------------------------
211     Options
212 ---------------------------------------------------------------------------*)
213
214Definition option_coder_def:
215   option_coder (p, e, d) =
216   (lift_option p, encode_option e, decode_option (lift_option p) d)
217End
218
219Theorem wf_coder_option:
220     !c. wf_coder c ==> wf_coder (option_coder c)
221Proof
222   REPEAT GEN_TAC
223   >> Know `?p e d. c = (p, e, d)` >- PROVE_TAC [pairTheory.ABS_PAIR_THM]
224   >> RW_TAC std_ss []
225   >> RW_TAC std_ss [decode_option_def, option_coder_def]
226   >> MATCH_MP_TAC wf_coder_op
227   >> FULL_SIMP_TAC std_ss [wf_coder_def, wf_encode_option, wf_pred_def]
228   >> CONJ_TAC >- (Q.EXISTS_TAC `NONE` >> RW_TAC std_ss [lift_option_def])
229   >> Induct
230   >> RW_TAC std_ss [encode_option_def, lift_option_def, dec2enc_enc2dec]
231QED
232
233(*---------------------------------------------------------------------------
234     Lists
235 ---------------------------------------------------------------------------*)
236
237Definition list_coder_def:
238   list_coder (p, e, d) =
239   (EVERY p, encode_list e, decode_list (EVERY p) d)
240End
241
242Theorem wf_coder_list:
243     !c. wf_coder c ==> wf_coder (list_coder c)
244Proof
245   REPEAT GEN_TAC
246   >> Know `?p e d. c = (p, e, d)` >- PROVE_TAC [pairTheory.ABS_PAIR_THM]
247   >> RW_TAC std_ss []
248   >> RW_TAC std_ss [decode_list_def, list_coder_def]
249   >> MATCH_MP_TAC wf_coder_op
250   >> FULL_SIMP_TAC std_ss [wf_coder_def, wf_encode_list, wf_pred_def]
251   >> CONJ_TAC >- (Q.EXISTS_TAC `[]` >> RW_TAC std_ss [EVERY_DEF])
252   >> Induct
253   >> RW_TAC std_ss [encode_list_def, EVERY_DEF, dec2enc_enc2dec]
254QED
255
256(*---------------------------------------------------------------------------
257     Bounded lists
258 ---------------------------------------------------------------------------*)
259
260Definition blist_coder_def:
261   blist_coder m (p, e, d) =
262   (lift_blist m p, encode_blist m e, decode_blist (lift_blist m p) m d)
263End
264
265Theorem wf_coder_blist:
266     !m c. wf_coder c ==> wf_coder (blist_coder m c)
267Proof
268   REPEAT GEN_TAC
269   >> Know `?p e d. c = (p, e, d)` >- PROVE_TAC [pairTheory.ABS_PAIR_THM]
270   >> RW_TAC std_ss []
271   >> RW_TAC std_ss [decode_blist_def, blist_coder_def]
272   >> MATCH_MP_TAC wf_coder_op
273   >> FULL_SIMP_TAC std_ss [wf_coder_def, wf_encode_blist, wf_pred_def]
274   >> Induct_on `m`
275   >- (REVERSE CONJ_TAC
276       >- RW_TAC std_ss [encode_blist_def]
277       >> Q.EXISTS_TAC `[]`
278       >> RW_TAC std_ss [lift_blist_def, LENGTH, EVERY_DEF])
279   >> POP_ASSUM STRIP_ASSUME_TAC
280   >> CONJ_TAC
281   >- (Q.EXISTS_TAC `x :: x'` >> RW_TAC std_ss [lift_blist_suc])
282   >> Cases >- RW_TAC std_ss [lift_blist_def, LENGTH]
283   >> RW_TAC std_ss
284      [lift_blist_suc, encode_blist_def, dec2enc_enc2dec, HD, TL]
285QED
286
287(*---------------------------------------------------------------------------
288     Nums (Norrish numerals)
289 ---------------------------------------------------------------------------*)
290
291Definition num_coder_def:   num_coder p = (p, encode_num, decode_num p)
292End
293
294Theorem wf_coder_num:
295     !p. wf_pred p ==> wf_coder (num_coder p)
296Proof
297   RW_TAC std_ss [num_coder_def, wf_encode_num, decode_num_def, wf_coder_def]
298QED
299
300(*---------------------------------------------------------------------------
301     Bounded numbers
302 ---------------------------------------------------------------------------*)
303
304Definition bnum_coder_def:
305   bnum_coder m p = (p, encode_bnum m, decode_bnum m p)
306End
307
308Theorem wf_coder_bnum:
309     !m p. wf_pred_bnum m p ==> wf_coder (bnum_coder m p)
310Proof
311   RW_TAC std_ss [bnum_coder_def, wf_encode_bnum, decode_bnum_def, wf_coder_def]
312   >> FULL_SIMP_TAC std_ss [wf_pred_bnum_def]
313   >> PROVE_TAC []
314QED
315
316(*---------------------------------------------------------------------------
317     Trees
318 ---------------------------------------------------------------------------*)
319
320Definition tree_coder_def:
321   tree_coder (p, e, d) =
322   (lift_tree p, encode_tree e, decode_tree (lift_tree p) d)
323End
324
325Theorem wf_coder_tree:
326     !c. wf_coder c ==> wf_coder (tree_coder c)
327Proof
328   REPEAT GEN_TAC
329   >> Know `?p e d. c = (p, e, d)` >- PROVE_TAC [pairTheory.ABS_PAIR_THM]
330   >> RW_TAC std_ss []
331   >> RW_TAC std_ss [decode_tree_def, tree_coder_def]
332   >> MATCH_MP_TAC wf_coder_op
333   >> FULL_SIMP_TAC std_ss [wf_coder_def, wf_encode_tree, wf_pred_def]
334   >> CONJ_TAC
335   >- (Q.EXISTS_TAC `Node x []` >> RW_TAC std_ss [lift_tree_def, EVERY_DEF])
336   >> HO_MATCH_MP_TAC tree_ind
337   >> RW_TAC std_ss [encode_tree_def,lift_tree_def,dec2enc_enc2dec,APPEND_11]
338   >> Induct_on `ts`
339   >> RW_TAC std_ss [encode_list_def, EVERY_DEF, dec2enc_enc2dec, MEM]
340QED
341