src/HaskProgrammingLanguage.v

   1 (*********************************************************************************************************************************)
   2 (* HaskProgrammingLanguage:                                                                                                      *)
   3 (*                                                                                                                               *)
   4 (*    System FC^\alpha is a ProgrammingLanguage.                                                                                 *)
   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 Algebras_ch4.
  16 Require Import Categories_ch1_3.
  17 Require Import Functors_ch1_4.
  18 Require Import Isomorphisms_ch1_5.
  19 Require Import ProductCategories_ch1_6_1.
  20 Require Import OppositeCategories_ch1_6_2.
  21 Require Import Enrichment_ch2_8.
  22 Require Import Subcategories_ch7_1.
  23 Require Import NaturalTransformations_ch7_4.
  24 Require Import NaturalIsomorphisms_ch7_5.
  25 Require Import MonoidalCategories_ch7_8.
  26 Require Import Coherence_ch7_8.
  27
  28 Require Import HaskKinds.
  29 Require Import HaskCoreTypes.
  30 Require Import HaskLiteralsAndTyCons.
  31 Require Import HaskStrongTypes.
  32 Require Import HaskProof.
  33 Require Import NaturalDeduction.
  34 Require Import NaturalDeductionCategory.
  35
  36 Require Import HaskStrongTypes.
  37 Require Import HaskStrong.
  38 Require Import HaskProof.
  39 Require Import HaskStrongToProof.
  40 Require Import HaskProofToStrong.
  41 Require Import ProgrammingLanguage.
  42 Require Import PCF.
  43
  44 Open Scope nd_scope.
  45
  46 Section HaskProgrammingLanguage.
  47
  48   Context (ndr_systemfc:@ND_Relation _ Rule).
  49   Context Γ (Δ:CoercionEnv Γ).
  50
  51   (* An organized deduction has been reorganized into contiguous blocks whose
  52    * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth.  The boolean
  53    * indicates if non-PCF rules have been used *)
  54   Inductive OrgR : Tree ??(@FCJudg Γ) -> Tree ??(@FCJudg Γ) -> Type :=
  55
  56   | org_fc        : forall (h c:Tree ??(FCJudg Γ))
  57     (r:Rule (mapOptionTree (fcjudg2judg Γ Δ) h) (mapOptionTree (fcjudg2judg Γ Δ) c)),
  58     Rule_Flat r ->
  59     OrgR h c
  60
  61   | org_pcf      : forall ec h c,
  62     ND (PCFRule Γ Δ ec)  h c  ->
  63     OrgR                (mapOptionTree (pcfjudg2fcjudg Γ ec) h)  (mapOptionTree (pcfjudg2fcjudg Γ ec) c).
  64
  65   (* any proof in organized form can be "dis-organized" *)
  66   (*
  67   Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c.
  68     intros.
  69     induction X.
  70       apply nd_rule.
  71       apply r.
  72     eapply nd_comp.
  73       (*
  74       apply (mkEsc h).
  75       eapply nd_comp; [ idtac |  apply (mkBrak c) ].
  76       apply pcfToND.
  77       apply n.
  78       *)
  79       Admitted.
  80   Definition unOrgND Γ Δ h c :  ND (OrgR Γ Δ) h c -> ND Rule h c := nd_map (unOrgR Γ Δ).
  81   *)
  82
  83   Definition SystemFCa_cut : forall a b c, ND OrgR ([(a,b)],,[(b,c)]) [(a,c)].
  84     intros.
  85     destruct b.
  86     destruct o.
  87     destruct c.
  88     destruct o.
  89
  90     (* when the cut is a single leaf and the RHS is a single leaf: *)
  91     (*
  92     eapply nd_comp.
  93       eapply nd_prod.
  94       apply nd_id.
  95       eapply nd_rule.
  96       set (@org_fc) as ofc.
  97       set (RArrange Γ Δ _ _ _ (RuCanL [l0])) as rule.
  98       apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [_])).
  99       auto.
 100       eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
 101       apply nd_rule.
 102       destruct l.
 103       destruct l0.
 104       assert (h0=h2). admit.
 105       subst.
 106       apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2).
 107       auto.
 108       auto.
 109       *)
 110     admit.
 111     apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[]]").
 112     apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
 113     apply (Prelude_error "systemfc rule invoked with [a|=[]]  [[]|=c]").
 114     apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
 115     Defined.
 116
 117   Instance SystemFCa_sequents : @SequentND _ OrgR _ _ :=
 118   { snd_cut := SystemFCa_cut }.
 119     apply Build_SequentND.
 120     intros.
 121     induction a.
 122     destruct a; simpl.
 123     (*
 124     apply nd_rule.
 125       destruct l.
 126       apply org_fc with (r:=RVar _ _ _ _).
 127       auto.
 128     apply nd_rule.
 129       apply org_fc with (r:=RVoid _ _ ).
 130       auto.
 131     eapply nd_comp.
 132       eapply nd_comp; [ apply nd_llecnac | idtac ].
 133       apply (nd_prod IHa1 IHa2).
 134       apply nd_rule.
 135         apply org_fc with (r:=RJoin _ _ _ _ _ _).
 136         auto.
 137       admit.
 138       *)
 139       admit.
 140       admit.
 141       admit.
 142       admit.
 143       Defined.
 144
 145   Definition SystemFCa_left a b c : ND OrgR [(b,c)] [((a,,b),(a,,c))].
 146     admit.
 147     (*
 148     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
 149     eapply nd_prod; [ apply snd_initial | apply nd_id ].
 150     apply nd_rule.
 151     apply org_fc with (r:=RJoin Γ Δ a b a c).
 152     auto.
 153     *)
 154     Defined.
 155
 156   Definition SystemFCa_right a b c : ND OrgR [(b,c)] [((b,,a),(c,,a))].
 157     admit.
 158     (*
 159     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
 160     eapply nd_prod; [ apply nd_id | apply snd_initial ].
 161     apply nd_rule.
 162     apply org_fc with (r:=RJoin Γ Δ b a c a).
 163     auto.
 164     *)
 165     Defined.
 166
 167   Instance SystemFCa_sequent_join : @ContextND _ _ _ _ SystemFCa_sequents :=
 168   { cnd_expand_left  := fun a b c => SystemFCa_left  c a b
 169   ; cnd_expand_right := fun a b c => SystemFCa_right c a b }.
 170     (*
 171     intros; apply nd_rule. simpl.
 172       apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))).
 173       auto.
 174
 175     intros; apply nd_rule. simpl.
 176       apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto.
 177
 178     intros; apply nd_rule. simpl.
 179       apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto.
 180
 181     intros; apply nd_rule. simpl.
 182       apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto.
 183
 184     intros; apply nd_rule. simpl.
 185       apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto.
 186
 187     intros; apply nd_rule. simpl.
 188       apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto.
 189       *)
 190       admit.
 191       admit.
 192       admit.
 193       admit.
 194       admit.
 195       admit.
 196       Defined.
 197
 198   Instance OrgFC : @ND_Relation _ OrgR.
 199     Admitted.
 200
 201   Instance OrgFC_SequentND_Relation : SequentND_Relation SystemFCa_sequent_join OrgFC.
 202     admit.
 203     Defined.
 204
 205   Definition OrgFC_ContextND_Relation
 206     : @ContextND_Relation _ _ _ _ _ SystemFCa_sequent_join OrgFC OrgFC_SequentND_Relation.
 207     admit.
 208     Defined.
 209
 210   (* 5.1.2 *)
 211   Instance SystemFCa : @ProgrammingLanguage (LeveledHaskType Γ ★) _ :=
 212   { pl_eqv                := OrgFC_ContextND_Relation
 213   ; pl_snd                := SystemFCa_sequents
 214   }.
 215
 216 End HaskProgrammingLanguage.