companionScript.sml
1(*
2 This development is based on Damien Pous' "Coinduction All the Way Up,
3 including the derivation of parameterized coinduction
4*)
5Theory companion
6Ancestors
7 pred_set fixedPoint poset
8
9Theorem lub_is_gfp:
10 poset (s,r) /\ function s s f /\ monotonic (s,r) f /\
11 lub (s,r) { x | r x (f x) } l
12 ==> gfp (s,r) f l
13Proof
14 rw[lub_def, gfp_def, monotonic_def, function_def] >>
15 subgoal ‘r l (f l)’ >-
16 (first_x_assum irule >> rw[] >>
17 drule_then irule poset_trans >>
18 first_assum $ irule_at Any >> rw[]) >>
19 drule_then irule poset_antisym >> rw[]
20QED
21
22(* core *)
23
24Definition lift_rel:
25 lift_rel (s,r) f g = !x. s x ==> r (f x) (g x)
26End
27
28(* f (b x) steps to f x *)
29Definition compatible_def:
30 compatible (s,r) b f = (function s s f /\ monotonic (s,r) f /\
31 lift_rel (s,r) (f o b) (b o f))
32End
33
34Theorem compatible_self:
35 poset (s,r) /\ function s s b /\ monotonic (s,r) b
36 ==> compatible (s,r) b b
37Proof
38 rw[poset_def, compatible_def, function_def, lift_rel]
39QED
40
41Theorem compatible_id:
42 poset (s,r) /\ function s s b /\ monotonic (s,r) b
43 ==> compatible (s,r) b I
44Proof
45 rw[compatible_def, monotonic_def, poset_def, function_def, lift_rel]
46QED
47
48(* this technique is 'complete' for valid deductions *)
49Theorem compatible_const_gfp:
50 poset (s,r) /\ function s s b /\ monotonic (s,r) b /\
51 gfp (s,r) b fp
52 ==> compatible (s,r) b (K fp)
53Proof
54 rw[compatible_def, gfp_def, poset_def, monotonic_def,
55 function_def, lift_rel]
56QED
57
58(* λX. BIGUNION {f X | f | compatible b f} *)
59Definition companion_def:
60 companion (s,r) b t = (function s s t /\
61 !x. lub (s,r) { f x | f | compatible (s,r) b f } (t x))
62End
63
64Theorem compatible_below_companion:
65 poset (s,r) /\
66 compatible (s,r) b f /\ companion (s,r) b t
67 ==> lift_rel (s,r) f t
68Proof
69 rw[companion_def, lift_rel] >>
70 ‘function s s f’ by fs[compatible_def] >>
71 gvs[lub_def, PULL_EXISTS, function_def]
72QED
73
74(* f x <= f y <= t y is upper bound, compatible f must be mono *)
75Theorem companion_mono:
76 poset (s,r) /\ function s s b /\ monotonic (s,r) b /\
77 companion (s,r) b t ==> monotonic (s,r) t
78Proof
79 rw[companion_def, lub_def, PULL_EXISTS] >>
80 drule_all_then strip_assume_tac compatible_self >>
81 rw[monotonic_def] >>
82 first_assum $ qspec_then ‘x’ strip_assume_tac >>
83 pop_assum match_mp_tac >> rw[] >>
84 (* establish fx < ty *)
85 last_x_assum $ qspec_then ‘y’ strip_assume_tac >> pop_assum kall_tac >>
86 drule_then irule poset_trans >>
87 rw[function_def] >>
88 metis_tac[compatible_def, monotonic_def, function_def]
89QED
90
91Theorem compatible_companion:
92 poset (s,r) /\ function s s b /\ monotonic (s,r) b /\
93 companion (s,r) b t ==> compatible (s,r) b t
94Proof
95 rw[compatible_def]
96 >- (fs[companion_def])
97 >- (metis_tac[companion_mono]) >>
98 rw[lift_rel] >>
99 gvs[companion_def, lub_def, PULL_EXISTS] >>
100 first_assum $ qspec_then ‘b x’ strip_assume_tac >>
101 pop_assum irule >>
102 rw[function_in] >>
103 fs[compatible_def] >>
104 drule_then irule poset_trans >>
105 rw[function_in] >>
106 gvs[function_def, monotonic_def, lift_rel] >>
107 metis_tac[]
108QED
109
110Theorem compatible_compose:
111 poset (s,r) /\ function s s b /\ monotonic (s,r) b /\
112 compatible (s,r) b f /\ compatible (s,r) b g
113 ==> compatible (s,r) b (f o g)
114Proof
115 rw[compatible_def, lift_rel] >-
116 (fs[function_def]) >-
117 (fs[function_in, monotonic_def]) >>
118 ‘r (f (g (b x))) (f (b (g x)))’ by metis_tac[monotonic_def, function_in] >>
119 drule_then irule poset_trans >> rw[function_in] >>
120 metis_tac[function_in]
121QED
122
123Theorem companion_expansive:
124 poset (s,r) /\ function s s b /\ monotonic (s,r) b /\
125 companion (s,r) b t /\
126 s x ==> r x (t x)
127Proof
128 strip_tac >>
129 ‘lift_rel (s,r) I t’ suffices_by rw[lift_rel] >>
130 ho_match_mp_tac compatible_below_companion >>
131 rw[function_def, compatible_companion] >>
132 rw[GSYM combinTheory.I_EQ_IDABS, compatible_id]
133QED
134
135Theorem companion_idem:
136 poset (s,r) /\ function s s b /\ monotonic (s,r) b /\
137 companion (s,r) b t /\
138 s x ==> t (t x) = t x
139Proof
140 rw[] >>
141 ‘function s s t’ by fs[companion_def] >>
142 drule_then irule poset_antisym >>
143 rw[function_in] >-
144 (‘lift_rel (s,r) (t o t) t’ suffices_by rw[lift_rel] >>
145 ho_match_mp_tac compatible_below_companion >>
146 rw[function_def, GSYM combinTheory.o_DEF] >>
147 irule compatible_compose >>
148 rw[compatible_companion]) >-
149 (metis_tac[companion_def, function_def, companion_expansive])
150QED
151
152Theorem companion_bot_gfp:
153 poset (s,r) /\ monotonic (s,r) b /\ function s s b /\
154 bottom (s,r) bot /\ gfp (s,r) b gfix /\
155 companion (s,r) b t
156 ==> t bot = gfix
157Proof
158 rw[] >>
159 drule_then irule poset_antisym >> rw[]
160 >- (fs[companion_def, function_in, bottom_def])
161 >- (fs[gfp_def])
162 (* t0 <= tb0 <= bt0 *)
163 >- (match_mp_tac gfp_coinduct >>
164 ‘function s s t’ by fs[companion_def] >>
165 fs[function_in, bottom_def] >>
166 drule_then match_mp_tac poset_trans >>
167 qexists_tac ‘t (b bot)’ >>
168 rw[bottom_def, function_in]
169 >- (irule (iffLR monotonic_def) >> metis_tac[companion_mono, function_def]) >>
170 ‘compatible (s,r) b t’ suffices_by fs[compatible_def, lift_rel] >>
171 irule compatible_companion >> rw[])
172 >- (drule_all compatible_const_gfp >> strip_tac >>
173 fs[companion_def, lub_def] >>
174 first_x_assum $ qspec_then ‘bot’ strip_assume_tac >>
175 first_x_assum irule >>
176 fs[gfp_def] >>
177 qexists_tac ‘K gfix’ >> rw[function_def])
178QED
179
180(* any post fixpoint is below the greatest fixpoint *)
181Theorem companion_coinduct:
182 poset (s,r) /\ monotonic (s,r) b /\ function s s b /\
183 companion (s,r) b t /\
184 gfp (s,r) b gfix /\
185 s x /\ r x ((b o t) x) ==> r x gfix
186Proof
187 rw[] >>
188 ‘function s s t’ by fs[companion_def] >>
189 drule_then match_mp_tac poset_trans >>
190 qexists_tac ‘t x’ >> rw[function_in]
191 >- (fs[gfp_def])
192 >- (ho_match_mp_tac companion_expansive >> rw[]) >>
193 match_mp_tac gfp_coinduct >>
194 rw[function_in] >>
195 drule_all compatible_companion >> strip_tac >>
196 drule_then match_mp_tac poset_trans >>
197 qexists_tac ‘t (b (t x))’ >>
198 reverse (rw[function_in])
199 >- (fs[compatible_def, lift_rel] >>
200 metis_tac[companion_idem, function_def]) >>
201 metis_tac[monotonic_def, companion_mono, function_in]
202QED
203
204(* bt is a sound enhancement *)
205Theorem enhanced_gfp:
206 poset (s,r) /\ monotonic (s,r) b /\ function s s b /\
207 gfp (s,r) b gfix /\
208 companion (s,r) b t /\ gfp (s,r) (b o t) efix
209 ==> efix = gfix
210Proof
211 rw[] >>
212 ‘function s s t’ by fs[companion_def] >>
213 drule_then irule poset_antisym >> rw[]
214 >- (fs[gfp_def])
215 >- (fs[gfp_def])
216 >- (drule_then match_mp_tac companion_coinduct >>
217 qexistsl_tac [‘t’,‘b’] >>
218 fs[gfp_def, poset_def]) >>
219 irule gfp_coinduct >>
220 qexistsl_tac [‘(b o t)’, ‘s’] >>
221 fs[gfp_def] >>
222 metis_tac[monotonic_def, function_def, companion_expansive]
223QED
224
225(*
226 * parameterized formalization following the cawu paper with 2nd order lattice
227 *)
228
229Theorem param_coind_init:
230 poset (s,r) /\ monotonic (s,r) b /\ function s s b /\
231 bottom (s,r) bot /\ gfp (s,r) b gfix /\
232 companion (s,r) b t
233 ==> r x (t bot) ==> r x gfix
234Proof
235 metis_tac[companion_bot_gfp]
236QED
237
238Theorem param_coind_done:
239 poset (s,r) /\ monotonic (s,r) b /\ function s s b /\
240 companion (s,r) b t
241 ==> s x /\ s y /\ r y x ==> r y (t x)
242Proof
243 rw[] >>
244 ‘function s s t’ by fs[companion_def] >>
245 drule_then match_mp_tac poset_trans >>
246 qexists_tac ‘x’ >> rw[function_in] >>
247 metis_tac[companion_expansive]
248QED
249
250Theorem param_coind_upto_f:
251 poset (s,r) /\ monotonic (s,r) b /\ function s s b /\
252 companion (s,r) b t
253 ==> function s s f /\ (!x. r (f x) (t x))
254 ==> s x /\ s y /\ r y (f (t x))
255 ==> r y (t x)
256Proof
257 rw[] >>
258 drule_then match_mp_tac poset_trans >>
259 first_x_assum $ irule_at Any >>
260 ‘function s s t’ by fs[companion_def] >>
261 simp[function_in] >>
262 metis_tac[companion_idem]
263QED
264
265Definition endo_def:
266 endo (s,r) f = (monotonic (s,r) f /\ !x. if s x then s (f x) else f x = @y. ~(s y))
267End
268
269Definition endo_lift_def:
270 endo_lift (s,r) = (endo (s,r) , lift_rel (s,r))
271End
272
273Theorem endo_in:
274 endo (s,r) t /\ s x ==> s (t x)
275Proof
276 rw[endo_def] >> metis_tac[]
277QED
278
279(* this is one reason why we need choose instead of ARB (which can be in s) *)
280Theorem endo_comp:
281 endo (s,r) f /\ endo (s,r) g ==> endo (s,r) (f o g)
282Proof
283 rw[endo_def] >-
284 (metis_tac[monotonic_comp, function_def]) >>
285 rw[] >> metis_tac[]
286QED
287
288Theorem endo_poset:
289 poset (s,r) ==> poset (endo_lift (s,r))
290Proof
291 rw[poset_def, endo_lift_def, lift_rel, endo_def]
292 >- (qexists_tac ‘λx. if s x then x else @y. ~s y’ >> rw[monotonic_def])
293 >- (metis_tac[])
294 >- (rw[FUN_EQ_THM] >> metis_tac[])
295 >- (metis_tac[])
296QED
297
298Definition B_join_def:
299 B_join (s,r) b B =
300 (function (endo (s,r)) (endo (s,r)) B /\ monotonic (endo_lift (s,r)) B /\
301 !g x. lub (s,r) { f x | f | endo (s,r) f /\ lift_rel (s,r) (f o b) (b o g) }
302 (B g x))
303End
304
305Theorem compatible_B_functional_postfix:
306 poset (s,r) /\ endo (s,r) b /\
307 B_join (s,r) b B /\
308 endo (s,r) f ==>
309 (lift_rel (s,r) f (B f) <=> lift_rel (s,r) (f o b) (b o f))
310Proof
311 reverse (rw[B_join_def, EQ_IMP_THM]) >-
312 (fs[lub_def, lift_rel] >> metis_tac[endo_in]) >>
313 (* look pointwise since the predicate is pointwise *)
314 subgoal ‘lift_rel (s,r) (B f o b) (b o f)’ >-
315 (fs[lub_def] >> rw[lift_rel] >>
316 first_x_assum $ qspecl_then [‘f’, ‘b x’] strip_assume_tac >>
317 first_x_assum irule >> rw[SF SFY_ss, endo_in] >>
318 fs[lift_rel]) >>
319 fs[lift_rel] >> rw[endo_in] >>
320 drule_then irule poset_trans >> rw[SF SFY_ss, endo_in] >>
321 fs[endo_lift_def] >>
322 metis_tac[endo_in, monotonic_def, function_def]
323QED
324
325Theorem endo_function:
326 endo (s,r) f ==> function s s f
327Proof
328 metis_tac[endo_def, function_def]
329QED
330
331Theorem B_greatest_fixpoint_is_companion:
332 poset (s,r) /\ endo (s,r) b /\
333 endo (s,r) t /\ companion (s,r) b t /\
334 B_join (s,r) b B
335 ==> gfp (endo_lift (s,r)) B t
336Proof
337 rw[EQ_IMP_THM] >>
338 drule endo_poset >> rw[] >>
339 fs[endo_lift_def] >>
340 qabbrev_tac ‘t' = (λx. if s x then t x else @y. ~s y)’ >>
341 subgoal ‘lub (endo (s,r),lift_rel (s,r)) {f | lift_rel (s,r) f (B f)} t'’ >-
342 (‘endo (s,r) t'’
343 by fs[Abbr ‘t'’, endo_def, monotonic_def, companion_def, function_def] >>
344 ‘compatible (s,r) b t’ by
345 metis_tac[compatible_companion, function_def, endo_def] >>
346 fs[companion_def, lub_def] >> rw[] >-
347 (rw[lift_rel] >>
348 last_x_assum $ qspec_then ‘x’ strip_assume_tac >>
349 fs[Abbr ‘t'’] >>
350 first_x_assum irule >> rw[SF SFY_ss, endo_in] >>
351 qexists_tac ‘y’ >> rw[compatible_def] >-
352 (metis_tac[endo_in, function_def]) >-
353 (fs[endo_def]) >>
354 metis_tac[compatible_B_functional_postfix]) >>
355 pop_assum irule >> rw[] >>
356 ‘lift_rel (s,r) (t' o b) (b o t')’
357 suffices_by metis_tac[compatible_B_functional_postfix] >>
358 fs[compatible_def, lift_rel, Abbr ‘t'’] >>
359 rw[] >>
360 metis_tac[endo_in]) >>
361 subgoal ‘lift_rel (s,r) (t' o b) (b o t')’ >-
362 (drule_then irule (iffLR compatible_B_functional_postfix) >>
363 fs[lub_def] >>
364 qexists_tac ‘B’ >> rw[] >>
365 first_x_assum irule >>
366 reverse conj_tac >- (fs[B_join_def, function_def, endo_lift_def]) >>
367 rw[] >>
368 fs[B_join_def, endo_lift_def] >>
369 ‘lift_rel (s,r) y t'’ by metis_tac[] >>
370 drule_then irule poset_trans >>
371 fs[function_def] >>
372 qexists_tac ‘B y’ >> rw[] >>
373 ‘monotonic (endo (s,r),lift_rel (s,r)) B’ by fs[endo_def] >>
374 fs[monotonic_def]) >>
375 subgoal ‘compatible (s,r) b t’ >-
376 (drule_then irule compatible_companion >>
377 fs[endo_def, function_def] >> metis_tac[]) >>
378 drule_all compatible_B_functional_postfix >> rw[] >>
379 (* argument: gfp B = lub of postfix points = lub of compat functions *)
380 irule lub_is_gfp >> rw[] >-
381 (metis_tac[endo_def, function_def, B_join_def, endo_lift_def]) >-
382 (fs[B_join_def, endo_lift_def, endo_def]) >>
383 ‘t = t'’ suffices_by metis_tac[] >>
384 drule_then irule poset_antisym >>
385 fs[B_join_def, companion_def, lub_def] >>
386 rw[] >-
387 (last_x_assum $ drule_then irule >> fs[compatible_def]) >>
388 rw[lift_rel] >>
389 last_x_assum $ qspec_then ‘x’ strip_assume_tac >>
390 first_x_assum irule >>
391 rw[SF SFY_ss, endo_in] >>
392 qexists_tac ‘t'’ >>
393 fs[compatible_def, SF SFY_ss, endo_function, endo_def]
394QED
395
396Theorem t_below_Tf:
397 poset (s,r) /\ endo (s,r) b /\
398 endo (s,r) t /\ companion (s,r) b t /\
399 B_join (s,r) b B /\
400 bottom (endo_lift (s,r)) bot /\
401 companion (endo_lift (s,r)) B T' /\
402 endo (s,r) f
403 ==> lift_rel (s,r) t (T' f)
404Proof
405 rw[] >>
406 drule endo_poset >>
407 drule_all B_greatest_fixpoint_is_companion >> rw[] >>
408 fs[endo_lift_def] >>
409 subgoal ‘T' bot = t’ >-
410 (irule companion_bot_gfp >>
411 qexistsl_tac [‘B’, ‘lift_rel (s,r)’, ‘endo (s,r)’] >>
412 fs[SRULE [endo_lift_def] endo_poset, B_join_def, endo_lift_def]) >>
413 subgoal ‘monotonic (endo (s,r),lift_rel (s,r)) T'’ >-
414 (irule companion_mono >> fs[function_def] >>
415 qexists_tac ‘B’ >> fs[B_join_def, endo_lift_def, function_def]) >>
416 fs[monotonic_def] >>
417 metis_tac[bottom_def]
418QED
419
420Theorem lift_rel_comp:
421 poset (s,r) /\
422 function s s g /\ function s s f /\ function s s f' /\ function s s g' /\
423 monotonic (s,r) f /\ monotonic (s,r) f' /\
424 lift_rel (s,r) f f' /\ lift_rel (s,r) g g'
425 ==> lift_rel (s,r) (f o g) (f' o g')
426Proof
427 rw[lift_rel, function_def] >>
428 drule_then irule poset_trans >> rw[] >>
429 metis_tac[monotonic_def, poset_trans]
430QED
431
432Theorem Bf_compatible_f:
433 poset (s,r) /\ endo (s,r) b /\ endo (s,r) f /\
434 B_join (s,r) b B
435 ==> lift_rel (s,r) (B f o b) (b o f)
436Proof
437 rw[B_join_def, endo_lift_def, lift_rel, lub_def] >>
438 first_x_assum $ qspecl_then [‘f’, ‘b x’] strip_assume_tac >>
439 pop_assum irule >> pop_assum kall_tac >> rw[] >>
440 metis_tac[endo_in]
441QED
442
443Theorem doubling_compatible_B:
444 poset (s,r) /\ endo (s,r) b /\
445 B_join (s,r) b B
446 ==> compatible (endo_lift (s,r)) B (λf. f o f)
447Proof
448 rw[compatible_def, endo_lift_def] >-
449 (rw[function_def, endo_def] >-
450 (irule monotonic_comp >> metis_tac[function_def]) >- (metis_tac[])) >-
451 (fs[monotonic_def, B_join_def, endo_lift_def] >> rw[] >>
452 metis_tac[lift_rel_comp, endo_def, function_def]) >>
453 rw[lift_rel] >>
454 rename1 ‘r (B f (B f y)) _’ >>
455 drule_all Bf_compatible_f >> rw[] >>
456 fs[lift_rel, B_join_def, endo_lift_def, lub_def] >> rw[] >>
457 first_x_assum $ qspecl_then [‘f o f’, ‘y’] strip_assume_tac >>
458 first_x_assum irule >> pop_assum kall_tac >> rw[] >-
459 (metis_tac[function_def, endo_def]) >>
460 qexists_tac ‘B f o B f’ >> rw[] >-
461 (metis_tac[function_def, endo_comp]) >>
462 drule_then irule poset_trans >> rw[] >-
463 (metis_tac[endo_in, function_in]) >- (metis_tac[endo_in]) >>
464 qexists_tac ‘B f (b (f x))’ >> rw[] >- (metis_tac[endo_in, function_in]) >-
465 (‘monotonic (s,r) (B f)’ by metis_tac[function_def, endo_def] >>
466 fs[monotonic_def] >> metis_tac[endo_def, function_def]) >>
467 metis_tac[endo_def, function_def]
468QED
469
470Theorem Tf_idem:
471 poset (s,r) /\ endo (s,r) b /\
472 B_join (s,r) b B /\
473 endo (s,r) t /\ companion (s,r) b t /\
474 companion (endo_lift (s,r)) B T' /\
475 bottom (endo_lift (s,r)) bot /\
476 endo (s,r) f
477 ==> T' f o T' f = T' f
478Proof
479 rw[endo_lift_def] >>
480 drule endo_poset >> rw[] >>
481 irule poset_antisym >>
482 qexistsl_tac [‘lift_rel (s,r)’, ‘endo (s,r)’] >> rw[] >-
483 (metis_tac[companion_def, function_def, endo_comp, endo_def]) >-
484 (metis_tac[companion_def, function_def, endo_comp, endo_def]) >-
485 (fs[endo_lift_def])
486 >- (irule poset_trans >>
487 qexistsl_tac [‘endo (s,r)’, ‘T' (T' f)’] >>
488 fs[B_join_def, endo_lift_def, function_def] >>
489 rw[] >-
490 (metis_tac[endo_comp, companion_def, function_def]) >-
491 (metis_tac[companion_def, function_def]) >-
492 (metis_tac[companion_def, function_def]) >-
493 (‘lift_rel (endo (s,r),lift_rel (s,r)) ((λf. f o f) o T') (T' o T')’
494 suffices_by fs[lift_rel] >>
495 irule lift_rel_comp >> fs[] >>
496 ‘function (endo (s,r)) (endo (s,r)) T'’ by metis_tac[companion_def] >>
497 rw[] >-
498 (rw[monotonic_def] >>
499 irule lift_rel_comp >> metis_tac[endo_def, function_def]) >-
500 (irule companion_mono >> metis_tac[function_def]) >-
501 (rw[function_def, endo_comp]) >-
502 (irule compatible_below_companion >> rw[] >>
503 qexists_tac ‘B’ >> rw[GSYM endo_lift_def] >>
504 irule doubling_compatible_B >>
505 rw[B_join_def, endo_lift_def] >> metis_tac[function_def]) >-
506 (rw[lift_rel] >> metis_tac[poset_refl, endo_in, function_def])) >-
507 (‘T' (T' f) = T' f’
508 suffices_by metis_tac[poset_refl, companion_def, function_def] >>
509 irule companion_idem >>
510 qexistsl_tac [‘B’, ‘lift_rel (s,r)’, ‘endo (s,r)’] >>
511 metis_tac[function_def, endo_def])) >>
512 (* Tf o id <= Tf o t <= Tf o Tf *)
513 ‘lift_rel (s,r) (T' f o I) (T' f o T' f)’ suffices_by rw[] >>
514 irule lift_rel_comp >>
515 ‘function s s (T' f)’ by metis_tac[function_def, companion_def, endo_def] >>
516 ‘monotonic (s,r) (T' f)’ by metis_tac[function_def, companion_def, endo_def] >>
517 rw[] >-
518 (fs[function_def]) >-
519 (rw[lift_rel] >> metis_tac[poset_refl, companion_def, function_def, endo_def]) >-
520 (drule_all (SRULE [endo_lift_def] t_below_Tf) >>
521 rw[lift_rel] >>
522 drule_then irule poset_trans >> rw[] >-
523 (metis_tac[companion_def, function_def, endo_def]) >>
524 qexists_tac ‘t x’ >> rw[SF SFY_ss, endo_in] >>
525 drule_then irule companion_expansive >>
526 metis_tac[function_def, endo_def])
527QED
528
529(* only needs finite lubs aside from t, B and T, completeness is just convenient *)
530(* maybe somehow B_join and the higher companion forces the boundedness? *)
531(* *)
532Theorem param_coind:
533 complete (s,r) /\ complete (endo_lift (s,r)) /\
534 poset (s,r) /\ endo (s,r) b /\
535 companion (s,r) b t /\ endo (s,r) t /\
536 B_join (s,r) b B /\ companion (endo_lift (s,r)) B T' /\
537 gfp (s,r) b gfix /\
538 s x /\ s y /\
539 lub (s,r) { x; y } xy
540 ==> r y (b (t xy)) ==> r y (t x)
541Proof
542 rw[] >>
543 ‘monotonic (s,r) t’ by metis_tac[companion_mono, lub_def, endo_def] >>
544 ‘monotonic (s,r) b’ by metis_tac[function_def, endo_def] >>
545 ‘?bot. lub (s,r) {} bot’ by metis_tac[complete_def] >>
546 reverse (subgoal ‘lift_rel (s,r)
547 (λz. if s z then (if r x z then y else bot) else @y. ~s y)
548 t’) >-
549 (fs[lift_rel] >>
550 pop_assum $ qspec_then ‘x’ strip_assume_tac >>
551 Cases_on ‘r x x’ >> metis_tac[poset_refl]) >>
552 qmatch_goalsub_abbrev_tac ‘lift_rel _ f _’ >>
553 subgoal ‘endo (s,r) f’ >-
554 (rw[endo_def, Abbr ‘f’] >-
555 (rw[monotonic_def] >>
556 Cases_on ‘r x z’ >-
557 (metis_tac[poset_refl, poset_trans]) >>
558 fs[lub_def] >> metis_tac[]) >>
559 Cases_on ‘r x z’ >> fs[lub_def] >> metis_tac[]) >>
560 drule_all B_greatest_fixpoint_is_companion >>
561 rw[endo_lift_def] >>
562 irule companion_coinduct >>
563 qexistsl_tac [‘B’, ‘endo (s,r)’, ‘T'’] >> rw[] >-
564 (* begin indent *)
565 (metis_tac[endo_poset, endo_lift_def]) >-
566 (‘?fxl. lub (s,r) { f x ; x } fxl’ by metis_tac[complete_def] >>
567 subgoal ‘xy = fxl’ >-
568 (drule_then irule lub_unique >>
569 ‘y = f x’ by metis_tac[Abbr ‘f’, poset_refl] >> fs[] >>
570 ‘{x; f x} = {f x; x}’ by rw[SET_EQ_SUBSET, SUBSET_DEF] >>
571 fs[] >> metis_tac[]) >>
572 drule_then strip_assume_tac (iffLR B_join_def) >>
573 fs[endo_lift_def] >>
574 rw[lift_rel] >>
575 last_x_assum $ qspecl_then [‘T' f’, ‘x'’] strip_assume_tac >>
576 pop_assum mp_tac >>
577 rw[lub_def] >>
578 first_x_assum irule >> pop_assum kall_tac >>
579 conj_tac >- (fs[Abbr ‘f’] >> Cases_on ‘r x x'’ >> fs[lub_def]) >>
580 qexists_tac ‘f’ >> rw[] >> ntac 2 (pop_assum kall_tac) >>
581 rw[lift_rel] >>
582 reverse (Cases_on ‘r x (b x')’) >-
583 (reverse (rw[Abbr ‘f’, endo_in]) >- (metis_tac[endo_in]) >>
584 fs[lub_def] >>
585 ‘s (T' (λz. if s z then if r x z then y else bot else @y. ~s y) x')’
586 suffices_by metis_tac[endo_in] >>
587 fs[companion_def] >>
588 metis_tac[function_def, endo_in]) >>
589 subgoal ‘f (b x') = y’ >- (fs[Abbr ‘f’] >> metis_tac[endo_in]) >>
590 rfs[] >> pop_assum kall_tac >>
591 drule_then irule poset_trans >>
592 ‘s (b (T' f x'))’ by metis_tac[endo_in, companion_def, function_def] >>
593 rw[] >>
594 qexists_tac ‘b (t fxl)’ >> rw[endo_in] >- (metis_tac[lub_def, endo_in]) >>
595 drule_then irule poset_trans >> rw[] >- (metis_tac[lub_def, endo_in]) >>
596 ‘?fbxl. lub (s,r) { f (b x') ; b x' } fbxl’ by metis_tac[complete_def] >>
597 qexists_tac ‘b (t fbxl)’ >> rw[] >-
598 (* split *)
599 (metis_tac[endo_in, lub_def]) >-
600 (‘r (t fxl) (t fbxl)’ suffices_by metis_tac[monotonic_def, lub_def,
601 endo_def, endo_in] >>
602 ‘r fxl fbxl’ suffices_by metis_tac[companion_mono, monotonic_def, lub_def,
603 function_def, endo_def] >>
604 fs[lub_def] >>
605 last_x_assum irule >> rw[] >-
606 (‘r (b x') fbxl’ by metis_tac[endo_in] >>
607 drule_then irule poset_trans >>
608 pop_assum $ irule_at Any >>
609 metis_tac[endo_in]) >-
610 (‘y = f x’ by metis_tac[Abbr ‘f’, poset_refl] >> fs[] >>
611 ‘r (f (b x')) fbxl’ by metis_tac[endo_in] >>
612 ‘monotonic (s,r) f’ by fs[endo_def] >>
613 metis_tac[monotonic_def, poset_trans, endo_in])) >>
614 subgoal ‘?fbl. !X. lub (s,r) { f (b X) ; b X } (fbl X)’ >-
615 (rw[GSYM SKOLEM_THM] >> metis_tac[complete_def]) >>
616 ‘fbxl = fbl x'’ by metis_tac[lub_unique] >> fs[] >>
617 ‘r (t (fbl x')) (T' f x')’ suffices_by metis_tac[monotonic_def, lub_def,
618 endo_def, endo_in] >>
619 ‘lift_rel (s,r) (t o fbl) (T' f)’ suffices_by
620 metis_tac[combinTheory.o_DEF, lift_rel] >>
621 subgoal ‘bottom (endo_lift (s,r)) (λx. if s x then bot else @y. ~s y)’ >-
622 (rw[bottom_def, endo_lift_def] >-
623 (rw[endo_def, monotonic_def] >-
624 (metis_tac[poset_refl, lub_def]) >-
625 (metis_tac[lub_def])) >-
626 (rw[lift_rel, lub_def] >>
627 fs[lub_def] >> metis_tac[endo_def])) >>
628 subgoal ‘T' f o T' f = T' f’ >-
629 (drule_then irule Tf_idem >> rw[] >- (metis_tac[]) >>
630 qexistsl_tac [‘B’, ‘b’, ‘t’] >> rw[endo_lift_def]) >>
631 ‘lift_rel (s,r) (t o fbl) (T' f o T' f)’ suffices_by metis_tac[] >>
632 subgoal ‘lift_rel (s,r) t (T' f)’ >-
633 (drule_then irule t_below_Tf >> rw[] >- (metis_tac[]) >>
634 qexistsl_tac [‘B’, ‘b’] >> rw[endo_lift_def]) >>
635 irule lift_rel_comp >> rw[] >-
636 (metis_tac[endo_def, companion_def, function_def]) >-
637 (metis_tac[endo_def, function_def]) >-
638 (metis_tac[endo_def, companion_def, function_def]) >-
639 (metis_tac[function_def, lub_def]) >-
640 (metis_tac[endo_def, companion_def, function_def]) >-
641 (‘!X. s (fbl X) /\ (!y. s y /\ (y = f (b X) \/ y = b X) ==> r y (fbl X)) /\
642 !z. s z /\ (!y. s y /\ (y = f (b X) \/ y = b X) ==> r y z) ==>
643 r (fbl X) z’ by fs[lub_def] >>
644 rw[lift_rel] >>
645 ‘r (t x'') (T' f x'')’ by fs[lift_rel] >>
646 first_x_assum $ qspec_then ‘x''’ strip_assume_tac >>
647 first_x_assum irule >> pop_assum kall_tac >>
648 rw[] >-
649 (metis_tac[companion_def, function_def, endo_def]) >-
650 (‘lift_rel (s,r) (f o b) (T' f o T' f)’
651 suffices_by metis_tac[lift_rel, combinTheory.o_DEF] >>
652 irule lift_rel_comp >> rw[SF SFY_ss, endo_function] >-
653 (fs[endo_def]) >-
654 (metis_tac[companion_def, function_def, endo_def]) >-
655 (metis_tac[companion_def, function_def, endo_def]) >-
656 (metis_tac[companion_def, function_def, endo_def]) >-
657 (irule companion_expansive >>
658 qexistsl_tac [‘B’, ‘endo (s,r)’] >> rw[] >>
659 metis_tac[endo_poset, endo_lift_def]) >-
660 (rw[lift_rel] >>
661 drule_then irule poset_trans >>
662 rw[SF SFY_ss, endo_in, endo_function] >-
663 (metis_tac[companion_def, function_def, endo_def]) >>
664 rename1 ‘_ /\ r (b a) _ /\ _’ >>
665 qexists_tac ‘t a’ >> rw[SF SFY_ss, endo_in] >-
666 (‘lift_rel (s,r) b t’ suffices_by rw[lift_rel] >>
667 drule_then irule compatible_below_companion >>
668 metis_tac[compatible_self, function_def, endo_def, lift_rel]) >>
669 rfs[lift_rel])) >-
670 (drule_then irule poset_trans >> rw[] >-
671 (metis_tac[companion_def, function_def, endo_def]) >>
672 qexists_tac ‘t x''’ >> rw[] >- (metis_tac[companion_def, function_def]) >>
673 metis_tac[compatible_below_companion, compatible_self,
674 function_def, endo_def, lift_rel]))) >-
675 (fs[B_join_def, endo_def, endo_lift_def]) >-
676 (fs[endo_lift_def]) >-
677 (fs[B_join_def, endo_lift_def])
678QED
679
680(* set helpers *)
681
682Definition set_compatible_def:
683 set_compatible b f = (monotone f /\ !X. f (b X) SUBSET b (f X))
684End
685
686Theorem set_compatible:
687 set_compatible b f ==> compatible (UNIV,$SUBSET) b f
688Proof
689 rw[set_compatible_def, compatible_def, lift_rel, function_def]
690QED
691
692Theorem set_compatible_self:
693 monotone b ==> set_compatible b b
694Proof
695 rw[set_compatible_def, monotone_def]
696QED
697
698Theorem set_compatible_id:
699 monotone b ==> set_compatible b I
700Proof
701 rw[set_compatible_def, monotone_def]
702QED
703
704Theorem set_compatible_compose:
705 monotone b ==>
706 set_compatible b f /\ set_compatible b g
707 ==> set_compatible b (f o g)
708Proof
709 rw[monotone_def, set_compatible_def] >>
710 metis_tac[SUBSET_DEF]
711QED
712
713Definition set_companion_def:
714 set_companion b X = BIGUNION { f X | f | set_compatible b f }
715End
716
717Theorem set_companion:
718 companion (UNIV,$SUBSET) b (set_companion b)
719Proof
720 rw[companion_def, set_companion_def, function_def] >>
721 rw[lub_def, compatible_def, set_compatible_def, lift_rel, function_def] >>
722 fs[SUBSET_DEF, BIGUNION, IN_DEF] >>
723 metis_tac[]
724QED
725
726Theorem set_companion_compatible:
727 monotone b ==> set_compatible b (set_companion b)
728Proof
729 rw[] >>
730 subgoal ‘compatible (UNIV,$SUBSET) b (set_companion b)’ >-
731 (irule compatible_companion >>
732 rw[set_companion, function_def]) >>
733 fs[compatible_def, lift_rel, set_compatible_def]
734QED
735
736Theorem set_companion_coinduct:
737 monotone b /\
738 X SUBSET (b o set_companion b) X
739 ==> X SUBSET gfp b
740Proof
741 rw[] >>
742 irule companion_coinduct >>
743 qexistsl_tac [‘b’, ‘UNIV’, ‘set_companion b’] >>
744 rw[function_def, gfp_poset_gfp, set_companion]
745QED
746
747Theorem set_compatible_enhance:
748 monotone b /\ set_compatible b f /\
749 Y SUBSET f X
750 ==> Y SUBSET set_companion b X
751Proof
752 rw[] >>
753 drule_then irule SUBSET_TRANS >>
754 irule (SRULE [lift_rel] compatible_below_companion) >>
755 qexistsl_tac [‘b’, ‘UNIV’] >>
756 rw[set_compatible, set_companion]
757QED
758
759Theorem set_gfp_sub_companion:
760 monotone b ==> gfp b SUBSET set_companion b x
761Proof
762 rw[] >>
763 irule set_compatible_enhance >> rw[] >>
764 qexists_tac ‘K (gfp b)’ >> rw[] >>
765 rw[set_compatible_def, monotone_def, gfp_greatest_fixedpoint]
766QED
767
768(* to prove X is in a coinductive set from b, consider t0 *)
769Theorem set_param_coind_init:
770 monotone b /\
771 X SUBSET set_companion b {}
772 ==> X SUBSET gfp b
773Proof
774 rw[] >>
775 drule_at_then Any irule param_coind_init >>
776 qexistsl_tac [‘b’, ‘UNIV’] >>
777 rw[bottom_def, set_companion, function_def, gfp_poset_gfp]
778QED
779
780(* pull f out of tX *)
781Theorem set_param_coind_upto_f:
782 monotone b /\
783 (!X. f X SUBSET set_companion b X) /\
784 Y SUBSET f (set_companion b X)
785 ==> Y SUBSET set_companion b X
786Proof
787 rw[] >>
788 drule_at_then Any irule param_coind_upto_f >> rw[] >>
789 qexistsl_tac [‘b’, ‘UNIV’] >>
790 rw[set_companion, function_def]
791QED
792
793(* conclude: X is a safe deduction from Y *)
794Theorem set_param_coind_done:
795 monotone b /\
796 Y SUBSET X ==> Y SUBSET set_companion b X
797Proof
798 rw[] >>
799 irule param_coind_done >> rw[] >>
800 qexistsl_tac [‘b’, ‘UNIV’] >>
801 rw[set_companion, function_def]
802QED
803
804Definition set_B_def:
805 set_B b = λg X. BIGUNION { f X | f | monotone f /\ !Y. f (b Y) SUBSET b (g Y) }
806End
807
808Definition higher_monotone:
809 higher_monotone fn = !f g. monotone f /\ monotone g /\
810 (!X. f X SUBSET g X) ==> (!X. (fn f) X SUBSET (fn g) X)
811End
812
813Definition higher_compat_def:
814 higher_compat fn b =
815 ((!f. monotone f ==> monotone (fn f)) /\ higher_monotone fn /\
816 !f X. monotone f ==> (fn (set_B b f)) X SUBSET (set_B b (fn f)) X)
817End
818
819Definition set_T_def:
820 set_T b = λf X. BIGUNION { (fn f) X | fn | monotone (fn f) /\ higher_compat fn b }
821End
822
823Theorem set_higher_complete:
824 complete (endo_lift (univ(:'a -> bool),$SUBSET))
825Proof
826 rw[complete_def, endo_lift_def] >-
827 (qexists_tac ‘λX. BIGUNION { f X | f | monotone f /\ c f }’ >>
828 rw[lub_def] >-
829 (rw[endo_def, monotone_def] >>
830 rw[BIGUNION_SUBSET] >>
831 rw[BIGUNION, Once SUBSET_DEF] >>
832 qexists_tac ‘f X'’ >> rw[] >> metis_tac[SUBSET_DEF]) >-
833 (fs[endo_def, lift_rel, BIGUNION, Once SUBSET_DEF] >> metis_tac[]) >>
834 fs[lift_rel, endo_def] >> rw[] >>
835 irule (iffRL BIGUNION_SUBSET) >> rw[] >> metis_tac[]) >>
836 (qexists_tac ‘λX. BIGINTER { f X | f | monotone f /\ c f }’ >>
837 rw[glb_def] >-
838 (rw[endo_def, monotone_def] >>
839 rw[SUBSET_BIGINTER] >>
840 rw[BIGINTER, Once SUBSET_DEF] >>
841 metis_tac[SUBSET_DEF]) >-
842 (fs[endo_def, lift_rel, BIGINTER, Once SUBSET_DEF] >> metis_tac[]) >>
843 fs[lift_rel, endo_def] >> rw[] >>
844 irule (iffRL SUBSET_BIGINTER) >> rw[] >> metis_tac[])
845QED
846
847(* do a deduction step, Y must step to itself or reach X
848 * proof: functionals on sets form a complete lattice under pointwise inclusion
849 * B is monotone with that ordering, and it can be defined via lub = BIGUNION
850 * hence B has a greatest fixpoint and we can instantiate *)
851Theorem set_param_coind:
852 monotone b
853 ==> Y SUBSET b (set_companion b (X UNION Y))
854 ==> Y SUBSET set_companion b X
855Proof
856 rw[] >>
857 drule_at_then Any irule param_coind >>
858 qexistsl_tac [‘set_B b’, ‘set_T b’, ‘gfp b’, ‘UNIV’] >>
859 rw[endo_def, set_companion, gfp_poset_gfp, set_higher_complete] >-
860 (metis_tac[set_companion_compatible, set_compatible_def]) >-
861 (rw[B_join_def, set_B_def, endo_lift_def, endo_def, function_def] >-
862 (rw[monotone_def, lift_rel] >>
863 rw[BIGUNION_SUBSET] >>
864 rw[BIGUNION, Once SUBSET_DEF] >>
865 qexists_tac ‘f X''’ >> rw[] >>
866 metis_tac[SUBSET_DEF, SUBSET_TRANS]) >-
867 (rw[monotonic_def, lift_rel] >>
868 rw[BIGUNION_SUBSET] >>
869 rw[BIGUNION, Once SUBSET_DEF] >>
870 qexists_tac ‘f X'’ >> rw[] >>
871 metis_tac[SUBSET_TRANS, monotone_def]) >-
872 (rw[lub_def, lift_rel] >-
873 (rw[BIGUNION, Once SUBSET_DEF] >> metis_tac[]) >>
874 rw[BIGUNION_SUBSET])) >-
875 (rw[companion_def, endo_lift_def, set_B_def, set_T_def] >-
876 (rw[function_def, endo_def, monotone_def] >>
877 rw[BIGUNION_SUBSET] >>
878 rw[BIGUNION, Once SUBSET_DEF] >>
879 metis_tac[SUBSET_DEF]) >>
880 rw[lub_def, endo_def, lift_rel]
881 >- (rw[monotone_def, BIGUNION_SUBSET] >>
882 rw[BIGUNION, Once SUBSET_DEF] >>
883 metis_tac[SUBSET_DEF])
884 >- (rw[BIGUNION, Once SUBSET_DEF] >>
885 pop_assum $ irule_at Any >>
886 rename [‘x f YY = _ ∧ monotone _ ∧ higher_compat _ _’] >>
887 qexists_tac ‘x’ >> rw[] >>
888 rw[higher_compat_def, higher_monotone] >-
889 (fs[compatible_def, function_def, endo_def, monotonic_def, lift_rel]) >>
890 fs[GSYM set_B_def] >>
891 fs[compatible_def, lift_rel, endo_def, monotonic_def])
892 >- (rw[BIGUNION_SUBSET] >>
893 first_x_assum irule >> rw[] >>
894 qexists_tac ‘fn’ >> rw[compatible_def] >-
895 (rw[function_def, endo_def] >>
896 fs[higher_compat_def, higher_monotone]) >-
897 (fs[higher_compat_def, higher_monotone] >>
898 rw[monotonic_def, lift_rel, endo_def]) >-
899 (rw[GSYM set_B_def] >>
900 rw[lift_rel] >>
901 fs[higher_compat_def, endo_def]))) >-
902 (rw[lub_def] >> rw[SUBSET_UNION])
903QED
904