1 (*********************************************************************************************************************************)
2 (* NaturalDeduction: *)
4 (* Structurally explicit natural deduction proofs. *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import Categories_ch1_3.
12 Require Import Functors_ch1_4.
13 Require Import Isomorphisms_ch1_5.
14 Require Import ProductCategories_ch1_6_1.
15 Require Import OppositeCategories_ch1_6_2.
16 Require Import Enrichment_ch2_8.
17 Require Import Subcategories_ch7_1.
18 Require Import NaturalTransformations_ch7_4.
19 Require Import NaturalIsomorphisms_ch7_5.
20 Require Import MonoidalCategories_ch7_8.
21 Require Import Coherence_ch7_8.
22 Require Import Enrichment_ch2_8.
23 Require Import RepresentableStructure_ch7_2.
24 Require Import NaturalDeduction.
28 * Everything in the rest of this section is just groundwork meant to
29 * build up to the definition of the AcceptableLanguage class, which
30 * appears at the end of the section. References to "the instance"
31 * mean instances of that class. Think of this section as being one
32 * big Class { ... } definition, except that we declare most of the
33 * stuff outside the curly brackets in order to take advantage of
34 * Coq's section mechanism.
36 Section Acceptable_Language.
38 (* Formalized Definition 4.1.1, production $\tau$ *)
39 Context {T : Type}. (* types of the language *)
41 Inductive Sequent := sequent : Tree ??T -> Tree ??T -> Sequent.
42 Notation "cs |= ss" := (sequent cs ss) : al_scope.
43 (* Because of term irrelevance we need only store the *erased* (def
44 * 4.4) trees; for this reason there is no Coq type directly
45 * corresponding to productions $e$ and $x$ of 4.1.1, and TreeOT can
46 * be used for productions $\Gamma$ and $\Sigma$ *)
48 (* to do: sequent calculus equals natural deduction over sequents, theorem equals sequent with null antecedent, *)
50 Context {Rule : Tree ??Sequent -> Tree ??Sequent -> Type}.
52 Notation "H /⋯⋯/ C" := (ND Rule H C) : al_scope.
58 (* Formalized Definition 4.1
60 * Note that from this abstract interface, the terms (expressions)
61 * in the proof are not accessible at all; they don't need to be --
62 * so long as we have access to the equivalence relation upon
63 * proof-conclusions. Moreover, hiding the expressions actually
64 * makes the encoding in CiC work out easier for two reasons:
66 * 1. Because the denotation function is provided a proof rather
67 * than a term, it is a total function (the denotation function is
68 * often undefined for ill-typed terms).
70 * 2. We can define arr_composition of proofs without having to know how
71 * to compose expressions. The latter task is left up to the client
72 * function which extracts an expression from a completed proof.
74 * This also means that we don't need an explicit proof obligation for 4.1.2.
76 Class AcceptableLanguage :=
78 (* Formalized Definition 4.1: denotational semantics equivalence relation on the conclusions of proofs *)
79 { al_eqv : @ND_Relation Sequent Rule
80 where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2)
82 (* Formalized Definition 4.1.3; note that t here is either $\top$ or a single type, not a Tree of types;
83 * we rely on "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents)
84 * to generate the rest *)
85 ; al_reflexive_seq : forall t, Rule [] [t|=t]
87 (* these can all be absorbed into a separate "sequent calculus" presentation *)
88 ; al_ant_assoc : forall {a b c d}, Rule [(a,,b),,c|=d] [(a,,(b,,c))|=d]
89 ; al_ant_cossa : forall {a b c d}, Rule [a,,(b,,c)|=d] [((a,,b),,c)|=d]
90 ; al_ant_cancell : forall {a b }, Rule [ [],,a |=b] [ a |=b]
91 ; al_ant_cancelr : forall {a b }, Rule [a,,[] |=b] [ a |=b]
92 ; al_ant_llecnac : forall {a b }, Rule [ a |=b] [ [],,a |=b]
93 ; al_ant_rlecnac : forall {a b }, Rule [ a |=b] [ a,,[] |=b]
94 ; al_suc_assoc : forall {a b c d}, Rule [d|=(a,,b),,c] [d|=(a,,(b,,c))]
95 ; al_suc_cossa : forall {a b c d}, Rule [d|=a,,(b,,c)] [d|=((a,,b),,c)]
96 ; al_suc_cancell : forall {a b }, Rule [a|=[],,b ] [a|= b ]
97 ; al_suc_cancelr : forall {a b }, Rule [a|=b,,[] ] [a|= b ]
98 ; al_suc_llecnac : forall {a b }, Rule [a|= b ] [a|=[],,b ]
99 ; al_suc_rlecnac : forall {a b }, Rule [a|= b ] [a|=b,,[] ]
101 ; al_horiz_expand_left : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma]
102 ; al_horiz_expand_right : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau]
104 (* these are essentially one way of formalizing
105 * "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents) *)
106 ; al_horiz_expand_left_reflexive : forall a b, [#al_reflexive_seq b#];;[#al_horiz_expand_left a#]===[#al_reflexive_seq (a,,b)#]
107 ; al_horiz_expand_right_reflexive : forall a b, [#al_reflexive_seq a#];;[#al_horiz_expand_right b#]===[#al_reflexive_seq (a,,b)#]
108 ; al_horiz_expand_right_then_cancel : forall a,
109 ((([#al_reflexive_seq (a,, [])#] ;; [#al_ant_cancelr#]);; [#al_suc_cancelr#]) === [#al_reflexive_seq a#])
111 ; al_vert_expand_ant_left : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [x,,a |= b ]/⋯⋯/[x,,c |= d ]
112 ; al_vert_expand_ant_right : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a,,x|= b ]/⋯⋯/[ c,,x|= d ]
113 ; al_vert_expand_suc_left : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a |=x,,b ]/⋯⋯/[ c |=x,,d ]
114 ; al_vert_expand_suc_right : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a |= b,,x]/⋯⋯/[ c |= d,,x]
115 ; al_vert_expand_ant_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
116 f===g -> al_vert_expand_ant_left x f === al_vert_expand_ant_left x g
117 ; al_vert_expand_ant_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
118 f===g -> al_vert_expand_ant_right x f === al_vert_expand_ant_right x g
119 ; al_vert_expand_suc_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
120 f===g -> al_vert_expand_suc_left x f === al_vert_expand_suc_left x g
121 ; al_vert_expand_suc_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
122 f===g -> al_vert_expand_suc_right x f === al_vert_expand_suc_right x g
123 ; al_vert_expand_ant_l_preserves_id : forall x a b, al_vert_expand_ant_left x (nd_id [a|=b]) === nd_id [x,,a|=b]
124 ; al_vert_expand_ant_r_preserves_id : forall x a b, al_vert_expand_ant_right x (nd_id [a|=b]) === nd_id [a,,x|=b]
125 ; al_vert_expand_suc_l_preserves_id : forall x a b, al_vert_expand_suc_left x (nd_id [a|=b]) === nd_id [a|=x,,b]
126 ; al_vert_expand_suc_r_preserves_id : forall x a b, al_vert_expand_suc_right x (nd_id [a|=b]) === nd_id [a|=b,,x]
127 ; al_vert_expand_ant_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
128 (al_vert_expand_ant_left x (h;;g)) === (al_vert_expand_ant_left x h);;(al_vert_expand_ant_left x g)
129 ; al_vert_expand_ant_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
130 (al_vert_expand_ant_right x (h;;g)) === (al_vert_expand_ant_right x h);;(al_vert_expand_ant_right x g)
131 ; al_vert_expand_suc_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
132 (al_vert_expand_suc_left x (h;;g)) === (al_vert_expand_suc_left x h);;(al_vert_expand_suc_left x g)
133 ; al_vert_expand_suc_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]),
134 (al_vert_expand_suc_right x (h;;g)) === (al_vert_expand_suc_right x h);;(al_vert_expand_suc_right x g)
136 ; al_subst : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
137 ; al_subst_associativity : forall {a b c d},
138 ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
142 ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
144 ; al_subst_associativity' : forall {a b c d},
146 ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
149 ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
152 ; al_subst_left_identity : forall `(pf:h/⋯⋯/[t1|=t2]), nd_llecnac;;(( [#al_reflexive_seq t1#]**pf);; al_subst _ _ _) === pf
153 ; al_subst_right_identity : forall `(pf:h/⋯⋯/[t1|=t2]), nd_rlecnac;;((pf**[#al_reflexive_seq t2#] );; al_subst _ _ _) === pf
154 ; al_subst_commutes_with_horiz_expand_left : forall a b c d,
155 [#al_horiz_expand_left d#] ** [#al_horiz_expand_left d#];; al_subst (d,, a) (d,, b) (d,, c)
156 === al_subst a b c;; [#al_horiz_expand_left d#]
157 ; al_subst_commutes_with_horiz_expand_right : forall a b c d,
158 [#al_horiz_expand_right d#] ** [#al_horiz_expand_right d#] ;; al_subst (a,, d) (b,, d) (c,, d)
159 === al_subst a b c;; [#al_horiz_expand_right d#]
160 ; al_subst_commutes_with_vertical_expansion : forall t0 t1 t2, forall (f:[[]|=t1]/⋯⋯/[[]|=t0])(g:[[]|=t0]/⋯⋯/[[]|=t2]),
162 ((([#al_reflexive_seq (t1,, [])#];; al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f));;
163 (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)) ** nd_id0);;
164 (nd_id [t1 |= t0]) **
165 ((([#al_reflexive_seq (t0,, [])#];; al_vert_expand_ant_left t0 (al_vert_expand_suc_right [] g));;
166 (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)));;
169 ((([#al_reflexive_seq (t1,, [])#];;
170 (al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f);;
171 al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] g)));;
172 (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr))
175 Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3.
176 Open Scope temporary_scope3.
178 Lemma al_subst_respects :
179 forall {AL:AcceptableLanguage}{a b c},
181 (f : [] /⋯⋯/ [a |= b])
182 (f' : [] /⋯⋯/ [a |= b])
183 (g : [] /⋯⋯/ [b |= c])
184 (g' : [] /⋯⋯/ [b |= c]),
187 (f ** g;; al_subst _ _ _) === (f' ** g';; al_subst _ _ _).
194 (* a contextually closed language *)
196 Class ContextuallyClosedAcceptableLanguage :=
197 { ccal_al : AcceptableLanguage
198 ; ccal_contextual_closure_operator : Tree ??T -> Tree ??T -> Tree ??T
199 where "a -~- b" := (ccal_contextual_closure_operator a b)
200 ; ccal_contextual_closure : forall {a b c d}(f:[a|=b]/⋯⋯/[c|=d]), [[]|=a-~-b]/⋯⋯/[[]|=c-~-d]
201 ; ccal_contextual_closure_respects : forall {a b c d}(f f':[a|=b]/⋯⋯/[c|=d]),
202 f===f' -> (ccal_contextual_closure f)===(ccal_contextual_closure f')
203 ; ccal_contextual_closure_preserves_comp : forall {a b c d e f}(f':[a|=b]/⋯⋯/[c|=d])(g':[c|=d]/⋯⋯/[e|=f]),
204 (ccal_contextual_closure f');;(ccal_contextual_closure g') === (ccal_contextual_closure (f';;g'))
205 ; ccal_contextual_closure_preserves_id : forall {a b}, ccal_contextual_closure (nd_id [a|=b]) === nd_id [[]|=a-~-b]
207 Coercion ccal_al : ContextuallyClosedAcceptableLanguage >-> AcceptableLanguage.
210 (* languages with unrestricted substructural rules (like that of Section 5) additionally implement this class *)
211 Class AcceptableLanguageWithUnrestrictedSubstructuralRules :=
212 { alwusr_al :> AcceptableLanguage
213 ; al_contr : forall a b, Rule [a,,a |= b ] [ a |= b]
214 ; al_exch : forall a b c, Rule [a,,b |= c ] [(b,,a)|= c]
215 ; al_weak : forall a b, Rule [[] |= b ] [ a |= b]
217 Coercion alwusr_al : AcceptableLanguageWithUnrestrictedSubstructuralRules >-> AcceptableLanguage.
219 (* languages with a fixpoint operator *)
220 Class AcceptableLanguageWithFixpointOperator `(al:AcceptableLanguage) :=
222 ; al_fix : forall a b x, Rule [a,,x |= b,,x] [a |= b]
224 Coercion alwfpo_al : AcceptableLanguageWithFixpointOperator >-> AcceptableLanguage.
226 Close Scope temporary_scope3.
227 Close Scope al_scope.
228 Close Scope nd_scope.
229 Close Scope pf_scope.
231 End Acceptable_Language.
233 Implicit Arguments ND [ Judgment ].
236 Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_right T Rule AL a b c d e)
237 with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
238 as parametric_morphism_al_vert_expand_suc_right.
239 intros; apply al_vert_expand_suc_r_respects; auto.
241 Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_left T Rule AL a b c d e)
242 with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
243 as parametric_morphism_al_vert_expand_suc_left.
244 intros; apply al_vert_expand_suc_l_respects; auto.
246 Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_right T Rule AL a b c d e)
247 with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
248 as parametric_morphism_al_vert_expand_ant_right.
249 intros; apply al_vert_expand_ant_r_respects; auto.
251 Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_left T Rule AL a b c d e)
252 with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
253 as parametric_morphism_al_vert_expand_ant_left.
254 intros; apply al_vert_expand_ant_l_respects; auto.
256 Close Scope nd_scope.
258 Notation "cs |= ss" := (@sequent _ cs ss) : al_scope.
260 Definition mapSequent {T R:Type}(f:Tree ??T -> Tree ??R)(seq:@Sequent T) : @Sequent R :=
261 match seq with sequentpair a b => pair (f a) (f b) end.
262 Implicit Arguments Sequent [ ].
266 (* proofs which are generic and apply to any acceptable langauge (most of section 4) *)
267 Section Acceptable_Language_Facts.
269 (* the ambient language about which we are proving facts *)
270 Context `(Lang : @AcceptableLanguage T Rule).
272 (* just for this section *)
276 Notation "H /⋯⋯/ C" := (@ND Sequent Rule H C) : temporary_scope4.
277 Notation "a === b" := (@ndr_eqv _ _ al_eqv _ _ a b) : temporary_scope4.
278 Open Scope temporary_scope4.
280 Definition lang_al_eqv := al_eqv(AcceptableLanguage:=Lang).
281 Existing Instance lang_al_eqv.
287 context ct [(?A ** ?B) ;; (?C ** ?D)] =>
288 setoid_rewrite <- (ndr_prod_preserves_comp A B C D)
292 Ltac sequentialize_product A B :=
296 | context ct [(A ** B)] =>
297 setoid_replace (A ** B)
298 with ((A ** (nd_id _)) ;; ((nd_id _) ** B))
299 (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*)
301 Ltac sequentialize_product' A B :=
305 | context ct [(A ** B)] =>
306 setoid_replace (A ** B)
307 with (((nd_id _) ** B) ;; (A ** (nd_id _)))
308 (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*)
314 context ct [(?A ;; ?B) ** (?C ;; ?D)] =>
315 setoid_rewrite (ndr_prod_preserves_comp A B C D)
318 Ltac distribute_left_product_with_id :=
322 context ct [(nd_id ?A) ** (?C ;; ?D)] =>
323 setoid_replace ((nd_id A) ** (C ;; D)) with ((nd_id A ;; nd_id A) ** (C ;; D));
324 [ setoid_rewrite (ndr_prod_preserves_comp (nd_id A) C (nd_id A) D) | idtac ]
327 Ltac distribute_right_product_with_id :=
331 context ct [(?C ;; ?D) ** (nd_id ?A)] =>
332 setoid_replace ((C ;; D) ** (nd_id A)) with ((C ;; D) ** (nd_id A ;; nd_id A));
333 [ setoid_rewrite (ndr_prod_preserves_comp C (nd_id A) D (nd_id A)) | idtac ]
337 (* another phrasing of al_subst_associativity; obligations tend to show up in this form *)
338 Lemma al_subst_associativity'' :
339 forall (a b : T) (f : [] /⋯⋯/ [[a] |= [b]]) (c : T) (g : [] /⋯⋯/ [[b] |= [c]])
340 (d : T) (h : [] /⋯⋯/ [[c] |= [d]]),
341 nd_llecnac;; ((nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) ** h;; al_subst [a] [c] [d]) ===
342 nd_llecnac;; (f ** (nd_llecnac;; (g ** h;; al_subst [b] [c] [d]));; al_subst [a] [b] [d]).
344 sequentialize_product' (nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) h.
345 repeat setoid_rewrite <- ndr_comp_associativity.
346 distribute_right_product_with_id.
347 repeat setoid_rewrite ndr_comp_associativity.
348 set (@al_subst_associativity) as q. setoid_rewrite q. clear q.
349 apply ndr_comp_respects; try reflexivity.
350 repeat setoid_rewrite <- ndr_comp_associativity.
351 apply ndr_comp_respects; try reflexivity.
352 sequentialize_product f ((nd_llecnac;; g ** h);; al_subst [b] [c] [d]).
353 distribute_left_product_with_id.
354 repeat setoid_rewrite <- ndr_comp_associativity.
355 apply ndr_comp_respects; try reflexivity.
356 setoid_rewrite <- ndr_prod_preserves_comp.
357 repeat setoid_rewrite ndr_comp_left_identity.
358 repeat setoid_rewrite ndr_comp_right_identity.
366 (* Formalized Definition 4.6 *)
368 Instance Types1 : Category T (fun t1 t2 => [ ] /⋯⋯/ [ [t1] |= [t2] ]) :=
369 { eqv := fun ta tb pf1 pf2 => pf1 === pf2
370 ; id := fun t => [#al_reflexive_seq [t]#]
371 ; comp := fun {ta tb tc:T}(pf1:[]/⋯⋯/[[ta]|=[tb]])(pf2:[]/⋯⋯/[[tb]|=[tc]]) => nd_llecnac ;; ((pf1 ** pf2) ;; (al_subst _ _ _))
373 intros; apply Build_Equivalence;
374 [ unfold Reflexive; intros; reflexivity
375 | unfold Symmetric; intros; symmetry; auto
376 | unfold Transitive; intros; transitivity y; auto ].
377 unfold Proper; unfold respectful; intros; simpl.
378 apply ndr_comp_respects. reflexivity.
379 apply al_subst_respects; auto.
380 intros; simpl. apply al_subst_left_identity.
382 assert (@nd_llecnac _ Rule [] === @nd_rlecnac _ _ []).
383 apply ndr_structural_indistinguishable; auto.
385 apply al_subst_right_identity.
386 intros; apply al_subst_associativity''.
390 (* Formalized Definition 4.10 *)
391 Instance Judgments : Category (Tree ??Sequent) (fun h c => h /⋯⋯/ c) :=
392 { id := fun h => nd_id _
393 ; comp := fun a b c f g => f ;; g
394 ; eqv := fun a b f g => f===g
396 intros; apply Build_Equivalence;
397 [ unfold Reflexive; intros; reflexivity
398 | unfold Symmetric; intros; symmetry; auto
399 | unfold Transitive; intros; transitivity y; auto ].
400 unfold Proper; unfold respectful; intros; simpl; apply ndr_comp_respects; auto.
401 intros; apply ndr_comp_left_identity.
402 intros; apply ndr_comp_right_identity.
403 intros; apply ndr_comp_associativity.
406 (* a "primitive" proof has exactly one hypothesis and one conclusion *)
407 Inductive IsPrimitive : forall (h_:Tree ??(@Sequent T)), Type :=
408 isPrimitive : forall h, IsPrimitive [h].
409 Hint Constructors IsPrimitive.
410 Instance IsPrimitiveSubCategory : SubCategory Judgments IsPrimitive (fun _ _ _ _ _ => True).
411 apply Build_SubCategory; intros; auto.
414 (* The primitive judgments form a subcategory; nearly all of the
415 * functors we build that go into Judgments will factor through the
416 * inclusion functor for this subcategory. Explicitly constructing
417 * it makes the formalization easier, but distracts from what's
418 * actually going on (from an expository perspective) *)
419 Definition PrimitiveJudgments := SubCategoriesAreCategories Judgments IsPrimitiveSubCategory.
420 Definition PrimitiveInclusion := InclusionFunctor Judgments IsPrimitiveSubCategory.
423 Inductive IsNil : Tree ??(@Sequent T) -> Prop := isnil : IsNil [].
424 Inductive IsClosed : Tree ??(@Sequent T) -> Prop := isclosed:forall t, IsClosed [[]|=[t]].
425 Inductive IsIdentity : forall h c, (h /⋯⋯/ c) -> Prop :=
426 | isidentity0 : forall t, IsIdentity t t (nd_id t)
427 | isidentity1 : forall t pf1 pf2, IsIdentity t t pf1 -> IsIdentity t t pf2 -> IsIdentity t t (pf1 ;; pf2).
428 Inductive IsInTypes0 (h c:Tree ??Sequent)(pf:h /⋯⋯/ c) : Prop :=
429 | iit0_id0 : IsNil h -> IsNil c -> IsIdentity _ _ pf -> IsInTypes0 _ _ pf
430 | iit0_id1 : @IsClosed h -> @IsClosed c -> IsIdentity _ _ pf -> IsInTypes0 _ _ pf
431 | iit0_term : IsNil h -> @IsClosed c -> IsInTypes0 _ _ pf.
432 Instance Types0P : SubCategory Judgments
433 (fun x:Judgments => IsInTypes0 _ _ (id(Category:=Judgments) x))
434 (fun h c _ _ f => IsInTypes0 h c f).
436 apply Build_SubCategory; intros; simpl.
441 inversion H; subst. inversion H4; subst.
442 apply iit0_id0; auto. apply isidentity1; auto.
447 inversion H3; subst. clear H8. clear H7.
448 inversion H; subst. inversion H5.
451 apply iit0_id1; auto. apply isidentity1; auto.
453 apply iit0_id1; auto. apply isidentity1; auto.
454 inversion H4; subst. inversion H; subst.
457 apply iit0_term; auto.
461 apply iit0_term; auto.
463 inversion H7; subst. clear H14.
464 apply iit0_id1; auto. apply isidentity1; auto.
466 apply iit0_id1; auto. apply isidentity1; auto.
471 apply iit0_term; auto.
474 inversion H3; subst. apply iit0_term; auto.
479 (* Formalized Definition 4.8 *)
480 Definition Types0 := SubCategoriesAreCategories Judgments Types0P.
483 (* Formalized Definition 4.11 *)
484 Instance Judgments_binoidal : BinoidalCat Judgments (fun a b:Tree ??Sequent => a,,b) :=
485 { bin_first := fun x => @Build_Functor _ _ Judgments _ _ Judgments (fun a => a,,x) (fun a b (f:a/⋯⋯/b) => f**(nd_id x)) _ _ _
486 ; bin_second := fun x => @Build_Functor _ _ Judgments _ _ Judgments (fun a => x,,a) (fun a b (f:a/⋯⋯/b) => (nd_id x)**f) _ _ _
488 intros. simpl. simpl in H. setoid_rewrite H. reflexivity.
489 intros. simpl. reflexivity.
490 intros. simpl. setoid_rewrite <- ndr_prod_preserves_comp. setoid_rewrite ndr_comp_left_identity. reflexivity.
491 intros. simpl. simpl in H. setoid_rewrite H. reflexivity.
492 intros. simpl. reflexivity.
493 intros. simpl. setoid_rewrite <- ndr_prod_preserves_comp. setoid_rewrite ndr_comp_left_identity. reflexivity.
496 Definition jud_assoc_iso (a b c:Judgments) : @Isomorphic _ _ Judgments ((a,,b),,c) (a,,(b,,c)).
497 apply (@Build_Isomorphic _ _ Judgments _ _ nd_assoc nd_cossa); simpl; auto.
499 Definition jud_cancelr_iso (a:Judgments) : @Isomorphic _ _ Judgments (a,,[]) a.
500 apply (@Build_Isomorphic _ _ Judgments _ _ nd_cancelr nd_rlecnac); simpl; auto.
502 Definition jud_cancell_iso (a:Judgments) : @Isomorphic _ _ Judgments ([],,a) a.
503 apply (@Build_Isomorphic _ _ Judgments _ _ nd_cancell nd_llecnac); simpl; auto.
506 (* just for this section *)
507 Notation "a ⊗ b" := (@bin_obj _ _ Judgments _ Judgments_binoidal a b).
508 Notation "c ⋊ -" := (@bin_second _ _ Judgments _ Judgments_binoidal c).
509 Notation "- ⋉ c" := (@bin_first _ _ Judgments _ Judgments_binoidal c).
510 Notation "c ⋊ f" := ((c ⋊ -) \ f).
511 Notation "g ⋉ c" := ((- ⋉ c) \ g).
513 Hint Extern 1 => apply (@nd_structural_id0 _ Rule).
514 Hint Extern 1 => apply (@nd_structural_id1 _ Rule).
515 Hint Extern 1 => apply (@nd_structural_weak _ Rule).
516 Hint Extern 1 => apply (@nd_structural_copy _ Rule).
517 Hint Extern 1 => apply (@nd_structural_prod _ Rule).
518 Hint Extern 1 => apply (@nd_structural_comp _ Rule).
519 Hint Extern 1 => apply (@nd_structural_cancell _ Rule).
520 Hint Extern 1 => apply (@nd_structural_cancelr _ Rule).
521 Hint Extern 1 => apply (@nd_structural_llecnac _ Rule).
522 Hint Extern 1 => apply (@nd_structural_rlecnac _ Rule).
523 Hint Extern 1 => apply (@nd_structural_assoc _ Rule).
524 Hint Extern 1 => apply (@nd_structural_cossa _ Rule).
525 Hint Extern 2 => apply (@ndr_structural_indistinguishable _ Rule).
527 Program Instance Judgments_premonoidal : PreMonoidalCat Judgments_binoidal [ ] :=
528 { pmon_assoc := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_assoc_iso a x b)) _
529 ; pmon_cancell := @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_cancell_iso x)) _
530 ; pmon_cancelr := @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_cancelr_iso x)) _
531 ; pmon_assoc_rr := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_assoc_iso x a b)⁻¹) _
532 ; pmon_assoc_ll := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => jud_assoc_iso a b x) _
535 setoid_rewrite (ndr_prod_associativity (nd_id a) f (nd_id b)).
536 repeat setoid_rewrite ndr_comp_associativity.
537 apply ndr_comp_respects; try reflexivity.
539 eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
540 apply ndr_comp_respects; try reflexivity; simpl; auto.
543 setoid_rewrite (ndr_prod_right_identity f).
544 repeat setoid_rewrite ndr_comp_associativity.
545 apply ndr_comp_respects; try reflexivity.
547 eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
548 apply ndr_comp_respects; try reflexivity; simpl; auto.
551 setoid_rewrite (ndr_prod_left_identity f).
552 repeat setoid_rewrite ndr_comp_associativity.
553 apply ndr_comp_respects; try reflexivity.
555 eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
556 apply ndr_comp_respects; try reflexivity; simpl; auto.
559 apply Build_Pentagon; intros.
560 simpl; apply ndr_structural_indistinguishable; auto.
563 apply Build_Triangle; intros;
564 simpl; apply ndr_structural_indistinguishable; auto.
567 setoid_rewrite (ndr_prod_associativity f (nd_id a) (nd_id b)).
568 repeat setoid_rewrite <- ndr_comp_associativity.
569 apply ndr_comp_respects; try reflexivity.
570 eapply transitivity; [ idtac | apply ndr_comp_left_identity ].
571 apply ndr_comp_respects; try reflexivity; simpl; auto.
574 setoid_rewrite (ndr_prod_associativity (nd_id a) (nd_id b) f).
575 repeat setoid_rewrite ndr_comp_associativity.
576 apply ndr_comp_respects; try reflexivity.
578 eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
579 apply ndr_comp_respects; try reflexivity; simpl; auto.
581 Check (@Judgments_premonoidal). (* to force Coq to verify that we've finished all the obligations *)
583 Definition Judgments_monoidal_endofunctor_fobj : Judgments ×× Judgments -> Judgments :=
586 | pair_obj x y => T_Branch x y
588 Definition Judgments_monoidal_endofunctor_fmor :
589 forall a b, (a~~{Judgments ×× Judgments}~~>b) ->
590 ((Judgments_monoidal_endofunctor_fobj a)~~{Judgments}~~>(Judgments_monoidal_endofunctor_fobj b)).
597 Definition Judgments_monoidal_endofunctor : Functor (Judgments ×× Judgments) Judgments Judgments_monoidal_endofunctor_fobj.
598 refine {| fmor := Judgments_monoidal_endofunctor_fmor |}; intros; simpl.
599 abstract (destruct a; destruct b; destruct f; destruct f'; auto; destruct H; apply ndr_prod_respects; auto).
600 abstract (destruct a; simpl; reflexivity).
601 abstract (destruct a; destruct b; destruct c; destruct f; destruct g; symmetry; apply ndr_prod_preserves_comp).
604 Instance Judgments_monoidal : MonoidalCat _ _ Judgments_monoidal_endofunctor [ ].
608 (* all morphisms in the category of Judgments are central; there's probably a very short route from here to CartesianCat *)
609 Lemma all_central : forall a b:Judgments, forall (f:a~>b), CentralMorphism f.
610 intros; apply Build_CentralMorphism; intros.
612 setoid_rewrite <- (ndr_prod_preserves_comp f (nd_id _) (nd_id _) g).
613 setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) g f (nd_id _)).
614 setoid_rewrite ndr_comp_left_identity.
615 setoid_rewrite ndr_comp_right_identity.
618 setoid_rewrite <- (ndr_prod_preserves_comp g (nd_id _) (nd_id _) f).
619 setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) f g (nd_id _)).
620 setoid_rewrite ndr_comp_left_identity.
621 setoid_rewrite ndr_comp_right_identity.
626 Instance NoHigherOrderFunctionTypes : SubCategory Judgments
627 Instance NoFunctionTypes : SubCategory Judgments
628 Lemma first_order_functions_eliminable : IsomorphicCategories NoHigherOrderFunctionTypes NoFunctionTypes
631 (* Formalized Theorem 4.19 *)
632 Instance Types_omega_e : ECategory Judgments_monoidal (Tree ??T) (fun tt1 tt2 => [ tt1 |= tt2 ]) :=
633 { eid := fun tt => [#al_reflexive_seq tt#]
634 ; ecomp := fun a b c => al_subst a b c
643 Definition Types_omega_monoidal_functor
644 : Functor (Types_omega_e ×× Types_omega_e) Types_omega_e (fun a => match a with pair_obj a1 a2 => a1,,a2 end).
648 Instance Types_omega_monoidal : MonoidalCat Types_omega_e _ Types_omega_monoidal_functor [].
652 Definition AL_Enrichment : Enrichment.
653 refine {| enr_c := Types_omega_e |}.
656 Definition AL_SurjectiveEnrichment : SurjectiveEnrichment.
657 refine {| se_enr := AL_Enrichment |}.
658 unfold treeDecomposition.
659 intros; induction d; simpl.
662 exists [pair t t0]; auto.
666 exists (x,,x0); subst; auto.
669 Definition AL_MonoidalEnrichment : MonoidalEnrichment.
670 refine {| me_enr := AL_SurjectiveEnrichment ; me_mon := Types_omega_monoidal |}.
674 Definition AL_MonicMonoidalEnrichment : MonicMonoidalEnrichment.
675 refine {| ffme_enr := AL_MonoidalEnrichment |}.
682 Instance Types_omega_be : BinoidalECategory Types_omega_e :=
683 { bec_obj := fun tt1 tt2 => tt1,,tt2
684 ; bec_efirst := fun a b c => nd_rule (@al_horiz_expand_right _ _ Lang _ _ _)
685 ; bec_esecond := fun a b c => nd_rule (@al_horiz_expand_left _ _ Lang _ _ _)
687 intros; apply all_central.
688 intros; apply all_central.
689 intros. unfold eid. simpl.
690 setoid_rewrite <- al_horiz_expand_right_reflexive.
692 intros. unfold eid. simpl.
693 setoid_rewrite <- al_horiz_expand_left_reflexive.
696 set (@al_subst_commutes_with_horiz_expand_right _ _ _ a b c d) as q.
697 setoid_rewrite <- q. clear q.
698 apply ndr_comp_respects; try reflexivity.
700 apply ndr_prod_respects.
701 eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
702 apply ndr_comp_respects; reflexivity.
703 eapply transitivity; [ idtac | apply ndr_comp_left_identity ].
704 apply ndr_comp_respects; reflexivity.
706 set (@al_subst_commutes_with_horiz_expand_left _ _ _ a b c d) as q.
707 setoid_rewrite <- q. clear q.
708 apply ndr_comp_respects; try reflexivity.
710 apply ndr_prod_respects.
711 eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
712 apply ndr_comp_respects; reflexivity.
713 eapply transitivity; [ idtac | apply ndr_comp_left_identity ].
714 apply ndr_comp_respects; reflexivity.
718 Definition Types_omega : Category _ (fun tt1 tt2 => [ ]/⋯⋯/[ tt1 |= tt2 ]) := Underlying Types_omega_e.
719 Existing Instance Types_omega.
722 Definition Types_omega_binoidal : BinoidalCat Types_omega (fun tt1 tt2 => tt1,,tt2) := Underlying_binoidal Types_omega_be.
723 Existing Instance Types_omega_binoidal.
726 (* takes an "operation in the context" (proof from [b|=Top]/⋯⋯/[a|=Top]) and turns it into a function a-->b; note the variance *)
727 Definition context_operation_as_function
728 : forall {a}{b} (f:[b|=[]]~~{Judgments}~~>[a|=[]]), []~~{Judgments}~~>[a|=b].
730 apply (@al_vert_expand_suc_right _ _ _ b _ _) in f.
732 apply (@al_vert_expand_ant_left _ _ _ [] _ _) in f.
734 set ([#al_reflexive_seq _#] ;; f ;; [#al_ant_cancell#] ;; [#al_suc_cancell#]) as f'.
738 (* takes an "operation in the context" (proof from [Top|=a]/⋯⋯/[Top|=b]) and turns it into a function a-->b; note the variance *)
739 Definition cocontext_operation_as_function
740 : forall {a}{b} (f:[[]|=a]~~{Judgments}~~>[[]|=b]), []~~{Judgments}~~>[a|=b].
741 intros. unfold hom. unfold hom in f.
742 apply al_vert_expand_ant_right with (x:=a) in f.
744 apply al_vert_expand_suc_left with (x:=[]) in f.
746 set ([#al_reflexive_seq _#] ;; f ;; [#al_ant_cancell#] ;; [#al_suc_cancell#]) as f'.
751 Definition function_as_context_operation
752 : forall {a}{b}{c} (f:[]~~{Judgments}~~>[a|=b]), [b|=c]~~{Judgments}~~>[a|=c]
753 := fun a b c f => RepresentableFunctorºᑭ Types_omega_e c \ f.
754 Definition function_as_cocontext_operation
755 : forall {a}{b}{c} (f:[]/⋯⋯/[a|=b]), [c|=a]~~{Judgments}~~>[c|=b]
756 := fun a b c f => RepresentableFunctor Types_omega_e c \ f.
758 Close Scope temporary_scope4.
759 Close Scope al_scope.
760 Close Scope nd_scope.
761 Close Scope pf_scope.
762 Close Scope isomorphism_scope.
763 End Acceptable_Language_Facts.
765 Coercion AL_SurjectiveEnrichment : AcceptableLanguage >-> SurjectiveEnrichment.
766 Coercion AL_MonicMonoidalEnrichment : AcceptableLanguage >-> MonicMonoidalEnrichment.