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.
60 Context (ndr_systemfc:@ND_Relation _ Rule).
62 Context Γ (Δ:CoercionEnv Γ).
63 Definition PCFJudg (ec:HaskTyVar Γ ★) :=
64 @prod (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
65 Definition pcfjudg (ec:HaskTyVar Γ ★) :=
66 @pair (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
68 (* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg
69 * from depth (depth) by wrapping brackets around everything in the
70 * succedent and repopulating *)
71 Definition brakify {ec} (j:PCFJudg ec) : Judg :=
73 (Σ,τ) => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil)
76 Definition pcf_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
77 := mapOptionTreeAndFlatten (fun lt =>
78 match lt with t @@ l => match l with
79 | ec'::nil => if eqd_dec ec ec' then [t] else []
84 Inductive MatchingJudgments {ec} : Tree ??(PCFJudg ec) -> Tree ??Judg -> Type :=
85 | match_nil : MatchingJudgments [] []
86 | match_branch : forall a b c d, MatchingJudgments a b -> MatchingJudgments c d -> MatchingJudgments (a,,c) (b,,d)
90 [((pcf_vars ec Σ) , τ )]
91 [Γ > Δ > Σ |- (mapOptionTree (HaskBrak ec) τ @@@ lev)].
93 Definition fc_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
94 := mapOptionTreeAndFlatten (fun lt =>
95 match lt with t @@ l => match l with
96 | ec'::nil => if eqd_dec ec ec' then [] else [t]
101 Definition pcfjudg2judg ec (cj:PCFJudg ec) :=
102 match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
104 (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
105 (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
106 (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *)
107 Inductive Rule_PCF (ec:HaskTyVar Γ ★)
108 : forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
109 | PCF_RArrange : ∀ x y t a, Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
110 | PCF_RLit : ∀ lit , Rule_PCF ec [ ] [ ([],[_]) ] (RLit Γ Δ lit (ec::nil))
111 | PCF_RNote : ∀ Σ τ n , Rule_PCF ec [(_,[_])] [(_,[_])] (RNote Γ Δ (Σ@@@(ec::nil)) τ (ec::nil) n)
112 | PCF_RVar : ∀ σ , Rule_PCF ec [ ] [([_],[_])] (RVar Γ Δ σ (ec::nil) )
113 | PCF_RLam : ∀ Σ tx te , Rule_PCF ec [((_,,[_]),[_])] [(_,[_])] (RLam Γ Δ (Σ@@@(ec::nil)) tx te (ec::nil) )
115 | PCF_RApp : ∀ Σ Σ' tx te ,
116 Rule_PCF ec ([(_,[_])],,[(_,[_])]) [((_,,_),[_])]
117 (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil))
119 | PCF_RLet : ∀ Σ Σ' σ₂ p,
120 Rule_PCF ec ([(_,[_])],,[((_,,[_]),[_])]) [((_,,_),[_])]
121 (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil))
123 | PCF_RVoid : Rule_PCF ec [ ] [([],[])] (RVoid Γ Δ )
124 (*| PCF_RLetRec : ∀ Σ₁ τ₁ τ₂ , Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*)
125 | PCF_RJoin : ∀ Σ₁ Σ₂ τ₁ τ₂, Rule_PCF ec ([(_,_)],,[(_,_)]) [((_,,_),(_,,_))]
126 (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
127 (* need int/boolean case *)
128 Implicit Arguments Rule_PCF [ ].
130 Definition PCFRule lev h c := { r:_ & @Rule_PCF lev h c r }.
133 Definition FCJudg Γ (Δ:CoercionEnv Γ) :=
134 @prod (Tree ??(LeveledHaskType Γ ★)) (Tree ??(LeveledHaskType Γ ★)).
135 Definition fcjudg2judg {Γ}{Δ}(fc:FCJudg Γ Δ) :=
137 (x,y) => Γ > Δ > x |- y
139 Coercion fcjudg2judg : FCJudg >-> Judg.
141 Definition pcfjudg2fcjudg {Γ}{Δ} ec (fc:PCFJudg Γ ec) : FCJudg Γ Δ :=
143 (x,y) => (x @@@ (ec::nil),y @@@ (ec::nil))
146 (* An organized deduction has been reorganized into contiguous blocks whose
147 * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth. The boolean
148 * indicates if non-PCF rules have been used *)
149 Inductive OrgR Γ Δ : Tree ??(FCJudg Γ Δ) -> Tree ??(FCJudg Γ Δ) -> Type :=
151 | org_fc : forall (h c:Tree ??(FCJudg Γ Δ))
152 (r:Rule (mapOptionTree fcjudg2judg h) (mapOptionTree fcjudg2judg c)),
156 | org_pcf : forall ec h c,
157 ND (PCFRule Γ Δ ec) h c ->
158 OrgR Γ Δ (mapOptionTree (pcfjudg2fcjudg ec) h) (mapOptionTree (pcfjudg2fcjudg ec) c).
160 Definition mkEsc Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
162 (mapOptionTree (brakify Γ Δ) h)
163 (mapOptionTree (pcfjudg2judg Γ Δ ec) h).
164 apply nd_replicate; intros.
165 destruct o; simpl in *.
171 apply (Prelude_error "mkEsc got multi-leaf succedent").
174 Definition mkBrak Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
176 (mapOptionTree (pcfjudg2judg Γ Δ ec) h)
177 (mapOptionTree (brakify Γ Δ) h).
178 apply nd_replicate; intros.
179 destruct o; simpl in *.
185 apply (Prelude_error "mkBrak got multi-leaf succedent").
189 Definition Partition {Γ} ec (Σ:Tree ??(LeveledHaskType Γ ★)) :=
191 fc_vars ec Σ = fst vars /\
192 pcf_vars ec Σ = snd vars }.
195 Definition pcfToND Γ Δ : forall ec h c,
196 ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c).
198 eapply (fun q => nd_map' _ q X).
205 Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) :=
206 { ndr_eqv := fun a b f g => (pcfToND _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
210 * An intermediate representation necessitated by Coq's termination
211 * conditions. This is basically a tree where each node is a
212 * subproof which is either entirely level-1 or entirely level-0
214 Inductive Alternating : Tree ??Judg -> Type :=
216 | alt_nil : Alternating []
218 | alt_branch : forall a b,
219 Alternating a -> Alternating b -> Alternating (a,,b)
221 | alt_fc : forall h c,
226 | alt_pcf : forall Γ Δ ec h c h' c',
227 MatchingJudgments Γ Δ h h' ->
228 MatchingJudgments Γ Δ c c' ->
230 ND (PCFRule Γ Δ ec) h c ->
233 Require Import Coq.Logic.Eqdep.
235 Lemma magic a b c d ec e :
236 ClosedSIND(Rule:=Rule) [a > b > c |- [d @@ (ec :: e)]] ->
237 ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@ (ec :: nil)]].
241 Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ].
244 fix orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] :=
245 let case_main := tt in _
246 with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c :=
247 (match c as C return C=c -> Alternating C with
248 | T_Leaf None => fun _ => alt_nil
249 | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _
250 | T_Branch b1 b2 => let case_branch := tt in fun eqpf => _
252 with orgify_pcf Γ Δ ec pcfj j (m:MatchingJudgments Γ Δ pcfj j)
253 (pf:ClosedSIND (mapOptionTree (pcfjudg2judg Γ Δ ec) pcfj)) {struct pf} : Alternating j :=
254 let case_pcf := tt in _
259 set (alt_fc _ _ (orgify_fc _ X) (nd_rule X0)) as backup.
260 refine (match X0 as R in Rule H C return
262 | T_Leaf (Some (Γ > Δ > Σ |- τ)) =>
263 h=H -> Alternating [Γ > Δ > Σ |- τ] -> Alternating [Γ > Δ > Σ |- τ]
267 | RBrak Σ a b c n m => let case_RBrak := tt in fun pf' backup => _
268 | REsc Σ a b c n m => let case_REsc := tt in fun pf' backup => _
269 | _ => fun pf' x => x
270 end (refl_equal _) backup).
271 clear backup0 backup.
275 set (@match_leaf Σ0 a ec n [b] m) as q.
276 set (orgify_pcf Σ0 a ec _ _ q) as q'.
284 apply (Prelude_error "encountered Esc in wrong side of mkalt").
291 destruct case_branch.
292 rewrite <- eqpf in pf.
294 apply no_rules_with_multiple_conclusions in X0.
296 exists b1. exists b2.
298 apply (alt_branch _ _ (orgify_fc _ X) (orgify_fc _ X0)).
303 Definition pcfify Γ Δ ec : forall Σ τ,
304 ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]
305 -> ND (PCFRule Γ Δ ec) [] [(Σ,τ)].
308 fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn}
309 : ND (PCFRule Γ Δ ec) [] [(Σ,τ)] :=
310 (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with
311 | cnd_weak => let case_nil := tt in _
312 | cnd_rule h c cnd' r => let case_rule := tt in _
313 | cnd_branch _ _ c1 c2 => let case_branch := tt in _
314 end (refl_equal _)))).
318 destruct c; try destruct o; inversion H.
322 (* any proof in organized form can be "dis-organized" *)
324 Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c.
332 eapply nd_comp; [ idtac | apply (mkBrak c) ].
337 Definition unOrgND Γ Δ h c : ND (OrgR Γ Δ) h c -> ND Rule h c := nd_map (unOrgR Γ Δ).
340 Hint Constructors Rule_Flat.
342 Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)].
346 Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([(a,b)],,[(b,c)]) [(a,c)].
353 (* when the cut is a single leaf and the RHS is a single leaf: *)
357 apply (PCF_Arrange [h] ([],,[h]) [h0]).
359 eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
362 set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
364 apply (PCF_RLet _ [] a h0 h).
365 apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]").
366 apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
367 apply (Prelude_error "cut rule invoked with [a|=[]] [[]|=c]").
368 apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
372 Instance PCF_sequents Γ Δ lev ec : @SequentND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ ec) :=
373 { snd_cut := PCF_cut Γ Δ lev }.
374 apply Build_SequentND.
379 exists (RVar _ _ _ _).
385 eapply nd_comp; [ apply nd_llecnac | idtac ].
386 apply (nd_prod IHa1 IHa2).
388 exists (RJoin _ _ _ _ _ _).
393 Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((a,,b),(a,,c))].
394 eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
395 eapply nd_prod; [ apply snd_initial | apply nd_id ].
397 set (@PCF_RJoin Γ Δ lev a b a c) as q'.
398 refine (existT _ _ _).
402 Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((b,,a),(c,,a))].
403 eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
404 eapply nd_prod; [ apply nd_id | apply snd_initial ].
406 set (@PCF_RJoin Γ Δ lev b a c a) as q'.
407 refine (existT _ _ _).
411 Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ lev) _ :=
412 { cnd_expand_left := fun a b c => PCF_left Γ Δ lev c a b
413 ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
415 intros; apply nd_rule. unfold PCFRule. simpl.
416 exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
417 apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
419 intros; apply nd_rule. unfold PCFRule. simpl.
420 exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
421 apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
423 intros; apply nd_rule. unfold PCFRule. simpl.
424 exists (RArrange _ _ _ _ _ (RCanL _)).
425 apply (PCF_RArrange _ _ lev ([],,a) _ _).
427 intros; apply nd_rule. unfold PCFRule. simpl.
428 exists (RArrange _ _ _ _ _ (RCanR _)).
429 apply (PCF_RArrange _ _ lev (a,,[]) _ _).
431 intros; apply nd_rule. unfold PCFRule. simpl.
432 exists (RArrange _ _ _ _ _ (RuCanL _)).
433 apply (PCF_RArrange _ _ lev _ ([],,a) _).
435 intros; apply nd_rule. unfold PCFRule. simpl.
436 exists (RArrange _ _ _ _ _ (RuCanR _)).
437 apply (PCF_RArrange _ _ lev _ (a,,[]) _).
440 Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev).
444 Definition OrgPCF_ContextND_Relation Γ Δ lev
445 : @ContextND_Relation _ _ _ _ _ (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev) (OrgPCF_SequentND_Relation Γ Δ lev).
450 Instance PCF Γ Δ lev : ProgrammingLanguage :=
451 { pl_cnd := PCF_sequent_join Γ Δ lev
452 ; pl_eqv := OrgPCF_ContextND_Relation Γ Δ lev
455 Definition SystemFCa_cut Γ Δ : forall a b c, ND (OrgR Γ Δ) ([(a,b)],,[(b,c)]) [(a,c)].
462 (* when the cut is a single leaf and the RHS is a single leaf: *)
468 set (@org_fc) as ofc.
469 set (RArrange Γ Δ _ _ _ (RuCanL [l0])) as rule.
470 apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [_])).
472 eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
476 assert (h0=h2). admit.
478 apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2).
483 apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[]]").
484 apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
485 apply (Prelude_error "systemfc rule invoked with [a|=[]] [[]|=c]").
486 apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
489 Instance SystemFCa_sequents Γ Δ : @SequentND _ (OrgR Γ Δ) _ _ :=
490 { snd_cut := SystemFCa_cut Γ Δ }.
491 apply Build_SequentND.
498 apply org_fc with (r:=RVar _ _ _ _).
501 apply org_fc with (r:=RVoid _ _ ).
504 eapply nd_comp; [ apply nd_llecnac | idtac ].
505 apply (nd_prod IHa1 IHa2).
507 apply org_fc with (r:=RJoin _ _ _ _ _ _).
517 Definition SystemFCa_left Γ Δ a b c : ND (OrgR Γ Δ) [(b,c)] [((a,,b),(a,,c))].
520 eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
521 eapply nd_prod; [ apply snd_initial | apply nd_id ].
523 apply org_fc with (r:=RJoin Γ Δ a b a c).
528 Definition SystemFCa_right Γ Δ a b c : ND (OrgR Γ Δ) [(b,c)] [((b,,a),(c,,a))].
531 eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
532 eapply nd_prod; [ apply nd_id | apply snd_initial ].
534 apply org_fc with (r:=RJoin Γ Δ b a c a).
539 Instance SystemFCa_sequent_join Γ Δ : @ContextND _ _ _ _ (SystemFCa_sequents Γ Δ) :=
540 { cnd_expand_left := fun a b c => SystemFCa_left Γ Δ c a b
541 ; cnd_expand_right := fun a b c => SystemFCa_right Γ Δ c a b }.
543 intros; apply nd_rule. simpl.
544 apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))).
547 intros; apply nd_rule. simpl.
548 apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto.
550 intros; apply nd_rule. simpl.
551 apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto.
553 intros; apply nd_rule. simpl.
554 apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto.
556 intros; apply nd_rule. simpl.
557 apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto.
559 intros; apply nd_rule. simpl.
560 apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto.
570 Instance OrgFC Γ Δ : @ND_Relation _ (OrgR Γ Δ).
573 Instance OrgFC_SequentND_Relation Γ Δ : SequentND_Relation (SystemFCa_sequent_join Γ Δ) (OrgFC Γ Δ).
577 Definition OrgFC_ContextND_Relation Γ Δ
578 : @ContextND_Relation _ _ _ _ _ (SystemFCa_sequent_join Γ Δ) (OrgFC Γ Δ) (OrgFC_SequentND_Relation Γ Δ).
583 Instance SystemFCa Γ Δ : @ProgrammingLanguage (LeveledHaskType Γ ★) _ :=
584 { pl_eqv := OrgFC_ContextND_Relation Γ Δ
585 ; pl_snd := SystemFCa_sequents Γ Δ
588 End HaskProofStratified.