src/HaskProofCategory.v

   1 (*********************************************************************************************************************************)
   2 (* HaskProofCategory:                                                                                                            *)
   3 (*                                                                                                                               *)
   4 (*    Natural Deduction proofs of the well-typedness of a Haskell term form a category                                           *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   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.
  14
  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.
  22
  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.
  35
  36 Require Import FreydCategories.
  37
  38
  39 Section HaskProofCategory.
  40
  41   (* This proof will work for any dynamic semantics you like, so
  42    * long as those semantics are an ND_Relation (associativity,
  43    * neutrality, etc) *)
  44   Context (dynamic_semantics   : @ND_Relation _ Rule).
  45
  46   Section SystemFC_Category.
  47
  48     Context {Γ:TypeEnv}
  49             {Δ:CoercionEnv Γ}.
  50
  51     Definition Context := Tree ??(LeveledHaskType Γ ★).
  52
  53     Notation "a |= b" := (Γ >> Δ > a |- b).
  54
  55     (* category of judgments in a fixed type/coercion context *)
  56     Definition JudgmentsFC :=
  57       @Judgments_Category_monoidal _ Rule dynamic_semantics (UJudg Γ Δ) UJudg2judg.
  58
  59     Definition identityProof t : [] ~~{JudgmentsFC}~~> [t |= t].
  60       unfold hom; simpl.
  61       admit.
  62       Defined.
  63
  64     Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsFC}~~> [a |= c].
  65       unfold hom; simpl.
  66       admit.
  67       Defined.
  68
  69     Definition TypesFC : ECategory JudgmentsFC Context (fun x y => [Γ >> Δ > x |- y]).
  70       refine
  71       {| eid   := identityProof
  72        ; ecomp := cutProof
  73       |}; intros.
  74       apply MonoidalCat_all_central.
  75       apply MonoidalCat_all_central.
  76       admit.
  77       admit.
  78       admit.
  79       Defined.
  80
  81     Definition TypesEnrichedInJudgments : Enrichment.
  82       refine {| enr_c := TypesFC |}.
  83       Defined.
  84
  85 (*
  86     Definition TwoLevelLanguage L2 :=
  87     { L1 : _ &
  88       Reification (TypesEnrichedInJudgments L1) (TypesEnrichedInJudgments L2) }
  89
  90     Inductive NLevelLanguage : nat -> Language -> Type :=
  91     | NLevelLanguage_zero : forall lang,    NLevelLanguage O lang
  92     | NLevelLanguage_succ : forall L1 L2 n, TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2
  93
  94     Definition OmegaLevelLanguage : Language -> Type :=
  95       forall n:nat, NLevelLanguage n L.
  96 *)
  97
  98
  99     (* The full subcategory of SystemFC(Γ,Δ) consisting only of judgments involving types at a fixed level.  Note that
 100      * code types are still permitted! *)
 101     Section SingleLevel.
 102       Context (lev:HaskLevel Γ).
 103
 104       Inductive ContextAtLevel : Context -> Prop :=
 105         | contextAtLevel_nil    :               ContextAtLevel []
 106         | contextAtLevel_leaf   : forall τ,     ContextAtLevel [τ @@ lev]
 107         | contextAtLevel_branch : forall b1 b2, ContextAtLevel b1 -> ContextAtLevel b2 -> ContextAtLevel (b1,,b2).
 108
 109       Inductive JudgmentsAtLevel : JudgmentsFC -> Prop :=
 110         | judgmentsAtLevel_nil    : JudgmentsAtLevel []
 111         | judgmentsAtLevel_leaf   : forall c1 c2, ContextAtLevel c1 -> ContextAtLevel c2 -> JudgmentsAtLevel [c1 |= c2]
 112         | judgmentsAtLevel_branch : forall j1 j2, JudgmentsAtLevel j1 -> JudgmentsAtLevel j2 -> JudgmentsAtLevel (j1,,j2).
 113
 114       Definition JudgmentsFCAtLevel := FullSubcategory JudgmentsFC JudgmentsAtLevel.
 115       Definition TypesFCAtLevel     := FullSubcategory TypesFC     ContextAtLevel.
 116     End SingleLevel.
 117
 118   End SystemFC_Category.
 119
 120   Implicit Arguments TypesFC [ ].
 121
 122   Definition Types_first c : EFunctor (TypesFC nil nil) (TypesFC nil nil) (fun x => x,,c ).
 123     admit.
 124     Defined.
 125   Definition Types_second c : EFunctor (TypesFC nil nil) (TypesFC nil nil) (fun x => c,,x ).
 126     admit.
 127     Defined.
 128
 129   Definition Types_binoidal : BinoidalCat (TypesFC nil nil) (@T_Branch _).
 130     refine
 131       {| bin_first  := Types_first
 132        ; bin_second := Types_second
 133        |}.
 134     Defined.
 135
 136   Definition Types_premonoidal : PreMonoidalCat Types_binoidal [].
 137     admit.
 138     Defined.
 139
 140 (*
 141   Definition ArrowInProgrammingLanguage :=
 142     FreydCategory Types_premonoidal Types_premonoidal.
 143
 144   FlatSubCategory
 145
 146   InitialGArrowsAllowFlattening
 147
 148   SystemFCa
 149
 150   PCF
 151
 152   SystemFCa_two_level
 153   SystemFCa_initial_GArrow
 154
 155
 156 *)
 157
 158
 159 (*
 160     Section EscBrak_Functor.
 161       Context
 162         (past:@Past V)
 163         (n:V)
 164         (Σ₁:Tree ??(@LeveledHaskType V)).
 165
 166       Definition EscBrak_Functor_Fobj
 167         : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past
 168         := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
 169           let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])).
 170
 171       Definition append_brak
 172       : forall {c}, ND_ML
 173           (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past))                        c )
 174           (mapOptionTree (ob2judgment                   past )  (EscBrak_Functor_Fobj c)).
 175         intros.
 176         unfold ND_ML.
 177         unfold EscBrak_Functor_Fobj.
 178         rewrite mapOptionTree_comp.
 179         simpl in *.
 180         apply nd_replicate.
 181         intro o; destruct o.
 182         apply nd_rule.
 183         apply MLRBrak.
 184         Defined.
 185
 186       Definition prepend_esc
 187       : forall {h}, ND_ML
 188           (mapOptionTree (ob2judgment                  past )  (EscBrak_Functor_Fobj h))
 189           (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past))                        h ).
 190         intros.
 191         unfold ND_ML.
 192         unfold EscBrak_Functor_Fobj.
 193         rewrite mapOptionTree_comp.
 194         simpl in *.
 195         apply nd_replicate.
 196         intro o; destruct o.
 197         apply nd_rule.
 198         apply MLREsc.
 199         Defined.
 200
 201       Definition EscBrak_Functor_Fmor
 202         : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b),
 203           (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b).
 204         intros.
 205         eapply nd_comp.
 206         apply prepend_esc.
 207         eapply nd_comp.
 208         eapply Flat_to_ML.
 209         apply f.
 210         apply append_brak.
 211         Defined.
 212
 213       Lemma esc_then_brak_is_id : forall a,
 214        ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak)
 215          (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))).
 216          admit.
 217          Qed.
 218
 219       Lemma brak_then_esc_is_id : forall a,
 220        ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc)
 221          (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)).
 222          admit.
 223          Qed.
 224
 225       Instance EscBrak_Functor
 226         : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj :=
 227         { fmor := fun a b f => EscBrak_Functor_Fmor a b f }.
 228         intros; unfold EscBrak_Functor_Fmor; simpl in *.
 229           apply ndr_comp_respects; try reflexivity.
 230           apply ndr_comp_respects; try reflexivity.
 231           auto.
 232         intros; unfold EscBrak_Functor_Fmor; simpl in *.
 233           set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
 234           setoid_rewrite q.
 235           apply esc_then_brak_is_id.
 236         intros; unfold EscBrak_Functor_Fmor; simpl in *.
 237           set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q.
 238           repeat setoid_rewrite q.
 239           apply ndr_comp_respects; try reflexivity.
 240           apply ndr_comp_respects; try reflexivity.
 241           repeat setoid_rewrite <- q.
 242           apply ndr_comp_respects; try reflexivity.
 243           setoid_rewrite brak_then_esc_is_id.
 244           clear q.
 245           set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
 246           setoid_rewrite q.
 247           reflexivity.
 248         Defined.
 249
 250     End EscBrak_Functor.
 251
 252
 253
 254   Ltac rule_helper_tactic' :=
 255     match goal with
 256     | [ H : ?A = ?A |- _ ] => clear H
 257     | [ H : [?A] = [] |- _ ] => inversion H; clear H
 258     | [ H : [] = [?A] |- _ ] => inversion H; clear H
 259     | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H
 260     | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H
 261     | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H
 262     | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H
 263     | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H
 264     | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H
 265 (*  | [ H : Sequent T |- _ ] => destruct H *)
 266 (*  | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*)
 267     | [ H : [?A] = [?B] |- _ ] => inversion H; clear H
 268     | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst
 269     | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl
 270     | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H
 271     end.
 272
 273   Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
 274     admit.
 275     Defined.
 276
 277   Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
 278     admit.
 279     Qed.
 280
 281   Definition append_brak_to_id : forall {c},
 282   @ND_FC V
 283       (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past))  c )
 284       (mapOptionTree (ob2judgment past)  (EscBrak_Functor_Fobj c)).
 285   admit.
 286   Defined.
 287
 288   Definition append_brak : forall {h c}
 289     (pf:@ND_FC V
 290       h
 291       (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past))  c )),
 292     @ND_FC V
 293        h
 294       (mapOptionTree (ob2judgment past)  (EscBrak_Functor_Fobj c)).
 295
 296       refine (fix append_brak h c nd {struct nd} :=
 297        ((match nd
 298             as nd'
 299             in @ND _ _ H C
 300             return
 301             (H=h) ->
 302             (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) ->
 303             ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
 304           with
 305           | nd_id0                     => let case_nd_id0     := tt in _
 306           | nd_id1     h               => let case_nd_id1     := tt in _
 307           | nd_weak    h               => let case_nd_weak    := tt in _
 308           | nd_copy    h               => let case_nd_copy    := tt in _
 309           | nd_prod    _ _ _ _ lpf rpf => let case_nd_prod    := tt in _
 310           | nd_comp    _ _ _   top bot => let case_nd_comp    := tt in _
 311           | nd_rule    _ _     rule    => let case_nd_rule    := tt in _
 312           | nd_cancell _               => let case_nd_cancell := tt in _
 313           | nd_cancelr _               => let case_nd_cancelr := tt in _
 314           | nd_llecnac _               => let case_nd_llecnac := tt in _
 315           | nd_rlecnac _               => let case_nd_rlecnac := tt in _
 316           | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
 317           | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
 318         end) (refl_equal _) (refl_equal _)
 319        ));
 320        simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *.
 321        destruct case_nd_id0. apply nd_id0.
 322        destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak.
 323        destruct case_nd_weak. apply nd_weak.
 324
 325        destruct case_nd_copy.
 326          (*
 327          destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
 328          inversion H0; subst.
 329          simpl.*)
 330          idtac.
 331          clear H0.
 332          admit.
 333
 334        destruct case_nd_prod.
 335          eapply nd_prod.
 336          apply (append_brak _ _ lpf).
 337          apply (append_brak _ _ rpf).
 338
 339        destruct case_nd_comp.
 340          apply append_brak in bot.
 341          apply (nd_comp top bot).
 342
 343        destruct case_nd_cancell.
 344          eapply nd_comp; [ apply nd_cancell | idtac ].
 345          apply append_brak_to_id.
 346
 347        destruct case_nd_cancelr.
 348          eapply nd_comp; [ apply nd_cancelr | idtac ].
 349          apply append_brak_to_id.
 350
 351        destruct case_nd_llecnac.
 352          eapply nd_comp; [ idtac | apply nd_llecnac ].
 353          apply append_brak_to_id.
 354
 355        destruct case_nd_rlecnac.
 356          eapply nd_comp; [ idtac | apply nd_rlecnac ].
 357          apply append_brak_to_id.
 358
 359        destruct case_nd_assoc.
 360          eapply nd_comp; [ apply nd_assoc | idtac ].
 361          repeat rewrite fixit.
 362          apply append_brak_to_id.
 363
 364        destruct case_nd_cossa.
 365          eapply nd_comp; [ idtac | apply nd_cossa ].
 366          repeat rewrite fixit.
 367          apply append_brak_to_id.
 368
 369        destruct case_nd_rule
 370
 371
 372
 373     Defined.
 374
 375   Definition append_brak {h c} : forall
 376       pf:@ND_FC V
 377         (fixify Γ ((⟨n, Σ₁ ⟩) :: past)                       h )
 378         c,
 379       @ND_FC V
 380         (fixify Γ                past  (EscBrak_Functor_Fobj h))
 381         c.
 382     admit.
 383     Defined.
 384 *)
 385 End HaskProofCategory.