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 FreydCategories.*)
42 (*Require Import ProgrammingLanguage.*)
44 Section HaskProofCategory.
46 Definition unitType {Γ} : RawHaskType Γ ★.
50 Definition brakifyType {Γ} (lt:LeveledHaskType Γ ★) : LeveledHaskType (★ ::Γ) ★ :=
52 t @@ l => HaskBrak (FreshHaskTyVar ★) (weakT t) @@ weakL l
55 Definition brakify (j:Judg) : Judg :=
58 (★ ::Γ) > weakCE Δ > mapOptionTree brakifyType Σ |- mapOptionTree brakifyType τ
61 (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
64 Context {Γ:TypeEnv}{Δ:CoercionEnv Γ}.
66 Inductive Rule_PCF : forall {h}{c}, Rule h c -> Prop :=
67 | PCF_RURule : ∀ h c r , Rule_PCF (RURule Γ Δ h c r)
68 | PCF_RNote : ∀ Σ τ l n , Rule_PCF (RNote Γ Δ Σ τ l n)
69 | PCF_RVar : ∀ σ l, Rule_PCF (RVar Γ Δ σ l)
70 | PCF_RLam : ∀ Σ tx te q , Rule_PCF (RLam Γ Δ Σ tx te q )
71 | PCF_RApp : ∀ Σ tx te p l, Rule_PCF (RApp Γ Δ Σ tx te p l)
72 | PCF_RLet : ∀ Σ σ₁ σ₂ p l, Rule_PCF (RLet Γ Δ Σ σ₁ σ₂ p l)
73 | PCF_RBindingGroup : ∀ q a b c d e , Rule_PCF (RBindingGroup q a b c d e)
74 | PCF_RCase : ∀ T κlen κ θ l x , Rule_PCF (RCase Γ Δ T κlen κ θ l x).
76 Inductive BoundedRule : nat -> Tree ??Judg -> Tree ??Judg -> Type :=
78 (* any proof using only PCF rules is an n-bounded proof for any n>0 *)
79 | br_pcf : forall n h c (r:Rule h c), Rule_PCF r -> BoundedRule n h c
81 (* any n-bounded proof may be used as an (n+1)-bounded proof by prepending Esc and appending Brak *)
82 | br_nest : forall n h c, ND (BoundedRule n) h c -> BoundedRule (S n) (mapOptionTree brakify h) (mapOptionTree brakify c)
85 Context (ndr:forall n, @ND_Relation _ (BoundedRule n)).
87 (* for every n we have a category of n-bounded proofs *)
88 Definition JudgmentsN n := @Judgments_Category_CartesianCat _ (BoundedRule n) (ndr n).
93 Definition TypesNmor (n:nat) (t1 t2:Tree ??(LeveledHaskType Γ ★)) : JudgmentsN n := [Γ > Δ > t1 |- t2].
94 Definition TypesN_id n (t:Tree ??(LeveledHaskType Γ ★)) : ND (BoundedRule n) [] [ Γ > Δ > t |- t ].
97 Definition TypesN_comp n t1 t2 t3 : ND (BoundedRule n) ([Γ > nil > t1 |- t2],,[Γ > nil > t2 |- t3]) [ Γ > nil > t1 |- t3 ].
100 Definition TypesN n : ECategory (JudgmentsN n) (Tree ??(LeveledHaskType Γ ★)) (TypesNmor n).
102 apply {| eid := TypesN_id n ; ecomp := TypesN_comp n |}; intros; simpl.
103 apply (@MonoidalCat_all_central _ _ (JudgmentsN n) _ _ _ (JudgmentsN n)).
104 apply (@MonoidalCat_all_central _ _ (JudgmentsN n) _ _ _ (JudgmentsN n)).
111 (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
112 Definition ReificationFunctor n : Functor (JudgmentsN n) (JudgmentsN (S n)) (mapOptionTree brakify).
113 refine {| fmor := fun h c (f:h~~{JudgmentsN n}~~>c) => nd_rule (br_nest _ _ _ f) |}; intros; simpl.
119 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
123 Definition makeTree : Tree ??(LeveledHaskType Γ ★) -> HaskType Γ ★.
127 Definition flattenType n (j:JudgmentsN n) : TypesN n.
130 refine (mapOptionTree _ j).
132 destruct j as [ Γ' Δ' Σ τ ].
133 assert (Γ'=Γ). admit.
137 refine (HaskBrak _ ( (makeTree Σ) ---> (makeTree τ) )); intros.
141 Definition FlattenFunctor_fmor n :
143 (h~~{JudgmentsN n}~~>c) ->
144 ((flattenType n h)~~{TypesN n}~~>(flattenType n c)).
146 unfold hom in *; simpl.
154 Definition FlattenFunctor n : Functor (JudgmentsN n) (TypesN n) (flattenType n).
155 refine {| fmor := FlattenFunctor_fmor n |}; intros.
162 Implicit Arguments Rule_PCF [ [h] [c] ].
163 Implicit Arguments BoundedRule [ ].
167 Definition code2garrow0 {Γ}(ec t1 t2:RawHaskType Γ ★) : RawHaskType Γ ★.
170 Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
172 (* | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx t'*)
173 | _ => code2garrow0 ec unitType t
176 Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
177 match ty as TY in RawHaskType _ K return RawHaskType TV K with
178 | TCode ec t => code2garrow _ ec t
179 | TApp _ _ t1 t2 => TApp (typeMap t1) (typeMap t2)
180 | TAll _ f => TAll _ (fun tv => typeMap (f tv))
181 | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
185 | TyFunApp tf rhtl => (* FIXME *) TyFunApp tf rhtl
188 Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
190 (* | t @@ nil => (fun TV ite => typeMap (t TV ite)) @@ lev*)
191 | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
194 Definition coMap {Γ}(ck:HaskCoercionKind Γ) :=
195 fun TV ite => match ck TV ite with
196 | mkRawCoercionKind _ t1 t2 => mkRawCoercionKind _ (typeMap t1) (typeMap t2)
199 Definition flattenCoercion {Γ}{Δ}{ck}(hk:HaskCoercion Γ Δ ck) : HaskCoercion Γ (map coMap Δ) (coMap ck).
203 Lemma update_typeMap Γ (lev:HaskLevel Γ) ξ v t
204 : (typeMap ○ (update_ξ ξ lev ((⟨v, t ⟩) :: nil)))
205 = ( update_ξ (typeMap ○ ξ) lev ((⟨v, typeMap_ t ⟩) :: nil)).
209 Lemma foo κ Γ σ τ : typeMap_ (substT σ τ) = substT(Γ:=Γ)(κ₁:=κ) (fun TV ite => typeMap ○ σ TV ite) τ.
213 Lemma lit_lemma lit Γ : typeMap_ (literalType lit) = literalType(Γ:=Γ) lit.
218 Definition flatten : forall h c, Rule h c -> @ND Judg Rule (mapOptionTree flattenJudgment h) (mapOptionTree flattenJudgment c).
220 refine (match r as R in Rule H C return ND Rule (mapOptionTree flattenJudgment H) (mapOptionTree flattenJudgment C) with
221 | RURule a b c d e => let case_RURule := tt in _
222 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
223 | RLit Γ Δ l _ => let case_RLit := tt in _
224 | RVar Γ Δ σ p => let case_RVar := tt in _
225 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
226 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
227 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
228 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
229 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
230 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
231 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
232 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
233 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
234 | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
235 | REmptyGroup _ _ => let case_REmptyGroup := tt in _
236 | RBrak Σ a b c n m => let case_RBrak := tt in _
237 | REsc Σ a b c n m => let case_REsc := tt in _
238 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
239 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
242 destruct case_RURule.
254 eapply nd_rule. simpl. apply RNote; auto.
259 set (@RNote Γ Δ Σ τ l) as q.
262 Definition flatten' {h}{c} (pf:ND Rule h c) := nd_map' flattenJudgment flatten pf.
265 @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
267 refine (fix flatten : forall Γ Δ Σ τ
268 (pf:SCND Rule [] [Γ > Δ > Σ |- τ ]) :
269 SCND Rule [] [Γ > Δ > mapOptionTree typeMap Σ |- mapOptionTree typeMap τ ] :=
271 | scnd_comp : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c]
272 | scnd_weak : forall c , SCND c []
273 | scnd_leaf : forall ht c , SCND ht [c] -> SCND ht [c]
274 | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2)
275 Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
279 Lemma all_lemma Γ κ σ l :
281 (@HaskTApp (κ :: Γ) κ (@weakF Γ κ ★ σ) (@FreshHaskTyVar Γ κ) @@
282 @weakL Γ κ l)) = (@typeMap Γ (@HaskTAll Γ κ σ @@ l)).
286 Definition flatten : forall Γ Δ ξ τ, Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
287 refine (fix flatten Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') : Expr Γ' (map coMap Δ') (typeMap ○ ξ') (typeMap τ') :=
288 match exp as E in Expr G D X T return Expr G (map coMap D) (typeMap ○ X) (typeMap T) with
289 | EGlobal Γ Δ ξ t wev => EGlobal _ _ _ _ wev
290 | EVar Γ Δ ξ ev => EVar _ _ _ ev
291 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
292 | EApp Γ Δ ξ t1 t2 lev e1 e2 => EApp _ _ _ _ _ _ (flatten _ _ _ _ e1) (flatten _ _ _ _ e2)
293 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in _
294 | ELet Γ Δ ξ tv t l ev elet ebody => let case_ELet := tt in _
295 | ELetRec Γ Δ ξ lev t tree branches ebody => let case_ELetRec := tt in _
296 | ECast Γ Δ ξ t1 t2 γ lev e => let case_ECast := tt in _
297 | ENote Γ Δ ξ t n e => ENote _ _ _ _ n (flatten _ _ _ _ e)
298 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in _
299 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in _
300 | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => let case_ECoApp := tt in _
301 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in _
302 | ECase Γ Δ ξ l tc tbranches atypes e alts' => let case_ECase := tt in _
304 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in _
305 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in _
306 end); clear exp ξ' τ' Γ' Δ'.
314 set (flatten _ _ _ _ e) as q.
315 rewrite update_typeMap in q.
316 apply (@ELam _ _ _ _ _ _ _ _ v q).
319 set (flatten _ _ _ _ ebody) as ebody'.
320 set (flatten _ _ _ _ elet) as elet'.
321 rewrite update_typeMap in ebody'.
322 apply (@ELet _ _ _ _ _ _ _ _ _ elet' ebody').
333 apply flattenCoercion in γ.
336 destruct case_ETyApp.
339 unfold HaskTAll in e.
340 unfold typeMap_ in e.
346 destruct case_ECoLam.
349 set (@ECoLam _ _ _ _ _ _ _ _ _ _ e) as x.
356 destruct case_ECoApp.
360 unfold mkHaskCoercionKind in *.
362 apply flattenCoercion in γ.
363 unfold coMap in γ at 2.
367 destruct case_ETyLam.
369 set (@ETyLam Unique _ Γ (map coMap Δ) (typeMap ○ ξ) κ (fun ite x => typeMap (σ x ite))) as e'.
370 unfold HaskTAll in *.
371 unfold typeMap_ in *.
372 rewrite <- foo in e'.
373 unfold typeMap in e'.
377 Set Printing Implicit.
387 destruct case_ELetRec.
391 (* This proof will work for any dynamic semantics you like, so
392 * long as those semantics are an ND_Relation (associativity,
393 * neutrality, etc) *)
394 Context (dynamic_semantics : @ND_Relation _ Rule).
396 Section SystemFC_Category.
401 Definition Context := Tree ??(LeveledHaskType Γ ★).
403 Notation "a |= b" := (Γ >> Δ > a |- b).
409 SystemFCa_initial_GArrow
412 Context (nd_eqv:@ND_Relation _ (@URule Γ Δ)).
413 Check (@ProgrammingLanguage).
414 Context (PL:@ProgrammingLanguage (LeveledHaskType Γ ★)
415 (fun x y => match x with x1|=x2 => match y with y1|=y2 => @URule Γ Δ)).
416 Definition JudgmentsFC := @Judgments_Category_CartesianCat _ (@URule Γ Δ) nd_eqv.
417 Definition TypesFC := @TypesL _ (@URule Γ Δ) nd_eqv.
419 (* The full subcategory of SystemFC(Γ,Δ) consisting only of judgments involving types at a fixed level. Note that
420 * code types are still permitted! *)
422 Context (lev:HaskLevel Γ).
424 Inductive ContextAtLevel : Context -> Prop :=
425 | contextAtLevel_nil : ContextAtLevel []
426 | contextAtLevel_leaf : forall τ, ContextAtLevel [τ @@ lev]
427 | contextAtLevel_branch : forall b1 b2, ContextAtLevel b1 -> ContextAtLevel b2 -> ContextAtLevel (b1,,b2).
429 Inductive JudgmentsAtLevel : JudgmentsFC -> Prop :=
430 | judgmentsAtLevel_nil : JudgmentsAtLevel []
431 | judgmentsAtLevel_leaf : forall c1 c2, ContextAtLevel c1 -> ContextAtLevel c2 -> JudgmentsAtLevel [c1 |= c2]
432 | judgmentsAtLevel_branch : forall j1 j2, JudgmentsAtLevel j1 -> JudgmentsAtLevel j2 -> JudgmentsAtLevel (j1,,j2).
434 Definition JudgmentsFCAtLevel := FullSubcategory JudgmentsFC JudgmentsAtLevel.
435 Definition TypesFCAtLevel := FullSubcategory TypesFC ContextAtLevel.
438 End SystemFC_Category.
440 Implicit Arguments TypesFC [ ].
443 Section EscBrak_Functor.
447 (Σ₁:Tree ??(@LeveledHaskType V)).
449 Definition EscBrak_Functor_Fobj
450 : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past
451 := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
452 let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])).
454 Definition append_brak
456 (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) c )
457 (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj c)).
460 unfold EscBrak_Functor_Fobj.
461 rewrite mapOptionTree_comp.
469 Definition prepend_esc
471 (mapOptionTree (ob2judgment past ) (EscBrak_Functor_Fobj h))
472 (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past)) h ).
475 unfold EscBrak_Functor_Fobj.
476 rewrite mapOptionTree_comp.
484 Definition EscBrak_Functor_Fmor
485 : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b),
486 (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b).
496 Lemma esc_then_brak_is_id : forall a,
497 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak)
498 (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))).
502 Lemma brak_then_esc_is_id : forall a,
503 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc)
504 (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)).
508 Instance EscBrak_Functor
509 : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj :=
510 { fmor := fun a b f => EscBrak_Functor_Fmor a b f }.
511 intros; unfold EscBrak_Functor_Fmor; simpl in *.
512 apply ndr_comp_respects; try reflexivity.
513 apply ndr_comp_respects; try reflexivity.
515 intros; unfold EscBrak_Functor_Fmor; simpl in *.
516 set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
518 apply esc_then_brak_is_id.
519 intros; unfold EscBrak_Functor_Fmor; simpl in *.
520 set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q.
521 repeat setoid_rewrite q.
522 apply ndr_comp_respects; try reflexivity.
523 apply ndr_comp_respects; try reflexivity.
524 repeat setoid_rewrite <- q.
525 apply ndr_comp_respects; try reflexivity.
526 setoid_rewrite brak_then_esc_is_id.
528 set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
537 Ltac rule_helper_tactic' :=
539 | [ H : ?A = ?A |- _ ] => clear H
540 | [ H : [?A] = [] |- _ ] => inversion H; clear H
541 | [ H : [] = [?A] |- _ ] => inversion H; clear H
542 | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H
543 | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H
544 | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H
545 | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H
546 | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H
547 | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H
548 (* | [ H : Sequent T |- _ ] => destruct H *)
549 (* | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*)
550 | [ H : [?A] = [?B] |- _ ] => inversion H; clear H
551 | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst
552 | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl
553 | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H
556 Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
560 Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
564 Definition append_brak_to_id : forall {c},
566 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )
567 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
571 Definition append_brak : forall {h c}
574 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )),
577 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
579 refine (fix append_brak h c nd {struct nd} :=
585 (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) ->
586 ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
588 | nd_id0 => let case_nd_id0 := tt in _
589 | nd_id1 h => let case_nd_id1 := tt in _
590 | nd_weak h => let case_nd_weak := tt in _
591 | nd_copy h => let case_nd_copy := tt in _
592 | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
593 | nd_comp _ _ _ top bot => let case_nd_comp := tt in _
594 | nd_rule _ _ rule => let case_nd_rule := tt in _
595 | nd_cancell _ => let case_nd_cancell := tt in _
596 | nd_cancelr _ => let case_nd_cancelr := tt in _
597 | nd_llecnac _ => let case_nd_llecnac := tt in _
598 | nd_rlecnac _ => let case_nd_rlecnac := tt in _
599 | nd_assoc _ _ _ => let case_nd_assoc := tt in _
600 | nd_cossa _ _ _ => let case_nd_cossa := tt in _
601 end) (refl_equal _) (refl_equal _)
603 simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *.
604 destruct case_nd_id0. apply nd_id0.
605 destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak.
606 destruct case_nd_weak. apply nd_weak.
608 destruct case_nd_copy.
610 destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
617 destruct case_nd_prod.
619 apply (append_brak _ _ lpf).
620 apply (append_brak _ _ rpf).
622 destruct case_nd_comp.
623 apply append_brak in bot.
624 apply (nd_comp top bot).
626 destruct case_nd_cancell.
627 eapply nd_comp; [ apply nd_cancell | idtac ].
628 apply append_brak_to_id.
630 destruct case_nd_cancelr.
631 eapply nd_comp; [ apply nd_cancelr | idtac ].
632 apply append_brak_to_id.
634 destruct case_nd_llecnac.
635 eapply nd_comp; [ idtac | apply nd_llecnac ].
636 apply append_brak_to_id.
638 destruct case_nd_rlecnac.
639 eapply nd_comp; [ idtac | apply nd_rlecnac ].
640 apply append_brak_to_id.
642 destruct case_nd_assoc.
643 eapply nd_comp; [ apply nd_assoc | idtac ].
644 repeat rewrite fixit.
645 apply append_brak_to_id.
647 destruct case_nd_cossa.
648 eapply nd_comp; [ idtac | apply nd_cossa ].
649 repeat rewrite fixit.
650 apply append_brak_to_id.
652 destruct case_nd_rule
658 Definition append_brak {h c} : forall
660 (fixify Γ ((⟨n, Σ₁ ⟩) :: past) h )
663 (fixify Γ past (EscBrak_Functor_Fobj h))
669 End HaskProofCategory.