Project

General

Profile

Statistics
| Branch: | Revision:

corque / lemma_9.v @ 4806fe22

History | View | Annotate | Download (53.8 KB)

1
Add LoadPath "~/Schreibtisch/svnba/Elgot/Coq/".
2
Require Import biCCC.
3
Require Import Lemmas_biCCC.
4
Require Import ElgotMonad.
5
Require Import Lemmas_ElgotMonad.
6
Require Import CofreeElgotMonad.
7
Require Import Lemmas_CofreeElgotMonad.
8
Require Import Coq_Steroids.
9
Require Import Setoid.
10
Open Scope c_scope.
11

    
12
Section ContextCofreeElgotMonad.
13
Context `(Co: CofreeElgotMonad).
14

    
15
Parameter a b : Obj.
16

    
17
(* --- *)
18

    
19

    
20
Theorem proving_kl1 : forall
21
(x : Obj), 
22
  (ηv (x:=x) (a:=a) (b:=b)) § = id.
23

    
24
Proof.
25
intros.
26
symmetry; apply lifting2; rewrite -> id_l.
27
rewrite -> out_unitcofree.
28
rewrite -> cont_id, -> id_l.
29
rewrite <- f_cpr, -> inl_inr_is_id, id_l.
30
rewrite -> kl1, id_r; trivial.
31
Qed.
32

    
33

    
34

    
35
Theorem proving_kl2 : forall
36
(x y : Obj)
37
(f: x ~> coext T a b y), 
38
  f § ∘ ηv (x:=x) = f.
39

    
40
Proof.
41
intros.
42
apply out_cong.
43
rewrite -> comp_assoc, lifting1.
44
rewrite <- comp_assoc, -> out_unitcofree.
45
rewrite -> comp_assoc, kl2.
46
rewrite -> cpr_inl; trivial.
47
Qed.
48

    
49

    
50

    
51
Theorem proving_kl3 : forall
52
(x y z : Obj)
53
(f : y ~> coext T a b z)
54
(g : x ~> coext T a b y),
55
  (f § ∘ g) § = f § ∘ g §.
56

    
57
Proof.
58
intros.
59
symmetry; apply lifting2.
60
rewrite -> comp_assoc, lifting1.
61
rewrite <- comp_assoc, -> lifting1.
62

    
63
rewrite -> comp_assoc with (f':=out); apply f_equal2; trivial.
64
rewrite <- kl3; apply f_equal1.
65

    
66
rewrite -> f_cpr.
67
rewrite <- comp_assoc with (f':=cont (g §)), -> comp_assoc with (g':=η), -> kl2.
68
rewrite -> comp_assoc with (g':=inr), cpr_inr.
69
rewrite <- comp_assoc with (f':=cont (g §)), -> cont_comp.
70

    
71
rewrite -> comp_assoc with (h':=out), -> lifting1.
72
rewrite -> comp_assoc with (f':=g); trivial.
73
Qed.
74

    
75

    
76

    
77
(* additional lemmas based on proving_kl1-3 *)
78
(* at the wrong place, change name? *)
79
Lemma mapc_unfold : forall
80
(x y : Obj)
81
(f:x ~> y),
82
  mapc f = (ηv (a:=a) (b:=b) ∘ f) §.
83

    
84
Proof.
85
intros.
86
unfold mapc.
87
symmetry; apply coit2.
88
rewrite -> comp_assoc, map_comp.
89
rewrite -> coprodhom_comp, id_r, id_l.
90
rewrite -> lifting1.
91
rewrite -> comp_assoc with (h':=out), out_unitcofree.
92

    
93
unfold map, coprodhom.
94
rewrite -> f_cpr, ->2 comp_assoc; trivial.
95
Qed.
96

    
97

    
98

    
99
Lemma liftingcofree_mapc : forall 
100
(x y z : Obj)
101
(f: y ~> coext T a b z)
102
(g: x ~> y),
103
  f § ∘ mapc g = (f ∘ g) §.
104

    
105
Proof.
106
intros.
107
rewrite -> mapc_unfold.
108
rewrite <- proving_kl3.
109
rewrite -> comp_assoc, proving_kl2.
110
trivial.
111
Qed.
112

    
113

    
114

    
115
Lemma mapc_liftingcofree : forall 
116
(x y z : Obj)
117
(f: y ~> z)
118
(g: x ~> coext T a b y),
119
  mapc f ∘ g § = (mapc f ∘ g) §.
120

    
121
Proof.
122
intros.
123
rewrite -> mapc_unfold.
124
rewrite <- proving_kl3.
125
trivial.
126
Qed.
127

    
128

    
129
(* --- *)
130

    
131

    
132

    
133
Theorem proving_unfolding : forall
134
(x y : Obj)
135
(f : x ~> (coext T a b (y ⊕ x))),
136
  [ηv , f †'] § ∘ f = f †'.
137

    
138
Proof.
139
intros.
140
symmetry; rewrite -> unfolding_triangle1 at 1.
141

    
142
unfold triangle.
143

    
144
rewrite <- comp_assoc with (h':=tuo), -> comp_assoc with (g':=tuo), -> liftingcofree_tuo.
145

    
146
rewrite -> comp_assoc with (g':=map (inl ⊕⊕ id)), <- comp_assoc with (h':=tuo), -> lifting_map.
147
rewrite -> cpr_coprodhom, cpr_inl, id_l.
148

    
149
rewrite <- unfolding.
150

    
151
rewrite <- comp_assoc with (h':=tuo), -> comp_assoc with (g':=(([η, ((π ∘ out) ∘ f) †]) *)).
152
rewrite <- kl3, -> f_cpr, -> kl2.
153
rewrite <- out_itercofree.
154

    
155
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (g':=π).
156
unfold π.
157
rewrite -> lifting_map.
158
rewrite -> f_cpr.
159
rewrite -> cpr_coprodhom, cpr_inl, id_l.
160
rewrite -> comp_assoc with (g':=inl), cpr_inl, cpr_inr.
161

    
162
rewrite ->2 comp_assoc, <- liftingcofree_tuo.
163
rewrite <- comp_assoc with (g':=tuo), -> tuo_out_is_id, id_l; trivial.
164

    
165
Qed.
166

    
167

    
168

    
169
(* --- *)
170

    
171

    
172

    
173
(* TODO: adjust name? *)
174
Lemma proving_naturality_h1 : forall (x y z : Obj)
175
(h: x ~> coext T a b (y ⊕ x))
176
(g: y ~> coext T a b z),
177
  guarded h ->  
178
    guarded ([mapc inl ∘ g, ηv ∘ inr] § ∘ h).
179

    
180
Proof.
181
intros.
182
unfold guarded in H; inversion H as [u' H1].
183

    
184
unfold guarded.
185

    
186
exists ([map (id ⊕⊕ id ×× mapc inl ^^ id) ∘ out ∘ g, η ∘ inr ∘ 
187
        cont (([mapc inl ∘ g, ηv ∘ inr]) §)] * ∘ u').
188

    
189
rewrite -> comp_assoc, lifting1.
190

    
191
rewrite <- comp_assoc, -> H1.
192

    
193
rewrite -> comp_assoc with (f':=u'), lifting_map.
194
rewrite -> cpr_coprodhom.
195
rewrite <- comp_assoc with (f':=inl), -> cpr_inl, id_l.
196
rewrite -> comp_assoc, out_mapc.
197

    
198
rewrite -> comp_assoc with (f':=u'); apply f_equal2; trivial.
199
rewrite -> map_lifting; apply f_equal1.
200

    
201
rewrite -> f_cpr.
202
rewrite ->2 comp_assoc, map_comp, coprodhom_comp, id_l, id_r.
203
rewrite <-2 comp_assoc with (h':=η), -> comp_assoc with (g':=η), map_unit.
204
rewrite <- comp_assoc with (h':=η), -> comp_assoc with (h':=inl ⊕⊕ id).
205
rewrite -> coprodhom_inr, id_l; trivial.
206

    
207
Qed.
208

    
209

    
210

    
211
(* TODO: change name, move ? *)
212
Theorem proving_naturality_h2 : forall (x y z : Obj)
213
(f : x ~> (coext T a b (y ⊕ x)))
214
(g : y ~> (coext T a b z)),
215
  ▷(([mapc inl ∘ g, ηv ∘ inr]) § ∘ f) = (([mapc inl ∘ g, ηv ∘ inr]) § ∘ ▷f).
216

    
217
Proof.
218
intros.
219

    
220
set (w:=[mapc inl ∘ g, ηv ∘ inr]).
221

    
222
rewrite <- guardedtriangle; trivial.
223

    
224
unfold triangle at 2 3.
225
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> lifting1.
226
rewrite <- comp_assoc with (g':=out), ->2 comp_assoc with (h':=out), -> out_tuo_is_id, -> id_r.
227
rewrite -> comp_assoc with (g':=map (inl ⊕⊕ id)), -> lifting_map, -> cpr_coprodhom, -> id_l.
228
rewrite <- comp_assoc with (g':=w); unfold w at 2.
229
rewrite -> cpr_inl.
230

    
231
rewrite -> comp_assoc with (h':=π); unfold π at 1.
232
rewrite -> map_lifting.
233
rewrite -> naturality.
234
rewrite <- codiagonal.
235
rewrite -> comp_assoc with (h':=map ([id, inr])), -> map_lifting.
236
rewrite -> f_cpr.
237
rewrite ->4 comp_assoc, ->2 map_comp.
238
rewrite -> cpr_inl, -> id_r.
239
rewrite -> comp_assoc with (g':=η), -> map_unit.
240
rewrite <- comp_assoc with (f':=inr), -> cpr_inr.
241

    
242
unfold π.
243
rewrite -> lifting_map.
244
rewrite -> f_cpr.
245
rewrite -> cpr_coprodhom.
246
rewrite <- comp_assoc with (f':=inl), -> cpr_inl, -> id_l.
247
rewrite -> comp_assoc with (g':=inl), -> cpr_inl.
248
rewrite <- comp_assoc with (f':=inr), -> cpr_inr.
249

    
250
assert (aux: map ([inl ⊕⊕ id, inl ∘ inr]) ∘ η ∘ inl ∘ inr = 
251
             η ∘ inr (a:=z ⊕ a × coext T a b (z ⊕ x) ^ b) (b:=x)).
252
rewrite -> map_unit.
253
rewrite <- comp_assoc with (f':=inl), -> cpr_inl.
254
rewrite <- comp_assoc, -> coprodhom_inr, -> id_l.
255
trivial.
256
rewrite <- aux; clear aux.
257

    
258
rewrite <-2 comp_assoc with (h':=map ([inl ⊕⊕ id, inl ∘ inr])), <-2 f_cpr.
259
rewrite <- map_lifting.
260
rewrite <- out_unitcofree.
261
rewrite <- comp_assoc with (h':=out), <- f_cpr.
262
rewrite <- comp_assoc with (f':=out), <- lifting1.
263
rewrite -> comp_assoc with (g':=out), <- comp_assoc with (f':=f).
264
trivial.
265

    
266

    
267
apply proving_naturality_h1.
268
apply guardedtriangle_def.
269

    
270
Qed.
271

    
272

    
273

    
274
Theorem proving_naturality : forall
275
(x y z : Obj)
276
(f : x ~> (coext T a b (y ⊕ x)))
277
(g : y ~> (coext T a b z)), 
278
  g § ∘ f †' = ([(ηv ∘ inl) § ∘ g  , ηv ∘ inr] § ∘ f) †'.
279

    
280
Proof.
281
intros.
282
rewrite <- mapc_unfold.
283

    
284
rewrite -> itercofree_triangle.
285
symmetry; rewrite -> itercofree_triangle; symmetry.
286

    
287
rewrite -> proving_naturality_h2.
288

    
289
apply unfolding_guarded2.
290

    
291
apply proving_naturality_h1.
292

    
293
apply guardedtriangle_def.
294

    
295
rewrite -> comp_assoc, <- proving_kl3.
296
rewrite -> f_cpr.
297
rewrite -> comp_assoc, -> liftingcofree_mapc.
298
rewrite -> cpr_inl.
299
rewrite -> proving_kl1, -> id_r.
300
rewrite -> comp_assoc, -> proving_kl2.
301
rewrite -> cpr_inr.
302

    
303
rewrite <- proving_unfolding at 1.
304
rewrite -> comp_assoc, <- proving_kl3.
305
rewrite -> f_cpr.
306
rewrite -> proving_kl2.
307
trivial.
308
Qed.
309

    
310

    
311

    
312
(* --- *)
313

    
314

    
315

    
316
Theorem proving_dinaturality : forall
317
(x y z : Obj)
318
(g: x ~> (coext T a b (y ⊕ z)))
319
(h : z ~> (coext T a b (y ⊕ x))),
320
  ([ηv ∘ inl , h] § ∘ g) †' =
321
    [ ηv , ([ηv ∘ inl , g] § ∘ h) †' ] § ∘ g.
322

    
323
Proof.
324
intros.
325

    
326
set (s:=[ηv ∘ inl, h] § ∘ g).
327
set (t:=[ηv ∘ inl, g] § ∘ h).
328
set (w:=[ηv, t †'] § ∘ g).
329

    
330

    
331
set (p:=(map ((id (a:=y) ⊕⊕ cont (a:=a) (b:=b) ([ηv ∘ inl, h] §)) ⊕⊕ id (a:=z)))).
332
set (q:=(map ((id (a:=y) ⊕⊕ cont (a:=a) (b:=b) ([ηv ∘ inl, g] §)) ⊕⊕ id (a:=x)))).
333

    
334

    
335
assert (Hp: (π ∘ out ∘ s) † = 
336
            ([η ∘ inl, π ∘ out ∘ h] * ∘ p ∘ π ∘ out ∘ g) †).
337
apply f_equal1.
338
unfold s.
339
rewrite -> comp_assoc; apply f_equal2;trivial.
340
rewrite <- comp_assoc, -> lifting1.
341
rewrite -> comp_assoc; apply f_equal2;trivial.
342
unfold π at 1.
343
rewrite -> map_lifting.
344
rewrite ->2 f_cpr.
345
rewrite -> comp_assoc with (h':=out), out_unitcofree.
346
rewrite -> f_cpr.
347
rewrite <- comp_assoc with (f':=inl), -> comp_assoc with (g':=η), map_unit.
348
rewrite <- comp_assoc with (h':=η), -> comp_assoc with (g':=inl), cpr_inl.
349
rewrite -> coprodhom_inl.
350
rewrite <- comp_assoc with (g':=inr),-> comp_assoc with (g':=η), map_unit.
351
rewrite <- comp_assoc with (h':=η), -> comp_assoc with (g':=inr), cpr_inr.
352
unfold p, π.
353
rewrite <- comp_assoc with (f':=map ([inl ⊕⊕ id, inl ∘ inr])), -> map_comp.
354
rewrite -> f_cpr.
355
rewrite -> coprodhom_comp, id_l.
356
rewrite -> comp_assoc with (g':=inl), coprodhom_inl, id_l.
357
rewrite -> comp_assoc with (g':=inl).
358
rewrite -> coprodhom_inl.
359
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr.
360
rewrite -> lifting_map; apply f_equal1.
361
rewrite -> f_cpr.
362
rewrite -> cpr_coprodhom, id_l.
363
rewrite -> comp_assoc with (g':=inl), cpr_inl.
364
rewrite ->4 comp_assoc; trivial.
365

    
366

    
367
assert (Hq: (π ∘ out ∘ t) † = 
368
            ([η ∘ inl, π ∘ out ∘ g] * ∘ q ∘ π ∘ out ∘ h) †).
369
apply f_equal1.
370
unfold t.
371
rewrite -> comp_assoc; apply f_equal2;trivial.
372
rewrite <- comp_assoc, -> lifting1.
373
rewrite -> comp_assoc; apply f_equal2;trivial.
374
unfold π at 1.
375
rewrite -> map_lifting.
376
rewrite ->2 f_cpr.
377
rewrite -> comp_assoc with (h':=out), -> out_unitcofree.
378
rewrite -> f_cpr.
379
rewrite <- comp_assoc with (f':=inl), -> comp_assoc with (g':=η), map_unit.
380
rewrite <- comp_assoc with (h':=η), -> comp_assoc with (g':=inl), cpr_inl.
381
rewrite -> coprodhom_inl.
382
rewrite <- comp_assoc with (g':=inr), -> comp_assoc with (g':=η), -> map_unit.
383
rewrite <- comp_assoc with (h':=η), -> comp_assoc with (g':=inr), -> cpr_inr.
384
unfold q, π.
385
rewrite <- comp_assoc with (f':=map ([inl ⊕⊕ id, inl ∘ inr])), -> map_comp.
386
rewrite -> f_cpr.
387
rewrite -> coprodhom_comp, -> id_l.
388
rewrite -> comp_assoc with (g':=inl), coprodhom_inl, id_l.
389
rewrite -> comp_assoc with (g':=inl), coprodhom_inl.
390
rewrite <- comp_assoc with (f':=inr), coprodhom_inr.
391
rewrite -> lifting_map; apply f_equal1.
392
rewrite -> f_cpr.
393
rewrite -> cpr_coprodhom, id_l.
394
rewrite -> comp_assoc with (g':=inl), cpr_inl.
395
rewrite ->4 comp_assoc; trivial.
396

    
397

    
398
assert (H_main: [ηv, w] § ∘ ▷ s = [ηv, t †'] § ∘ [ ηv ∘ inl , ▷ t] § ∘ g).
399

    
400
(* left-hand side *)
401
apply out_cong.
402
rewrite -> comp_assoc, -> lifting1 at 1.
403
unfold triangle at 1.
404
rewrite <- comp_assoc with (h':=tuo), <- comp_assoc with (g':=out), comp_assoc with (g':=tuo);
405
rewrite -> out_tuo_is_id, id_r.
406
rewrite -> comp_assoc, lifting_map.
407
rewrite -> cpr_coprodhom.
408
rewrite <- comp_assoc with (f':=inl), -> cpr_inl.
409
rewrite -> out_unitcofree, id_l. 
410

    
411
rewrite -> Hp.
412

    
413
rewrite <- comp_assoc with (g':=p), <- comp_assoc with (f':=g), <- comp_assoc with (f':=out ∘ g).
414
rewrite -> dinaturality.
415

    
416
unfold p at 2.
417
rewrite <- comp_assoc with (h':=map ((id ⊕⊕ cont (([ηv ∘ inl, h]) §) ⊕⊕ id)));
418
rewrite -> comp_assoc with (g':=map ((id ⊕⊕ cont (([ηv ∘ inl, h]) §) ⊕⊕ id)));
419
rewrite -> lifting_map.
420
rewrite -> cpr_coprodhom, id_l.
421

    
422
rewrite -> comp_assoc, <- kl3.
423
rewrite -> f_cpr.
424
rewrite -> comp_assoc with (g':=η), kl2.
425
rewrite -> cpr_coprodhom, id_l.
426
rewrite <- comp_assoc with (h':=η ∘ inr), -> cont_comp.
427
rewrite <- proving_kl3.
428
rewrite -> f_cpr.
429
rewrite -> comp_assoc with (g':=ηv), proving_kl2.
430
rewrite -> cpr_inl. 
431

    
432
assert (aux1: t †' = ([ηv, w]) § ∘ h).
433
rewrite <- proving_unfolding.
434
unfold w, t.
435
rewrite -> comp_assoc, <- proving_kl3.
436
rewrite -> f_cpr.
437
rewrite -> comp_assoc with (f':=inl), -> proving_kl2.
438
rewrite -> cpr_inl.
439
trivial.
440
rewrite <- aux1.
441

    
442

    
443
(* right-hand side *)
444
rewrite -> comp_assoc with (h':=out), -> lifting1.
445
rewrite <-2 comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> lifting1.
446

    
447
assert (aux2: (([out ∘ [ηv ∘ inl, ▷t], η ∘ inr ∘ cont (([ηv ∘ inl, ▷t]) §)]) *
448
         = ([η ∘ (inl ⊕⊕ cont (([ηv ∘ inl, ▷t]) §)), out ∘ ▷t] * ∘ π))).
449
unfold π.
450
rewrite -> lifting_map.
451
rewrite ->2 f_cpr.
452
rewrite -> cpr_coprodhom.
453
rewrite <- comp_assoc with (f':=inl), -> coprodhom_inl, id_l.
454
rewrite ->2 comp_assoc with (g':=inl), cpr_inl.
455
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr.
456
rewrite -> comp_assoc with (h':=out), out_unitcofree.
457
rewrite -> comp_assoc;trivial.
458
rewrite <- comp_assoc with (f':=g), -> aux2; clear aux2.
459

    
460
rewrite <-2 comp_assoc with (g':=π), -> comp_assoc with (f':=π ∘ (out ∘ g)), <- kl3.
461
rewrite -> f_cpr.
462
rewrite -> comp_assoc with (g':=η), kl2.
463
rewrite -> cpr_coprodhom.
464
rewrite <- comp_assoc with (h':=η ∘ inr), -> cont_comp.
465
rewrite <- comp_assoc with (f':=inl), -> cpr_inl.
466
rewrite -> out_unitcofree.
467
rewrite <- proving_kl3.
468
rewrite -> f_cpr.
469
rewrite -> comp_assoc with (f':=inl), proving_kl2.
470
rewrite -> cpr_inl.
471
rewrite <- unfolding_triangle1.
472

    
473

    
474
apply f_equal2;trivial.
475
apply f_equal1.
476
apply f_equal2;trivial.
477

    
478

    
479
(* left-hand side *)
480
rewrite -> naturality.
481
rewrite -> f_cpr.
482
rewrite -> comp_assoc with (g':=η), map_unit.
483
rewrite <- comp_assoc with (g':=inr), -> comp_assoc with (g':=η), -> map_unit.
484

    
485
rewrite -> comp_assoc, <- kl3.
486
rewrite -> f_cpr.
487
rewrite -> comp_assoc with (g':=η), kl2.
488
rewrite -> cpr_inl.
489
rewrite <- f_cpr.
490

    
491
rewrite -> comp_assoc with (g':=p); unfold p.
492
rewrite -> lifting_map.
493
rewrite -> cpr_coprodhom, -> id_l.
494
rewrite <- comp_assoc with (f':=id ⊕⊕ cont (([ηv ∘ inl, h]) §)), -> cpr_coprodhom, -> id_l.
495
rewrite <- comp_assoc with (f':=cont (([ηv ∘ inl, h]) §)), -> cont_comp.
496
rewrite <- proving_kl3.
497
rewrite -> f_cpr with (f:=([ηv, w]) §).
498
rewrite -> comp_assoc with (g':=ηv), -> proving_kl2, -> cpr_inl.
499
rewrite <- aux1.
500

    
501
assert (aux3: ([(η ∘ inl) ∘ ([inl, inr ∘ cont (([ηv, t †']) §)]), η ∘ inr]) *
502
            ∘ η ∘ inl ∘ (id ⊕⊕ cont ([ηv ∘ inl, g] §))
503
            = (η ∘ inl (b:=z)) ∘ ([inl, inr (a:=y) ∘ cont (a:=a) (b:=b) (([ηv, w]) §)])).
504
rewrite -> kl2.
505
rewrite -> cpr_inl.
506
rewrite <- comp_assoc, -> cpr_coprodhom, -> id_l.
507
rewrite <- comp_assoc with (h':=inr), -> cont_comp.
508
rewrite <- proving_kl3.
509
rewrite -> f_cpr with (f:=([ηv, t †']) §).
510
rewrite -> comp_assoc with (f':=inl), -> proving_kl2.
511
rewrite -> cpr_inl.
512
trivial.
513
rewrite <- aux3; clear aux3.
514

    
515
rewrite <-2 comp_assoc, <- f_cpr.
516

    
517
rewrite <- comp_assoc with (h':=η), <- f_cpr.
518

    
519
assert (aux4: map (([inl, inr ∘ cont (([ηv, t †']) §)]) ⊕⊕ id) = 
520
              (η ∘ ([inl ∘ ([inl, inr (a:=y) ∘ cont (a:=a) (b:=b) (([ηv, t †']) §)]), inr (b:=z)])) *).
521
unfold map, coprodhom; rewrite -> id_l.
522
trivial.
523
rewrite <- aux4; clear aux4.
524

    
525
rewrite <- map_lifting, <- comp_assoc, <- map_naturality.
526

    
527

    
528
(* right-hand side *)
529
unfold triangle.
530
rewrite <- comp_assoc with (h':=tuo), <- comp_assoc with (g':=out), -> comp_assoc with (g':=tuo);
531
rewrite -> out_tuo_is_id, id_r.
532

    
533
rewrite -> comp_assoc with (g':=map (inl ⊕⊕ id)), -> lifting_map.
534
rewrite -> cpr_coprodhom, -> id_l.
535
rewrite <- comp_assoc with (f':=inl), -> cpr_inl.
536
rewrite -> out_unitcofree.
537

    
538
apply f_equal2.
539
unfold map; rewrite -> f_cpr.
540
rewrite -> comp_assoc; trivial.
541

    
542
rewrite -> comp_assoc with (f':=t), -> Hq.
543
unfold q.
544
rewrite -> lifting_map.
545
rewrite -> cpr_coprodhom, -> id_l.
546
rewrite ->4 comp_assoc; trivial.
547

    
548

    
549

    
550
symmetry.
551
apply unfolding_triangle2.
552

    
553
rewrite -> H_main.
554

    
555
rewrite -> comp_assoc, <- proving_kl3.
556
rewrite -> f_cpr.
557
rewrite -> comp_assoc with (f':=inl), proving_kl2.
558
rewrite -> cpr_inl.
559

    
560
rewrite <- unfolding_triangle1.
561
trivial.
562
Qed.
563

    
564

    
565

    
566
(* --- *)
567

    
568
(* proving codiagonal, split in multiple lemmas/theorems *)
569

    
570
Definition ξ (x y : Obj) :=
571
([inl ⊕⊕ id, inl (b:=x) ∘ inr (a:=y) (b:=x)]).
572
Arguments ξ [x y].
573

    
574

    
575
Lemma ξ1 : forall (x y : Obj),
576
mapc ξ ∘ mapc (a:=a) (b:=b) (ξ (x:=x) (y:=y)) = id.
577
Proof.
578
intros.
579
rewrite -> mapc_comp.
580
unfold ξ.
581
rewrite -> f_cpr.
582
rewrite -> cpr_coprodhom.
583
rewrite -> coprodhom_inl, -> id_l.
584
rewrite -> comp_assoc with (g':=inl), -> cpr_inl.
585
rewrite -> coprodhom_inr, -> id_l.
586
rewrite <- f_cpr.
587
rewrite -> inl_inr_is_id, -> id_l.
588
rewrite -> inl_inr_is_id.
589
apply mapc_id.
590
Qed.
591

    
592

    
593
Lemma ξ2 : forall (x y : Obj),
594
mapc ([id, inr]) ∘ mapc (ξ (x:=x) (y:=y)) = mapc (a:=a) (b:=b) ([id, inr]).
595
Proof.
596
intros.
597
rewrite -> mapc_comp.
598
unfold ξ.
599
rewrite -> f_cpr.
600
rewrite -> cpr_coprodhom, -> id_l, id_r.
601
rewrite -> inl_inr_is_id.
602
rewrite -> comp_assoc, -> cpr_inl, -> id_r.
603
trivial.
604
Qed.
605

    
606

    
607

    
608
(* A.11 *)
609
Lemma proving_codiagonal_h0 : forall (x y : Obj) (g': x ~> (coext T a b (y ⊕ x ⊕ x)))
610
(h': x ~> (coext T a b (y ⊕ x ⊕ x))),
611
  (h' †') †' = ([ηv, (h' †') †']) § ∘  ▷(mapc ([id, inr]) ∘ g') ->
612
  (h' †') †' = (mapc ([id, inr]) ∘ g') †'.
613

    
614
Proof.
615
intros.
616

    
617
rewrite -> itercofree_triangle with (f:=mapc ([id, inr]) ∘ g').
618
apply unfolding_guarded2.
619
apply guardedtriangle_def.
620
exact H.
621

    
622
Qed.
623

    
624

    
625

    
626
Theorem proving_codiagonal_clause1 : forall (x y : Obj) (g': x ~> (coext T a b (y ⊕ x ⊕ x))),
627
guarded (mapc ([id, inr]) ∘ g') -> 
628
  (g' †') †' = ([ηv, (g' †') †']) § ∘ ▷(mapc ([id, inr]) ∘ g').
629

    
630
Proof.
631
intros.
632
rewrite <- proving_unfolding at 1.
633

    
634
assert (aux:([ηv, (g' †') †']) § ∘ g' †' = [ηv, (g' †') †'] § ∘ [ηv, g' †'] § ∘ g').
635
symmetry; rewrite -> proving_unfolding at 1; trivial.
636
rewrite -> aux at 1; clear aux.
637

    
638
rewrite -> comp_assoc, <- proving_kl3.
639
rewrite -> f_cpr.
640
rewrite -> proving_kl2.
641

    
642
rewrite -> proving_unfolding.
643

    
644

    
645
rewrite -> guardedtriangle with (f':=mapc ([id, inr]) ∘ g'); trivial.
646

    
647
rewrite -> comp_assoc, -> liftingcofree_mapc.
648
rewrite -> f_cpr, -> id_l.
649
rewrite -> cpr_inr.
650
trivial.
651

    
652
Qed.
653

    
654

    
655

    
656
(* A.10 *)
657
Lemma proving_codiagonal_h1 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))),
658
  ▷(mapc ([id, inr]) ∘ ▷g) = ▷(mapc ([id, inr]) ∘ g).
659

    
660
Proof.
661
intros.
662
apply out_cong.
663
rewrite ->2 out_triangle.
664
rewrite <-2 comp_assoc with (g':=out), ->2 comp_assoc with (h':=out), -> out_mapc.
665
rewrite ->4 comp_assoc, -> map_comp.
666
rewrite -> cpr_coprodhom.
667
rewrite -> f_cpr, -> id_l.
668
rewrite -> cpr_inr.
669
rewrite <- comp_assoc, -> out_triangle.
670
rewrite -> map_naturality.
671
rewrite ->2 comp_assoc, -> map_comp.
672
rewrite <- codiagonal.
673
apply f_equal1.
674
rewrite ->2 comp_assoc, -> map_comp.
675
apply f_equal2;trivial; apply f_equal2;trivial.
676
unfold map.
677
apply f_equal1.
678
rewrite <- comp_assoc; apply f_equal2;trivial.
679

    
680
case_distinction.
681

    
682
case_distinction.
683
rewrite ->3 comp_assoc, <- comp_assoc with (h':=([id, inr])), -> coprodhom_inl.
684
rewrite -> comp_assoc, -> cpr_inl.
685
rewrite -> id_r, -> cpr_inl.
686
rewrite -> cpr_inl.
687
trivial.
688

    
689
rewrite -> coprodhom_inr, -> id_l.
690
rewrite -> cpr_inr.
691
trivial.
692

    
693
rewrite -> comp_assoc with (f':=inr), -> coprodhom_inl.
694
rewrite ->2 comp_assoc, -> cpr_inl, -> id_r.
695
rewrite -> cpr_inr.
696
trivial.
697

    
698
Qed.
699

    
700

    
701

    
702
Theorem proving_codiagonal_clause2 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))),
703
  guarded (mapc ξ ∘ g) ->
704
  (g †') †' = ▷(mapc ([id, inr]) ∘ g) †'.
705

    
706
Proof.
707
intros.
708

    
709
rewrite <- itercofree_triangle.
710
apply proving_codiagonal_h0.
711

    
712
rewrite <- proving_codiagonal_h1.
713

    
714
assert (aux: (g †') †' = (▷g †') †').
715
rewrite <- itercofree_triangle;trivial.
716
rewrite -> aux; clear aux.
717

    
718
apply proving_codiagonal_clause1.
719

    
720

    
721
unfold guarded in H.
722
inversion H as [u' H'].
723

    
724
assert (aux1: g = mapc ξ ∘ tuo ∘ map (inl ⊕⊕ id) ∘ u').
725
rewrite <- comp_assoc, <- H'.
726
rewrite <- comp_assoc with (g':=tuo), -> comp_assoc with (g':=out), -> tuo_out_is_id, -> id_r.
727
rewrite -> comp_assoc, -> ξ1, -> id_r.
728
trivial.
729

    
730

    
731
unfold guarded.
732

    
733
rewrite -> aux1; clear aux1.
734
unfold triangle.
735

    
736
rewrite <- comp_assoc with (g':=out), <-2 comp_assoc with (h':=mapc ξ),
737
  -> comp_assoc with (g':=mapc ξ), -> out_mapc.
738
rewrite <- comp_assoc with (g':=out), <-2 comp_assoc with (h':=tuo),
739
  -> comp_assoc with (f':=map (inl ⊕⊕ id) ∘ u'), -> out_tuo_is_id, -> id_r.
740

    
741
rewrite -> comp_assoc with (h':=map (ξ ⊕⊕ cont (mapc ξ))), -> map_comp.
742
rewrite -> coprodhom_comp, -> id_l.
743

    
744
(*
745
assert (aux2: map ((inl ⊕⊕ id) ⊕⊕ id) ∘ π = π ∘ map (ξ (x:=x) (y:=y) ∘ inl 
746
              ⊕⊕ cont (a:=a) (b:=b) (mapc (a:=a) (b:=b) (ξ (x:=x) (y:=y))))).
747
unfold π.
748
rewrite ->2 map_comp.
749
rewrite -> cpr_coprodhom.
750
rewrite -> f_cpr.
751
rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl.
752
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr, -> id_l.
753
rewrite -> coprodhom_comp, -> id_l.
754
rewrite -> coprodhom_inl.
755
(* is this even true ? see paper *)
756
*)
757

    
758

    
759
rewrite -> comp_assoc, -> out_mapc.
760
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> out_tuo_is_id, -> id_r.
761

    
762
rewrite -> comp_assoc, -> map_comp.
763
rewrite -> coprodhom_comp, -> cpr_inl, -> id_l.
764
rewrite -> map_naturality.
765
rewrite -> comp_assoc; unfold π.
766
rewrite -> comp_assoc, ->2 map_comp.
767
rewrite -> f_cpr.
768
rewrite -> coprodhom_comp.
769
rewrite -> coprodhom_inl, ->2 id_l.
770
rewrite -> comp_assoc, -> coprodhom_inl.
771
rewrite <- comp_assoc, -> coprodhom_inr.
772
rewrite -> cpr_coprodhom.
773
unfold ξ at 1; rewrite -> cpr_inl.
774
rewrite -> coprodhom_comp, -> id_l.
775
rewrite <-2 comp_assoc with (f':=cont (mapc ξ)), -> cont_comp.
776
rewrite -> ξ2.
777

    
778
exists (map (id ⊕⊕ cont (mapc ([id, inr]))) ∘ (map ([inl ⊕⊕ id, inl ∘ inr]) ∘ u') †).
779

    
780
rewrite ->2 map_naturality.
781
apply f_equal1.
782
rewrite ->3 comp_assoc, ->2 map_comp.
783
apply f_equal2; trivial.
784
apply f_equal1.
785

    
786
rewrite ->2 coprodhom_comp, ->2 id_l, -> id_r.
787
rewrite -> f_cpr.
788
rewrite -> coprodhom_comp.
789
rewrite -> coprodhom_inl, -> id_l.
790
rewrite -> comp_assoc, -> coprodhom_inl.
791
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr.
792
rewrite -> comp_assoc; trivial.
793

    
794
Qed.
795

    
796

    
797

    
798
(* A.12 *)
799
Theorem proving_codiagonal_h2 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))),
800
  guarded g ->
801
    ▷(g †') = [ηv, g †'] § ∘ mapc ξ ∘ ▷ (mapc ξ ∘ g).
802

    
803
Proof.
804
intros.
805

    
806
apply out_cong.
807

    
808
(* right-hand side *)
809
rewrite ->2 comp_assoc, -> lifting1.
810
unfold triangle at 2.
811

    
812
rewrite <- comp_assoc with (g':=out), -> out_mapc.
813
rewrite -> comp_assoc with (f':=out), <- comp_assoc with (g':=out), ->2 comp_assoc with (h':=out),
814
-> out_tuo_is_id, -> id_r.
815
rewrite -> lifting_map.
816
rewrite -> cpr_coprodhom.
817
rewrite <- comp_assoc with (f':=cont (mapc ξ)), -> cont_comp.
818
rewrite -> comp_assoc, -> lifting_map.
819
rewrite -> cpr_coprodhom, -> id_l.
820

    
821
unfold ξ at 1.
822
rewrite <- comp_assoc with (f':=inl), -> cpr_inl.
823
rewrite <- comp_assoc with (h':=out), -> cpr_coprodhom, -> id_l.
824
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> out_mapc.
825

    
826
rewrite -> naturality.
827

    
828
rewrite ->3 f_cpr.
829
rewrite -> comp_assoc with (h':=out), -> out_unitcofree.
830
rewrite ->5 comp_assoc with (h':=map inl), -> map_unit.
831

    
832
unfold π.
833
rewrite -> comp_assoc, -> lifting_map.
834
rewrite -> f_cpr.
835
rewrite -> cpr_coprodhom, -> id_l.
836
rewrite -> cpr_inl.
837
rewrite -> comp_assoc with (g':=inl), -> cpr_inl.
838
rewrite -> cpr_inr.
839

    
840
unfold guarded in H.
841
inversion H as [u' H'].
842
rewrite <- comp_assoc with (f':=g), -> H'.
843

    
844
rewrite -> comp_assoc with (f':=u'), -> map_comp, -> coprodhom_comp, -> id_l.
845
rewrite -> comp_assoc, -> lifting_map.
846
rewrite -> cpr_coprodhom.
847
rewrite <- comp_assoc with (f':=cont (mapc ξ)), -> cont_comp.
848

    
849
unfold ξ at 1.
850
rewrite -> cpr_inl.
851
rewrite -> cpr_coprodhom, -> id_l.
852
rewrite -> cpr_inl.
853
rewrite <- comp_assoc with (g':=mapc ξ), -> ξ1, -> id_l.
854

    
855

    
856
(* left-hand side *)
857
unfold triangle.
858
rewrite ->2 comp_assoc, -> out_tuo_is_id, -> id_r.
859

    
860
rewrite -> map_naturality.
861
unfold π.
862
rewrite ->2 comp_assoc, -> map_comp, -> f_cpr.
863
rewrite -> coprodhom_comp, -> coprodhom_inl, -> id_l.
864
rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl.
865
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr, -> id_l.
866

    
867
rewrite <- comp_assoc with (g':=out), <- proving_unfolding at 1.
868
rewrite -> comp_assoc with (h':=out), -> lifting1.
869

    
870
rewrite -> f_cpr, -> out_unitcofree.
871
rewrite <- comp_assoc with (f':=g), -> H'.
872
rewrite -> comp_assoc with (f':=u'), -> lifting_map.
873
rewrite -> cpr_coprodhom, -> id_l.
874
rewrite -> cpr_inl.
875

    
876
rewrite -> comp_assoc with (f':=u'), -> map_lifting, -> f_cpr.
877
rewrite ->3 comp_assoc, -> map_unit.
878
rewrite <-2 comp_assoc with (h':=η), -> cpr_inl, -> cpr_inr.
879
unfold coprodhom.
880
rewrite -> f_cpr, -> id_l, ->3 comp_assoc.
881

    
882
trivial.
883
Qed.
884

    
885

    
886

    
887
Theorem proving_codiagonal_h3 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))),
888
guarded g ->
889
(g †') †' = (([ηv ∘ inl, g †']) § ∘ (mapc ξ ∘ g) †') †'.
890

    
891
Proof.
892
intros.
893

    
894
set (h:= mapc ξ ∘ ▷ (mapc ξ ∘ g)).
895
rewrite -> itercofree_triangle at 1.
896
rewrite -> proving_codiagonal_h2.
897

    
898
rewrite <- id_l with (f':=ηv).
899
rewrite <- inl_inr_is_id.
900
rewrite -> f_cpr.
901

    
902
rewrite -> liftingcofree_mapc.
903
unfold ξ at 1.
904
rewrite -> f_cpr.
905
rewrite -> cpr_coprodhom.
906
rewrite -> cpr_inl, -> id_l.
907
rewrite -> comp_assoc with (g':=inl), -> cpr_inl.
908
rewrite -> cpr_inr.
909

    
910
assert (aux1: mapc ([id, inr]) ∘ ([[ηv ∘ inl ∘ inl, mapc inl ∘ g †'], ηv ∘ inr]) §
911
              = ([[ηv ∘ inl, g †'], ηv ∘ inr]) §).
912
rewrite -> mapc_liftingcofree.
913
rewrite ->2 f_cpr.
914
rewrite ->2 comp_assoc, -> mapc_unitcofree.
915
rewrite <- comp_assoc with (g':=[id, inr]), -> cpr_inl, -> id_l.
916
rewrite -> comp_assoc with (g':=mapc inl), -> mapc_comp.
917
rewrite -> cpr_inl, -> mapc_id, -> id_r.
918
rewrite -> comp_assoc, -> mapc_unitcofree.
919
rewrite <- comp_assoc, -> cpr_inr.
920
trivial.
921
rewrite <- aux1; clear aux1.
922

    
923
rewrite -> itercofree_triangle.
924
rewrite <- comp_assoc, <- proving_codiagonal_clause2.
925

    
926
assert (aux2: mapc inl ∘ ([ηv ∘ inl, g †']) = [(ηv ∘ inl) ∘ inl, mapc (inl (b:=x)) ∘ g †']).
927
rewrite -> f_cpr.
928
rewrite -> comp_assoc, -> mapc_unitcofree.
929
trivial.
930
rewrite <- aux2; clear aux2.
931

    
932
rewrite -> mapc_unfold at 1.
933
rewrite <- proving_naturality.
934

    
935
rewrite <- itercofree_triangle.
936

    
937
trivial.
938

    
939

    
940
unfold guarded.
941

    
942

    
943
assert (aux4: exists u : x ~> T (y ⊕ a × coext T a b ((y ⊕ x) ⊕ x) ^ b), out∘ ▷(mapc ξ ∘ g) = map (inl ∘  inl ⊕⊕ id) ∘ u).
944
unfold triangle.
945
rewrite ->2 comp_assoc, -> out_tuo_is_id, -> id_r.
946
rewrite -> comp_assoc, <- comp_assoc with (g':=out), -> out_mapc.
947
rewrite -> comp_assoc; unfold π.
948
rewrite -> map_comp.
949
rewrite -> cpr_coprodhom.
950
unfold ξ.
951
rewrite -> f_cpr.
952
rewrite -> coprodhom_comp, -> id_r.
953
rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl, <- comp_assoc with (g':=out).
954

    
955
unfold guarded in H.
956
inversion H as [z Q].
957
rewrite -> Q.
958
rewrite -> comp_assoc, -> map_comp.
959
rewrite -> cpr_coprodhom, -> id_l.
960
rewrite -> cpr_inl.
961
unfold coprodhom at 2; rewrite -> id_l.
962

    
963
assert (aux5: z =  π ∘  π ∘ z).
964
unfold π.
965
rewrite -> map_comp.
966
unfold coprodhom.
967
coprod_simp.
968
rewrite ->2 id_l.
969
rewrite <- f_cpr.
970
rewrite -> inl_inr_is_id, -> id_l.
971
rewrite -> inl_inr_is_id, -> map_id, -> id_r; trivial.
972
rewrite -> aux5; clear aux5.
973

    
974
rewrite <- comp_assoc with (g':=π), -> comp_assoc with (g':=π);
975
unfold π at 1.
976
rewrite -> map_comp.
977
rewrite -> f_cpr.
978
rewrite -> cpr_coprodhom, -> cpr_inl, -> id_l.
979
rewrite -> comp_assoc with (g':=inl) (f':=inr), -> cpr_inl.
980
rewrite -> cpr_inr, <- comp_assoc with (h':=inl) (g':=inr).
981
rewrite <- f_cpr.
982
unfold map at 2.
983
rewrite -> f_cpr with (f:=η).
984
rewrite <- map_unit.
985
rewrite <- map_comp, <- comp_assoc with (h':=map inl).
986

    
987

    
988
rewrite <- naturality.
989

    
990
rewrite -> comp_assoc, -> map_lifting.
991
rewrite -> comp_assoc, -> map_comp.
992
unfold coprodhom at 1.
993
rewrite -> f_cpr.
994
rewrite -> comp_assoc with (g':=inl), -> cpr_inl.
995
rewrite -> comp_assoc with (g':=inr), -> cpr_inr, -> id_l.
996
rewrite <- comp_assoc with (g':=inl), <- map_lifting.
997
rewrite -> kl1, -> id_l.
998

    
999
exists (map (id  ⊕⊕ cont (mapc ([inl ⊕⊕ id, inl ∘ inr]))) ∘ (π ∘ z) †).
1000

    
1001
rewrite ->2 comp_assoc, -> map_comp.
1002
unfold coprodhom.
1003
coprod_simp.
1004
rewrite ->3 id_l, -> comp_assoc.
1005
trivial.
1006

    
1007

    
1008
inversion aux4 as [w H'].
1009

    
1010
rewrite -> comp_assoc with (h':=mapc ξ).
1011
rewrite -> mapc_liftingcofree.
1012
rewrite ->2 f_cpr.
1013
rewrite ->4 comp_assoc with (h':=mapc ξ), -> mapc_unitcofree, -> mapc_comp.
1014
rewrite <-2 comp_assoc with (g':=ξ).
1015
unfold ξ at 1 2 3.
1016
rewrite -> cpr_inl, -> cpr_inr.
1017
rewrite <- comp_assoc with (f':=inl), -> coprodhom_inl.
1018
rewrite -> comp_assoc, -> lifting1.
1019
rewrite ->2 f_cpr.
1020
rewrite <- comp_assoc with (g':=out), -> H'.
1021
rewrite -> comp_assoc, -> lifting_map.
1022
rewrite -> cpr_coprodhom, -> id_l.
1023
rewrite -> comp_assoc with (g':=inl), ->2 cpr_inl.
1024
rewrite -> comp_assoc with (h':=out), -> out_unitcofree.
1025
rewrite -> comp_assoc.
1026
rewrite <- cpr_coprodhom with (f:=(η ∘ inl) ∘ inl) (i:=cont
1027
       (([[ηv ∘ (inl ∘ inl), mapc (inl ⊕⊕ id) ∘ g †'], ηv ∘ (inl ∘ inr)]) §)).
1028
rewrite <- comp_assoc, <- f_cpr.
1029
rewrite <- map_unit.
1030
rewrite <- comp_assoc with (g':=η).
1031
rewrite <- map_lifting.
1032
rewrite <- comp_assoc with (h':=map ([inl ∘ inl, inr])).
1033
exists ((η ∘ (inl ⊕⊕ cont (([[ηv ∘ (inl ∘ inl), mapc (inl ⊕⊕ id) ∘ g †'],
1034
                ηv ∘ (inl ∘ inr)]) §))) * ∘ w).
1035
unfold coprodhom at 3.
1036
rewrite -> id_l.
1037
trivial.
1038

    
1039

    
1040
exact H.
1041

    
1042
Qed.
1043

    
1044

    
1045

    
1046
Theorem proving_codiagonal_h4 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))),
1047
guarded g ->
1048
((mapc ξ ∘ g) †') †' = (g †') †'.
1049

    
1050
Proof.
1051
intros.
1052

    
1053
set (h:= mapc ξ ∘ ▷ (mapc ξ ∘ g)).
1054

    
1055

    
1056
symmetry.
1057
apply unfolding_guarded2.
1058

    
1059
unfold guarded.
1060
unfold guarded in H.
1061
inversion H as [u' H'].
1062

    
1063
exists (map (id ⊕⊕ cont ([ηv,( mapc ξ ∘ g) †'] §) ) ∘ (map ([inl ⊕⊕ id, inl ∘ inr]) ∘ map (id ⊕⊕ cont (mapc ξ)) ∘ u') †).
1064
rewrite -> out_itercofree.
1065
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> out_mapc.
1066
rewrite <- comp_assoc with (g':=out), -> H'.
1067
rewrite -> naturality.
1068
rewrite -> map_naturality.
1069
rewrite -> map_naturality.
1070
apply f_equal1.
1071
unfold π.
1072
rewrite -> comp_assoc, -> lifting_map.
1073
rewrite -> comp_assoc, -> lifting_map.
1074
rewrite -> comp_assoc, -> lifting_map.
1075
rewrite -> comp_assoc, -> map_comp.
1076
rewrite ->2 comp_assoc, ->2 map_comp.
1077
apply f_equal2; trivial.
1078
rewrite -> f_cpr.
1079
rewrite ->3 cpr_coprodhom.
1080
rewrite -> id_l.
1081
rewrite ->2 coprodhom_comp.
1082
rewrite ->2 id_l, ->2 id_r.
1083
rewrite -> f_cpr with (f:=(inl ⊕⊕ cont (([ηv, (mapc ξ ∘ g) †']) §)) ⊕⊕ id).
1084
rewrite -> cpr_coprodhom.
1085
rewrite -> id_l.
1086
unfold map.
1087
apply f_equal1.
1088
case_distinction.
1089
rewrite <- comp_assoc with (f':=inl).
1090
rewrite -> cpr_inl.
1091
rewrite -> coprodhom_comp.
1092
rewrite -> coprodhom_inl.
1093
unfold ξ.
1094
rewrite -> cpr_inl.
1095
rewrite -> cpr_coprodhom.
1096
rewrite -> comp_assoc, -> kl2.
1097
unfold coprodhom.
1098
rewrite -> f_cpr.
1099
rewrite ->3 id_l.
1100
rewrite ->2 comp_assoc.
1101
trivial.
1102
rewrite <- comp_assoc with (f':=inr).
1103
rewrite ->2 cpr_inr.
1104
rewrite -> comp_assoc with (g':=inl), -> cpr_inl.
1105
rewrite <- comp_assoc with (f':=inr).
1106
rewrite -> cpr_inr.
1107
rewrite ->2 comp_assoc, -> kl2.
1108
rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl.
1109
rewrite <-2 comp_assoc with (f':=inr).
1110
rewrite -> coprodhom_inr.
1111
rewrite ->4 comp_assoc.
1112
trivial. (* this might be possible in a much simpler way *)
1113

    
1114

    
1115
rewrite -> proving_codiagonal_h3 at 1.
1116

    
1117
rewrite <- proving_unfolding at 1.
1118

    
1119
rewrite <- proving_codiagonal_h3.
1120

    
1121
rewrite -> comp_assoc, <- proving_kl3.
1122
rewrite -> f_cpr.
1123
rewrite -> comp_assoc, -> proving_kl2.
1124
rewrite -> cpr_inl.
1125

    
1126
rewrite -> proving_unfolding.
1127
trivial.
1128

    
1129
exact H.
1130
exact H.
1131
Qed.
1132

    
1133

    
1134

    
1135
Theorem proving_codiagonal_clause3 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))),
1136
guarded g ->
1137
(mapc ([id, inr]) ∘ g) †' = (g †') †'.
1138

    
1139
Proof.
1140
intros.
1141

    
1142
set (h:= mapc ξ ∘ ▷ (mapc ξ ∘ g)).
1143

    
1144
transitivity (((mapc ξ ∘ g) †') †').
1145

    
1146
rewrite -> proving_codiagonal_clause2.
1147
rewrite <- itercofree_triangle.
1148
rewrite -> comp_assoc, -> ξ2.
1149
trivial.
1150

    
1151
unfold guarded.
1152
rewrite -> comp_assoc with (f':=g), -> ξ1, -> id_r.
1153
exact H.
1154

    
1155

    
1156
apply proving_codiagonal_h4.
1157
apply H.
1158

    
1159
Qed.
1160

    
1161

    
1162

    
1163
Theorem proving_codiagonal : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))),
1164
    ((ηv ∘ ([id, inr])) § ∘ g) †' = (g †') †'.
1165

    
1166
Proof.
1167
intros.
1168
rewrite <- mapc_unfold.
1169

    
1170
(* clause 4 *)
1171

    
1172
set (h:= mapc ξ ∘ ▷ g).
1173

    
1174

    
1175
transitivity (((mapc ξ ∘ h) †') †').
1176

    
1177
rewrite <- proving_codiagonal_clause3.
1178

    
1179
rewrite -> comp_assoc, ξ2.
1180

    
1181
unfold h.
1182

    
1183
rewrite -> comp_assoc, ξ2.
1184

    
1185
rewrite -> itercofree_triangle with (f:=mapc ([id, inr]) ∘ ▷g).
1186

    
1187
rewrite -> proving_codiagonal_h1.
1188

    
1189
apply itercofree_triangle.
1190

    
1191
unfold h.
1192
rewrite -> comp_assoc, -> ξ1, -> id_r.
1193
apply guardedtriangle_def.
1194

    
1195

    
1196
unfold h.
1197

    
1198
rewrite -> comp_assoc, -> ξ1, -> id_r.
1199
rewrite <- itercofree_triangle.
1200
trivial.
1201

    
1202
Qed.
1203

    
1204

    
1205

    
1206
(* --- *)
1207

    
1208

    
1209

    
1210
Theorem proving_uniformity_guarded : forall x y z (f : x ~> coext T a b (y ⊕ x)) (g: z ~> coext T a b (y ⊕ z)) (h: z ~> x),
1211
    guarded g ->
1212
    f ∘ h = mapc (id ⊕⊕ h) ∘ g ->
1213
    f †' ∘ h = g †'.
1214

    
1215
Proof.
1216
intros.
1217

    
1218
apply unfolding_guarded2.
1219
apply H.
1220

    
1221
assert (aux: ([ηv, f †' ∘ h]) § = ([ηv, f †']) § ∘ mapc (id ⊕⊕ h)).
1222
rewrite -> liftingcofree_mapc.
1223
rewrite -> cpr_coprodhom, id_l; trivial.
1224
rewrite -> aux.
1225

    
1226
rewrite <- comp_assoc, <- H0.
1227
rewrite -> comp_assoc, -> proving_unfolding.
1228
trivial.
1229
Qed.
1230

    
1231

    
1232

    
1233
Theorem proving_uniformity : forall x y z (f : x ~> coext T a b (y ⊕ x)) (g: z ~> coext T a b (y ⊕ z)) (h: z ~> x),
1234
    f ∘ h = (ηv ∘ (id ⊕⊕ h)) § ∘ g ->
1235
    f †' ∘ h = g †'.
1236

    
1237
Proof.
1238
intros.
1239
rewrite <- mapc_unfold in H.
1240

    
1241
assert (H1: (π ∘ out ∘ f) † ∘ h = 
1242
            map (id ⊕⊕ cont (mapc (id ⊕⊕ h))) ∘ (π ∘ out ∘ g) †).
1243

    
1244
rewrite -> map_naturality.
1245

    
1246
apply uniformity.
1247

    
1248
rewrite <- comp_assoc, -> H.
1249
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> out_mapc.
1250

    
1251
rewrite <-2 comp_assoc with (f':=g), ->3 comp_assoc with (f':=out ∘ g);
1252
apply f_equal2;trivial.
1253

    
1254
unfold π.
1255
rewrite ->3 map_comp.
1256
apply f_equal1.
1257
rewrite -> cpr_coprodhom.
1258
rewrite -> coprodhom_comp, -> id_l, -> id_r.
1259
rewrite -> f_cpr.
1260
rewrite -> coprodhom_comp, -> id_l.
1261
rewrite -> coprodhom_inl, -> id_l.
1262
rewrite -> comp_assoc, -> coprodhom_inl.
1263
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr.
1264
rewrite -> f_cpr.
1265
rewrite -> coprodhom_comp, -> id_l, -> id_r.
1266
rewrite -> comp_assoc, -> coprodhom_inl, -> id_l.
1267
rewrite -> comp_assoc; trivial.
1268

    
1269

    
1270
assert (H2: (▷f) ∘ h = mapc (id ⊕⊕ h) ∘ ▷g).
1271
unfold triangle.
1272
rewrite <- comp_assoc, -> H1.
1273
rewrite ->2 comp_assoc; apply f_equal2; trivial.
1274
apply out_cong.
1275
rewrite -> comp_assoc with (g':=mapc (id ⊕⊕ h)), -> out_mapc.
1276
rewrite ->2 comp_assoc with (h':=out), -> out_tuo_is_id, -> id_r.
1277
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (g':=tuo), -> out_tuo_is_id, -> id_r.
1278
rewrite ->2 map_comp.
1279
rewrite ->2 coprodhom_comp, -> id_l.
1280
rewrite -> coprodhom_inl.
1281
rewrite ->2 id_l, -> id_r; trivial.
1282

    
1283
rewrite -> itercofree_triangle.
1284
symmetry; rewrite -> itercofree_triangle; symmetry.
1285

    
1286
apply proving_uniformity_guarded.
1287

    
1288
apply guardedtriangle_def.
1289

    
1290
apply H2.
1291

    
1292
Qed.
1293

    
1294

    
1295

    
1296
(* --- *)
1297

    
1298

    
1299

    
1300
Theorem proving_str1 : forall
1301
(x : Obj),
1302
  pr2 (a:=terminal_obj) (b:=coext T a b x) = (ηv ∘ pr2) § ∘ τv.
1303

    
1304
Proof.
1305
intros.
1306
rewrite <- mapc_unfold.
1307

    
1308
assert (H1: pr2 (a:=terminal_obj) (b:=coext T a b x) = mapc pr2 ∘ (mapc (pair bang id) ∘ pr2)).
1309
rewrite -> comp_assoc, -> mapc_comp.
1310
rewrite -> pr2_pair.
1311
rewrite -> mapc_id, -> id_r.
1312
trivial.
1313

    
1314
rewrite -> H1.
1315
apply f_equal2;trivial.
1316

    
1317

    
1318
apply strength2.
1319

    
1320
assert (H2: id (a:=terminal_obj × x) = (pair bang id) ∘ pr2).
1321
rewrite -> pair_f, -> id_r.
1322

    
1323
assert (aux1: bang ∘ pr2 (a:=terminal_obj) (b:=x) = pr1).
1324
transitivity (bang (a:=terminal_obj × x)).
1325
apply bang_axiom.
1326
symmetry; apply bang_axiom.
1327
rewrite -> aux1; clear aux1.
1328
symmetry; apply pr1_pr2_is_id.
1329

    
1330
rewrite -> H2.
1331

    
1332

    
1333
rewrite -> map_comp.
1334
assert (aux2: ((pair bang id) ∘ pr2 (a:=terminal_obj) (b:=x) ⊕⊕ cont (mapc (pair bang id) ∘ pr2)) ∘ δ = 
1335
        ((pair bang id) ⊕⊕ cont (a:=a) (b:=b) (mapc (a:=a) (b:=b) (pair bang id (a:=x))))  ∘ pr2).
1336
set (y:=(pair bang id)).
1337
rewrite <-2 pr2_prodhom with (f:=id).
1338
rewrite <- cont_comp.
1339
rewrite <- coprodhom_comp.
1340
rewrite <- comp_assoc, -> delta.
1341
unfold δ.
1342
rewrite ->2 comp_assoc, -> coprodhom_comp, -> id_l.
1343
unfold cont at 1.
1344
rewrite -> prodhom_pair, -> id_r.
1345
rewrite -> curry2.
1346
rewrite -> pr2_pair.
1347
rewrite -> curry_uncurry.
1348
rewrite <- pair_f.
1349
rewrite -> pr1_pr2_is_id, -> id_r.
1350
unfold dist2.
1351
rewrite -> comp_assoc, <- uncurry2.
1352
rewrite -> f_cpr.
1353
rewrite ->2 curry2.
1354
rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl.
1355
rewrite -> comp_assoc with (g':=inr), -> coprodhom_inr.
1356
rewrite <-2 comp_assoc with (g':=pr2).
1357
rewrite <- comp_assoc, -> swap_prodhom.
1358
rewrite -> comp_assoc, <- uncurry1.
1359
rewrite -> cpr_coprodhom.
1360
rewrite ->2 curry1.
1361
rewrite <-2 comp_assoc with (f':=y ×× id), -> swap_prodhom.
1362
rewrite -> comp_assoc with (g':=id ×× y), -> pr2_prodhom.
1363
rewrite <-2 comp_assoc with (f':=cont (mapc y) ×× id), -> swap_prodhom.
1364
rewrite -> comp_assoc with (g':=id ×× cont (mapc y)), -> pr2_prodhom.
1365
rewrite <-2 comp_assoc with (f':=swapp); unfold swapp.
1366
rewrite ->2 pr2_pair.
1367
rewrite ->2 comp_assoc, -> curry_cpr_pr1.
1368
rewrite <- comp_assoc, -> pr1_pair.
1369
trivial.
1370
rewrite -> aux2; clear aux2.
1371

    
1372
rewrite <- comp_assoc, <- map_comp.
1373
rewrite <- comp_assoc, -> comp_assoc with (g':=τ).
1374
rewrite <- str1.
1375
rewrite -> pr2_prodhom.
1376
rewrite -> comp_assoc, -> out_mapc.
1377
rewrite -> comp_assoc; trivial.
1378

    
1379
Qed.
1380

    
1381

    
1382

    
1383
Theorem proving_str2 : forall
1384
(x y z : Obj),
1385
  (ηv ∘ p_assoc1) § ∘ τv (x:=(x × y)) (y:=z) (a:=a) (b:=b) = 
1386
    τv ∘ (id ×× τv) ∘ p_assoc1.
1387

    
1388
Proof.
1389
intros.
1390
rewrite <- mapc_unfold.
1391

    
1392
assert (H_main: τv (x:=(x × y)) (y:=z) (a:=a) (b:=b) 
1393
            = mapc p_assoc2 ∘ (τv ∘ (id ×× τv)) ∘ p_assoc1).
1394
symmetry.
1395
apply strength2.
1396
rewrite ->2 comp_assoc, -> out_mapc.
1397
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> strength1.
1398
rewrite <- comp_assoc with (f':=id ×× τv), -> prodhom_comp, -> id_l.
1399
rewrite -> strength1.
1400
rewrite ->3 comp_assoc, -> map_comp.
1401
rewrite -> coprodhom_comp, -> id_l, -> cont_comp.
1402

    
1403
rewrite <- comp_assoc with (g':=τ).
1404
assert (aux1: map (id ×× (((id ⊕⊕ cont τv) ∘ δ))) ∘ τ ∘ (id ×× (τ ∘ (id ×× out)))
1405
        = (τ ∘ (id (a:=x) ×× ((map (id ⊕⊕ cont τv) ∘ map δ) ∘ τ) ∘ (id (a:=y) ×× out (x:=z) (a:=a) (b:=b))))).
1406
rewrite -> map_comp.
1407
rewrite <- id_l with (f':=id), <-2 comp_assoc.
1408
rewrite <- prodhom_comp with (h:=map ((id ⊕⊕ cont τv) ∘ δ)).
1409
rewrite ->2 comp_assoc, <- str_map.
1410
rewrite -> id_l; trivial.
1411
rewrite <- aux1; clear aux1.
1412

    
1413
rewrite <-6 comp_assoc.
1414
assert (aux2: map p_assoc1 ∘ τ ∘ (id ×× out) = τ ∘ ((id ×× τ ∘ (id ×× out (x:=z) (a:=a) (b:=b))) ∘ p_assoc1 (a:=x) (b:=y))).
1415
rewrite -> str2.
1416
unfold p_assoc1.
1417
rewrite <- comp_assoc with (g':=id ×× τ), -> prodhom_pair, -> id_r.
1418
rewrite -> prodhom_pair, -> id_r.
1419
rewrite <- comp_assoc with (g':=id ×× out), -> prodhom_pair, -> id_r.
1420
rewrite <- comp_assoc, -> pair_f.
1421
rewrite <- comp_assoc, -> pr1_prodhom, -> id_r.
1422
rewrite <- comp_assoc, -> pair_f.
1423
rewrite <- comp_assoc, -> pr1_prodhom, -> id_r.
1424
rewrite -> pr2_prodhom.
1425
trivial.
1426
rewrite <- aux2; clear aux2.
1427

    
1428
rewrite -> comp_assoc, -> map_comp.
1429
rewrite -> comp_assoc, -> map_comp.
1430
rewrite ->2 comp_assoc, -> map_comp.
1431
rewrite <- comp_assoc with (g':=δ), <-3 comp_assoc with (f':=p_assoc1).
1432

    
1433
assert (aux3: (p_assoc1 ⊕⊕ (id ×× ((id ×× τv) ∘ p_assoc1) ^^ id)) ∘ δ
1434
         = δ ∘ ((id ×× (id ⊕⊕ cont (τv  (y:=z) (a:=a) (b:=b))) ∘ δ (a:=a) (b:=b) (y:=z)) ∘ p_assoc1 (a:=x) (b:=y))).
1435
rewrite -> comp_assoc.
1436
symmetry.
1437
rewrite <- id_l with (f':=id).
1438
rewrite <- prodhom_comp.
1439
rewrite -> comp_assoc.
1440
rewrite <- delta.
1441
rewrite -> prodhom_id.
1442
rewrite <-2 comp_assoc, <- p_assoc_delta.
1443
rewrite -> comp_assoc, -> coprodhom_comp, -> id_r.
1444
rewrite -> cont_comp, -> id_l.
1445
unfold cont.
1446
trivial.
1447
rewrite <- aux3; clear aux3.
1448

    
1449
rewrite ->3 comp_assoc, -> coprodhom_comp.
1450
rewrite -> p_assoc_id2.
1451
unfold cont.
1452
rewrite -> prodhom_comp, -> id_l.
1453
rewrite -> post_comp_comp.
1454
rewrite -> map_comp.
1455
rewrite ->3 comp_assoc;trivial.
1456

    
1457
rewrite -> H_main.
1458
rewrite ->2 comp_assoc, -> mapc_comp.
1459
rewrite -> p_assoc_id1.
1460
rewrite -> mapc_id, -> id_r.
1461
trivial.
1462
Qed.
1463

    
1464

    
1465

    
1466
Theorem proving_str3 :forall (x y : Obj),
1467
    τv (x:=x) (y:=y) (a:=a) (b:=b) ∘ (id ×× ηv) = ηv.
1468

    
1469
Proof.
1470
intros.
1471
symmetry.
1472
unfold ηv at 1.
1473
apply out_cong.
1474
rewrite ->2 comp_assoc; rewrite -> out_tuo_is_id; rewrite -> id_r.
1475
rewrite -> comp_assoc; rewrite -> strength1.
1476

    
1477
assert (aux: τ ∘ ((id ×× out) ∘ (id (a:=x) ×× ηv (a:=a) (b:=b) (x:=y))) = η ∘ (id ×× inl)).
1478
rewrite -> prodhom_comp; rewrite -> id_l; rewrite -> out_unitcofree.
1479
rewrite <- id_r with (f':=id) at 1; rewrite <- prodhom_comp with (g:=id); rewrite -> comp_assoc.
1480
rewrite -> str3.
1481
trivial.
1482
rewrite <- comp_assoc with (f':=id ×× ηv); rewrite <- comp_assoc with (g':=τ); rewrite -> aux; clear aux.
1483

    
1484
rewrite <- map_unit with (f:=id ×× inl).
1485
rewrite -> comp_assoc; rewrite <- comp_assoc with (g':=map δ); rewrite -> map_comp.
1486
unfold δ.
1487
rewrite <- comp_assoc with (g':=dist2), -> dist2_inl.
1488
rewrite -> coprodhom_inl, -> id_l.
1489
rewrite -> map_comp; rewrite -> coprodhom_inl; rewrite -> id_l.
1490
rewrite -> map_unit; trivial.
1491

    
1492
Qed.
1493

    
1494

    
1495

    
1496
Theorem proving_str4 : forall x y z (f: x ~> (coext T a b y)),
1497
    (τv ∘ (id ×× f)) § ∘ τv = τv ∘ (id (a:=z) ×× f §).
1498

    
1499
Proof.
1500
intros.
1501

    
1502
set (g:=[f,ηv]).
1503

    
1504
assert (H1: id = g § ∘ mapc inr).
1505
unfold g.
1506
rewrite -> liftingcofree_mapc.
1507
rewrite -> cpr_inr.
1508
rewrite -> proving_kl1.
1509
trivial.
1510

    
1511
assert (H2: f = g ∘ inl).
1512
unfold g; rewrite -> cpr_inl; trivial.
1513

    
1514

    
1515
assert (H_main: (τv ∘ (id ×× g)) § ∘ τv = τv ∘ (id (a:=z) ×× g §)).
1516

    
1517
transitivity (coit ((map δ) ∘ τ ∘ (id (a:=z) ×× [map (id ⊕⊕ cont (mapc inr)) ∘ out ∘ g, η ∘ inr]* ∘ out))).
1518

    
1519
apply coit2.
1520

    
1521
set (h:=map (id ⊕⊕ cont (mapc (inr (a:=x)))) ∘ out ∘ g).
1522

    
1523
assert (aux1: [(map δ) ∘ τ ∘ (id ×× h), η ∘ inr] * ∘ (map δ) = (map δ) ∘ (τ ∘ (id (a:=z) ×× [h, η ∘ inr]))*).
1524
unfold δ at 2.
1525
rewrite -> lifting_map.
1526
rewrite -> comp_assoc.
1527
rewrite -> cpr_coprodhom.
1528
rewrite -> id_l.
1529

    
1530
rewrite -> map_lifting.
1531
apply f_equal1.
1532

    
1533
assert (aux2: η ∘ δ  ∘  (id ×× inr (a:=y)) = 
1534
(η ∘ inr) ∘ (pair (pr1 ∘ pr2) (curry (pair (pr1 ∘ pr1) 
1535
(uncurry (b:=b) (c:=coext T a b (x ⊕ y)) (pr2 (a:=a) ∘ pr2 (a:=z))))))).
1536
unfold δ.
1537
rewrite <-2 comp_assoc, -> dist2_inr.
1538
rewrite -> coprodhom_inr.
1539
rewrite <- comp_assoc; trivial.
1540
rewrite <- aux2; clear aux2.
1541

    
1542
rewrite <- map_unit.
1543
rewrite <- str3.
1544
rewrite <-2 comp_assoc with (f':=id ×× inr).
1545
rewrite -> prodhom_comp, -> id_l.
1546
unfold dist2.
1547
rewrite -> comp_assoc, <- uncurry2.
1548
rewrite -> f_cpr.
1549
rewrite ->2 curry2.
1550
rewrite -> comp_assoc, -> cpr_inl.
1551
rewrite -> comp_assoc, -> cpr_inr.
1552
apply swapp_switch.
1553
apply curry_cong.
1554
rewrite -> curry_uncurry.
1555
case_distinction.
1556
rewrite -> cpr_inl.
1557
rewrite -> curry1.
1558
rewrite <- comp_assoc with (g':=swapp), -> swap_prodhom.
1559
rewrite -> comp_assoc with (f':=swapp), <-2 comp_assoc with (f':=id ×× inl), -> prodhom_comp.
1560
rewrite -> cpr_inl, -> id_l.
1561
rewrite -> comp_assoc; trivial.
1562
rewrite -> cpr_inr.
1563
rewrite -> curry1.
1564
rewrite <- comp_assoc with (g':=swapp), -> swap_prodhom.
1565
rewrite -> comp_assoc with (f':=swapp), <-2 comp_assoc with (f':=id ×× inr), -> prodhom_comp.
1566
rewrite -> cpr_inr, -> id_l.
1567
rewrite -> comp_assoc; trivial.
1568

    
1569
rewrite <- comp_assoc with (g':=τ).
1570
assert (aux3: (τ ∘ (id ×× [h, η ∘ inr])) * ∘ τ ∘ (id ×× out) = τ ∘ (id (a:=z) ×× ([h, η ∘ inr]) * ∘ out)).
1571
rewrite -> str4.
1572
rewrite <- comp_assoc.
1573
rewrite -> prodhom_comp.
1574
rewrite -> id_l; trivial.
1575
rewrite <- aux3; clear aux3.
1576

    
1577
rewrite ->2 comp_assoc with (h':=map δ).
1578
rewrite <- aux1; clear aux1.
1579

    
1580
unfold h.
1581
rewrite <- comp_assoc with (h':=map δ).
1582
assert (aux4: (id ×× (map (id ⊕⊕ cont (mapc inr)))) ∘ (id ×× (out ∘ g)) = id (a:=z) ×× (map (id ⊕⊕ cont (mapc (inr (a:=x)))) ∘ out) ∘ g).
1583
rewrite -> prodhom_comp, -> id_l.
1584
rewrite -> comp_assoc; trivial.
1585
rewrite <- aux4; clear aux4.
1586

    
1587
rewrite -> comp_assoc with (h':=τ), <- str_map.
1588
rewrite ->2 comp_assoc with (h':=map δ), -> map_comp.
1589
rewrite <- delta.
1590
rewrite -> prodhom_id.
1591
rewrite ->4 comp_assoc, -> map_lifting.
1592
rewrite -> f_cpr.
1593
rewrite ->2 comp_assoc, -> map_comp.
1594
rewrite -> comp_assoc with (g':=η), -> map_unit.
1595
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr.
1596

    
1597
assert (aux5: (id ⊕⊕ cont ((τv ∘ (id ×× (g ∘ inr))) § ∘ τv)) = (id ⊕⊕ cont ((τv ∘ (id ×× g)) § ∘ τv)) ∘ ((id (a:=(z × y)) ⊕⊕ cont (a:=a) (b:=b) (id (a:=z) ×× mapc inr)))).
1598
rewrite -> coprodhom_comp, -> id_l, -> cont_comp.
1599
rewrite <- comp_assoc, -> naturality_τv.
1600
rewrite -> comp_assoc, -> liftingcofree_mapc.
1601
rewrite <- comp_assoc, -> prodhom_comp, -> id_l.
1602
trivial.
1603
rewrite ->2 comp_assoc.
1604
rewrite <- aux5; clear aux5.
1605

    
1606
symmetry; unfold g at 1; symmetry.
1607
rewrite -> cpr_inr.
1608
rewrite -> proving_str3.
1609
rewrite -> proving_kl1, -> id_r.
1610

    
1611
rewrite -> lifting1.
1612
rewrite <- comp_assoc, -> strength1.
1613
rewrite ->3 comp_assoc, -> lifting_map.
1614
rewrite -> cpr_coprodhom, -> id_l.
1615
rewrite -> comp_assoc, -> strength1.
1616
rewrite <- comp_assoc with (g':=id ×× out), -> prodhom_comp, -> id_l.
1617
rewrite -> map_comp.
1618
rewrite <- comp_assoc with (f':=cont τv), -> cont_comp.
1619
trivial.
1620

    
1621

    
1622

    
1623
unfold τv.
1624
apply fusion.
1625
rewrite ->2 comp_assoc, -> map_comp.
1626
rewrite <- comp_assoc with (f':=(id ×× g §)), -> prodhom_comp, -> id_l.
1627
rewrite -> lifting1.
1628
rewrite <- prodhom_id.
1629
rewrite -> delta.
1630
rewrite <-2 comp_assoc with (g':=τ).
1631

    
1632
assert (aux6: id ×× ([out ∘ g, η ∘ inr ∘ cont (g §)]) * ∘ out = 
1633
       (id ×× ([out ∘ g, η ∘ inr ∘ cont (g §)]) *) ∘ (id (a:=z) ×× out)).
1634
rewrite -> prodhom_comp, -> id_l.
1635
trivial.
1636
rewrite -> aux6; clear aux6.
1637

    
1638
assert (aux7: id ×× ([(map (id ⊕⊕ cont (mapc inr)) ∘ out) ∘ g, η ∘ inr]) * ∘ out = 
1639
       (id ×× ([(map (id ⊕⊕ cont (mapc inr)) ∘ out) ∘ g, η ∘ inr]) *) ∘ (id (a:=z) ×× out)).
1640
rewrite -> prodhom_comp, -> id_l.
1641
trivial.
1642
rewrite -> aux7; clear aux7.
1643

    
1644
rewrite ->2 comp_assoc with (h':=τ), <-2 str4.
1645
rewrite ->4 comp_assoc;
1646
apply f_equal2;trivial.
1647
apply f_equal2;trivial.
1648
rewrite ->2 map_lifting.
1649
apply f_equal1.
1650
rewrite <- map_comp, <- comp_assoc with (h':=map δ).
1651
apply f_equal2;trivial.
1652
rewrite -> comp_assoc, -> str_map, <- comp_assoc with (h':=τ).
1653
apply f_equal2;trivial.
1654
rewrite -> prodhom_comp, -> id_l.
1655
apply f_equal2;trivial.
1656
rewrite -> f_cpr.
1657
rewrite ->2 comp_assoc, -> map_comp.
1658
rewrite -> coprodhom_comp.
1659
rewrite -> cont_comp, -> id_l.
1660
rewrite -> comp_assoc, -> map_unit.
1661
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr.
1662
rewrite -> comp_assoc; apply f_equal2;trivial.
1663
rewrite <- H1.
1664
rewrite -> cont_id.
1665
rewrite -> coprodhom_id.
1666
rewrite -> map_id, -> id_r.
1667
trivial.
1668

    
1669

    
1670
rewrite -> H2.
1671
rewrite <- id_l with (f':=id) at 1.
1672
rewrite <- prodhom_comp.
1673
rewrite -> comp_assoc, <- liftingcofree_mapc.
1674
rewrite <- comp_assoc, <- naturality_τv.
1675
rewrite -> comp_assoc, -> H_main.
1676
rewrite <- comp_assoc, -> prodhom_comp, -> id_l.
1677
rewrite -> liftingcofree_mapc.
1678
trivial.
1679

    
1680
Qed.
1681

    
1682

    
1683

    
1684
(* --- *)
1685

    
1686

    
1687

    
1688
Theorem proving_strength_iteration_guarded : forall x y z (f: x ~> coext T a b (y ⊕ x)), 
1689
guarded f ->
1690
    τv ∘ (id ×× f †') = (mapc dist2 ∘ τv ∘ (id (a:=z) ×× f)) †'.
1691

    
1692
Proof.
1693
intros.
1694
unfold guarded in H.
1695
inversion H as [u' H'].
1696

    
1697
apply unfolding_guarded2.
1698
unfold guarded.
1699
exists (map (id ⊕⊕ cont (mapc dist2 ∘ τv)) ∘ map δ ∘ τ ∘ (id ×× u')).
1700
rewrite ->5 comp_assoc.
1701
rewrite ->2 map_comp.
1702
rewrite -> out_mapc.
1703
rewrite -> coprodhom_comp, -> id_l, -> id_r.
1704
rewrite <- comp_assoc with (g':=out), -> strength1.
1705
rewrite <-2 comp_assoc with (f':=id ×× f), -> prodhom_comp.
1706
rewrite -> H'.
1707
rewrite <- prodhom_comp.
1708
rewrite ->3 comp_assoc; apply f_equal2;trivial.
1709
rewrite -> comp_assoc, ->2 map_comp.
1710
rewrite -> coprodhom_comp, -> id_l.
1711
rewrite -> cont_comp.
1712
rewrite <- comp_assoc, <- str_map.
1713
rewrite -> comp_assoc; apply f_equal2;trivial.
1714
rewrite -> map_comp; apply f_equal1.
1715
rewrite <- cont_id.
1716
rewrite <- comp_assoc, <- delta.
1717
rewrite -> prodhom_id.
1718
rewrite -> cont_id.
1719
rewrite -> comp_assoc with (g':=(id ×× inl ⊕⊕ id)), -> coprodhom_comp, -> id_l.
1720
apply f_equal2;trivial.
1721
apply f_equal2;trivial.
1722
apply dist2_inl.
1723

    
1724

    
1725
rewrite <- proving_unfolding at 1.
1726
rewrite <- id_l with (f':=id) at 1.
1727
rewrite <- prodhom_comp.
1728
rewrite -> comp_assoc, <- proving_str4.
1729

    
1730
assert (aux: ([ηv, τv ∘ (id ×× f †')]) ∘ dist2 = τv ∘ (id (a:=z) ×× [ηv, f †'])).
1731
unfold dist2.
1732
rewrite -> comp_assoc, <- uncurry2.
1733
rewrite -> f_cpr.
1734
rewrite ->2 curry2.
1735
rewrite -> comp_assoc, -> cpr_inl.
1736
rewrite -> comp_assoc, -> cpr_inr.
1737
apply swapp_switch.
1738
apply curry_cong.
1739
rewrite -> curry_uncurry.
1740
case_distinction.
1741
rewrite -> cpr_inl.
1742
rewrite -> curry1.
1743
rewrite <- comp_assoc with (g':=swapp), -> swap_prodhom.
1744
rewrite -> comp_assoc with (g':=id ×× inl), <- comp_assoc with (f':=id ×× inl), -> prodhom_comp.
1745
rewrite -> cpr_inl, -> id_l.
1746
rewrite -> proving_str3.
1747
trivial.
1748
rewrite -> cpr_inr.
1749
rewrite -> curry1.
1750
rewrite <- comp_assoc with (g':=swapp), -> swap_prodhom.
1751
rewrite -> comp_assoc with (g':=id ×× inr), <- comp_assoc with (f':=id ×× inr), -> prodhom_comp.
1752
rewrite -> cpr_inr, -> id_l.
1753
trivial.
1754
rewrite <- aux; clear aux.
1755

    
1756

    
1757
rewrite <- liftingcofree_mapc.
1758
rewrite ->2 comp_assoc.
1759
trivial.
1760
Qed.
1761

    
1762

    
1763

    
1764
Theorem proving_strength_iteration : forall x y (f: x ~> coext T a b (y ⊕ x)), 
1765
    τv ∘ (id ×× f †') = ((ηv ∘ dist2) § ∘ τv ∘ (id (a:=x) ×× f)) †'.
1766

    
1767
Proof.
1768
intros.
1769
rewrite <- mapc_unfold.
1770

    
1771

    
1772
rewrite -> itercofree_triangle.
1773

    
1774
rewrite -> proving_strength_iteration_guarded.
1775

    
1776
symmetry; rewrite -> itercofree_triangle; symmetry.
1777

    
1778

    
1779
apply f_equal1.
1780
unfold triangle.
1781

    
1782
rewrite <- id_l with (f':=id).
1783
rewrite <- comp_assoc with (h':=tuo), <- prodhom_comp, -> id_l, -> comp_assoc.
1784

    
1785

    
1786
assert (bottom_triangle: tuo ∘ map (dist2 ⊕⊕ cont (mapc dist2 ∘ τv)) ∘ map δ ∘ τ
1787
 = mapc (dist2 (x:=x) (y:=y)) ∘ τv ∘ (id (a:=x) ×× tuo (a:=a) (b:=b))).
1788
symmetry.
1789

    
1790
assert (aux2: τv (x:=x) (y:=(y ⊕ x)) (a:=a) (b:=b) = tuo ∘ map (id ⊕⊕ cont τv) ∘ map δ ∘ τ ∘ (id ×× out)).
1791
apply out_cong.
1792
rewrite -> strength1.
1793
rewrite ->4 comp_assoc with (h':=out).
1794
rewrite -> out_tuo_is_id, -> id_r.
1795
trivial.
1796
rewrite -> aux2 at 1; clear aux2.
1797

    
1798
rewrite <-2 comp_assoc with (f':=id ×× tuo), -> prodhom_comp, -> id_r.
1799
rewrite -> out_tuo_is_id, -> prodhom_id, -> id_l.
1800

    
1801
apply out_cong.
1802
rewrite ->7 comp_assoc.
1803
rewrite -> out_tuo_is_id, -> id_r.
1804
rewrite -> out_mapc.
1805
rewrite <- comp_assoc with (g':=out), -> out_tuo_is_id, -> id_l.
1806
rewrite -> map_comp.
1807
rewrite -> coprodhom_comp, -> id_l.
1808
rewrite -> cont_comp.
1809
trivial.
1810
rewrite <- bottom_triangle.
1811

    
1812
assert (aux3: (id ×× map (inl ⊕⊕ id)) ∘ (id ×× ((π ∘ out) ∘ f) †)
1813
  = id (a:=x) ×× map (inl (b:=x) ⊕⊕ id) ∘ ((π ∘ out) ∘ f) †).
1814
rewrite -> prodhom_comp.
1815
rewrite -> id_l.
1816
trivial.
1817
rewrite <- aux3; clear aux3.
1818

    
1819
rewrite -> comp_assoc with (g':=id ×× map (inl ⊕⊕ id)).
1820
rewrite <-5 comp_assoc with (h':=tuo).
1821
apply f_equal2; trivial.
1822

    
1823

    
1824
assert (middle_square: map (inl ⊕⊕ id) ∘ map (id ⊕⊕ cont (mapc dist2 ∘ τv)) ∘ map δ ∘ τ =
1825
  map (dist2 ⊕⊕ cont (mapc (dist2 (x:=x) (y:=y)) ∘ τv (a:=a) (b:=b))) ∘ map (δ (a:=a) (b:=b)) ∘ τ ∘ (id (a:=x) ×× map (inl (a:=y) (b:=x) ⊕⊕ id))).
1826
rewrite <- comp_assoc with (g':=τ), <- str_map.
1827
rewrite <-2 comp_assoc with (g':=map δ).
1828
rewrite -> comp_assoc with (h':=map δ), -> map_comp with (g:=id ×× (inl ⊕⊕ id)), <-2 cont_id.
1829
rewrite <- delta.
1830
rewrite -> prodhom_id.
1831
rewrite ->2 cont_id.
1832
rewrite ->2 comp_assoc, ->3 map_comp.
1833
rewrite -> comp_assoc, ->2 coprodhom_comp, ->2 id_l, -> id_r.
1834
rewrite -> dist2_inl.
1835
trivial.
1836
rewrite <- middle_square.
1837

    
1838
rewrite <- comp_assoc with (f':=map δ), -> map_comp.
1839

    
1840
set (p:= (id ⊕⊕ cont (mapc dist2 ∘ τv)) ∘ δ).
1841

    
1842
rewrite <-2 comp_assoc with (h':=map (inl ⊕⊕ id)).
1843
apply f_equal2; trivial.
1844

    
1845
(* top triangle *)
1846
rewrite <- comp_assoc, -> strength_iteration.
1847
rewrite -> map_naturality.
1848

    
1849
assert (aux4: (id ×× π) ∘ (id ×× out) ∘ (id ×× f) 
1850
  = id (a:=x) ×× (π ∘ out) ∘ f).
1851
rewrite ->2 prodhom_comp.
1852
rewrite ->2 id_l.
1853
trivial.
1854
rewrite <- aux4; clear aux4.
1855

    
1856
unfold π.
1857
rewrite <- comp_assoc with (g':=τ), ->2 comp_assoc with (h':=τ), <- str_map.
1858
rewrite -> comp_assoc, -> map_comp.
1859
rewrite ->3 comp_assoc, -> map_comp.
1860
apply f_equal1.
1861
rewrite <- comp_assoc with (g':=out), ->2 comp_assoc with (h':=out), -> out_mapc.
1862
rewrite ->3 comp_assoc, -> map_comp.
1863
apply f_equal2; trivial.
1864
rewrite <- comp_assoc with (g':=out), -> strength1.
1865
rewrite -> comp_assoc with (f':=id ×× out);apply f_equal2; trivial.
1866
rewrite -> comp_assoc with (f':=τ); apply f_equal2; trivial.
1867
rewrite ->2 map_comp.
1868
apply f_equal1.
1869
rewrite <- comp_assoc with (g':=dist2 ⊕⊕ cont (mapc dist2)), -> comp_assoc with (g':=id ⊕⊕ cont τv),
1870
  -> coprodhom_comp.
1871
rewrite -> cont_comp, -> id_l.
1872
rewrite -> comp_assoc, -> cpr_coprodhom.
1873
unfold δ.
1874
rewrite -> comp_assoc, -> cpr_coprodhom, -> id_l.
1875
unfold dist2 at 4.
1876
rewrite -> comp_assoc, <- uncurry2, -> f_cpr.
1877
rewrite ->2 curry2.
1878
rewrite -> comp_assoc, -> cpr_inl.
1879
rewrite -> comp_assoc, -> cpr_inr.
1880
symmetry; apply swapp_switch; symmetry.
1881
apply curry_cong.
1882
rewrite -> curry_uncurry.
1883

    
1884
case_distinction.
1885

    
1886
rewrite -> cpr_inl.
1887
rewrite -> curry1.
1888
rewrite <- comp_assoc, -> swap_prodhom.
1889
rewrite -> comp_assoc with (f':=swapp), <- comp_assoc with (f':=id ×× inl), -> prodhom_comp.
1890
rewrite -> cpr_inl, -> id_l.
1891
rewrite <- comp_assoc with (g':=dist2), <- naturality_dist2.
1892
rewrite -> comp_assoc, -> coprodhom_comp.
1893
rewrite -> prodhom_id, -> id_l.
1894
apply f_equal1.
1895
apply f_equal2;trivial.
1896
apply f_equal2;trivial.
1897
apply f_equal2;trivial.
1898
unfold p.
1899
unfold δ.
1900
rewrite <-2 comp_assoc.
1901
rewrite -> dist2_inl.
1902
rewrite -> coprodhom_inl, -> id_l.
1903
rewrite -> coprodhom_inl, -> id_l.
1904
trivial.
1905

    
1906
rewrite -> cpr_inr.
1907
rewrite -> curry1, <- comp_assoc.
1908
rewrite -> swap_prodhom.
1909
rewrite -> comp_assoc with (f':=swapp), <- comp_assoc with (f':=id ×× inr), -> prodhom_comp.
1910
rewrite -> cpr_inr.
1911
rewrite <- prodhom_comp.
1912
rewrite <- comp_assoc with (g':=dist2), -> comp_assoc with (h':=dist2), -> dist2_inl.
1913
rewrite -> comp_assoc, -> coprodhom_inl.
1914
apply f_equal1.
1915
apply f_equal2;trivial.
1916
rewrite <-3 comp_assoc; apply f_equal2;trivial.
1917
unfold p.
1918
unfold δ.
1919
rewrite ->2 comp_assoc, -> coprodhom_comp, -> id_l.
1920
rewrite <- comp_assoc, -> dist2_inr.
1921
rewrite -> coprodhom_inr, -> comp_assoc.
1922
trivial.
1923

    
1924
apply guardedtriangle_def.
1925

    
1926
Qed.
1927

    
1928

    
1929

    
1930
(* incorporate parameters a, b into definitions for the instance declaration;
1931
   this doesn't change the significance of the proofs established above *)
1932
Definition ηv' (x : Obj) :=
1933
ηv (x:=x) (a:=a) (b:=b).
1934

    
1935
Definition lifting_cofree' (x y : Obj) (f: x ~> coext T a b y) :=
1936
f §.
1937

    
1938
Definition iter_cofree' (x y : Obj) (f: x ~> coext T a b (y ⊕ x)) :=
1939
f †'.
1940

    
1941
Definition τv' (x y : Obj) := 
1942
τv (x:=x) (y:=y) (a:=a) (b:=b).
1943

    
1944

    
1945
(* Proof that a cofree extension is an ElgotMonad *)
1946
Instance cofree : ElgotMonad Obj Hom0 C (coext T a b) := {
1947
    η := ηv';
1948
    lifting := lifting_cofree';
1949
    iter := iter_cofree';
1950
    τ := τv'
1951
}.
1952

    
1953
Proof.
1954

    
1955
apply proving_kl1.
1956

    
1957
apply proving_kl2.
1958

    
1959
apply proving_kl3.
1960

    
1961
apply proving_str1.
1962

    
1963
apply proving_str2.
1964

    
1965
apply proving_str3.
1966

    
1967
apply proving_str4.
1968

    
1969
apply proving_unfolding.
1970

    
1971
apply proving_naturality.
1972

    
1973
apply proving_dinaturality.
1974

    
1975
apply proving_codiagonal.
1976

    
1977
apply proving_uniformity.
1978

    
1979
apply proving_strength_iteration.
1980

    
1981
Qed.
1982

    
1983
(*
1984
Print Assumptions cofree.
1985
*)
1986

    
1987

    
1988
End ContextCofreeElgotMonad.