1 (*********************************************************************************************************************************)
2 (* HaskProofCategory: *)
4 (* Natural Deduction proofs of the well-typedness of a Haskell term form a category *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import NaturalDeduction.
12 Require Import Coq.Strings.String.
13 Require Import Coq.Lists.List.
15 Require Import HaskKinds.
16 Require Import HaskCoreTypes.
17 Require Import HaskLiteralsAndTyCons.
18 Require Import HaskStrongTypes.
19 Require Import HaskProof.
20 Require Import NaturalDeduction.
21 Require Import NaturalDeductionCategory.
23 Require Import Algebras_ch4.
24 Require Import Categories_ch1_3.
25 Require Import Functors_ch1_4.
26 Require Import Isomorphisms_ch1_5.
27 Require Import ProductCategories_ch1_6_1.
28 Require Import OppositeCategories_ch1_6_2.
29 Require Import Enrichment_ch2_8.
30 Require Import Subcategories_ch7_1.
31 Require Import NaturalTransformations_ch7_4.
32 Require Import NaturalIsomorphisms_ch7_5.
33 Require Import MonoidalCategories_ch7_8.
34 Require Import Coherence_ch7_8.
36 Require Import HaskStrongTypes.
37 Require Import HaskStrong.
38 Require Import HaskProof.
39 Require Import HaskStrongToProof.
40 Require Import HaskProofToStrong.
41 Require Import ProgrammingLanguage.
43 Section HaskProofCategory.
45 Definition unitType {Γ} : RawHaskType Γ ★.
49 Definition brakifyType {Γ} (lt:LeveledHaskType Γ ★) : LeveledHaskType (★ ::Γ) ★ :=
51 t @@ l => HaskBrak (FreshHaskTyVar ★) (weakT t) @@ weakL l
54 Definition brakify (j:Judg) : Judg :=
57 (★ ::Γ) > weakCE Δ > mapOptionTree brakifyType Σ |- mapOptionTree brakifyType τ
60 (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
63 Context {Γ:TypeEnv}{Δ:CoercionEnv Γ}.
65 (* Rule_PCF consists of the rules allowed in flat PCF: everything except
66 * AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *)
67 Inductive Rule_PCF : forall {h}{c}, Rule h c -> Prop :=
68 | PCF_RURule : ∀ h c r , Rule_PCF (RURule Γ Δ h c r)
69 | PCF_RLit : ∀ Γ Δ Σ τ , Rule_PCF (RLit Γ Δ Σ τ )
70 | PCF_RNote : ∀ Σ τ l n , Rule_PCF (RNote Γ Δ Σ τ l n)
71 | PCF_RVar : ∀ σ l, Rule_PCF (RVar Γ Δ σ l)
72 | PCF_RLam : ∀ Σ tx te q , Rule_PCF (RLam Γ Δ Σ tx te q )
73 | PCF_RApp : ∀ Σ tx te p l, Rule_PCF (RApp Γ Δ Σ tx te p l)
74 | PCF_RLet : ∀ Σ σ₁ σ₂ p l, Rule_PCF (RLet Γ Δ Σ σ₁ σ₂ p l)
75 | PCF_RBindingGroup : ∀ q a b c d e , Rule_PCF (RBindingGroup q a b c d e)
76 | PCF_RCase : ∀ T κlen κ θ l x , Rule_PCF (RCase Γ Δ T κlen κ θ l x) (* FIXME: only for boolean and int *)
77 | Flat_REmptyGroup : ∀ q a , Rule_PCF (REmptyGroup q a)
78 | Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev , Rule_PCF (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
80 (* "RulePCF n" is the type of rules permitted in PCF with n-level deep nesting (so, "RulePCF 0" is flat PCF) *)
81 Inductive RulePCF : nat -> Tree ??Judg -> Tree ??Judg -> Type :=
83 (* any proof using only PCF rules is an n-bounded proof for any n>0 *)
84 | pcf_flat : forall n h c (r:Rule h c), Rule_PCF r -> RulePCF n h c
86 (* any n-bounded proof may be used as an (n+1)-bounded proof by prepending Esc and appending Brak *)
87 | pfc_nest : forall n h c, ND (RulePCF n) h c -> RulePCF (S n) (mapOptionTree brakify h) (mapOptionTree brakify c)
93 Context {Γ:TypeEnv}{Δ:CoercionEnv Γ}.
95 (* "RuleSystemFCa n" is the type of rules permitted in SystemFC^\alpha with n-level-deep nesting
96 * in a fixed Γ,Δ context. This is a subcategory of the "complete" SystemFCa, but it's enough to
97 * do the flattening transformation *)
98 Inductive RuleSystemFCa : nat -> Tree ??Judg -> Tree ??Judg -> Type :=
99 | sfc_flat : forall n h c (r:Rule h c), Rule_Flat r -> RuleSystemFCa n h c
100 | sfc_nest : forall n h c, ND (@RulePCF Γ Δ n) h c -> RuleSystemFCa (S n) h c
103 Context (ndr_systemfca:forall n, @ND_Relation _ (RuleSystemFCa n)).
105 Hint Constructors Rule_Flat.
107 Definition SystemFC_SC n : @SequentCalculus _ (RuleSystemFCa n) _ (mkJudg Γ Δ).
108 apply Build_SequentCalculus.
114 apply sfc_flat with (r:=RVar _ _ _ _).
117 apply sfc_flat with (r:=REmptyGroup _ _).
119 eapply nd_comp; [ apply nd_llecnac | idtac ].
120 eapply nd_comp; [ eapply nd_prod | idtac ].
124 apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
128 Existing Instance SystemFC_SC.
130 Lemma systemfc_cut n : ∀a b c,
131 ND (RuleSystemFCa n) ([Γ > Δ > a |- b],, [Γ > Δ > b |- c]) [Γ > Δ > a |- c].
136 Lemma systemfc_cutrule n
137 : @CutRule _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfca n) (SystemFC_SC n).
138 apply Build_CutRule with (nd_cut:=systemfc_cut n).
144 Definition systemfc_left n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > a,, b |- a,, c].
145 eapply nd_comp; [ apply nd_llecnac | idtac ].
146 eapply nd_comp; [ eapply nd_prod | idtac ].
149 apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
152 apply nd_seq_reflexive.
156 Definition systemfc_right n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > b,,a |- c,,a].
157 eapply nd_comp; [ apply nd_rlecnac | idtac ].
158 eapply nd_comp; [ eapply nd_prod | idtac ].
160 apply (nd_seq_reflexive a).
162 apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
166 Definition systemfc_expansion n
167 : @SequentExpansion _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfca n) (SystemFC_SC n) (systemfc_cutrule n).
168 Check (@Build_SequentExpansion).
169 apply (@Build_SequentExpansion _ _ _ _ (ndr_systemfca n) _ _ (systemfc_left n) (systemfc_right n)).
170 refine {| se_expand_left:=systemfc_left n
171 ; se_expand_right:=systemfc_right n |}.
175 Instance SystemFCa n : @ProgrammingLanguage _ Judg (mkJudg Γ Δ) (RuleSystemFCa n) :=
176 { pl_eqv := ndr_systemfca n
177 ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
178 ; pl_sc := SystemFC_SC n
179 ; pl_subst := systemfc_cutrule n
180 ; pl_sequent_join := systemfc_expansion n
182 apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
183 apply sfc_flat with (r:=RURule _ _ _ _ (RCossa _ a b c)); auto. apply Flat_RURule.
184 apply sfc_flat with (r:=RURule _ _ _ _ (RAssoc _ a b c)); auto. apply Flat_RURule.
185 apply sfc_flat with (r:=RURule _ _ _ _ (RCanL _ a )); auto. apply Flat_RURule.
186 apply sfc_flat with (r:=RURule _ _ _ _ (RCanR _ a )); auto. apply Flat_RURule.
187 apply sfc_flat with (r:=RURule _ _ _ _ (RuCanL _ a )); auto. apply Flat_RURule.
188 apply sfc_flat with (r:=RURule _ _ _ _ (RuCanR _ a )); auto. apply Flat_RURule.
195 Context (ndr_pcf :forall n Γ Δ, @ND_Relation _ (@RulePCF Γ Δ n)).
198 Instance PCF n Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) (@RulePCF Γ Δ n) :=
199 { pl_eqv := _ (*@ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2)*)
200 ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
201 ; pl_sc := _ (*@SequentCalculus Judg Rule _ sequent*)
202 ; pl_subst := _ (*@CutRule Judg Rule _ sequent pl_eqv pl_sc*)
203 ; pl_sequent_join := _ (*@SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst*)
208 Definition ReificationFunctor n : Functor (JudgmentsN n) (JudgmentsN (S n)) (mapOptionTree brakify).
209 refine {| fmor := fun h c (f:h~~{JudgmentsN n}~~>c) => nd_rule (br_nest _ _ _ f) |}; intros; simpl.
215 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
216 refine {| plsmme_pl := PCF n Γ Δ |}.
220 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
221 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
225 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
230 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
232 (* ... and the retraction exists *)
235 (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so
236 * it falls within (SystemFCa n) for some n. This function calculates that "n" and performs the translation *)
238 Definition HaskProof_to_SystemFCa :
239 forall h c (pf:ND Rule h c),
240 { n:nat & h ~~{JudgmentsL (SystemFCa_SMME n)}~~> c }.
243 (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
246 Definition makeTree : Tree ??(LeveledHaskType Γ ★) -> HaskType Γ ★.
250 Definition flattenType n (j:JudgmentsN n) : TypesN n.
253 refine (mapOptionTree _ j).
255 destruct j as [ Γ' Δ' Σ τ ].
256 assert (Γ'=Γ). admit.
260 refine (HaskBrak _ ( (makeTree Σ) ---> (makeTree τ) )); intros.
264 Definition FlattenFunctor_fmor n :
266 (h~~{JudgmentsN n}~~>c) ->
267 ((flattenType n h)~~{TypesN n}~~>(flattenType n c)).
269 unfold hom in *; simpl.
277 Definition FlattenFunctor n : Functor (JudgmentsN n) (TypesN n) (flattenType n).
278 refine {| fmor := FlattenFunctor_fmor n |}; intros.
285 Implicit Arguments Rule_PCF [ [h] [c] ].
286 Implicit Arguments BoundedRule [ ].
290 Definition code2garrow0 {Γ}(ec t1 t2:RawHaskType Γ ★) : RawHaskType Γ ★.
293 Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
295 (* | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx t'*)
296 | _ => code2garrow0 ec unitType t
299 Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
300 match ty as TY in RawHaskType _ K return RawHaskType TV K with
301 | TCode ec t => code2garrow _ ec t
302 | TApp _ _ t1 t2 => TApp (typeMap t1) (typeMap t2)
303 | TAll _ f => TAll _ (fun tv => typeMap (f tv))
304 | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
308 | TyFunApp tf rhtl => (* FIXME *) TyFunApp tf rhtl
311 Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
313 (* | t @@ nil => (fun TV ite => typeMap (t TV ite)) @@ lev*)
314 | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
317 Definition coMap {Γ}(ck:HaskCoercionKind Γ) :=
318 fun TV ite => match ck TV ite with
319 | mkRawCoercionKind _ t1 t2 => mkRawCoercionKind _ (typeMap t1) (typeMap t2)
322 Definition flattenCoercion {Γ}{Δ}{ck}(hk:HaskCoercion Γ Δ ck) : HaskCoercion Γ (map coMap Δ) (coMap ck).
326 Lemma update_typeMap Γ (lev:HaskLevel Γ) ξ v t
327 : (typeMap ○ (update_ξ ξ lev ((⟨v, t ⟩) :: nil)))
328 = ( update_ξ (typeMap ○ ξ) lev ((⟨v, typeMap_ t ⟩) :: nil)).
332 Lemma foo κ Γ σ τ : typeMap_ (substT σ τ) = substT(Γ:=Γ)(κ₁:=κ) (fun TV ite => typeMap ○ σ TV ite) τ.
336 Lemma lit_lemma lit Γ : typeMap_ (literalType lit) = literalType(Γ:=Γ) lit.
341 Definition flatten : forall h c, Rule h c -> @ND Judg Rule (mapOptionTree flattenJudgment h) (mapOptionTree flattenJudgment c).
343 refine (match r as R in Rule H C return ND Rule (mapOptionTree flattenJudgment H) (mapOptionTree flattenJudgment C) with
344 | RURule a b c d e => let case_RURule := tt in _
345 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
346 | RLit Γ Δ l _ => let case_RLit := tt in _
347 | RVar Γ Δ σ p => let case_RVar := tt in _
348 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
349 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
350 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
351 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
352 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
353 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
354 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
355 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
356 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
357 | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
358 | REmptyGroup _ _ => let case_REmptyGroup := tt in _
359 | RBrak Σ a b c n m => let case_RBrak := tt in _
360 | REsc Σ a b c n m => let case_REsc := tt in _
361 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
362 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
365 destruct case_RURule.
377 eapply nd_rule. simpl. apply RNote; auto.
382 set (@RNote Γ Δ Σ τ l) as q.
385 Definition flatten' {h}{c} (pf:ND Rule h c) := nd_map' flattenJudgment flatten pf.
388 @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
390 refine (fix flatten : forall Γ Δ Σ τ
391 (pf:SCND Rule [] [Γ > Δ > Σ |- τ ]) :
392 SCND Rule [] [Γ > Δ > mapOptionTree typeMap Σ |- mapOptionTree typeMap τ ] :=
394 | scnd_comp : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c]
395 | scnd_weak : forall c , SCND c []
396 | scnd_leaf : forall ht c , SCND ht [c] -> SCND ht [c]
397 | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2)
398 Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
402 Lemma all_lemma Γ κ σ l :
404 (@HaskTApp (κ :: Γ) κ (@weakF Γ κ ★ σ) (@FreshHaskTyVar Γ κ) @@
405 @weakL Γ κ l)) = (@typeMap Γ (@HaskTAll Γ κ σ @@ l)).
409 Definition flatten : forall Γ Δ ξ τ, Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
410 refine (fix flatten Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') : Expr Γ' (map coMap Δ') (typeMap ○ ξ') (typeMap τ') :=
411 match exp as E in Expr G D X T return Expr G (map coMap D) (typeMap ○ X) (typeMap T) with
412 | EGlobal Γ Δ ξ t wev => EGlobal _ _ _ _ wev
413 | EVar Γ Δ ξ ev => EVar _ _ _ ev
414 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
415 | EApp Γ Δ ξ t1 t2 lev e1 e2 => EApp _ _ _ _ _ _ (flatten _ _ _ _ e1) (flatten _ _ _ _ e2)
416 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in _
417 | ELet Γ Δ ξ tv t l ev elet ebody => let case_ELet := tt in _
418 | ELetRec Γ Δ ξ lev t tree branches ebody => let case_ELetRec := tt in _
419 | ECast Γ Δ ξ t1 t2 γ lev e => let case_ECast := tt in _
420 | ENote Γ Δ ξ t n e => ENote _ _ _ _ n (flatten _ _ _ _ e)
421 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in _
422 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in _
423 | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => let case_ECoApp := tt in _
424 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in _
425 | ECase Γ Δ ξ l tc tbranches atypes e alts' => let case_ECase := tt in _
427 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in _
428 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in _
429 end); clear exp ξ' τ' Γ' Δ'.
437 set (flatten _ _ _ _ e) as q.
438 rewrite update_typeMap in q.
439 apply (@ELam _ _ _ _ _ _ _ _ v q).
442 set (flatten _ _ _ _ ebody) as ebody'.
443 set (flatten _ _ _ _ elet) as elet'.
444 rewrite update_typeMap in ebody'.
445 apply (@ELet _ _ _ _ _ _ _ _ _ elet' ebody').
456 apply flattenCoercion in γ.
459 destruct case_ETyApp.
462 unfold HaskTAll in e.
463 unfold typeMap_ in e.
469 destruct case_ECoLam.
472 set (@ECoLam _ _ _ _ _ _ _ _ _ _ e) as x.
479 destruct case_ECoApp.
483 unfold mkHaskCoercionKind in *.
485 apply flattenCoercion in γ.
486 unfold coMap in γ at 2.
490 destruct case_ETyLam.
492 set (@ETyLam Unique _ Γ (map coMap Δ) (typeMap ○ ξ) κ (fun ite x => typeMap (σ x ite))) as e'.
493 unfold HaskTAll in *.
494 unfold typeMap_ in *.
495 rewrite <- foo in e'.
496 unfold typeMap in e'.
500 Set Printing Implicit.
510 destruct case_ELetRec.
514 (* This proof will work for any dynamic semantics you like, so
515 * long as those semantics are an ND_Relation (associativity,
516 * neutrality, etc) *)
517 Context (dynamic_semantics : @ND_Relation _ Rule).
519 Section SystemFC_Category.
524 Definition Context := Tree ??(LeveledHaskType Γ ★).
526 Notation "a |= b" := (Γ >> Δ > a |- b).
532 SystemFCa_initial_GArrow
535 Context (nd_eqv:@ND_Relation _ (@URule Γ Δ)).
536 Check (@ProgrammingLanguage).
537 Context (PL:@ProgrammingLanguage (LeveledHaskType Γ ★)
538 (fun x y => match x with x1|=x2 => match y with y1|=y2 => @URule Γ Δ)).
539 Definition JudgmentsFC := @Judgments_Category_CartesianCat _ (@URule Γ Δ) nd_eqv.
540 Definition TypesFC := @TypesL _ (@URule Γ Δ) nd_eqv.
542 (* The full subcategory of SystemFC(Γ,Δ) consisting only of judgments involving types at a fixed level. Note that
543 * code types are still permitted! *)
545 Context (lev:HaskLevel Γ).
547 Inductive ContextAtLevel : Context -> Prop :=
548 | contextAtLevel_nil : ContextAtLevel []
549 | contextAtLevel_leaf : forall τ, ContextAtLevel [τ @@ lev]
550 | contextAtLevel_branch : forall b1 b2, ContextAtLevel b1 -> ContextAtLevel b2 -> ContextAtLevel (b1,,b2).
552 Inductive JudgmentsAtLevel : JudgmentsFC -> Prop :=
553 | judgmentsAtLevel_nil : JudgmentsAtLevel []
554 | judgmentsAtLevel_leaf : forall c1 c2, ContextAtLevel c1 -> ContextAtLevel c2 -> JudgmentsAtLevel [c1 |= c2]
555 | judgmentsAtLevel_branch : forall j1 j2, JudgmentsAtLevel j1 -> JudgmentsAtLevel j2 -> JudgmentsAtLevel (j1,,j2).
557 Definition JudgmentsFCAtLevel := FullSubcategory JudgmentsFC JudgmentsAtLevel.
558 Definition TypesFCAtLevel := FullSubcategory TypesFC ContextAtLevel.
561 End SystemFC_Category.
563 Implicit Arguments TypesFC [ ].
566 Section EscBrak_Functor.
570 (Σ₁:Tree ??(@LeveledHaskType V)).
572 Definition EscBrak_Functor_Fobj
573 : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past
574 := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
575 let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])).
577 Definition append_brak
579 (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) c )
580 (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj c)).
583 unfold EscBrak_Functor_Fobj.
584 rewrite mapOptionTree_comp.
592 Definition prepend_esc
594 (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj h))
595 (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) h ).
598 unfold EscBrak_Functor_Fobj.
599 rewrite mapOptionTree_comp.
607 Definition EscBrak_Functor_Fmor
608 : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b),
609 (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b).
619 Lemma esc_then_brak_is_id : forall a,
620 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak)
621 (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))).
625 Lemma brak_then_esc_is_id : forall a,
626 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc)
627 (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)).
631 Instance EscBrak_Functor
632 : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj :=
633 { fmor := fun a b f => EscBrak_Functor_Fmor a b f }.
634 intros; unfold EscBrak_Functor_Fmor; simpl in *.
635 apply ndr_comp_respects; try reflexivity.
636 apply ndr_comp_respects; try reflexivity.
638 intros; unfold EscBrak_Functor_Fmor; simpl in *.
639 set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
641 apply esc_then_brak_is_id.
642 intros; unfold EscBrak_Functor_Fmor; simpl in *.
643 set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q.
644 repeat setoid_rewrite q.
645 apply ndr_comp_respects; try reflexivity.
646 apply ndr_comp_respects; try reflexivity.
647 repeat setoid_rewrite <- q.
648 apply ndr_comp_respects; try reflexivity.
649 setoid_rewrite brak_then_esc_is_id.
651 set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
660 Ltac rule_helper_tactic' :=
662 | [ H : ?A = ?A |- _ ] => clear H
663 | [ H : [?A] = [] |- _ ] => inversion H; clear H
664 | [ H : [] = [?A] |- _ ] => inversion H; clear H
665 | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H
666 | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H
667 | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H
668 | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H
669 | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H
670 | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H
671 (* | [ H : Sequent T |- _ ] => destruct H *)
672 (* | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*)
673 | [ H : [?A] = [?B] |- _ ] => inversion H; clear H
674 | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst
675 | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl
676 | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H
679 Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
683 Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
687 Definition append_brak_to_id : forall {c},
689 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )
690 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
694 Definition append_brak : forall {h c}
697 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )),
700 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
702 refine (fix append_brak h c nd {struct nd} :=
708 (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) ->
709 ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
711 | nd_id0 => let case_nd_id0 := tt in _
712 | nd_id1 h => let case_nd_id1 := tt in _
713 | nd_weak h => let case_nd_weak := tt in _
714 | nd_copy h => let case_nd_copy := tt in _
715 | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
716 | nd_comp _ _ _ top bot => let case_nd_comp := tt in _
717 | nd_rule _ _ rule => let case_nd_rule := tt in _
718 | nd_cancell _ => let case_nd_cancell := tt in _
719 | nd_cancelr _ => let case_nd_cancelr := tt in _
720 | nd_llecnac _ => let case_nd_llecnac := tt in _
721 | nd_rlecnac _ => let case_nd_rlecnac := tt in _
722 | nd_assoc _ _ _ => let case_nd_assoc := tt in _
723 | nd_cossa _ _ _ => let case_nd_cossa := tt in _
724 end) (refl_equal _) (refl_equal _)
726 simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *.
727 destruct case_nd_id0. apply nd_id0.
728 destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak.
729 destruct case_nd_weak. apply nd_weak.
731 destruct case_nd_copy.
733 destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
740 destruct case_nd_prod.
742 apply (append_brak _ _ lpf).
743 apply (append_brak _ _ rpf).
745 destruct case_nd_comp.
746 apply append_brak in bot.
747 apply (nd_comp top bot).
749 destruct case_nd_cancell.
750 eapply nd_comp; [ apply nd_cancell | idtac ].
751 apply append_brak_to_id.
753 destruct case_nd_cancelr.
754 eapply nd_comp; [ apply nd_cancelr | idtac ].
755 apply append_brak_to_id.
757 destruct case_nd_llecnac.
758 eapply nd_comp; [ idtac | apply nd_llecnac ].
759 apply append_brak_to_id.
761 destruct case_nd_rlecnac.
762 eapply nd_comp; [ idtac | apply nd_rlecnac ].
763 apply append_brak_to_id.
765 destruct case_nd_assoc.
766 eapply nd_comp; [ apply nd_assoc | idtac ].
767 repeat rewrite fixit.
768 apply append_brak_to_id.
770 destruct case_nd_cossa.
771 eapply nd_comp; [ idtac | apply nd_cossa ].
772 repeat rewrite fixit.
773 apply append_brak_to_id.
775 destruct case_nd_rule
781 Definition append_brak {h c} : forall
783 (fixify Γ ((⟨n, Σ₁ ⟩) :: past) h )
786 (fixify Γ past (EscBrak_Functor_Fobj h))
792 End HaskProofCategory.