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) }.
204 * An intermediate representation necessitated by Coq's termination
205 * conditions. This is basically a tree where each node is a
206 * subproof which is either entirely level-1 or entirely level-0
208 Inductive Alternating : Tree ??Judg -> Type :=
210 | alt_nil : Alternating []
212 | alt_branch : forall a b,
213 Alternating a -> Alternating b -> Alternating (a,,b)
215 | alt_fc : forall h c,
220 | alt_pcf : forall Γ Δ ec h c h' c',
221 MatchingJudgments h h' ->
222 MatchingJudgments c c' ->
224 ND (PCFRule Γ Δ ec) h c ->
227 Require Import Coq.Logic.Eqdep.
229 Lemma magic a b c d ec e :
230 ClosedSIND(Rule:=Rule) [a > b > c |- [d @@ (ec :: e)]] ->
231 ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@ (ec :: nil)]].
235 Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ].
238 fix orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] :=
239 let case_main := tt in _
240 with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c :=
241 (match c as C return C=c -> Alternating C with
242 | T_Leaf None => fun _ => alt_nil
243 | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _
244 | T_Branch b1 b2 => let case_branch := tt in fun eqpf => _
246 with orgify_pcf Γ Δ ec pcfj j (m:MatchingJudgments pcfj j)
247 (pf:ClosedSIND (mapOptionTree (pcfjudg2judg ec) pcfj)) {struct pf} : Alternating j :=
248 let case_pcf := tt in _
253 set (alt_fc _ _ (orgify_fc _ X) (nd_rule X0)) as backup.
254 refine (match X0 as R in Rule H C return
256 | T_Leaf (Some (Γ > Δ > Σ |- τ)) =>
257 h=H -> Alternating [Γ > Δ > Σ |- τ] -> Alternating [Γ > Δ > Σ |- τ]
261 | RBrak Σ a b c n m => let case_RBrak := tt in fun pf' backup => _
262 | REsc Σ a b c n m => let case_REsc := tt in fun pf' backup => _
263 | _ => fun pf' x => x
264 end (refl_equal _) backup).
265 clear backup0 backup.
269 set (@match_leaf Σ0 a ec n [b] m) as q.
270 set (orgify_pcf Σ0 a ec _ _ q) as q'.
278 apply (Prelude_error "encountered Esc in wrong side of mkalt").
285 destruct case_branch.
286 rewrite <- eqpf in pf.
288 apply no_rules_with_multiple_conclusions in X0.
290 exists b1. exists b2.
292 apply (alt_branch _ _ (orgify_fc _ X) (orgify_fc _ X0)).
297 Definition pcfify Γ Δ ec : forall Σ τ,
298 ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]
299 -> ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ].
302 fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn}
303 : ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ] :=
304 (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with
305 | cnd_weak => let case_nil := tt in _
306 | cnd_rule h c cnd' r => let case_rule := tt in _
307 | cnd_branch _ _ c1 c2 => let case_branch := tt in _
308 end (refl_equal _)))).
312 destruct c; try destruct o; inversion H.
316 (* any proof in organized form can be "dis-organized" *)
317 Definition unOrgR : forall h c, OrgR h c -> ND Rule h c.
327 eapply nd_comp; [ idtac | apply (mkBrak c) ].
333 Definition unOrgND h c : ND OrgR h c -> ND Rule h c := nd_map unOrgR.
335 Instance OrgNDR : @ND_Relation _ OrgR :=
336 { ndr_eqv := fun a b f g => (unOrgND _ _ f) === (unOrgND _ _ g) }.
350 Hint Constructors Rule_Flat.
352 Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [pcfjudg x z] [pcfjudg y z].
356 Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([ pcfjudg a b ],,[ pcfjudg b c ]) [ pcfjudg a c ].
363 (* when the cut is a single leaf and the RHS is a single leaf: *)
367 apply (PCF_Arrange [h] ([],,[h]) [h0]).
369 eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
372 set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
374 apply (PCF_RLet _ [] a h0 h).
375 apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]").
376 apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
377 apply (Prelude_error "cut rule invoked with [a|=[]] [[]|=c]").
378 apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
387 Instance PCF_sequents Γ Δ lev : @SequentND _ (PCFRule Γ Δ lev) _ pcfjudg :=
388 { snd_cut := PCF_cut Γ Δ lev }.
389 apply Build_SequentND.
394 exists (RVar _ _ _ _).
400 eapply nd_comp; [ apply nd_llecnac | idtac ].
401 apply (nd_prod IHa1 IHa2).
403 exists (RJoin _ _ _ _ _ _).
408 Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (a,,b) (a,,c)].
409 eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
410 eapply nd_prod; [ apply snd_initial | apply nd_id ].
412 set (@PCF_RJoin Γ Δ lev a b a c) as q'.
413 refine (existT _ _ _).
417 Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (b,,a) (c,,a)].
418 eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
419 eapply nd_prod; [ apply nd_id | apply snd_initial ].
421 set (@PCF_RJoin Γ Δ lev b a c a) as q'.
422 refine (existT _ _ _).
426 Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ pcfjudg _ :=
427 { cnd_expand_left := fun a b c => PCF_left Γ Δ lev c a b
428 ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
437 Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) OrgND.
441 Instance OrgPCF_ContextND_Relation Γ Δ lev : ContextND_Relation (PCF_sequent_join Γ Δ lev).
446 Instance PCF Γ Δ lev : @ProgrammingLanguage _ _ pcfjudg (PCFRule Γ Δ lev) :=
447 { pl_eqv := OrgPCF_ContextND_Relation Γ Δ lev
448 ; pl_snd := PCF_sequents Γ Δ 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,,[]) _).
479 Definition SystemFCa_cut Γ Δ : forall a b c, ND OrgR ([ Γ > Δ > a |- b ],,[ Γ > Δ > b |- c ]) [ Γ > Δ > a |- c ].
486 (* when the cut is a single leaf and the RHS is a single leaf: *)
491 apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [l])).
493 eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
497 assert (h0=h2). admit.
499 apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2).
502 apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[]]").
503 apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
504 apply (Prelude_error "systemfc rule invoked with [a|=[]] [[]|=c]").
505 apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
508 Instance SystemFCa_sequents Γ Δ : @SequentND _ OrgR _ (mkJudg Γ Δ) :=
509 { snd_cut := SystemFCa_cut Γ Δ }.
510 apply Build_SequentND.
516 apply org_fc with (r:=RVar _ _ _ _).
519 apply org_fc with (r:=RVoid _ _ ).
522 eapply nd_comp; [ apply nd_llecnac | idtac ].
523 apply (nd_prod IHa1 IHa2).
525 apply org_fc with (r:=RJoin _ _ _ _ _ _).
530 Definition SystemFCa_left Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (a,,b) |- (a,,c)].
531 eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
532 eapply nd_prod; [ apply snd_initial | apply nd_id ].
534 apply org_fc with (r:=RJoin Γ Δ a b a c).
538 Definition SystemFCa_right Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (b,,a) |- (c,,a)].
539 eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
540 eapply nd_prod; [ apply nd_id | apply snd_initial ].
542 apply org_fc with (r:=RJoin Γ Δ b a c a).
547 Instance SystemFCa_sequent_join Γ Δ : @SequentExpansion _ _ _ _ _ (SystemFCa_sequents Γ Δ) (SystemFCa_cutrule Γ Δ) :=
548 { se_expand_left := SystemFCa_left Γ Δ
549 ; se_expand_right := SystemFCa_right Γ Δ }.
557 Instance SystemFCa Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) OrgR.
560 ; pl_sn := SystemFCa_sequents Γ Δ
561 ; pl_subst := SystemFCa_cutrule Γ Δ
562 ; pl_sequent_join := SystemFCa_sequent_join Γ Δ
564 apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
565 apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa a b c))). apply Flat_RArrange.
566 apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc a b c))). apply Flat_RArrange.
567 apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL a ))). apply Flat_RArrange.
568 apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR a ))). apply Flat_RArrange.
569 apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL a ))). apply Flat_RArrange.
570 apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR a ))). apply Flat_RArrange.
575 End HaskProofStratified.