1 (*********************************************************************************************************************************)
2 (* ProgrammingLanguageCategory *)
4 (* The category Types(L) *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import Categories_ch1_3.
12 Require Import InitialTerminal_ch2_2.
13 Require Import Functors_ch1_4.
14 Require Import Isomorphisms_ch1_5.
15 Require Import ProductCategories_ch1_6_1.
16 Require Import OppositeCategories_ch1_6_2.
17 Require Import Enrichment_ch2_8.
18 Require Import Subcategories_ch7_1.
19 Require Import NaturalTransformations_ch7_4.
20 Require Import NaturalIsomorphisms_ch7_5.
21 Require Import BinoidalCategories.
22 Require Import PreMonoidalCategories.
23 Require Import MonoidalCategories_ch7_8.
24 Require Import Coherence_ch7_8.
25 Require Import Enrichment_ch2_8.
26 Require Import RepresentableStructure_ch7_2.
27 Require Import FunctorCategories_ch7_7.
29 Require Import NaturalDeduction.
30 Require Import ProgrammingLanguage.
31 Export ProgrammingLanguage.
33 Require Import NaturalDeductionCategory.
36 (* I am at a loss to explain why "auto" can't handle this *)
39 | [ |- NDPredicateClosure ?P (?A ;; ?B) ] => apply ndpc_comp; ndpc_tac
40 | [ |- NDPredicateClosure ?P (?A ** ?B) ] => apply ndpc_prod; ndpc_tac
44 (* this tactical searches the environment; setoid_rewrite doesn't seem to be able to do that properly sometimes *)
45 Ltac nd_swap_ltac P EQV :=
47 [ |- context [ (?F ** nd_id _) ;; (nd_id _ ** ?G) ] ] =>
48 set (@nd_swap _ _ EQV _ _ _ _ F G) as P
51 (* I still wish I knew why "Hint Constructors" doesn't work *)
52 Hint Extern 5 => apply snd_inert_initial.
53 Hint Extern 5 => apply snd_inert_cut.
54 Hint Extern 5 => apply snd_inert_structural.
55 Hint Extern 5 => apply cnd_inert_initial.
56 Hint Extern 5 => apply cnd_inert_cut.
57 Hint Extern 5 => apply cnd_inert_structural.
58 Hint Extern 5 => apply cnd_inert_cnd_ant_assoc.
59 Hint Extern 5 => apply cnd_inert_cnd_ant_cossa.
60 Hint Extern 5 => apply cnd_inert_cnd_ant_cancell.
61 Hint Extern 5 => apply cnd_inert_cnd_ant_cancelr.
62 Hint Extern 5 => apply cnd_inert_cnd_ant_llecnac.
63 Hint Extern 5 => apply cnd_inert_cnd_ant_rlecnac.
64 Hint Extern 5 => apply cnd_inert_se_expand_left.
65 Hint Extern 5 => apply cnd_inert_se_expand_right.
67 Hint Extern 2 (@Structural _ _ _ _ (@nd_id _ _ [] )) => simpl; auto.
68 Hint Extern 2 (@Structural _ _ _ _ (@nd_id _ _ [ _ ])) => simpl; auto.
70 Section ProgrammingLanguageCategory.
72 Context {T : Type}. (* types of the language *)
74 Context {Rule : Tree ??(@PLJudg T) -> Tree ??(@PLJudg T) -> Type}.
75 Notation "cs |= ss" := (@sequent T cs ss) : pl_scope.
77 Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope.
83 Context (PL:@ProgrammingLanguage T Rule).
85 (* category of judgments in a fixed type/coercion context *)
86 Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv.
88 Definition JudgmentsL := Judgments_cartesian.
90 Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
95 Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
100 Instance TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]) :=
101 { eid := identityProof
104 intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
105 intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
106 abstract (intros; unfold identityProof; unfold cutProof; simpl; eapply cndr_inert; auto; apply PL).
107 abstract (intros; unfold identityProof; unfold cutProof; simpl; eapply cndr_inert; auto; apply PL).
108 abstract (intros; unfold identityProof; unfold cutProof; simpl; eapply cndr_inert;
109 [ apply PL | idtac | idtac ]; apply ndpc_comp; auto).
112 Instance Types_first c : EFunctor TypesL TypesL (fun x => x,,c ) :=
113 { efunc := fun x y => cnd_expand_right(ContextND:=pl_cnd) x y c }.
114 intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
115 abstract (intros; simpl; apply (cndr_inert pl_cnd); auto).
116 abstract (intros; unfold ehom; unfold comp; simpl; unfold cutProof;
117 rewrite <- (@ndr_prod_preserves_comp _ _ PL _ _ (cnd_expand_right _ _ c) _ _ (nd_id1 (b|=c0))
118 _ (nd_id1 (a,,c |= b,,c)) _ (cnd_expand_right _ _ c));
119 setoid_rewrite (@ndr_comp_right_identity _ _ PL _ [a,, c |= b,, c]);
120 setoid_rewrite (@ndr_comp_left_identity _ _ PL [b |= c0]);
121 simpl; eapply cndr_inert; [ apply PL | auto | auto ]).
124 Instance Types_second c : EFunctor TypesL TypesL (fun x => c,,x) :=
125 { efunc := fun x y => ((@cnd_expand_left _ _ _ _ _ _ x y c)) }.
126 intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
127 abstract (intros; simpl; apply (cndr_inert pl_cnd); auto).
128 intros; unfold ehom; unfold comp; simpl; unfold cutProof;
129 abstract (rewrite <- (@ndr_prod_preserves_comp _ _ PL _ _ (cnd_expand_left _ _ c) _ _ (nd_id1 (b|=c0))
130 _ (nd_id1 (c,,a |= c,,b)) _ (cnd_expand_left _ _ c));
131 setoid_rewrite (@ndr_comp_right_identity _ _ PL _ [c,,a |= c,,b]);
132 setoid_rewrite (@ndr_comp_left_identity _ _ PL [b |= c0]);
133 simpl; eapply cndr_inert; [ apply PL | auto | auto ]).
136 Instance Types_binoidal : EBinoidalCat TypesL (@T_Branch _) :=
137 { ebc_first := Types_first
138 ; ebc_second := Types_second
141 Instance Types_assoc_iso a b c : Isomorphic(C:=TypesL) ((a,,b),,c) (a,,(b,,c)) :=
142 { iso_forward := snd_initial _ ;; cnd_ant_cossa _ a b c
143 ; iso_backward := snd_initial _ ;; cnd_ant_assoc _ a b c
145 abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
146 abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
149 Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a :=
150 { iso_forward := snd_initial _ ;; cnd_ant_rlecnac _ a
151 ; iso_backward := snd_initial _ ;; cnd_ant_cancelr _ a
153 abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
154 abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
157 Instance Types_cancell_iso a : Isomorphic(C:=TypesL) ([],,a) a :=
158 { iso_forward := snd_initial _ ;; cnd_ant_llecnac _ a
159 ; iso_backward := snd_initial _ ;; cnd_ant_cancell _ a
161 abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
162 abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
165 Lemma coincide' : nd_llecnac === nd_rlecnac.
166 set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
167 set (isos_forward_equal_then_backward_equal _ _ q') as qq.
171 Lemma Types_assoc_lemma : ∀a b X Y : TypesL,
172 ∀f : X ~~{ TypesL }~~> Y,
173 #(Types_assoc_iso a X b) >>> (Types_first b >>>> Types_second a) \ f ~~
174 (Types_second a >>>> Types_first b) \ f >>> #(Types_assoc_iso a Y b).
185 repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
187 setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []).
188 setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []).
189 setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
190 setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
192 setoid_rewrite (@ndr_comp_associativity _ Rule PL).
193 setoid_rewrite (@ndr_comp_associativity _ Rule PL).
194 setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
196 set (ni_commutes' (jud_mon_cancelr PL) f) as q.
201 set (ni_commutes' (jud_mon_cancell PL) f) as q.
203 setoid_rewrite coincide' in q.
207 setoid_rewrite (@ndr_comp_associativity _ Rule PL).
208 apply ndr_comp_respects; try reflexivity.
210 apply (cndr_inert pl_cnd); auto; ndpc_tac; auto.
213 Instance Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a :=
214 { ni_iso := fun c => Types_assoc_iso a c b }.
215 apply Types_assoc_lemma.
218 Lemma Types_assoc_ll_lemma :
220 ∀f : X ~~{ TypesL }~~> Y,
221 #(Types_assoc_iso a b X) >>> (Types_second b >>>> Types_second a) \ f ~~
222 Types_second (a,, b) \ f >>> #(Types_assoc_iso a b Y).
233 setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []).
234 setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []).
235 setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
237 repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
238 setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
240 set (ni_commutes' (jud_mon_cancelr PL) f) as q.
246 set (ni_commutes' (jud_mon_cancell PL) f) as q.
248 set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
249 set (isos_forward_equal_then_backward_equal _ _ q') as qq.
251 setoid_rewrite qq in q.
255 setoid_rewrite (@ndr_comp_associativity _ Rule PL).
256 apply ndr_comp_respects; try reflexivity.
259 apply (cndr_inert pl_cnd); auto; ndpc_tac.
262 Instance Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a :=
263 { ni_iso := fun c => Types_assoc_iso a b c }.
264 apply Types_assoc_ll_lemma.
267 Lemma Types_assoc_rr_lemma :
269 ∀f : A ~~{ TypesL }~~> B,
270 #(Types_assoc_iso A a b) ⁻¹ >>> (Types_first a >>>> Types_first b) \ f ~~
271 Types_first (a,, b) \ f >>> #(Types_assoc_iso B a b) ⁻¹.
284 setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []).
285 setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []).
286 setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
288 repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
289 setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
291 set (ni_commutes' (jud_mon_cancelr PL) f) as q.
297 set (ni_commutes' (jud_mon_cancell PL) f) as q.
299 set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
300 set (isos_forward_equal_then_backward_equal _ _ q') as qq.
302 setoid_rewrite qq in q.
306 setoid_rewrite (@ndr_comp_associativity _ Rule PL).
307 apply ndr_comp_respects; try reflexivity.
310 apply (cndr_inert pl_cnd); auto; ndpc_tac.
313 Instance Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b :=
314 { ni_iso := fun c => iso_inv _ _ (Types_assoc_iso c a b) }.
315 apply Types_assoc_rr_lemma.
318 Lemma Types_cancelr_lemma :
320 ∀f : A ~~{ TypesL }~~> B,
321 #(Types_cancelr_iso A) >>> functor_id TypesL \ f ~~
322 Types_first [] \ f >>> #(Types_cancelr_iso B).
329 setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
330 repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
331 setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
333 set (ni_commutes' (jud_mon_cancelr PL) f) as q.
339 set (ni_commutes' (jud_mon_cancell PL) f) as q.
341 set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
342 set (isos_forward_equal_then_backward_equal _ _ q') as qq.
344 setoid_rewrite qq in q.
348 setoid_rewrite (@ndr_comp_associativity _ Rule PL).
349 apply ndr_comp_respects; try reflexivity.
352 apply (cndr_inert pl_cnd); auto; ndpc_tac.
355 Instance Types_cancelr : Types_first [] <~~~> functor_id _ :=
356 { ni_iso := Types_cancelr_iso }.
357 apply Types_cancelr_lemma.
360 Lemma Types_cancell_lemma :
362 ∀f : A ~~{ TypesL }~~> B,
363 #(Types_cancell_iso A) >>> functor_id TypesL \ f ~~
364 Types_second [] \ f >>> #(Types_cancell_iso B).
371 setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
372 repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
373 setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
375 set (ni_commutes' (jud_mon_cancelr PL) f) as q.
381 set (ni_commutes' (jud_mon_cancell PL) f) as q.
383 set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
384 set (isos_forward_equal_then_backward_equal _ _ q') as qq.
386 setoid_rewrite qq in q.
389 setoid_rewrite (@ndr_comp_associativity _ Rule PL).
391 apply ndr_comp_respects; try reflexivity.
394 apply (cndr_inert pl_cnd); auto; ndpc_tac.
397 Instance Types_cancell : Types_second [] <~~~> functor_id _ :=
398 { ni_iso := Types_cancell_iso }.
399 apply Types_cancell_lemma.
402 Lemma TypesL_assoc_central a b c : CentralMorphism(H:=Types_binoidal) #((Types_assoc a b) c).
404 apply Build_CentralMorphism.
414 setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []).
415 setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
416 repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
417 setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
419 set (ni_commutes' (jud_mon_cancelr PL) g) as q.
425 set (ni_commutes' (jud_mon_cancell PL) g) as q.
427 set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
428 set (isos_forward_equal_then_backward_equal _ _ q') as qq.
430 setoid_rewrite qq in q.
434 setoid_rewrite (@ndr_comp_associativity _ Rule PL).
435 apply ndr_comp_respects.
439 apply (cndr_inert pl_cnd); auto; ndpc_tac.
451 setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []).
452 setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
453 repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
454 setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
456 set (ni_commutes' (jud_mon_cancelr PL) g) as q.
462 set (ni_commutes' (jud_mon_cancell PL) g) as q.
464 set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
465 set (isos_forward_equal_then_backward_equal _ _ q') as qq.
467 setoid_rewrite qq in q.
471 setoid_rewrite (@ndr_comp_associativity _ Rule PL).
472 apply ndr_comp_respects.
476 apply (cndr_inert pl_cnd); auto; ndpc_tac.
479 Lemma TypesL_cancell_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancell a).
481 apply Build_CentralMorphism.
491 setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []).
492 setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
493 repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
494 setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
496 set (ni_commutes' (jud_mon_cancelr PL) g) as q.
502 set (ni_commutes' (jud_mon_cancell PL) g) as q.
504 set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
505 set (isos_forward_equal_then_backward_equal _ _ q') as qq.
507 setoid_rewrite qq in q.
511 setoid_rewrite (@ndr_comp_associativity _ Rule PL).
512 apply ndr_comp_respects.
516 apply (cndr_inert pl_cnd); auto; ndpc_tac.
528 setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []).
529 setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
530 repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
531 setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
533 set (ni_commutes' (jud_mon_cancelr PL) g) as q.
539 set (ni_commutes' (jud_mon_cancell PL) g) as q.
541 set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
542 set (isos_forward_equal_then_backward_equal _ _ q') as qq.
544 setoid_rewrite qq in q.
548 setoid_rewrite (@ndr_comp_associativity _ Rule PL).
549 apply ndr_comp_respects.
553 apply (cndr_inert pl_cnd); auto; ndpc_tac.
556 Lemma TypesL_cancelr_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancelr a).
558 apply Build_CentralMorphism.
568 setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []).
569 setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
570 repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
571 setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
573 set (ni_commutes' (jud_mon_cancelr PL) g) as q.
579 set (ni_commutes' (jud_mon_cancell PL) g) as q.
581 set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
582 set (isos_forward_equal_then_backward_equal _ _ q') as qq.
584 setoid_rewrite qq in q.
588 setoid_rewrite (@ndr_comp_associativity _ Rule PL).
589 apply ndr_comp_respects.
593 apply (cndr_inert pl_cnd); auto; ndpc_tac.
605 setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []).
606 setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
607 repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
608 setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
610 set (ni_commutes' (jud_mon_cancelr PL) g) as q.
616 set (ni_commutes' (jud_mon_cancell PL) g) as q.
618 set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
619 set (isos_forward_equal_then_backward_equal _ _ q') as qq.
621 setoid_rewrite qq in q.
625 setoid_rewrite (@ndr_comp_associativity _ Rule PL).
626 apply ndr_comp_respects.
630 apply (cndr_inert pl_cnd); auto; ndpc_tac.
633 Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
634 { pmon_assoc := Types_assoc
635 ; pmon_cancell := Types_cancell
636 ; pmon_cancelr := Types_cancelr
637 ; pmon_assoc_rr := Types_assoc_rr
638 ; pmon_assoc_ll := Types_assoc_ll
640 abstract (apply Build_Pentagon; intros; simpl; eapply cndr_inert; try apply PL; ndpc_tac).
641 abstract (apply Build_Triangle; intros; simpl; eapply cndr_inert; try apply PL; ndpc_tac).
642 intros; simpl; reflexivity.
643 intros; simpl; reflexivity.
644 apply TypesL_assoc_central.
645 apply TypesL_cancelr_central.
646 apply TypesL_cancell_central.
649 End ProgrammingLanguageCategory.