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)
91 (* "RuleSystemFCa n" is the type of rules permitted in SystemFC^\alpha with n-level-deep nesting
92 * (so, "RuleSystemFCa 0" is damn close to System FC) *)
93 Inductive RuleSystemFCa : nat -> Tree ??Judg -> Tree ??Judg -> Type :=
94 | sfc_flat : forall n h c (r:Rule h c), Rule_Flat r -> RuleSystemFCa n h c
95 | sfc_nest : forall n h c Γ Δ, ND (@RulePCF Γ Δ n) h c -> RuleSystemFCa (S n) h c
98 Context (ndr_pcf :forall n Γ Δ, @ND_Relation _ (@RulePCF Γ Δ n)).
99 Context (ndr_systemfca:forall n, @ND_Relation _ (RuleSystemFCa n)).
102 Instance PCF n Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) (@RulePCF Γ Δ n) :=
103 { pl_eqv := _ (*@ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2)*)
104 ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
105 ; pl_sc := _ (*@SequentCalculus Judg Rule _ sequent*)
106 ; pl_subst := _ (*@CutRule Judg Rule _ sequent pl_eqv pl_sc*)
107 ; pl_sequent_join := _ (*@SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst*)
112 Instance SystemFCa n Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) (RuleSystemFCa n) :=
113 { pl_eqv := _ (*@ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2)*)
114 ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
115 ; pl_sc := _ (*@SequentCalculus Judg Rule _ sequent*)
116 ; pl_subst := _ (*@CutRule Judg Rule _ sequent pl_eqv pl_sc*)
117 ; pl_sequent_join := _ (*@SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst*)
121 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
122 refine {| plsmme_pl := PCF n Γ Δ |}.
126 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
127 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
132 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
135 (* ... and the retraction exists *)
137 (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so
138 * it falls within (SystemFCa n) for some n. This function calculates that "n" and performs the translation *)
139 (*Definition HaskProof_to_SystemFCa :
140 forall h c (pf:ND Judg h c),
141 { n:nat & h ~~{JudgmentsL SystemFCa_SMME n *)
143 (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
145 Definition ReificationFunctor n : Functor (JudgmentsN n) (JudgmentsN (S n)) (mapOptionTree brakify).
146 refine {| fmor := fun h c (f:h~~{JudgmentsN n}~~>c) => nd_rule (br_nest _ _ _ f) |}; intros; simpl.
152 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
156 Definition makeTree : Tree ??(LeveledHaskType Γ ★) -> HaskType Γ ★.
160 Definition flattenType n (j:JudgmentsN n) : TypesN n.
163 refine (mapOptionTree _ j).
165 destruct j as [ Γ' Δ' Σ τ ].
166 assert (Γ'=Γ). admit.
170 refine (HaskBrak _ ( (makeTree Σ) ---> (makeTree τ) )); intros.
174 Definition FlattenFunctor_fmor n :
176 (h~~{JudgmentsN n}~~>c) ->
177 ((flattenType n h)~~{TypesN n}~~>(flattenType n c)).
179 unfold hom in *; simpl.
187 Definition FlattenFunctor n : Functor (JudgmentsN n) (TypesN n) (flattenType n).
188 refine {| fmor := FlattenFunctor_fmor n |}; intros.
195 Implicit Arguments Rule_PCF [ [h] [c] ].
196 Implicit Arguments BoundedRule [ ].
200 Definition code2garrow0 {Γ}(ec t1 t2:RawHaskType Γ ★) : RawHaskType Γ ★.
203 Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
205 (* | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx t'*)
206 | _ => code2garrow0 ec unitType t
209 Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
210 match ty as TY in RawHaskType _ K return RawHaskType TV K with
211 | TCode ec t => code2garrow _ ec t
212 | TApp _ _ t1 t2 => TApp (typeMap t1) (typeMap t2)
213 | TAll _ f => TAll _ (fun tv => typeMap (f tv))
214 | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
218 | TyFunApp tf rhtl => (* FIXME *) TyFunApp tf rhtl
221 Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
223 (* | t @@ nil => (fun TV ite => typeMap (t TV ite)) @@ lev*)
224 | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
227 Definition coMap {Γ}(ck:HaskCoercionKind Γ) :=
228 fun TV ite => match ck TV ite with
229 | mkRawCoercionKind _ t1 t2 => mkRawCoercionKind _ (typeMap t1) (typeMap t2)
232 Definition flattenCoercion {Γ}{Δ}{ck}(hk:HaskCoercion Γ Δ ck) : HaskCoercion Γ (map coMap Δ) (coMap ck).
236 Lemma update_typeMap Γ (lev:HaskLevel Γ) ξ v t
237 : (typeMap ○ (update_ξ ξ lev ((⟨v, t ⟩) :: nil)))
238 = ( update_ξ (typeMap ○ ξ) lev ((⟨v, typeMap_ t ⟩) :: nil)).
242 Lemma foo κ Γ σ τ : typeMap_ (substT σ τ) = substT(Γ:=Γ)(κ₁:=κ) (fun TV ite => typeMap ○ σ TV ite) τ.
246 Lemma lit_lemma lit Γ : typeMap_ (literalType lit) = literalType(Γ:=Γ) lit.
251 Definition flatten : forall h c, Rule h c -> @ND Judg Rule (mapOptionTree flattenJudgment h) (mapOptionTree flattenJudgment c).
253 refine (match r as R in Rule H C return ND Rule (mapOptionTree flattenJudgment H) (mapOptionTree flattenJudgment C) with
254 | RURule a b c d e => let case_RURule := tt in _
255 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
256 | RLit Γ Δ l _ => let case_RLit := tt in _
257 | RVar Γ Δ σ p => let case_RVar := tt in _
258 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
259 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
260 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
261 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
262 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
263 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
264 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
265 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
266 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
267 | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
268 | REmptyGroup _ _ => let case_REmptyGroup := tt in _
269 | RBrak Σ a b c n m => let case_RBrak := tt in _
270 | REsc Σ a b c n m => let case_REsc := tt in _
271 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
272 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
275 destruct case_RURule.
287 eapply nd_rule. simpl. apply RNote; auto.
292 set (@RNote Γ Δ Σ τ l) as q.
295 Definition flatten' {h}{c} (pf:ND Rule h c) := nd_map' flattenJudgment flatten pf.
298 @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
300 refine (fix flatten : forall Γ Δ Σ τ
301 (pf:SCND Rule [] [Γ > Δ > Σ |- τ ]) :
302 SCND Rule [] [Γ > Δ > mapOptionTree typeMap Σ |- mapOptionTree typeMap τ ] :=
304 | scnd_comp : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c]
305 | scnd_weak : forall c , SCND c []
306 | scnd_leaf : forall ht c , SCND ht [c] -> SCND ht [c]
307 | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2)
308 Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
312 Lemma all_lemma Γ κ σ l :
314 (@HaskTApp (κ :: Γ) κ (@weakF Γ κ ★ σ) (@FreshHaskTyVar Γ κ) @@
315 @weakL Γ κ l)) = (@typeMap Γ (@HaskTAll Γ κ σ @@ l)).
319 Definition flatten : forall Γ Δ ξ τ, Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
320 refine (fix flatten Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') : Expr Γ' (map coMap Δ') (typeMap ○ ξ') (typeMap τ') :=
321 match exp as E in Expr G D X T return Expr G (map coMap D) (typeMap ○ X) (typeMap T) with
322 | EGlobal Γ Δ ξ t wev => EGlobal _ _ _ _ wev
323 | EVar Γ Δ ξ ev => EVar _ _ _ ev
324 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
325 | EApp Γ Δ ξ t1 t2 lev e1 e2 => EApp _ _ _ _ _ _ (flatten _ _ _ _ e1) (flatten _ _ _ _ e2)
326 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in _
327 | ELet Γ Δ ξ tv t l ev elet ebody => let case_ELet := tt in _
328 | ELetRec Γ Δ ξ lev t tree branches ebody => let case_ELetRec := tt in _
329 | ECast Γ Δ ξ t1 t2 γ lev e => let case_ECast := tt in _
330 | ENote Γ Δ ξ t n e => ENote _ _ _ _ n (flatten _ _ _ _ e)
331 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in _
332 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in _
333 | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => let case_ECoApp := tt in _
334 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in _
335 | ECase Γ Δ ξ l tc tbranches atypes e alts' => let case_ECase := tt in _
337 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in _
338 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in _
339 end); clear exp ξ' τ' Γ' Δ'.
347 set (flatten _ _ _ _ e) as q.
348 rewrite update_typeMap in q.
349 apply (@ELam _ _ _ _ _ _ _ _ v q).
352 set (flatten _ _ _ _ ebody) as ebody'.
353 set (flatten _ _ _ _ elet) as elet'.
354 rewrite update_typeMap in ebody'.
355 apply (@ELet _ _ _ _ _ _ _ _ _ elet' ebody').
366 apply flattenCoercion in γ.
369 destruct case_ETyApp.
372 unfold HaskTAll in e.
373 unfold typeMap_ in e.
379 destruct case_ECoLam.
382 set (@ECoLam _ _ _ _ _ _ _ _ _ _ e) as x.
389 destruct case_ECoApp.
393 unfold mkHaskCoercionKind in *.
395 apply flattenCoercion in γ.
396 unfold coMap in γ at 2.
400 destruct case_ETyLam.
402 set (@ETyLam Unique _ Γ (map coMap Δ) (typeMap ○ ξ) κ (fun ite x => typeMap (σ x ite))) as e'.
403 unfold HaskTAll in *.
404 unfold typeMap_ in *.
405 rewrite <- foo in e'.
406 unfold typeMap in e'.
410 Set Printing Implicit.
420 destruct case_ELetRec.
424 (* This proof will work for any dynamic semantics you like, so
425 * long as those semantics are an ND_Relation (associativity,
426 * neutrality, etc) *)
427 Context (dynamic_semantics : @ND_Relation _ Rule).
429 Section SystemFC_Category.
434 Definition Context := Tree ??(LeveledHaskType Γ ★).
436 Notation "a |= b" := (Γ >> Δ > a |- b).
442 SystemFCa_initial_GArrow
445 Context (nd_eqv:@ND_Relation _ (@URule Γ Δ)).
446 Check (@ProgrammingLanguage).
447 Context (PL:@ProgrammingLanguage (LeveledHaskType Γ ★)
448 (fun x y => match x with x1|=x2 => match y with y1|=y2 => @URule Γ Δ)).
449 Definition JudgmentsFC := @Judgments_Category_CartesianCat _ (@URule Γ Δ) nd_eqv.
450 Definition TypesFC := @TypesL _ (@URule Γ Δ) nd_eqv.
452 (* The full subcategory of SystemFC(Γ,Δ) consisting only of judgments involving types at a fixed level. Note that
453 * code types are still permitted! *)
455 Context (lev:HaskLevel Γ).
457 Inductive ContextAtLevel : Context -> Prop :=
458 | contextAtLevel_nil : ContextAtLevel []
459 | contextAtLevel_leaf : forall τ, ContextAtLevel [τ @@ lev]
460 | contextAtLevel_branch : forall b1 b2, ContextAtLevel b1 -> ContextAtLevel b2 -> ContextAtLevel (b1,,b2).
462 Inductive JudgmentsAtLevel : JudgmentsFC -> Prop :=
463 | judgmentsAtLevel_nil : JudgmentsAtLevel []
464 | judgmentsAtLevel_leaf : forall c1 c2, ContextAtLevel c1 -> ContextAtLevel c2 -> JudgmentsAtLevel [c1 |= c2]
465 | judgmentsAtLevel_branch : forall j1 j2, JudgmentsAtLevel j1 -> JudgmentsAtLevel j2 -> JudgmentsAtLevel (j1,,j2).
467 Definition JudgmentsFCAtLevel := FullSubcategory JudgmentsFC JudgmentsAtLevel.
468 Definition TypesFCAtLevel := FullSubcategory TypesFC ContextAtLevel.
471 End SystemFC_Category.
473 Implicit Arguments TypesFC [ ].
476 Section EscBrak_Functor.
480 (Σ₁:Tree ??(@LeveledHaskType V)).
482 Definition EscBrak_Functor_Fobj
483 : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past
484 := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
485 let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])).
487 Definition append_brak
489 (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) c )
490 (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj c)).
493 unfold EscBrak_Functor_Fobj.
494 rewrite mapOptionTree_comp.
502 Definition prepend_esc
504 (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj h))
505 (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) h ).
508 unfold EscBrak_Functor_Fobj.
509 rewrite mapOptionTree_comp.
517 Definition EscBrak_Functor_Fmor
518 : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b),
519 (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b).
529 Lemma esc_then_brak_is_id : forall a,
530 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak)
531 (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))).
535 Lemma brak_then_esc_is_id : forall a,
536 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc)
537 (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)).
541 Instance EscBrak_Functor
542 : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj :=
543 { fmor := fun a b f => EscBrak_Functor_Fmor a b f }.
544 intros; unfold EscBrak_Functor_Fmor; simpl in *.
545 apply ndr_comp_respects; try reflexivity.
546 apply ndr_comp_respects; try reflexivity.
548 intros; unfold EscBrak_Functor_Fmor; simpl in *.
549 set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
551 apply esc_then_brak_is_id.
552 intros; unfold EscBrak_Functor_Fmor; simpl in *.
553 set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q.
554 repeat setoid_rewrite q.
555 apply ndr_comp_respects; try reflexivity.
556 apply ndr_comp_respects; try reflexivity.
557 repeat setoid_rewrite <- q.
558 apply ndr_comp_respects; try reflexivity.
559 setoid_rewrite brak_then_esc_is_id.
561 set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
570 Ltac rule_helper_tactic' :=
572 | [ H : ?A = ?A |- _ ] => clear H
573 | [ H : [?A] = [] |- _ ] => inversion H; clear H
574 | [ H : [] = [?A] |- _ ] => inversion H; clear H
575 | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H
576 | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H
577 | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H
578 | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H
579 | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H
580 | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H
581 (* | [ H : Sequent T |- _ ] => destruct H *)
582 (* | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*)
583 | [ H : [?A] = [?B] |- _ ] => inversion H; clear H
584 | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst
585 | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl
586 | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H
589 Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
593 Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
597 Definition append_brak_to_id : forall {c},
599 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )
600 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
604 Definition append_brak : forall {h c}
607 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )),
610 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
612 refine (fix append_brak h c nd {struct nd} :=
618 (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) ->
619 ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
621 | nd_id0 => let case_nd_id0 := tt in _
622 | nd_id1 h => let case_nd_id1 := tt in _
623 | nd_weak h => let case_nd_weak := tt in _
624 | nd_copy h => let case_nd_copy := tt in _
625 | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
626 | nd_comp _ _ _ top bot => let case_nd_comp := tt in _
627 | nd_rule _ _ rule => let case_nd_rule := tt in _
628 | nd_cancell _ => let case_nd_cancell := tt in _
629 | nd_cancelr _ => let case_nd_cancelr := tt in _
630 | nd_llecnac _ => let case_nd_llecnac := tt in _
631 | nd_rlecnac _ => let case_nd_rlecnac := tt in _
632 | nd_assoc _ _ _ => let case_nd_assoc := tt in _
633 | nd_cossa _ _ _ => let case_nd_cossa := tt in _
634 end) (refl_equal _) (refl_equal _)
636 simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *.
637 destruct case_nd_id0. apply nd_id0.
638 destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak.
639 destruct case_nd_weak. apply nd_weak.
641 destruct case_nd_copy.
643 destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
650 destruct case_nd_prod.
652 apply (append_brak _ _ lpf).
653 apply (append_brak _ _ rpf).
655 destruct case_nd_comp.
656 apply append_brak in bot.
657 apply (nd_comp top bot).
659 destruct case_nd_cancell.
660 eapply nd_comp; [ apply nd_cancell | idtac ].
661 apply append_brak_to_id.
663 destruct case_nd_cancelr.
664 eapply nd_comp; [ apply nd_cancelr | idtac ].
665 apply append_brak_to_id.
667 destruct case_nd_llecnac.
668 eapply nd_comp; [ idtac | apply nd_llecnac ].
669 apply append_brak_to_id.
671 destruct case_nd_rlecnac.
672 eapply nd_comp; [ idtac | apply nd_rlecnac ].
673 apply append_brak_to_id.
675 destruct case_nd_assoc.
676 eapply nd_comp; [ apply nd_assoc | idtac ].
677 repeat rewrite fixit.
678 apply append_brak_to_id.
680 destruct case_nd_cossa.
681 eapply nd_comp; [ idtac | apply nd_cossa ].
682 repeat rewrite fixit.
683 apply append_brak_to_id.
685 destruct case_nd_rule
691 Definition append_brak {h c} : forall
693 (fixify Γ ((⟨n, Σ₁ ⟩) :: past) h )
696 (fixify Γ past (EscBrak_Functor_Fobj h))
702 End HaskProofCategory.