1 (*********************************************************************************************************************************)
2 (* HaskProgrammingLanguage: *)
4 (* System FC^\alpha is a ProgrammingLanguage. *)
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 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.
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.
36 Require Import HaskStrongTypes.
37 Require Import HaskStrong.
38 Require Import HaskProof.
39 Require Import HaskStrongToProof.
40 Require Import HaskProofToStrong.
41 Require Import ProgrammingLanguage.
46 Section HaskProgrammingLanguage.
48 Context (ndr_systemfc:@ND_Relation _ Rule).
49 Context Γ (Δ:CoercionEnv Γ).
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 :=
56 | org_fc : forall (h c:Tree ??(FCJudg Γ))
57 (r:Rule (mapOptionTree (fcjudg2judg Γ Δ) h) (mapOptionTree (fcjudg2judg Γ Δ) c)),
61 | org_pcf : forall ec h c,
62 ND (PCFRule Γ Δ ec) h c ->
63 OrgR (mapOptionTree (pcfjudg2fcjudg Γ ec) h) (mapOptionTree (pcfjudg2fcjudg Γ ec) c).
65 (* any proof in organized form can be "dis-organized" *)
67 Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c.
75 eapply nd_comp; [ idtac | apply (mkBrak c) ].
80 Definition unOrgND Γ Δ h c : ND (OrgR Γ Δ) h c -> ND Rule h c := nd_map (unOrgR Γ Δ).
83 Definition SystemFCa_cut : forall a b c, ND OrgR ([(a,b)],,[(b,c)]) [(a,c)].
90 (* when the cut is a single leaf and the RHS is a single leaf: *)
97 set (RArrange Γ Δ _ _ _ (RuCanL [l0])) as rule.
98 apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [_])).
100 eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
104 assert (h0=h2). admit.
106 apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2).
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]").
117 Instance SystemFCa_sequents : @SequentND _ OrgR _ _ :=
118 { snd_cut := SystemFCa_cut }.
119 apply Build_SequentND.
126 apply org_fc with (r:=RVar _ _ _ _).
129 apply org_fc with (r:=RVoid _ _ ).
132 eapply nd_comp; [ apply nd_llecnac | idtac ].
133 apply (nd_prod IHa1 IHa2).
135 apply org_fc with (r:=RJoin _ _ _ _ _ _).
145 Definition SystemFCa_left a b c : ND OrgR [(b,c)] [((a,,b),(a,,c))].
148 eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
149 eapply nd_prod; [ apply snd_initial | apply nd_id ].
151 apply org_fc with (r:=RJoin Γ Δ a b a c).
156 Definition SystemFCa_right a b c : ND OrgR [(b,c)] [((b,,a),(c,,a))].
159 eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
160 eapply nd_prod; [ apply nd_id | apply snd_initial ].
162 apply org_fc with (r:=RJoin Γ Δ b a c a).
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 }.
171 intros; apply nd_rule. simpl.
172 apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))).
175 intros; apply nd_rule. simpl.
176 apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto.
178 intros; apply nd_rule. simpl.
179 apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto.
181 intros; apply nd_rule. simpl.
182 apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto.
184 intros; apply nd_rule. simpl.
185 apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto.
187 intros; apply nd_rule. simpl.
188 apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto.
198 Instance OrgFC : @ND_Relation _ OrgR.
201 Instance OrgFC_SequentND_Relation : SequentND_Relation SystemFCa_sequent_join OrgFC.
205 Definition OrgFC_ContextND_Relation
206 : @ContextND_Relation _ _ _ _ _ SystemFCa_sequent_join OrgFC OrgFC_SequentND_Relation.
211 Instance SystemFCa : @ProgrammingLanguage (LeveledHaskType Γ ★) _ :=
212 { pl_eqv := OrgFC_ContextND_Relation
213 ; pl_snd := SystemFCa_sequents
216 End HaskProgrammingLanguage.