1 (*********************************************************************************************************************************)
2 (* HaskProofStratified: *)
4 (* An alternate representation for HaskProof which ensures that deductions on a given level are grouped into contiguous *)
5 (* blocks. This representation lacks the attractive compositionality properties of HaskProof, but makes it easier to *)
6 (* perform the flattening process. *)
8 (*********************************************************************************************************************************)
10 Generalizable All Variables.
11 Require Import Preamble.
12 Require Import General.
13 Require Import NaturalDeduction.
14 Require Import Coq.Strings.String.
15 Require Import Coq.Lists.List.
17 Require Import HaskKinds.
18 Require Import HaskCoreTypes.
19 Require Import HaskLiteralsAndTyCons.
20 Require Import HaskStrongTypes.
21 Require Import HaskProof.
22 Require Import NaturalDeduction.
23 Require Import NaturalDeductionCategory.
25 Require Import Algebras_ch4.
26 Require Import Categories_ch1_3.
27 Require Import Functors_ch1_4.
28 Require Import Isomorphisms_ch1_5.
29 Require Import ProductCategories_ch1_6_1.
30 Require Import OppositeCategories_ch1_6_2.
31 Require Import Enrichment_ch2_8.
32 Require Import Subcategories_ch7_1.
33 Require Import NaturalTransformations_ch7_4.
34 Require Import NaturalIsomorphisms_ch7_5.
35 Require Import MonoidalCategories_ch7_8.
36 Require Import Coherence_ch7_8.
38 Require Import HaskStrongTypes.
39 Require Import HaskStrong.
40 Require Import HaskProof.
41 Require Import HaskStrongToProof.
42 Require Import HaskProofToStrong.
43 Require Import ProgrammingLanguage.
49 * The flattening transformation. Currently only TWO-level languages are
50 * supported, and the level-1 sublanguage is rather limited.
52 * This file abuses terminology pretty badly. For purposes of this file,
53 * "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
54 * the whole language (level-0 language including bracketed level-1 terms)
56 Section HaskProofStratified.
58 Context (ndr_systemfc:@ND_Relation _ Rule).
60 Inductive PCFJudg Γ (Δ:CoercionEnv Γ) (ec:HaskTyVar Γ ★) :=
61 pcfjudg : Tree ??(HaskType Γ ★) -> Tree ??(HaskType Γ ★) -> PCFJudg Γ Δ ec.
62 Implicit Arguments pcfjudg [ [Γ] [Δ] [ec] ].
64 (* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg
65 * from depth (depth) by wrapping brackets around everything in the
66 * succedent and repopulating *)
67 Definition brakify {Γ}{Δ}{ec} (j:PCFJudg Γ Δ ec) : Judg :=
69 pcfjudg Σ τ => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil)
72 Definition pcf_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
73 := mapOptionTreeAndFlatten (fun lt =>
74 match lt with t @@ l => match l with
75 | ec'::nil => if eqd_dec ec ec' then [t] else []
80 Inductive MatchingJudgments {Γ}{Δ}{ec} : Tree ??(PCFJudg Γ Δ ec) -> Tree ??Judg -> Type :=
81 | match_nil : MatchingJudgments [] []
82 | match_branch : forall a b c d, MatchingJudgments a b -> MatchingJudgments c d -> MatchingJudgments (a,,c) (b,,d)
86 [pcfjudg (pcf_vars ec Σ) τ ]
87 [Γ > Δ > Σ |- (mapOptionTree (HaskBrak ec) τ @@@ lev)].
89 Definition fc_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
90 := mapOptionTreeAndFlatten (fun lt =>
91 match lt with t @@ l => match l with
92 | ec'::nil => if eqd_dec ec ec' then [] else [t]
97 Definition pcfjudg2judg {Γ}{Δ:CoercionEnv Γ} ec (cj:PCFJudg Γ Δ ec) :=
98 match cj with pcfjudg Σ τ => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
100 (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
101 (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
102 (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *)
103 Inductive Rule_PCF {Γ}{Δ:CoercionEnv Γ} (ec:HaskTyVar Γ ★)
104 : forall (h c:Tree ??(PCFJudg Γ Δ ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
105 | PCF_RArrange : ∀ x y t a, Rule_PCF ec [pcfjudg _ _ ] [ pcfjudg _ _ ] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
106 | PCF_RLit : ∀ lit , Rule_PCF ec [ ] [ pcfjudg [] [_] ] (RLit Γ Δ lit (ec::nil))
107 | PCF_RNote : ∀ Σ τ n , Rule_PCF ec [pcfjudg _ [_]] [ pcfjudg _ [_] ] (RNote Γ Δ (Σ@@@(ec::nil)) τ (ec::nil) n)
108 | PCF_RVar : ∀ σ , Rule_PCF ec [ ] [ pcfjudg [_] [_] ] (RVar Γ Δ σ (ec::nil) )
109 | PCF_RLam : ∀ Σ tx te , Rule_PCF ec [pcfjudg (_,,[_]) [_] ] [ pcfjudg _ [_] ] (RLam Γ Δ (Σ@@@(ec::nil)) tx te (ec::nil) )
111 | PCF_RApp : ∀ Σ Σ' tx te ,
112 Rule_PCF ec ([pcfjudg _ [_]],,[pcfjudg _ [_]]) [pcfjudg (_,,_) [_]]
113 (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil))
115 | PCF_RLet : ∀ Σ Σ' σ₂ p,
116 Rule_PCF ec ([pcfjudg _ [_]],,[pcfjudg (_,,[_]) [_]]) [pcfjudg (_,,_) [_]]
117 (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil))
119 | PCF_RVoid : Rule_PCF ec [ ] [ pcfjudg [] [] ] (RVoid Γ Δ )
120 (*| PCF_RLetRec : ∀ Σ₁ τ₁ τ₂ , Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*)
121 | PCF_RJoin : ∀ Σ₁ Σ₂ τ₁ τ₂, Rule_PCF ec ([pcfjudg _ _],,[pcfjudg _ _]) [pcfjudg (_,,_) (_,,_)]
122 (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
123 (* need int/boolean case *)
124 Implicit Arguments Rule_PCF [ ].
126 Definition PCFRule Γ Δ lev h c := { r:_ & @Rule_PCF Γ Δ lev h c r }.
128 (* An organized deduction has been reorganized into contiguous blocks whose
129 * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth. The boolean
130 * indicates if non-PCF rules have been used *)
131 Inductive OrgR : Tree ??Judg -> Tree ??Judg -> Type :=
133 | org_fc : forall h c (r:Rule h c),
137 | org_pcf : forall Γ Δ ec h h' c c',
138 MatchingJudgments h h' ->
139 MatchingJudgments c c' ->
140 ND (PCFRule Γ Δ ec) h c ->
143 Definition mkEsc {Γ}{Δ}{ec}(h:Tree ??(PCFJudg Γ Δ ec))
145 (mapOptionTree brakify h)
146 (mapOptionTree (pcfjudg2judg ec) h).
147 apply nd_replicate; intros.
148 destruct o; simpl in *.
154 apply (Prelude_error "mkEsc got multi-leaf succedent").
157 Definition mkBrak {Γ}{Δ}{ec}(h:Tree ??(PCFJudg Γ Δ ec))
159 (mapOptionTree (pcfjudg2judg ec) h)
160 (mapOptionTree brakify h).
161 apply nd_replicate; intros.
162 destruct o; simpl in *.
168 apply (Prelude_error "mkBrak got multi-leaf succedent").
172 Definition Partition {Γ} ec (Σ:Tree ??(LeveledHaskType Γ ★)) :=
174 fc_vars ec Σ = fst vars /\
175 pcf_vars ec Σ = snd vars }.
178 Definition pcfToND : forall Γ Δ ec h c,
179 ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c).
181 eapply (fun q => nd_map' _ q X).
188 Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) :=
189 { ndr_eqv := fun a b f g => (pcfToND _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
206 * An intermediate representation necessitated by Coq's termination
207 * conditions. This is basically a tree where each node is a
208 * subproof which is either entirely level-1 or entirely level-0
210 Inductive Alternating : Tree ??Judg -> Type :=
212 | alt_nil : Alternating []
214 | alt_branch : forall a b,
215 Alternating a -> Alternating b -> Alternating (a,,b)
217 | alt_fc : forall h c,
222 | alt_pcf : forall Γ Δ ec h c h' c',
223 MatchingJudgments h h' ->
224 MatchingJudgments c c' ->
226 ND (PCFRule Γ Δ ec) h c ->
229 Require Import Coq.Logic.Eqdep.
231 Lemma magic a b c d ec e :
232 ClosedSIND(Rule:=Rule) [a > b > c |- [d @@ (ec :: e)]] ->
233 ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@ (ec :: nil)]].
237 Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ].
240 fix orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] :=
241 let case_main := tt in _
242 with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c :=
243 (match c as C return C=c -> Alternating C with
244 | T_Leaf None => fun _ => alt_nil
245 | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _
246 | T_Branch b1 b2 => let case_branch := tt in fun eqpf => _
248 with orgify_pcf Γ Δ ec pcfj j (m:MatchingJudgments pcfj j)
249 (pf:ClosedSIND (mapOptionTree (pcfjudg2judg ec) pcfj)) {struct pf} : Alternating j :=
250 let case_pcf := tt in _
255 set (alt_fc _ _ (orgify_fc _ X) (nd_rule X0)) as backup.
256 refine (match X0 as R in Rule H C return
258 | T_Leaf (Some (Γ > Δ > Σ |- τ)) =>
259 h=H -> Alternating [Γ > Δ > Σ |- τ] -> Alternating [Γ > Δ > Σ |- τ]
263 | RBrak Σ a b c n m => let case_RBrak := tt in fun pf' backup => _
264 | REsc Σ a b c n m => let case_REsc := tt in fun pf' backup => _
265 | _ => fun pf' x => x
266 end (refl_equal _) backup).
267 clear backup0 backup.
271 set (@match_leaf Σ0 a ec n [b] m) as q.
272 set (orgify_pcf Σ0 a ec _ _ q) as q'.
280 apply (Prelude_error "encountered Esc in wrong side of mkalt").
287 destruct case_branch.
288 rewrite <- eqpf in pf.
290 apply no_rules_with_multiple_conclusions in X0.
292 exists b1. exists b2.
294 apply (alt_branch _ _ (orgify_fc _ X) (orgify_fc _ X0)).
299 Definition pcfify Γ Δ ec : forall Σ τ,
300 ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]
301 -> ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ].
304 fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn}
305 : ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ] :=
306 (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with
307 | cnd_weak => let case_nil := tt in _
308 | cnd_rule h c cnd' r => let case_rule := tt in _
309 | cnd_branch _ _ c1 c2 => let case_branch := tt in _
310 end (refl_equal _)))).
314 destruct c; try destruct o; inversion H.
318 (* any proof in organized form can be "dis-organized" *)
319 Definition unOrgR : forall h c, OrgR h c -> ND Rule h c.
329 eapply nd_comp; [ idtac | apply (mkBrak c) ].
335 Definition unOrgND h c : ND OrgR h c -> ND Rule h c := nd_map unOrgR.
337 Instance OrgNDR : @ND_Relation _ OrgR :=
338 { ndr_eqv := fun a b f g => (unOrgND _ _ f) === (unOrgND _ _ g) }.
354 Hint Constructors Rule_Flat.
356 Instance PCF_sequents Γ Δ lev : @SequentCalculus _ (PCFRule Γ Δ lev) _ pcfjudg.
357 apply Build_SequentCalculus.
362 exists (RVar _ _ _ _).
368 eapply nd_comp; [ apply nd_llecnac | idtac ].
369 apply (nd_prod IHa1 IHa2).
371 exists (RJoin _ _ _ _ _ _).
375 Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [pcfjudg x z] [pcfjudg y z].
379 Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([ pcfjudg a b ],,[ pcfjudg b c ]) [ pcfjudg a c ].
386 (* when the cut is a single leaf and the RHS is a single leaf: *)
390 apply (PCF_Arrange [h] ([],,[h]) [h0]).
392 eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
395 set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
397 apply (PCF_RLet _ [] a h0 h).
398 apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]").
399 apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
400 apply (Prelude_error "cut rule invoked with [a|=[]] [[]|=c]").
401 apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
410 Instance PCF_cutrule Γ Δ lev : CutRule (PCF_sequents Γ Δ lev) :=
411 { nd_cut := PCF_cut Γ Δ lev }.
417 Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (a,,b) (a,,c)].
418 eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
419 eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ].
421 set (@PCF_RJoin Γ Δ lev a b a c) as q'.
422 refine (existT _ _ _).
426 Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (b,,a) (c,,a)].
427 eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
428 eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ].
430 set (@PCF_RJoin Γ Δ lev b a c a) as q'.
431 refine (existT _ _ _).
435 Instance PCF_sequent_join Γ Δ lev : @SequentExpansion _ _ _ _ _ (PCF_sequents Γ Δ lev) (PCF_cutrule Γ Δ lev) :=
436 { se_expand_left := PCF_left Γ Δ lev
437 ; se_expand_right := PCF_right Γ Δ lev }.
445 Instance PCF Γ Δ lev : @ProgrammingLanguage _ _ pcfjudg (PCFRule Γ Δ lev) :=
446 { pl_eqv := OrgPCF Γ Δ lev
447 ; pl_sc := PCF_sequents Γ Δ lev
448 ; pl_subst := PCF_cutrule Γ Δ lev
449 ; pl_sequent_join := PCF_sequent_join Γ Δ lev
451 apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
453 apply nd_rule. unfold PCFRule. simpl.
454 exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
455 apply (PCF_RArrange lev ((a,,b),,c) (a,,(b,,c)) x).
457 apply nd_rule. unfold PCFRule. simpl.
458 exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
459 apply (PCF_RArrange lev (a,,(b,,c)) ((a,,b),,c) x).
461 apply nd_rule. unfold PCFRule. simpl.
462 exists (RArrange _ _ _ _ _ (RCanL _)).
463 apply (PCF_RArrange lev ([],,a) _ _).
465 apply nd_rule. unfold PCFRule. simpl.
466 exists (RArrange _ _ _ _ _ (RCanR _)).
467 apply (PCF_RArrange lev (a,,[]) _ _).
469 apply nd_rule. unfold PCFRule. simpl.
470 exists (RArrange _ _ _ _ _ (RuCanL _)).
471 apply (PCF_RArrange lev _ ([],,a) _).
473 apply nd_rule. unfold PCFRule. simpl.
474 exists (RArrange _ _ _ _ _ (RuCanR _)).
475 apply (PCF_RArrange lev _ (a,,[]) _).
478 Instance SystemFCa_sequents Γ Δ : @SequentCalculus _ OrgR _ (mkJudg Γ Δ).
479 apply Build_SequentCalculus.
485 apply org_fc with (r:=RVar _ _ _ _).
488 apply org_fc with (r:=RVoid _ _ ).
491 eapply nd_comp; [ apply nd_llecnac | idtac ].
492 apply (nd_prod IHa1 IHa2).
494 apply org_fc with (r:=RJoin _ _ _ _ _ _).
498 Definition SystemFCa_cut Γ Δ : forall a b c, ND OrgR ([ Γ > Δ > a |- b ],,[ Γ > Δ > b |- c ]) [ Γ > Δ > a |- c ].
505 (* when the cut is a single leaf and the RHS is a single leaf: *)
510 apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [l])).
512 eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
516 assert (h0=h2). admit.
518 apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2).
521 apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[]]").
522 apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
523 apply (Prelude_error "systemfc rule invoked with [a|=[]] [[]|=c]").
524 apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
527 Instance SystemFCa_cutrule Γ Δ : CutRule (SystemFCa_sequents Γ Δ) :=
528 { nd_cut := SystemFCa_cut Γ Δ }.
534 Definition SystemFCa_left Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (a,,b) |- (a,,c)].
535 eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
536 eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ].
538 apply org_fc with (r:=RJoin Γ Δ a b a c).
542 Definition SystemFCa_right Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (b,,a) |- (c,,a)].
543 eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
544 eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ].
546 apply org_fc with (r:=RJoin Γ Δ b a c a).
550 Instance SystemFCa_sequent_join Γ Δ : @SequentExpansion _ _ _ _ _ (SystemFCa_sequents Γ Δ) (SystemFCa_cutrule Γ Δ) :=
551 { se_expand_left := SystemFCa_left Γ Δ
552 ; se_expand_right := SystemFCa_right Γ Δ }.
560 Instance SystemFCa Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) OrgR :=
562 ; pl_sc := SystemFCa_sequents Γ Δ
563 ; pl_subst := SystemFCa_cutrule Γ Δ
564 ; pl_sequent_join := SystemFCa_sequent_join Γ Δ
566 apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
567 apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa a b c))). apply Flat_RArrange.
568 apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc a b c))). apply Flat_RArrange.
569 apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL a ))). apply Flat_RArrange.
570 apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR a ))). apply Flat_RArrange.
571 apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL a ))). apply Flat_RArrange.
572 apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR a ))). apply Flat_RArrange.
575 End HaskProofStratified.