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 {Γ} (v:HaskTyVar Γ ★)(lt:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
51 t @@ l => HaskBrak v t @@ l
54 Definition brakifyu {Γ}{Δ}(v:HaskTyVar Γ ★)(j:UJudg Γ Δ) : UJudg Γ Δ :=
57 Γ >> Δ > mapOptionTree (brakifyType v) Σ |- mapOptionTree (brakifyType v) τ
60 Definition mkEsc {Γ}{Δ}(j:Tree ??(UJudg Γ Δ)) v h
62 (mapOptionTree (@UJudg2judg Γ Δ) h)
63 (mapOptionTree (fun j => @UJudg2judg Γ Δ (brakifyu v j)) h).
67 Definition mkBrak {Γ}{Δ}(j:Tree ??(UJudg Γ Δ)) v h
69 (mapOptionTree (fun j => @UJudg2judg Γ Δ (brakifyu v j)) h)
70 (mapOptionTree (@UJudg2judg Γ Δ ) h).
74 Context (ndr_systemfc:@ND_Relation _ Rule).
78 (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
79 (* Rule_PCF consists of the rules allowed in flat PCF: everything except
80 * AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *)
81 Inductive Rule_PCF {Γ:TypeEnv}{Δ:CoercionEnv Γ} : forall {h}{c}, Rule h c -> Type :=
82 | PCF_RURule : ∀ h c r , Rule_PCF (RURule Γ Δ h c r)
83 | PCF_RLit : ∀ Σ τ , Rule_PCF (RLit Γ Δ Σ τ )
84 | PCF_RNote : ∀ Σ τ l n , Rule_PCF (RNote Γ Δ Σ τ l n)
85 | PCF_RVar : ∀ σ l, Rule_PCF (RVar Γ Δ σ l)
86 | PCF_RLam : ∀ Σ tx te q , Rule_PCF (RLam Γ Δ Σ tx te q )
87 | PCF_RApp : ∀ Σ tx te p l, Rule_PCF (RApp Γ Δ Σ tx te p l)
88 | PCF_RLet : ∀ Σ σ₁ σ₂ p l, Rule_PCF (RLet Γ Δ Σ σ₁ σ₂ p l)
89 | PCF_RBindingGroup : ∀ q a b c d e , Rule_PCF (RBindingGroup q a b c d e)
90 | PCF_RCase : ∀ T κlen κ θ l x , Rule_PCF (RCase Γ Δ T κlen κ θ l x) (* FIXME: only for boolean and int *)
91 | PCF_REmptyGroup : ∀ q a , Rule_PCF (REmptyGroup q a)
92 | PCF_RLetRec : ∀ Σ₁ τ₁ τ₂ lev , Rule_PCF (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
93 Implicit Arguments Rule_PCF [ ].
95 Definition PCFR Γ Δ h c := { r:_ & Rule_PCF Γ Δ h c r }.
97 (* An organized deduction has been reorganized into contiguous blocks whose
98 * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth. The boolean
99 * indicates if non-PCF rules have been used *)
100 Inductive OrgR : bool -> nat -> forall Γ Δ, Tree ??(UJudg Γ Δ) -> Tree ??(UJudg Γ Δ) -> Type :=
102 | org_pcf : forall n Γ Δ h c b,
103 PCFR Γ Δ (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c) -> OrgR b n Γ Δ h c
105 | org_fc : forall n Γ Δ h c,
106 ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c) -> OrgR true n Γ Δ h c
108 | org_nest : forall n Γ Δ h c b v,
110 OrgR b (S n) _ _ (mapOptionTree (brakifyu v) h) (mapOptionTree (brakifyu v) c)
113 Definition OrgND b n Γ Δ := ND (OrgR b n Γ Δ).
115 (* any proof in organized form can be "dis-organized" *)
116 Definition unOrgR b n Γ Δ : forall h c, OrgR b n Γ Δ h c ->
117 ND Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c).
128 rewrite <- mapOptionTree_compose.
129 rewrite <- mapOptionTree_compose.
132 eapply nd_comp; [ idtac | apply (mkEsc c) ].
136 Definition unOrgND b n Γ Δ h c :
137 ND (OrgR b n Γ Δ) h c -> ND Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c)
138 := nd_map' (@UJudg2judg Γ Δ) (unOrgR b n Γ Δ).
140 Instance OrgNDR b n Γ Δ : @ND_Relation _ (OrgR b n Γ Δ) :=
141 { ndr_eqv := fun a b f g => (unOrgND _ _ _ _ _ _ f) === (unOrgND _ _ _ _ _ _ g) }.
158 Hint Constructors Rule_Flat.
160 Definition SystemFC_SC n : @SequentCalculus _ (RuleSystemFCa n) _ (mkJudg Γ Δ).
161 apply Build_SequentCalculus.
167 apply sfc_flat with (r:=RVar _ _ _ _).
170 apply sfc_flat with (r:=REmptyGroup _ _).
172 eapply nd_comp; [ apply nd_llecnac | idtac ].
173 eapply nd_comp; [ eapply nd_prod | idtac ].
177 apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
181 Existing Instance SystemFC_SC.
183 Lemma systemfc_cut n : ∀a b c,
184 ND (RuleSystemFCa n) ([Γ > Δ > a |- b],, [Γ > Δ > b |- c]) [Γ > Δ > a |- c].
189 Lemma systemfc_cutrule n
190 : @CutRule _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfc n) (SystemFC_SC n).
191 apply Build_CutRule with (nd_cut:=systemfc_cut n).
197 Definition systemfc_left n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > a,, b |- a,, c].
198 eapply nd_comp; [ apply nd_llecnac | idtac ].
199 eapply nd_comp; [ eapply nd_prod | idtac ].
202 apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
205 apply nd_seq_reflexive.
209 Definition systemfc_right n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > b,,a |- c,,a].
210 eapply nd_comp; [ apply nd_rlecnac | idtac ].
211 eapply nd_comp; [ eapply nd_prod | idtac ].
213 apply (nd_seq_reflexive a).
215 apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
220 Definition systemfc_expansion n
221 : @SequentExpansion _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfca n) (SystemFC_SC n) (systemfc_cutrule n).
222 Check (@Build_SequentExpansion).
223 apply (@Build_SequentExpansion _ _ _ _ (ndr_systemfca n) _ _ (systemfc_left n) (systemfc_right n)).
224 refine {| se_expand_left:=systemfc_left n
225 ; se_expand_right:=systemfc_right n |}.
230 Instance SystemFCa n Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR true n Γ Δ) :=
231 { pl_eqv := OrgNDR true n Γ Δ
232 ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
235 ; pl_sequent_join := _
237 apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
238 apply nd_rule; apply org_fc; apply nd_rule; simpl. apply (RURule _ _ _ _ (RCossa _ a b c)).
239 apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RAssoc _ a b c)).
240 apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RCanL _ a )).
241 apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RCanR _ a )).
242 apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RuCanL _ a )).
243 apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RuCanR _ a )).
246 (* "flat" SystemFC: no brackets allowed *)
247 Instance SystemFC Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR true O Γ Δ) :=
248 { pl_eqv := OrgNDR true O Γ Δ
249 ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
252 ; pl_sequent_join := _
257 Instance PCF n Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR false n Γ Δ) :=
258 { pl_eqv := OrgNDR false n Γ Δ
259 ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
262 ; pl_sequent_join := _
264 apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
265 apply nd_rule; apply org_pcf; simpl; exists (RCossa _ a b c); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
266 apply nd_rule; apply org_pcf; simpl; exists (RAssoc _ a b c); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
267 apply nd_rule; apply org_pcf; simpl; exists (RCanL _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
268 apply nd_rule; apply org_pcf; simpl; exists (RCanR _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
269 apply nd_rule; apply org_pcf; simpl; exists (RuCanL _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
270 apply nd_rule; apply org_pcf; simpl; exists (RuCanR _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
273 (* gathers a tree of guest-language types into a single host-language types via the tensor *)
274 Definition tensorizeType {Γ} (lt:Tree ??(LeveledHaskType Γ ★)) : HaskType Γ ★.
278 Definition mkGA {Γ} : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★.
282 Definition guestJudgmentAsGArrowType {Γ}{Δ} (lt:UJudg Γ Δ) : LeveledHaskType Γ ★ :=
285 (mkGA (tensorizeType x) (tensorizeType y)) @@ nil
288 Fixpoint obact n {Γ}{Δ}(X:Tree ??(UJudg Γ Δ)) : Tree ??(LeveledHaskType Γ ★) :=
290 | 0 => mapOptionTree guestJudgmentAsGArrowType X
291 | S n' => let t := obact n' X
292 in [guestJudgmentAsGArrowType (Γ >> Δ > [] |- t )]
298 Definition magic {Γ}{Δ} h c n x :
299 Rule_PCF Γ Δ (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c) x
300 -> ND (OrgR true n Γ Δ) []
301 [Γ >> Δ > mapOptionTree guestJudgmentAsGArrowType h
302 |- mapOptionTree guestJudgmentAsGArrowType c].
307 * Here it is, what you've all been waiting for! When reading this,
308 * it might help to have the definition for "Inductive ND" (see
309 * NaturalDeduction.v) handy as a cross-reference.
311 Definition FlatteningFunctor_fmor {Γ}{Δ}
313 (h~~{JudgmentsL _ _ (PCF 0 Γ Δ)}~~>c) ->
314 ((obact 0 h)~~{TypesL _ _ (SystemFC Γ Δ)}~~>(obact 0 c)).
315 unfold hom; unfold ob; unfold ehom; simpl; unfold mon_i; unfold obact; intros.
319 (* the proof from no hypotheses of no conclusions (nd_id0) becomes REmptyGroup *)
320 apply nd_rule; apply org_fc; simpl. apply nd_rule. apply REmptyGroup.
322 (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
323 apply nd_rule; apply org_fc; simpl. apply nd_rule. destruct (guestJudgmentAsGArrowType h). apply RVar.
325 (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;REmptyGroup *)
326 apply nd_rule; apply org_fc; simpl.
327 eapply nd_comp; [ idtac | apply (nd_rule (RURule _ _ _ _ (RWeak _ _))) ].
328 apply nd_rule. apply REmptyGroup.
330 (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RBindingGroup;;RCont *)
331 eapply nd_comp; [ idtac | eapply nd_rule; eapply org_fc; apply (nd_rule (RURule _ _ _ _ (RCont _ _))) ].
332 eapply nd_comp; [ apply nd_llecnac | idtac ].
333 set (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ)) (mapOptionTree guestJudgmentAsGArrowType h)) as q.
338 apply nd_rule; eapply org_fc.
343 (* nd_prod becomes nd_llecnac;;nd_prod;;RBindingGroup *)
345 apply (nd_llecnac ;; nd_prod IHX1 IHX2).
346 apply nd_rule; apply org_fc; simpl.
347 eapply nd_rule. apply RBindingGroup.
349 (* nd_comp becomes pl_subst (aka nd_cut) *)
351 apply (nd_llecnac ;; nd_prod IHX1 IHX2).
352 clear IHX1 IHX2 X1 X2.
353 apply (@nd_cut _ _ _ _ _ _ (@pl_subst _ _ _ _ (SystemFC Γ Δ))).
355 (* nd_cancell becomes RVar;;RuCanL *)
357 [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RuCanL _ _)) ].
358 apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ))).
360 (* nd_cancelr becomes RVar;;RuCanR *)
362 [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RuCanR _ _)) ].
363 apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ))).
365 (* nd_llecnac becomes RVar;;RCanL *)
367 [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RCanL _ _)) ].
368 apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ))).
370 (* nd_rlecnac becomes RVar;;RCanR *)
372 [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RCanR _ _)) ].
373 apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ))).
375 (* nd_assoc becomes RVar;;RAssoc *)
377 [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RAssoc _ _ _ _)) ].
378 apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ))).
380 (* nd_coss becomes RVar;;RCossa *)
382 [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RCossa _ _ _ _)) ].
383 apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFC Γ Δ))).
385 (* now, the interesting stuff: the inference rules of Judgments(PCF) become GArrow-parameterized terms *)
386 refine (match r as R in OrgR B N G D H C return
389 | O => if B then True
390 else ND (OrgR true 0 G D)
392 [G >> D > mapOptionTree guestJudgmentAsGArrowType H |- mapOptionTree guestJudgmentAsGArrowType C]
394 | org_pcf n Γ Δ h c b r => _
395 | org_fc n Γ Δ h c r => _
396 | org_nest n Γ Δ h c b v q => _
397 end); destruct n; try destruct b; try apply I.
401 rename r0 into r; rename h0 into h; rename c0 into c; rename Γ0 into Γ; rename Δ0 into Δ.
403 refine (match r as R in Rule_PCF G D H C with
404 | PCF_RURule h c r => let case_RURule := tt in _
405 | PCF_RLit Σ τ => let case_RLit := tt in _
406 | PCF_RNote Σ τ l n => let case_RNote := tt in _
407 | PCF_RVar σ l=> let case_RVar := tt in _
408 | PCF_RLam Σ tx te q => let case_RLam := tt in _
409 | PCF_RApp Σ tx te p l=> let case_RApp := tt in _
410 | PCF_RLet Σ σ₁ σ₂ p l=> let case_RLet := tt in _
411 | PCF_RBindingGroup q a b c d e => let case_RBindingGroup := tt in _
412 | PCF_RCase T κlen κ θ l x => let case_RCase := tt in _
413 | PCF_REmptyGroup q a => let case_REmptyGroup := tt in _
414 | PCF_RLetRec Σ₁ τ₁ τ₂ lev => let case_RLetRec := tt in _
418 apply (magic _ _ _ _ r0).
421 Instance FlatteningFunctor {n}{Γ}{Δ} : Functor (JudgmentsL _ _ (PCF n Γ Δ)) (TypesL _ _ (SystemFCa n Γ Δ)) obact :=
422 { fmor := FlatteningFunctor_fmor }.
423 unfold hom; unfold ob; unfold ehom; intros; simpl.
426 Definition productifyType {Γ} (lt:Tree ??(LeveledHaskType Γ ★)) : LeveledHaskType Γ ★.
430 Definition exponent {Γ} : LeveledHaskType Γ ★ -> LeveledHaskType Γ ★ -> LeveledHaskType Γ ★.
434 Definition brakify {Γ}(Σ τ:Tree ??(LeveledHaskType Γ ★)) := exponent (productifyType Σ) (productifyType τ).
436 Definition brakifyJudg (j:Judg) : Judg :=
439 Γ > Δ > [] |- [brakify Σ τ]
442 Definition brakifyUJudg (j:Judg) : Judg :=
445 Γ > Δ > [] |- [brakify Σ τ]
451 Context (ndr_pcf :forall n Γ Δ, @ND_Relation _ (@RulePCF Γ Δ n)).
454 Instance PCF n Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) (@RulePCF Γ Δ n) :=
456 ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
457 ; pl_sc := _ (*@SequentCalculus Judg Rule _ sequent*)
458 ; pl_subst := _ (*@CutRule Judg Rule _ sequent pl_eqv pl_sc*)
459 ; pl_sequent_join := _ (*@SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst*)
463 Inductive RuleX : nat -> Tree ??Judg -> Tree ??Judg -> Type :=
464 | x_flat : forall n h c (r:Rule h c), Rule_Flat r -> RuleX n h c
465 | x_nest : forall n Γ Δ h c, ND (@RulePCF Γ Δ n) h c ->
466 RuleX (S n) (mapOptionTree brakifyJudg h) (mapOptionTree brakifyJudg c).
471 Context (ndr:@ND_Relation _ (RuleX (S n))).
473 Definition SystemFCa' := Judgments_Category ndr.
475 Definition ReificationFunctor_fmor Γ Δ
477 (h~~{JudgmentsL _ _ (PCF n Γ Δ)}~~>c) ->
478 ((mapOptionTree brakifyJudg h)~~{SystemFCa'}~~>(mapOptionTree brakifyJudg c)).
479 unfold hom; unfold ob; simpl.
486 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
487 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
488 unfold ReificationFunctor_fmor; simpl.
490 unfold ReificationFunctor_fmor; simpl.
492 unfold ReificationFunctor_fmor; simpl.
496 Definition FlatteningFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakify).
497 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
498 unfold ReificationFunctor_fmor; simpl.
500 unfold ReificationFunctor_fmor; simpl.
502 unfold ReificationFunctor_fmor; simpl.
506 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
507 refine {| plsmme_pl := PCF n Γ Δ |}.
511 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
512 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
516 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
521 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
523 (* ... and the retraction exists *)
526 (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so
527 * it falls within (SystemFCa n) for some n. This function calculates that "n" and performs the translation *)
529 Definition HaskProof_to_SystemFCa :
530 forall h c (pf:ND Rule h c),
531 { n:nat & h ~~{JudgmentsL (SystemFCa_SMME n)}~~> c }.
534 (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
537 Definition makeTree : Tree ??(LeveledHaskType Γ ★) -> HaskType Γ ★.
541 Definition flattenType n (j:JudgmentsN n) : TypesN n.
544 refine (mapOptionTree _ j).
546 destruct j as [ Γ' Δ' Σ τ ].
547 assert (Γ'=Γ). admit.
551 refine (HaskBrak _ ( (makeTree Σ) ---> (makeTree τ) )); intros.
555 Definition FlattenFunctor_fmor n :
557 (h~~{JudgmentsN n}~~>c) ->
558 ((flattenType n h)~~{TypesN n}~~>(flattenType n c)).
560 unfold hom in *; simpl.
568 Definition FlattenFunctor n : Functor (JudgmentsN n) (TypesN n) (flattenType n).
569 refine {| fmor := FlattenFunctor_fmor n |}; intros.
576 Implicit Arguments Rule_PCF [ [h] [c] ].
577 Implicit Arguments BoundedRule [ ].
581 Definition code2garrow0 {Γ}(ec t1 t2:RawHaskType Γ ★) : RawHaskType Γ ★.
584 Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
586 (* | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx t'*)
587 | _ => code2garrow0 ec unitType t
590 Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
591 match ty as TY in RawHaskType _ K return RawHaskType TV K with
592 | TCode ec t => code2garrow _ ec t
593 | TApp _ _ t1 t2 => TApp (typeMap t1) (typeMap t2)
594 | TAll _ f => TAll _ (fun tv => typeMap (f tv))
595 | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
599 | TyFunApp tf rhtl => (* FIXME *) TyFunApp tf rhtl
602 Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
604 (* | t @@ nil => (fun TV ite => typeMap (t TV ite)) @@ lev*)
605 | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
608 Definition coMap {Γ}(ck:HaskCoercionKind Γ) :=
609 fun TV ite => match ck TV ite with
610 | mkRawCoercionKind _ t1 t2 => mkRawCoercionKind _ (typeMap t1) (typeMap t2)
613 Definition flattenCoercion {Γ}{Δ}{ck}(hk:HaskCoercion Γ Δ ck) : HaskCoercion Γ (map coMap Δ) (coMap ck).
617 Lemma update_typeMap Γ (lev:HaskLevel Γ) ξ v t
618 : (typeMap ○ (update_ξ ξ lev ((⟨v, t ⟩) :: nil)))
619 = ( update_ξ (typeMap ○ ξ) lev ((⟨v, typeMap_ t ⟩) :: nil)).
623 Lemma foo κ Γ σ τ : typeMap_ (substT σ τ) = substT(Γ:=Γ)(κ₁:=κ) (fun TV ite => typeMap ○ σ TV ite) τ.
627 Lemma lit_lemma lit Γ : typeMap_ (literalType lit) = literalType(Γ:=Γ) lit.
632 Definition flatten : forall h c, Rule h c -> @ND Judg Rule (mapOptionTree flattenJudgment h) (mapOptionTree flattenJudgment c).
634 refine (match r as R in Rule H C return ND Rule (mapOptionTree flattenJudgment H) (mapOptionTree flattenJudgment C) with
635 | RURule a b c d e => let case_RURule := tt in _
636 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
637 | RLit Γ Δ l _ => let case_RLit := tt in _
638 | RVar Γ Δ σ p => let case_RVar := tt in _
639 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
640 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
641 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
642 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
643 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
644 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
645 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
646 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
647 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
648 | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
649 | REmptyGroup _ _ => let case_REmptyGroup := tt in _
650 | RBrak Σ a b c n m => let case_RBrak := tt in _
651 | REsc Σ a b c n m => let case_REsc := tt in _
652 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
653 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
656 destruct case_RURule.
668 eapply nd_rule. simpl. apply RNote; auto.
673 set (@RNote Γ Δ Σ τ l) as q.
676 Definition flatten' {h}{c} (pf:ND Rule h c) := nd_map' flattenJudgment flatten pf.
679 @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
681 refine (fix flatten : forall Γ Δ Σ τ
682 (pf:SCND Rule [] [Γ > Δ > Σ |- τ ]) :
683 SCND Rule [] [Γ > Δ > mapOptionTree typeMap Σ |- mapOptionTree typeMap τ ] :=
685 | scnd_comp : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c]
686 | scnd_weak : forall c , SCND c []
687 | scnd_leaf : forall ht c , SCND ht [c] -> SCND ht [c]
688 | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2)
689 Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
693 Lemma all_lemma Γ κ σ l :
695 (@HaskTApp (κ :: Γ) κ (@weakF Γ κ ★ σ) (@FreshHaskTyVar Γ κ) @@
696 @weakL Γ κ l)) = (@typeMap Γ (@HaskTAll Γ κ σ @@ l)).
700 Definition flatten : forall Γ Δ ξ τ, Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
701 refine (fix flatten Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') : Expr Γ' (map coMap Δ') (typeMap ○ ξ') (typeMap τ') :=
702 match exp as E in Expr G D X T return Expr G (map coMap D) (typeMap ○ X) (typeMap T) with
703 | EGlobal Γ Δ ξ t wev => EGlobal _ _ _ _ wev
704 | EVar Γ Δ ξ ev => EVar _ _ _ ev
705 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
706 | EApp Γ Δ ξ t1 t2 lev e1 e2 => EApp _ _ _ _ _ _ (flatten _ _ _ _ e1) (flatten _ _ _ _ e2)
707 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in _
708 | ELet Γ Δ ξ tv t l ev elet ebody => let case_ELet := tt in _
709 | ELetRec Γ Δ ξ lev t tree branches ebody => let case_ELetRec := tt in _
710 | ECast Γ Δ ξ t1 t2 γ lev e => let case_ECast := tt in _
711 | ENote Γ Δ ξ t n e => ENote _ _ _ _ n (flatten _ _ _ _ e)
712 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in _
713 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in _
714 | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => let case_ECoApp := tt in _
715 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in _
716 | ECase Γ Δ ξ l tc tbranches atypes e alts' => let case_ECase := tt in _
718 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in _
719 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in _
720 end); clear exp ξ' τ' Γ' Δ'.
728 set (flatten _ _ _ _ e) as q.
729 rewrite update_typeMap in q.
730 apply (@ELam _ _ _ _ _ _ _ _ v q).
733 set (flatten _ _ _ _ ebody) as ebody'.
734 set (flatten _ _ _ _ elet) as elet'.
735 rewrite update_typeMap in ebody'.
736 apply (@ELet _ _ _ _ _ _ _ _ _ elet' ebody').
747 apply flattenCoercion in γ.
750 destruct case_ETyApp.
753 unfold HaskTAll in e.
754 unfold typeMap_ in e.
760 destruct case_ECoLam.
763 set (@ECoLam _ _ _ _ _ _ _ _ _ _ e) as x.
770 destruct case_ECoApp.
774 unfold mkHaskCoercionKind in *.
776 apply flattenCoercion in γ.
777 unfold coMap in γ at 2.
781 destruct case_ETyLam.
783 set (@ETyLam Unique _ Γ (map coMap Δ) (typeMap ○ ξ) κ (fun ite x => typeMap (σ x ite))) as e'.
784 unfold HaskTAll in *.
785 unfold typeMap_ in *.
786 rewrite <- foo in e'.
787 unfold typeMap in e'.
791 Set Printing Implicit.
801 destruct case_ELetRec.
805 (* This proof will work for any dynamic semantics you like, so
806 * long as those semantics are an ND_Relation (associativity,
807 * neutrality, etc) *)
808 Context (dynamic_semantics : @ND_Relation _ Rule).
810 Section SystemFC_Category.
815 Definition Context := Tree ??(LeveledHaskType Γ ★).
817 Notation "a |= b" := (Γ >> Δ > a |- b).
823 SystemFCa_initial_GArrow
826 Context (nd_eqv:@ND_Relation _ (@URule Γ Δ)).
827 Check (@ProgrammingLanguage).
828 Context (PL:@ProgrammingLanguage (LeveledHaskType Γ ★)
829 (fun x y => match x with x1|=x2 => match y with y1|=y2 => @URule Γ Δ)).
830 Definition JudgmentsFC := @Judgments_Category_CartesianCat _ (@URule Γ Δ) nd_eqv.
831 Definition TypesFC := @TypesL _ (@URule Γ Δ) nd_eqv.
833 (* The full subcategory of SystemFC(Γ,Δ) consisting only of judgments involving types at a fixed level. Note that
834 * code types are still permitted! *)
836 Context (lev:HaskLevel Γ).
838 Inductive ContextAtLevel : Context -> Prop :=
839 | contextAtLevel_nil : ContextAtLevel []
840 | contextAtLevel_leaf : forall τ, ContextAtLevel [τ @@ lev]
841 | contextAtLevel_branch : forall b1 b2, ContextAtLevel b1 -> ContextAtLevel b2 -> ContextAtLevel (b1,,b2).
843 Inductive JudgmentsAtLevel : JudgmentsFC -> Prop :=
844 | judgmentsAtLevel_nil : JudgmentsAtLevel []
845 | judgmentsAtLevel_leaf : forall c1 c2, ContextAtLevel c1 -> ContextAtLevel c2 -> JudgmentsAtLevel [c1 |= c2]
846 | judgmentsAtLevel_branch : forall j1 j2, JudgmentsAtLevel j1 -> JudgmentsAtLevel j2 -> JudgmentsAtLevel (j1,,j2).
848 Definition JudgmentsFCAtLevel := FullSubcategory JudgmentsFC JudgmentsAtLevel.
849 Definition TypesFCAtLevel := FullSubcategory TypesFC ContextAtLevel.
852 End SystemFC_Category.
854 Implicit Arguments TypesFC [ ].
857 Section EscBrak_Functor.
861 (Σ₁:Tree ??(@LeveledHaskType V)).
863 Definition EscBrak_Functor_Fobj
864 : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past
865 := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
866 let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])).
869 Definition EscBrak_Functor_Fmor
870 : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b),
871 (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b).
881 Lemma esc_then_brak_is_id : forall a,
882 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak)
883 (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))).
887 Lemma brak_then_esc_is_id : forall a,
888 ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc)
889 (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)).
893 Instance EscBrak_Functor
894 : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj :=
895 { fmor := fun a b f => EscBrak_Functor_Fmor a b f }.
896 intros; unfold EscBrak_Functor_Fmor; simpl in *.
897 apply ndr_comp_respects; try reflexivity.
898 apply ndr_comp_respects; try reflexivity.
900 intros; unfold EscBrak_Functor_Fmor; simpl in *.
901 set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
903 apply esc_then_brak_is_id.
904 intros; unfold EscBrak_Functor_Fmor; simpl in *.
905 set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q.
906 repeat setoid_rewrite q.
907 apply ndr_comp_respects; try reflexivity.
908 apply ndr_comp_respects; try reflexivity.
909 repeat setoid_rewrite <- q.
910 apply ndr_comp_respects; try reflexivity.
911 setoid_rewrite brak_then_esc_is_id.
913 set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
922 Ltac rule_helper_tactic' :=
924 | [ H : ?A = ?A |- _ ] => clear H
925 | [ H : [?A] = [] |- _ ] => inversion H; clear H
926 | [ H : [] = [?A] |- _ ] => inversion H; clear H
927 | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H
928 | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H
929 | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H
930 | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H
931 | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H
932 | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H
933 (* | [ H : Sequent T |- _ ] => destruct H *)
934 (* | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*)
935 | [ H : [?A] = [?B] |- _ ] => inversion H; clear H
936 | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst
937 | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl
938 | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H
941 Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
945 Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
949 Definition append_brak_to_id : forall {c},
951 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )
952 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
956 Definition append_brak : forall {h c}
959 (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c )),
962 (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c)).
964 refine (fix append_brak h c nd {struct nd} :=
970 (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) ->
971 ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
973 | nd_id0 => let case_nd_id0 := tt in _
974 | nd_id1 h => let case_nd_id1 := tt in _
975 | nd_weak h => let case_nd_weak := tt in _
976 | nd_copy h => let case_nd_copy := tt in _
977 | nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
978 | nd_comp _ _ _ top bot => let case_nd_comp := tt in _
979 | nd_rule _ _ rule => let case_nd_rule := tt in _
980 | nd_cancell _ => let case_nd_cancell := tt in _
981 | nd_cancelr _ => let case_nd_cancelr := tt in _
982 | nd_llecnac _ => let case_nd_llecnac := tt in _
983 | nd_rlecnac _ => let case_nd_rlecnac := tt in _
984 | nd_assoc _ _ _ => let case_nd_assoc := tt in _
985 | nd_cossa _ _ _ => let case_nd_cossa := tt in _
986 end) (refl_equal _) (refl_equal _)
988 simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *.
989 destruct case_nd_id0. apply nd_id0.
990 destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak.
991 destruct case_nd_weak. apply nd_weak.
993 destruct case_nd_copy.
995 destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
1002 destruct case_nd_prod.
1004 apply (append_brak _ _ lpf).
1005 apply (append_brak _ _ rpf).
1007 destruct case_nd_comp.
1008 apply append_brak in bot.
1009 apply (nd_comp top bot).
1011 destruct case_nd_cancell.
1012 eapply nd_comp; [ apply nd_cancell | idtac ].
1013 apply append_brak_to_id.
1015 destruct case_nd_cancelr.
1016 eapply nd_comp; [ apply nd_cancelr | idtac ].
1017 apply append_brak_to_id.
1019 destruct case_nd_llecnac.
1020 eapply nd_comp; [ idtac | apply nd_llecnac ].
1021 apply append_brak_to_id.
1023 destruct case_nd_rlecnac.
1024 eapply nd_comp; [ idtac | apply nd_rlecnac ].
1025 apply append_brak_to_id.
1027 destruct case_nd_assoc.
1028 eapply nd_comp; [ apply nd_assoc | idtac ].
1029 repeat rewrite fixit.
1030 apply append_brak_to_id.
1032 destruct case_nd_cossa.
1033 eapply nd_comp; [ idtac | apply nd_cossa ].
1034 repeat rewrite fixit.
1035 apply append_brak_to_id.
1037 destruct case_nd_rule
1043 Definition append_brak {h c} : forall
1045 (fixify Γ ((⟨n, Σ₁ ⟩) :: past) h )
1048 (fixify Γ past (EscBrak_Functor_Fobj h))
1054 End HaskProofCategory.