From: Adam Megacz Date: Tue, 3 May 2011 07:01:21 +0000 (-0700) Subject: separate HaskProofStratified into PCF.v, HaskProgrammingLanguage.v, and HaskFlattener... X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=94ad996f571e3c9fd622bc56d9b57118a7e5333a;hp=d6342fb07462cc126df948459ce98ea9caadb95c separate HaskProofStratified into PCF.v, HaskProgrammingLanguage.v, and HaskFlattener.v, major improvements to flattening algorithm --- diff --git a/src/All.v b/src/All.v index d4956dd..9443bbb 100644 --- a/src/All.v +++ b/src/All.v @@ -1,4 +1,7 @@ Require Import ExtractionMain. +Require Import HaskProgrammingLanguage. +Require Import PCF. +Require Import HaskFlattener. Require Import ProgrammingLanguageArrow. Require Import ProgrammingLanguageReification. Require Import ProgrammingLanguageFlattening. diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 35ab0d5..65e0637 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -56,64 +56,693 @@ Open Scope nd_scope. *) Section HaskFlattener. - Context {Γ:TypeEnv}. - Context {Δ:CoercionEnv Γ}. - Context {ec:HaskTyVar Γ ★}. + (* this actually has nothing to do with categories; it shows that proofs [|-A]//[|-B] are one-to-one with []//[A|-B] *) + (* TODO Lemma hom_functor_full*) + + (* lemma: if a proof from no hypotheses contains no Brak's or Esc's, then the context contains no variables at level!=0 *) + + (* In a tree of types, replace any type at level "lev" with None *) + Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) := + mapTree (fun t => match t with + | Some (ttype @@ tlev) => if eqd_dec tlev lev then None else t + | _ => t + end) tt. + (* The opposite: replace any type which is NOT at level "lev" with None *) + Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) := + mapTree (fun t => match t with + | Some (ttype @@ tlev) => if eqd_dec tlev lev then Some ttype else None + | _ => None + end) tt. + + (* In a tree of types, replace any type at depth "lev" or greater None *) + Definition drop_depth {Γ}(n:nat)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) := + mapTree (fun t => match t with + | Some (ttype @@ tlev) => if eqd_dec (length tlev) n then None else t + | _ => t + end) tt. + + (* delete from the tree any type which is NOT at level "lev" *) + + Fixpoint take_lev' {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : ??(Tree ??(HaskType Γ ★)) := + match tt with + | T_Leaf None => Some (T_Leaf None) (* FIXME: unsure of this; it ends up on both sides *) + | T_Branch b1 b2 => + let b1' := take_lev' lev b1 in + let b2' := take_lev' lev b2 in + match b1' with + | None => b2' + | Some b1'' => match b2' with + | None => Some b1'' + | Some b2'' => Some (b1'',,b2'') + end + end + | T_Leaf (Some (ttype@@tlev)) => + if eqd_dec tlev lev + then Some [ttype] + else None + end. + + Context (ga' : forall TV, TV ★ -> Tree ??(RawHaskType TV ★) -> Tree ??(RawHaskType TV ★) -> RawHaskType TV ★). + + Definition ga : forall Γ, HaskTyVar Γ ★ -> Tree ??(HaskType Γ ★) -> Tree ??(HaskType Γ ★) -> HaskType Γ ★ + := fun Γ ec ant suc => + fun TV ite => + ga' + TV + (ec TV ite) + (mapOptionTree (fun x => x TV ite) ant) + (mapOptionTree (fun x => x TV ite) suc). + + Implicit Arguments ga [ [Γ] ]. + Notation "a ~~~~> b" := (@ga _ _ a b) (at level 20). + + Context (unit_type : forall TV, RawHaskType TV ★). + + (* + * The story: + * - code types <[t]>@c become garrows c () t + * - free variables of type t at a level lev deeper than the succedent become garrows c () t + * - free variables at the level of the succedent become + *) + Fixpoint flatten_rawtype {TV}{κ}(depth:nat)(exp: RawHaskType TV κ) : RawHaskType TV κ := + match exp with + | TVar _ x => TVar x + | TAll _ y => TAll _ (fun v => flatten_rawtype depth (y v)) + | TApp _ _ x y => TApp (flatten_rawtype depth x) (flatten_rawtype depth y) + | TCon tc => TCon tc + | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype depth t1) (flatten_rawtype depth t2) (flatten_rawtype depth t) + | TArrow => TArrow + | TCode v e => match depth with + | O => match v return RawHaskType TV ★ with + | TVar ★ ec => ga' TV ec [] [flatten_rawtype depth e] + | _ => unit_type TV + end + | (S depth') => TCode v (flatten_rawtype depth' e) + end + | TyFunApp tfc lt => TyFunApp tfc (flatten_rawtype_list _ depth lt) + end + with flatten_rawtype_list {TV}(lk:list Kind)(depth:nat)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk := + match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with + | TyFunApp_nil => TyFunApp_nil + | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype depth t) (flatten_rawtype_list _ depth rest) + end. + + Inductive AllT {T:Type}{P:T->Prop} : Tree ??T -> Prop := + | allt_none : AllT [] + | allt_some : forall t, P t -> AllT [t] + | allt_branch : forall b1 b2, AllT b1 -> AllT b2 -> AllT (b1,,b2) + . + Implicit Arguments AllT [[T]]. + + Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end. + + Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) := + match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with + Γ > _ > _ |- s => s + end. + + Definition getlev {Γ}{κ}(lht:LeveledHaskType Γ κ) := + match lht with t@@l => l end. + + (* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different + * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it + * picks nil *) + Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ := + match tt with + | T_Leaf None => nil + | T_Leaf (Some (_ @@ lev)) => lev + | T_Branch b1 b2 => + match getjlev b1 with + | nil => getjlev b2 + | lev => lev + end + end. + + (* an XJudg is a Judg for which the SUCCEDENT types all come from the same level, and that level is no deeper than "n" *) + (* even the empty succedent [] has a level... *) + Definition QJudg (n:nat)(j:Judg) := le (length (getjlev (getSuc j))) n. + +(* Definition qjudg2judg {n}(qj:QJudg n) : Judg := projT1 qj.*) + + Inductive QRule : nat -> Tree ??Judg -> Tree ??Judg -> Type := + mkQRule : forall n h c, + Rule h c -> + ITree _ (QJudg n) h -> + ITree _ (QJudg n) c -> + QRule n h c. + + Definition QND n := ND (QRule n). + + (* + * Any type "t" at a level with length "n" becomes (g () t) + * Any type "<[t]>" at a level with length "n-1" becomes (g () t) + *) + + Definition flatten_type {Γ}(n:nat)(ht:HaskType Γ ★) : HaskType Γ ★ := + fun TV ite => + flatten_rawtype n (ht TV ite). + + Definition minus' n m := + match m with + | 0 => n + | _ => n - m + end. + + (* to do: integrate this more cleanly with qjudg *) + Definition flatten_leveled_type {Γ}(n:nat)(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ := + match ht with + htt @@ htlev => + flatten_type (minus' n (length htlev)) htt @@ htlev + end. + + Definition flatten_qjudg_ok (n:nat)(j:Judg) : Judg := + match j with + Γ > Δ > ant |- suc => + let ant' := mapOptionTree (flatten_leveled_type n) ant in + let suc' := mapOptionTree (flatten_leveled_type n) suc + in (Γ > Δ > ant' |- suc') + end. + + Definition take_lev'' {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) := + match (take_lev' lev tt) with + | None => [] + | Some x => x + end. + + Definition flatten_qjudg : forall (n:nat), Judg -> Judg. + refine (fun {n}{j} => + match j as J return Judg with + Γ > Δ > ant |- suc => + match getjlev suc with + | nil => flatten_qjudg_ok n j + | (ec::lev') => if eqd_dec (length lev') n + then let ant_host := drop_depth (S n) ant in + let ant_guest := take_lev (ec::lev') ant in (* FIXME: I want take_lev''!!!!! *) + (Γ > Δ > ant_host |- [ga ec ant_guest (mapOptionTree unlev suc) @@ lev']) + else flatten_qjudg_ok n j + end + end). + Defined. + + Axiom literal_types_unchanged : forall n Γ l, flatten_type n (literalType l) = literalType(Γ:=Γ) l. + + Lemma drop_depth_lemma : forall Γ (lev:HaskLevel Γ) x, drop_depth (length lev) [x @@ lev] = []. + admit. + Defined. + + Lemma drop_depth_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_depth (S (length lev)) [x @@ (ec :: lev)] = []. + admit. + Defined. + + Ltac drop_simplify := + match goal with + | [ |- context[@drop_depth ?G (length ?L) [ ?X @@ ?L ] ] ] => + rewrite (drop_depth_lemma G L X) + | [ |- context[@drop_depth ?G (S (length ?L)) [ ?X @@ (?E :: ?L) ] ] ] => + rewrite (drop_depth_lemma_s G L E X) + | [ |- context[@drop_depth ?G ?N (?A,,?B)] ] => + change (@drop_depth G N (A,,B)) with ((@drop_depth G N A),,(@drop_depth G N B)) + | [ |- context[@drop_depth ?G ?N (T_Leaf None)] ] => + change (@drop_depth G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★))) + end. + + Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [x]. + admit. + Defined. + + Ltac take_simplify := + match goal with + | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] => + rewrite (take_lemma G L X) + | [ |- context[@take_lev ?G ?N (?A,,?B)] ] => + change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B)) + | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] => + change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★))) + end. + + Class garrow := + { ga_id : ∀ Γ Δ ec lev a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a a @@ lev] ] + ; ga_comp : ∀ Γ Δ ec lev a b c, ND Rule [] [Γ > Δ > [@ga Γ ec a b @@ lev],,[@ga Γ ec b c @@ lev] |- [@ga Γ ec a c @@ lev] ] + ; ga_cancelr : ∀ Γ Δ ec lev a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec (a,,[]) a @@ lev] ] + ; ga_cancell : ∀ Γ Δ ec lev a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec ([],,a) a @@ lev] ] + ; ga_uncancelr : ∀ Γ Δ ec lev a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a (a,,[]) @@ lev] ] + ; ga_uncancell : ∀ Γ Δ ec lev a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a ([],,a) @@ lev] ] + ; ga_assoc : ∀ Γ Δ ec lev a b c, ND Rule [] [Γ > Δ > [] |- [@ga Γ ec ((a,,b),,c) (a,,(b,,c)) @@ lev] ] + ; ga_unassoc : ∀ Γ Δ ec lev a b c, ND Rule [] [Γ > Δ > [] |- [@ga Γ ec (a,,(b,,c)) ((a,,b),,c) @@ lev] ] + ; ga_swap : ∀ Γ Δ ec lev a b , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec (a,,b) (b,,a) @@ lev] ] + ; ga_drop : ∀ Γ Δ ec lev a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a [] @@ lev] ] + ; ga_copy : ∀ Γ Δ ec lev a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a (a,,a) @@ lev] ] + ; ga_first : ∀ Γ Δ ec lev a b x, ND Rule [] [Γ > Δ > [@ga Γ ec a b @@ lev] |- [@ga Γ ec (a,,x) (b,,x) @@ lev] ] + ; ga_second : ∀ Γ Δ ec lev a b x, ND Rule [] [Γ > Δ > [@ga Γ ec a b @@ lev] |- [@ga Γ ec (x,,a) (x,,b) @@ lev] ] + ; ga_lit : ∀ Γ Δ ec lev lit , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec [] [literalType lit] @@ lev] ] + ; ga_curry : ∀ Γ Δ ec lev a b c, ND Rule [] [Γ > Δ > [@ga Γ ec (a,,[b]) [c] @@ lev] |- [@ga Γ ec a [b ---> c] @@ lev] ] + ; ga_apply : ∀ Γ Δ ec lev a a' b c, ND Rule [] [Γ > Δ > + [@ga Γ ec a [b ---> c] @@ lev],,[@ga Γ ec a' [b] @@ lev] + |- + [@ga Γ ec (a,,a') [c] @@ lev] ] + }. + + Context (gar:garrow). + + Definition boost : forall Γ Δ ant x y, + ND Rule [] [ Γ > Δ > x |- y ] -> + ND Rule [ Γ > Δ > ant |- x ] [ Γ > Δ > ant |- y ]. + admit. + Defined. + Definition postcompose : ∀ Γ Δ ec lev a b c, + ND Rule [] [ Γ > Δ > [] |- [@ga Γ ec a b @@ lev] ] -> + ND Rule [] [ Γ > Δ > [@ga Γ ec b c @@ lev] |- [@ga Γ ec a c @@ lev] ]. + admit. + Defined. + Definition precompose : ∀ Γ Δ lev a b c x, + ND Rule [] [ Γ > Δ > a |- x,,[b @@ lev] ] -> + ND Rule [] [ Γ > Δ > [b @@ lev] |- [c @@ lev] ] -> + ND Rule [] [ Γ > Δ > a,,x |- [c @@ lev] ]. + admit. + Defined. + + Set Printing Width 130. + + Definition garrowfy_arrangement' : + forall Γ (Δ:CoercionEnv Γ) + (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2), + ND Rule [] [Γ > Δ > [] |- [@ga _ ec (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev] ]. + + intros Γ Δ ec lev. + refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2): + ND Rule [] [Γ > Δ > [] |- [@ga _ ec (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev]] := + match r as R in Arrange A B return + ND Rule [] [Γ > Δ > [] |- [@ga _ ec (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ lev]] + with + | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _ + | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _ + | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _ + | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _ + | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _ + | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _ + | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _ + | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _ + | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _ + | RLeft a b c r' => let case_RLeft := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _) + | RRight a b c r' => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _) + | RComp a b c r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2) + end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros. + + destruct case_RComp. + (* + set (ga_comp Γ Δ ec lev (``c) (``b) (``a)) as q. + eapply precompose. + Focus 2. + apply q. + refine ( _ ;; boost _ _ _ _ _ (ga_comp _ _ _ _ _ _ _)). + apply precompose. + Focus 2. + eapply ga_comp. + *) + admit. + Defined. + + Definition garrowfy_arrangement : + forall Γ (Δ:CoercionEnv Γ) n + (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ, + (*ec :: lev = getjlev succ ->*) + (* H0 : left (Datatypes.length lev ≠ n) e = Peano_dec.eq_nat_dec (Datatypes.length lev) n *) + ND Rule + [Γ > Δ > drop_depth n ant1 |- [@ga _ ec (take_lev (ec :: lev) ant1) (mapOptionTree unlev succ) @@ lev]] + [Γ > Δ > drop_depth n ant2 |- [@ga _ ec (take_lev (ec :: lev) ant2) (mapOptionTree unlev succ) @@ lev]]. + intros. + refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))). + apply nd_rule. + apply RArrange. + refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) := + match r as R in Arrange A B return Arrange (drop_depth _ A) (drop_depth _ B) with + | RCanL a => let case_RCanL := tt in RCanL _ + | RCanR a => let case_RCanR := tt in RCanR _ + | RuCanL a => let case_RuCanL := tt in RuCanL _ + | RuCanR a => let case_RuCanR := tt in RuCanR _ + | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _ + | RCossa a b c => let case_RCossa := tt in RCossa _ _ _ + | RExch a b => let case_RExch := tt in RExch _ _ + | RWeak a => let case_RWeak := tt in RWeak _ + | RCont a => let case_RCont := tt in RCont _ + | RLeft a b c r' => let case_RLeft := tt in RLeft _ (garrowfy _ _ r') + | RRight a b c r' => let case_RRight := tt in RRight _ (garrowfy _ _ r') + | RComp a b c r1 r2 => let case_RComp := tt in RComp (garrowfy _ _ r1) (garrowfy _ _ r2) + end) ant1 ant2 r); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros. + Defined. - Lemma unlev_lemma : forall (x:Tree ??(HaskType Γ ★)) lev, x = mapOptionTree unlev (x @@@ lev). + Definition flatten_arrangement : + forall n Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2), + ND Rule (mapOptionTree (flatten_qjudg n) [Γ > Δ > ant1 |- succ]) + (mapOptionTree (flatten_qjudg n) [Γ > Δ > ant2 |- succ]). intros. - rewrite <- mapOptionTree_compose. - simpl. - induction x. - destruct a; simpl; auto. simpl. - rewrite IHx1 at 1. - rewrite IHx2 at 1. - reflexivity. - Qed. + set (getjlev succ) as succ_lev. + assert (succ_lev=getjlev succ). + reflexivity. + + destruct succ_lev. + apply nd_rule. + apply RArrange. + induction r; simpl. + apply RCanL. + apply RCanR. + apply RuCanL. + apply RuCanR. + apply RAssoc. + apply RCossa. + apply RExch. + apply RWeak. + apply RCont. + apply RLeft; auto. + apply RRight; auto. + eapply RComp; [ apply IHr1 | apply IHr2 ]. + + set (Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n) as lev_is_n. + assert (lev_is_n=Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n). + reflexivity. + destruct lev_is_n. + rewrite <- e. + apply garrowfy_arrangement. + apply r. + auto. + apply nd_rule. + apply RArrange. + induction r; simpl. + apply RCanL. + apply RCanR. + apply RuCanL. + apply RuCanR. + apply RAssoc. + apply RCossa. + apply RExch. + apply RWeak. + apply RCont. + apply RLeft; auto. + apply RRight; auto. + eapply RComp; [ apply IHr1 | apply IHr2 ]. + Defined. + + Lemma flatten_coercion : forall n Γ Δ σ τ (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)), + HaskCoercion Γ Δ (flatten_type n σ ∼∼∼ flatten_type n τ). + admit. + Defined. + + Ltac eqd_dec_refl' := + match goal with + | [ |- context[@eqd_dec ?T ?V ?X ?X] ] => + destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2]; + [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ] + end. + + +(* + Lemma foog : forall Γ Δ, + ND Rule + ( [ Γ > Δ > Σ₁ |- a ],,[ Γ > Δ > Σ₂ |- b ] ) + [ Γ > Δ > Σ₁,,Σ₂ |- a,,b ] +*) + + Notation "` x" := (take_lev _ x) (at level 20). + Notation "`` x" := (mapOptionTree unlev x) (at level 20). + Notation "``` x" := (drop_depth _ x) (at level 20). + + Definition flatten : + forall n {h}{c}, + QND (S n) h c -> + ND Rule (mapOptionTree (flatten_qjudg n) h) (mapOptionTree (flatten_qjudg n) c). + intros. + eapply nd_map'; [ idtac | apply X ]. + clear h c X. + intros. + simpl in *. + + inversion X. + subst. + refine (match X0 as R in Rule H C with + | RArrange Γ Δ a b x d => let case_RArrange := tt in _ + | RNote Γ Δ Σ τ l n => let case_RNote := tt in _ + | RLit Γ Δ l _ => let case_RLit := tt in _ + | RVar Γ Δ σ lev => let case_RVar := tt in _ + | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _ + | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _ + | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _ + | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _ + | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _ + | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _ + | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _ + | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _ + | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _ + | RJoin Γ p lri m x q => let case_RJoin := tt in _ + | RVoid _ _ => let case_RVoid := tt in _ + | RBrak Σ a b c n m => let case_RBrak := tt in _ + | REsc Σ a b c n m => let case_REsc := tt in _ + | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _ + | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _ + end); clear X X0 X1 X2 h c. + + destruct case_RArrange. + apply (flatten_arrangement n Γ Δ a b x d). + + destruct case_RBrak. + admit. + + destruct case_REsc. + admit. + + destruct case_RNote. + simpl. + destruct l; simpl. + apply nd_rule; apply RNote; auto. + destruct (Peano_dec.eq_nat_dec (Datatypes.length l) n). + apply nd_rule; apply RNote; auto. + apply nd_rule; apply RNote; auto. - Context (ga_rep : Tree ??(HaskType Γ ★) -> HaskType Γ ★ ). - Context (ga_type : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★). + destruct case_RLit. + simpl. + destruct l0; simpl. + rewrite literal_types_unchanged. + apply nd_rule; apply RLit. + destruct (Peano_dec.eq_nat_dec (Datatypes.length l0) n); unfold mapTree; unfold mapOptionTree; simpl. + unfold take_lev; simpl. + unfold drop_depth; simpl. + apply ga_lit. + rewrite literal_types_unchanged. + apply nd_rule. + apply RLit. - (*Notation "a ~~~~> b" := (ND Rule [] [ Γ > Δ > a |- b ]) (at level 20).*) - Notation "a ~~~~> b" := (ND (OrgR Γ Δ) [] [ (a , b) ]) (at level 20). + destruct case_RVar. + simpl. + destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RVar | idtac ]. + destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RVar ]; simpl. + rewrite <- e. + clear e n. + repeat drop_simplify. + repeat take_simplify. + apply ga_id. + + destruct case_RGlobal. + simpl. + destruct l as [|ec lev]; simpl; [ apply nd_rule; apply RGlobal; auto | idtac ]. + destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RGlobal; auto ]; simpl. + apply (Prelude_error "found RGlobal at depth >0"). - Lemma magic : forall a b c, - ([] ~~~~> [ga_type a b @@ nil]) -> - ([ga_type b c @@ nil] ~~~~> [ga_type a c @@ nil]). + destruct case_RLam. + simpl. + destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ]. + destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLam; auto ]; simpl. + rewrite <- e. + clear e n. + repeat drop_simplify. + repeat take_simplify. + eapply nd_comp. + eapply nd_rule. + eapply RArrange. + apply RCanR. + apply boost. + apply ga_curry. + + destruct case_RCast. + simpl. + destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ]. + apply flatten_coercion; auto. + destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RCast; auto ]; simpl. + apply (Prelude_error "RCast at level >0"). + apply flatten_coercion; auto. + + destruct case_RJoin. + simpl. + destruct (getjlev x); destruct (getjlev q). + apply nd_rule. + apply RJoin. + apply (Prelude_error "RJoin at depth >0"). + apply (Prelude_error "RJoin at depth >0"). + apply (Prelude_error "RJoin at depth >0"). + + destruct case_RApp. + simpl. + + destruct lev as [|ec lev]. simpl. apply nd_rule. + replace (flatten_type n (tx ---> te)) with ((flatten_type n tx) ---> (flatten_type n te)). + apply RApp. + unfold flatten_type. + simpl. + reflexivity. + + destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n). + eapply nd_comp. + eapply nd_rule. + apply RJoin. + repeat drop_simplify. + repeat take_simplify. + apply boost. + apply ga_apply. + + replace (flatten_type (minus' n (length (ec::lev))) (tx ---> te)) + with ((flatten_type (minus' n (length (ec::lev))) tx) ---> (flatten_type (minus' n (length (ec::lev))) te)). + apply nd_rule. + apply RApp. + unfold flatten_type. + simpl. + reflexivity. + + destruct case_RLet. + simpl. + destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ]. + destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLet; auto ]; simpl. + repeat drop_simplify. + repeat take_simplify. + admit. (* FIXME *) + + destruct case_RVoid. + simpl. + apply nd_rule. + apply RVoid. + + destruct case_RAppT. + simpl. destruct lev; simpl. + admit. + admit. + + destruct case_RAbsT. + simpl. destruct lev; simpl. + admit. + admit. + + destruct case_RAppCo. + simpl. destruct lev; simpl. + admit. + admit. + + destruct case_RAbsCo. + simpl. destruct lev; simpl. + admit. + admit. + + destruct case_RLetRec. + simpl. + admit. + + destruct case_RCase. + simpl. + admit. + Defined. + + Lemma flatten_qjudg_qjudg : forall {n}{j} (q:QJudg (S n) j), QJudg n (flatten_qjudg n j). + admit. + (* + intros. + destruct q. + destruct a. + unfold flatten_qjudg. + destruct j. + destruct (eqd_dec (Datatypes.length x) (S n)). + destruct x. + inversion e. + exists x; split. + simpl in e. + inversion e. + auto. + simpl in *. + apply allt_some. + simpl. + auto. + unfold QJudg. + exists x. + split; auto. + clear a. + Set Printing Implicit. + simpl. + set (length x) as x'. + assert (x'=length x). + reflexivity. + simpl in *. + rewrite <- H. + Unset Printing Implicit. + idtac. + omega. + simpl in *. + induction t0. + destruct a0; simpl in *. + apply allt_some. + inversion a. + subst. + destruct l0. + simpl. + auto. + apply allt_none. + simpl in *. + inversion a; subst. + apply allt_branch. + apply IHt0_1; auto. + apply IHt0_2; auto. + *) + Defined. + + + (* + Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) := + { fmor := FlatteningFunctor_fmor }. + Admitted. + + Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg). + refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros. + Admitted. + + Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME. + refine {| plsmme_pl := PCF n Γ Δ |}. admit. - Qed. - - Context (ga_lit : ∀ lit, [] ~~~~> [ga_type (ga_rep [] ) (ga_rep [literalType lit])@@ nil]). - Context (ga_id : ∀ σ, [] ~~~~> [ga_type (ga_rep σ ) (ga_rep σ )@@ nil]). - Context (ga_cancell : ∀ c , [] ~~~~> [ga_type (ga_rep ([],,c)) (ga_rep c )@@ nil]). - Context (ga_cancelr : ∀ c , [] ~~~~> [ga_type (ga_rep (c,,[])) (ga_rep c )@@ nil]). - Context (ga_uncancell: ∀ c , [] ~~~~> [ga_type (ga_rep c ) (ga_rep ([],,c) )@@ nil]). - Context (ga_uncancelr: ∀ c , [] ~~~~> [ga_type (ga_rep c ) (ga_rep (c,,[]) )@@ nil]). - Context (ga_assoc : ∀ a b c,[] ~~~~> [ga_type (ga_rep ((a,,b),,c)) (ga_rep (a,,(b,,c)) )@@ nil]). - Context (ga_unassoc : ∀ a b c,[] ~~~~> [ga_type (ga_rep ( a,,(b,,c))) (ga_rep ((a,,b),,c)) @@ nil]). - Context (ga_swap : ∀ a b, [] ~~~~> [ga_type (ga_rep (a,,b) ) (ga_rep (b,,a) )@@ nil]). - Context (ga_copy : ∀ a , [] ~~~~> [ga_type (ga_rep a ) (ga_rep (a,,a) )@@ nil]). - Context (ga_drop : ∀ a , [] ~~~~> [ga_type (ga_rep a ) (ga_rep [] )@@ nil]). - Context (ga_first : ∀ a b c, - [ga_type (ga_rep a) (ga_rep b) @@nil] ~~~~> [ga_type (ga_rep (a,,c)) (ga_rep (b,,c)) @@nil]). - Context (ga_second : ∀ a b c, - [ga_type (ga_rep a) (ga_rep b) @@nil] ~~~~> [ga_type (ga_rep (c,,a)) (ga_rep (c,,b)) @@nil]). - Context (ga_comp : ∀ a b c, - ([ga_type (ga_rep a) (ga_rep b) @@nil],,[ga_type (ga_rep b) (ga_rep c) @@nil]) - ~~~~> - [ga_type (ga_rep a) (ga_rep c) @@nil]). - - Definition guestJudgmentAsGArrowType (lt:PCFJudg Γ ec) : HaskType Γ ★ := - match lt with - (x,y) => (ga_type (ga_rep x) (ga_rep y)) - end. + Defined. + + Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME. + refine {| plsmme_pl := SystemFCa n Γ Δ |}. + admit. + Defined. + + Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n). + admit. + Defined. + + (* 5.1.4 *) + Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ). + admit. + Defined. + *) + (* ... and the retraction exists *) + +End HaskFlattener. + - Definition obact (X:Tree ??(PCFJudg Γ ec)) : Tree ??(LeveledHaskType Γ ★) := - mapOptionTree guestJudgmentAsGArrowType X @@@ nil. - Hint Constructors Rule_Flat. - Context {ndr:@ND_Relation _ Rule}. + + + + + + +(* + + Old flattening code; ignore this - just to remind me how I used to do it (* * Here it is, what you've all been waiting for! When reading this, @@ -124,7 +753,7 @@ Section HaskFlattener. Definition FlatteningFunctor_fmor : forall h c, (ND (PCFRule Γ Δ ec) h c) -> - ((obact h)~~~~>(obact c)). + ((obact h)====>(obact c)). set (@nil (HaskTyVar Γ ★)) as lev. @@ -367,36 +996,4 @@ Section HaskFlattener. (* this assumes we want effects to occur in syntactically-left-to-right order *) admit. Defined. - -(* - Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) := - { fmor := FlatteningFunctor_fmor }. - Admitted. - - Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg). - refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros. - Admitted. - - Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME. - refine {| plsmme_pl := PCF n Γ Δ |}. - admit. - Defined. - - Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME. - refine {| plsmme_pl := SystemFCa n Γ Δ |}. - admit. - Defined. - - Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n). - admit. - Defined. - - (* 5.1.4 *) - Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ). - admit. - Defined. -*) - (* ... and the retraction exists *) - -End HaskFlattener. - +*) \ No newline at end of file diff --git a/src/HaskProgrammingLanguage.v b/src/HaskProgrammingLanguage.v index 0d612d6..9801168 100644 --- a/src/HaskProgrammingLanguage.v +++ b/src/HaskProgrammingLanguage.v @@ -39,48 +39,26 @@ Require Import HaskProof. Require Import HaskStrongToProof. Require Import HaskProofToStrong. Require Import ProgrammingLanguage. -Require Import PCF. Open Scope nd_scope. +(* The judgments any specific Γ,Δ form a category with proofs as morphisms *) Section HaskProgrammingLanguage. Context (ndr_systemfc:@ND_Relation _ Rule). - Context Γ (Δ:CoercionEnv Γ). - - (* An organized deduction has been reorganized into contiguous blocks whose - * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth. The boolean - * indicates if non-PCF rules have been used *) - Inductive OrgR : Tree ??(@FCJudg Γ) -> Tree ??(@FCJudg Γ) -> Type := - | org_fc : forall (h c:Tree ??(FCJudg Γ)) - (r:Rule (mapOptionTree (fcjudg2judg Γ Δ) h) (mapOptionTree (fcjudg2judg Γ Δ) c)), - Rule_Flat r -> - OrgR h c + Context Γ (Δ:CoercionEnv Γ). - | org_pcf : forall ec h c, - ND (PCFRule Γ Δ ec) h c -> - OrgR (mapOptionTree (pcfjudg2fcjudg Γ ec) h) (mapOptionTree (pcfjudg2fcjudg Γ ec) c). + + Definition JudgΓΔ := prod (Tree ??(LeveledHaskType Γ ★)) (Tree ??(LeveledHaskType Γ ★)). - (* any proof in organized form can be "dis-organized" *) - (* - Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c. - intros. - induction X. - apply nd_rule. - apply r. - eapply nd_comp. - (* - apply (mkEsc h). - eapply nd_comp; [ idtac | apply (mkBrak c) ]. - apply pcfToND. - apply n. - *) - Admitted. - Definition unOrgND Γ Δ h c : ND (OrgR Γ Δ) h c -> ND Rule h c := nd_map (unOrgR Γ Δ). - *) + Definition RuleΓΔ : Tree ??JudgΓΔ -> Tree ??JudgΓΔ -> Type := + fun h c => + Rule + (mapOptionTree (fun j => Γ > Δ > fst j |- snd j) h) + (mapOptionTree (fun j => Γ > Δ > fst j |- snd j) c). - Definition SystemFCa_cut : forall a b c, ND OrgR ([(a,b)],,[(b,c)]) [(a,c)]. + Definition SystemFCa_cut : forall a b c, ND RuleΓΔ ([(a,b)],,[(b,c)]) [(a,c)]. intros. destruct b. destruct o. @@ -114,7 +92,7 @@ Section HaskProgrammingLanguage. apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]"). Defined. - Instance SystemFCa_sequents : @SequentND _ OrgR _ _ := + Instance SystemFCa_sequents : @SequentND _ RuleΓΔ _ _ := { snd_cut := SystemFCa_cut }. apply Build_SequentND. intros. @@ -142,7 +120,7 @@ Section HaskProgrammingLanguage. admit. Defined. - Definition SystemFCa_left a b c : ND OrgR [(b,c)] [((a,,b),(a,,c))]. + Definition SystemFCa_left a b c : ND RuleΓΔ [(b,c)] [((a,,b),(a,,c))]. admit. (* eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ]. @@ -153,7 +131,7 @@ Section HaskProgrammingLanguage. *) Defined. - Definition SystemFCa_right a b c : ND OrgR [(b,c)] [((b,,a),(c,,a))]. + Definition SystemFCa_right a b c : ND RuleΓΔ [(b,c)] [((b,,a),(c,,a))]. admit. (* eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ]. @@ -195,7 +173,7 @@ Section HaskProgrammingLanguage. admit. Defined. - Instance OrgFC : @ND_Relation _ OrgR. + Instance OrgFC : @ND_Relation _ RuleΓΔ. Admitted. Instance OrgFC_SequentND_Relation : SequentND_Relation SystemFCa_sequent_join OrgFC. diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v deleted file mode 100644 index 2797716..0000000 --- a/src/HaskProofFlattener.v +++ /dev/null @@ -1,396 +0,0 @@ -(*********************************************************************************************************************************) -(* HaskProofFlattener: *) -(* *) -(* The Flattening Functor. *) -(* *) -(*********************************************************************************************************************************) - -Generalizable All Variables. -Require Import Preamble. -Require Import General. -Require Import NaturalDeduction. -Require Import Coq.Strings.String. -Require Import Coq.Lists.List. - -Require Import HaskKinds. -Require Import HaskCoreTypes. -Require Import HaskLiteralsAndTyCons. -Require Import HaskStrongTypes. -Require Import HaskProof. -Require Import NaturalDeduction. -Require Import NaturalDeductionCategory. - -Require Import Algebras_ch4. -Require Import Categories_ch1_3. -Require Import Functors_ch1_4. -Require Import Isomorphisms_ch1_5. -Require Import ProductCategories_ch1_6_1. -Require Import OppositeCategories_ch1_6_2. -Require Import Enrichment_ch2_8. -Require Import Subcategories_ch7_1. -Require Import NaturalTransformations_ch7_4. -Require Import NaturalIsomorphisms_ch7_5. -Require Import BinoidalCategories. -Require Import PreMonoidalCategories. -Require Import MonoidalCategories_ch7_8. -Require Import Coherence_ch7_8. - -Require Import HaskStrongTypes. -Require Import HaskStrong. -Require Import HaskProof. -Require Import HaskStrongToProof. -Require Import HaskProofToStrong. -Require Import ProgrammingLanguage. -Require Import HaskProofStratified. - -Open Scope nd_scope. - -(* - * The flattening transformation. Currently only TWO-level languages are - * supported, and the level-1 sublanguage is rather limited. - * - * This file abuses terminology pretty badly. For purposes of this file, - * "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means - * the whole language (level-0 language including bracketed level-1 terms) - *) -Section HaskProofFlattener. - - Context {Γ:TypeEnv}. - Context {Δ:CoercionEnv Γ}. - Context {ec:HaskTyVar Γ ★}. - - Lemma unlev_lemma : forall (x:Tree ??(HaskType Γ ★)) lev, x = mapOptionTree unlev (x @@@ lev). - intros. - rewrite <- mapOptionTree_compose. - simpl. - induction x. - destruct a; simpl; auto. - simpl. - rewrite IHx1 at 1. - rewrite IHx2 at 1. - reflexivity. - Qed. - - Context (ga_rep : Tree ??(HaskType Γ ★) -> HaskType Γ ★ ). - Context (ga_type : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★). - - Lemma magic : forall a b c, - ([] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type a b @@ nil]) -> - ([ga_type b c @@ nil] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type a c @@ nil]). - admit. - Qed. - - Context (ga_lit : forall lit, [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep [] ) (ga_rep [literalType lit])@@ nil]). - Context (ga_id : forall σ, [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep σ ) (ga_rep σ )@@ nil]). - Context (ga_cancell : forall c , [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep ([],,c)) (ga_rep c )@@ nil]). - Context (ga_cancelr : forall c , [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep (c,,[])) (ga_rep c )@@ nil]). - Context (ga_uncancell : forall c , [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep c ) (ga_rep ([],,c) )@@ nil]). - Context (ga_uncancelr : forall c , [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep c ) (ga_rep (c,,[]) )@@ nil]). - Context (ga_assoc : forall a b c, [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep ((a,,b),,c)) (ga_rep (a,,(b,,c)) )@@ nil]). - Context (ga_unassoc : forall a b c, [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep ( a,,(b,,c))) (ga_rep ((a,,b),,c)) @@ nil]). - Context (ga_swap : forall a b, [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep (a,,b) ) (ga_rep (b,,a) )@@ nil]). - Context (ga_copy : forall a , [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep a ) (ga_rep (a,,a) )@@ nil]). - Context (ga_drop : forall a , [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep a ) (ga_rep [] )@@ nil]). - Context (ga_first : forall a b c, [ga_type (ga_rep a) (ga_rep b) @@nil] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep (a,,c)) (ga_rep (b,,c)) @@nil]). - Context (ga_second : forall a b c, [ga_type (ga_rep a) (ga_rep b) @@nil] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep (c,,a)) (ga_rep (c,,b)) @@nil]). - Context (ga_comp : forall a b c, - [ga_type (ga_rep a) (ga_rep b) @@nil],,[ga_type (ga_rep b) (ga_rep c) @@nil] - ~~{TypesL (SystemFCa Γ Δ)}~~> - [ga_type (ga_rep a) (ga_rep c) @@nil]). - - Definition guestJudgmentAsGArrowType (lt:PCFJudg Γ ec) : HaskType Γ ★ := - match lt with - (x,y) => (ga_type (ga_rep x) (ga_rep y)) - end. - - Definition obact (X:Tree ??(PCFJudg Γ ec)) : Tree ??(LeveledHaskType Γ ★) := - mapOptionTree guestJudgmentAsGArrowType X @@@ nil. - - Hint Constructors Rule_Flat. - Context {ndr:@ND_Relation _ Rule}. - - (* - * Here it is, what you've all been waiting for! When reading this, - * it might help to have the definition for "Inductive ND" (see - * NaturalDeduction.v) handy as a cross-reference. - *) - Hint Constructors Rule_Flat. - Definition FlatteningFunctor_fmor - : forall h c, - (h~~{JudgmentsL (PCF Γ Δ ec)}~~>c) -> - ((obact h)~~{TypesL (SystemFCa Γ Δ)}~~>(obact c)). - - set (@nil (HaskTyVar Γ ★)) as lev. - - unfold hom; unfold ob; unfold ehom; simpl; unfold pmon_I; unfold obact; intros. - - induction X; simpl. - - (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *) - apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVoid _ _)). apply Flat_RVoid. - - (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *) - apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)). apply Flat_RVar. - - (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *) - eapply nd_comp; - [ idtac - | eapply nd_rule - ; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RWeak _))) - ; auto ]. - eapply nd_rule. - eapply (org_fc _ _ [] [(_,_)] (RVoid _ _)); auto. apply Flat_RVoid. - apply Flat_RArrange. - - (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *) - eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCont _))) ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - set (snd_initial(SequentND:=pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ)) - (mapOptionTree (guestJudgmentAsGArrowType) h @@@ lev)) as q. - eapply nd_comp. - eapply nd_prod. - apply q. - apply q. - apply nd_rule. - eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )). - destruct h; simpl. - destruct o. - simpl. - apply Flat_RJoin. - apply Flat_RJoin. - apply Flat_RJoin. - apply Flat_RArrange. - - (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *) - eapply nd_comp. - apply (nd_llecnac ;; nd_prod IHX1 IHX2). - apply nd_rule. - eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )). - apply (Flat_RJoin Γ Δ (mapOptionTree guestJudgmentAsGArrowType h1 @@@ nil) - (mapOptionTree guestJudgmentAsGArrowType h2 @@@ nil) - (mapOptionTree guestJudgmentAsGArrowType c1 @@@ nil) - (mapOptionTree guestJudgmentAsGArrowType c2 @@@ nil)). - - (* nd_comp becomes pl_subst (aka nd_cut) *) - eapply nd_comp. - apply (nd_llecnac ;; nd_prod IHX1 IHX2). - clear IHX1 IHX2 X1 X2. - apply (@snd_cut _ _ _ _ (pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))). - - (* nd_cancell becomes RVar;;RuCanL *) - eapply nd_comp; - [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanL _))) ]. - apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))). - apply Flat_RArrange. - - (* nd_cancelr becomes RVar;;RuCanR *) - eapply nd_comp; - [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanR _))) ]. - apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))). - apply Flat_RArrange. - - (* nd_llecnac becomes RVar;;RCanL *) - eapply nd_comp; - [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanL _))) ]. - apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))). - apply Flat_RArrange. - - (* nd_rlecnac becomes RVar;;RCanR *) - eapply nd_comp; - [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanR _))) ]. - apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))). - apply Flat_RArrange. - - (* nd_assoc becomes RVar;;RAssoc *) - eapply nd_comp; - [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RAssoc _ _ _))) ]. - apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))). - apply Flat_RArrange. - - (* nd_cossa becomes RVar;;RCossa *) - eapply nd_comp; - [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCossa _ _ _))) ]. - apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))). - apply Flat_RArrange. - - destruct r as [r rp]. - rename h into h'. - rename c into c'. - rename r into r'. - - refine (match rp as R in @Rule_PCF _ _ _ H C _ - return - ND (OrgR Γ Δ) [] - [sequent (mapOptionTree guestJudgmentAsGArrowType H @@@ nil) - (mapOptionTree guestJudgmentAsGArrowType C @@@ nil)] - with - | PCF_RArrange h c r q => let case_RURule := tt in _ - | PCF_RLit lit => let case_RLit := tt in _ - | PCF_RNote Σ τ n => let case_RNote := tt in _ - | PCF_RVar σ => let case_RVar := tt in _ - | PCF_RLam Σ tx te => let case_RLam := tt in _ - | PCF_RApp Σ tx te p => let case_RApp := tt in _ - | PCF_RLet Σ σ₁ σ₂ p => let case_RLet := tt in _ - | PCF_RJoin b c d e => let case_RJoin := tt in _ - | PCF_RVoid => let case_RVoid := tt in _ - (*| PCF_RCase T κlen κ θ l x => let case_RCase := tt in _*) - (*| PCF_RLetRec Σ₁ τ₁ τ₂ lev => let case_RLetRec := tt in _*) - end); simpl in *. - clear rp h' c' r'. - - rewrite (unlev_lemma h (ec::nil)). - rewrite (unlev_lemma c (ec::nil)). - destruct case_RURule. - refine (match q as Q in Arrange H C - return - H=(h @@@ (ec :: nil)) -> - C=(c @@@ (ec :: nil)) -> - ND (OrgR Γ Δ) [] - [sequent - [ga_type (ga_rep (mapOptionTree unlev H)) (ga_rep r) @@ nil ] - [ga_type (ga_rep (mapOptionTree unlev C)) (ga_rep r) @@ nil ] ] - with - | RLeft a b c r => let case_RLeft := tt in _ - | RRight a b c r => let case_RRight := tt in _ - | RCanL b => let case_RCanL := tt in _ - | RCanR b => let case_RCanR := tt in _ - | RuCanL b => let case_RuCanL := tt in _ - | RuCanR b => let case_RuCanR := tt in _ - | RAssoc b c d => let case_RAssoc := tt in _ - | RCossa b c d => let case_RCossa := tt in _ - | RExch b c => let case_RExch := tt in _ - | RWeak b => let case_RWeak := tt in _ - | RCont b => let case_RCont := tt in _ - | RComp a b c f g => let case_RComp := tt in _ - end (refl_equal _) (refl_equal _)); - intros; simpl in *; - subst; - try rewrite <- unlev_lemma in *. - - destruct case_RCanL. - apply magic. - apply ga_uncancell. - - destruct case_RCanR. - apply magic. - apply ga_uncancelr. - - destruct case_RuCanL. - apply magic. - apply ga_cancell. - - destruct case_RuCanR. - apply magic. - apply ga_cancelr. - - destruct case_RAssoc. - apply magic. - apply ga_assoc. - - destruct case_RCossa. - apply magic. - apply ga_unassoc. - - destruct case_RExch. - apply magic. - apply ga_swap. - - destruct case_RWeak. - apply magic. - apply ga_drop. - - destruct case_RCont. - apply magic. - apply ga_copy. - - destruct case_RLeft. - apply magic. - (*apply ga_second.*) - admit. - - destruct case_RRight. - apply magic. - (*apply ga_first.*) - admit. - - destruct case_RComp. - apply magic. - (*apply ga_comp.*) - admit. - - destruct case_RLit. - apply ga_lit. - - (* hey cool, I figured out how to pass CoreNote's through... *) - destruct case_RNote. - eapply nd_comp. - eapply nd_rule. - eapply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)) . auto. - apply Flat_RVar. - apply nd_rule. - apply (org_fc _ _ [(_,_)] [(_,_)] (RNote _ _ _ _ _ n)). auto. - apply Flat_RNote. - - destruct case_RVar. - apply ga_id. - - (* - * class GArrow g (**) u => GArrowApply g (**) u (~>) where - * ga_applyl :: g (x**(x~>y) ) y - * ga_applyr :: g ( (x~>y)**x) y - * - * class GArrow g (**) u => GArrowCurry g (**) u (~>) where - * ga_curryl :: g (x**y) z -> g x (y~>z) - * ga_curryr :: g (x**y) z -> g y (x~>z) - *) - destruct case_RLam. - (* GArrowCurry.ga_curry *) - admit. - - destruct case_RApp. - (* GArrowApply.ga_apply *) - admit. - - destruct case_RLet. - admit. - - destruct case_RVoid. - apply ga_id. - - destruct case_RJoin. - (* this assumes we want effects to occur in syntactically-left-to-right order *) - admit. - Defined. - -(* - Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) := - { fmor := FlatteningFunctor_fmor }. - Admitted. - - Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg). - refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros. - Admitted. - - Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME. - refine {| plsmme_pl := PCF n Γ Δ |}. - admit. - Defined. - - Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME. - refine {| plsmme_pl := SystemFCa n Γ Δ |}. - admit. - Defined. - - Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n). - admit. - Defined. - - (* 5.1.4 *) - Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ). - admit. - Defined. -*) - (* ... and the retraction exists *) - -End HaskProofFlattener. - diff --git a/src/HaskProofStratified.v b/src/HaskProofStratified.v deleted file mode 100644 index 177bd6d..0000000 --- a/src/HaskProofStratified.v +++ /dev/null @@ -1,588 +0,0 @@ -(*********************************************************************************************************************************) -(* HaskProofStratified: *) -(* *) -(* An alternate representation for HaskProof which ensures that deductions on a given level are grouped into contiguous *) -(* blocks. This representation lacks the attractive compositionality properties of HaskProof, but makes it easier to *) -(* perform the flattening process. *) -(* *) -(*********************************************************************************************************************************) - -Generalizable All Variables. -Require Import Preamble. -Require Import General. -Require Import NaturalDeduction. -Require Import Coq.Strings.String. -Require Import Coq.Lists.List. - -Require Import HaskKinds. -Require Import HaskCoreTypes. -Require Import HaskLiteralsAndTyCons. -Require Import HaskStrongTypes. -Require Import HaskProof. -Require Import NaturalDeduction. -Require Import NaturalDeductionCategory. - -Require Import Algebras_ch4. -Require Import Categories_ch1_3. -Require Import Functors_ch1_4. -Require Import Isomorphisms_ch1_5. -Require Import ProductCategories_ch1_6_1. -Require Import OppositeCategories_ch1_6_2. -Require Import Enrichment_ch2_8. -Require Import Subcategories_ch7_1. -Require Import NaturalTransformations_ch7_4. -Require Import NaturalIsomorphisms_ch7_5. -Require Import MonoidalCategories_ch7_8. -Require Import Coherence_ch7_8. - -Require Import HaskStrongTypes. -Require Import HaskStrong. -Require Import HaskProof. -Require Import HaskStrongToProof. -Require Import HaskProofToStrong. -Require Import ProgrammingLanguage. - -Open Scope nd_scope. - - -(* - * The flattening transformation. Currently only TWO-level languages are - * supported, and the level-1 sublanguage is rather limited. -* - * This file abuses terminology pretty badly. For purposes of this file, - * "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means - * the whole language (level-0 language including bracketed level-1 terms) - *) -Section HaskProofStratified. - - Section PCF. - - Context (ndr_systemfc:@ND_Relation _ Rule). - - Context Γ (Δ:CoercionEnv Γ). - Definition PCFJudg (ec:HaskTyVar Γ ★) := - @prod (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)). - Definition pcfjudg (ec:HaskTyVar Γ ★) := - @pair (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)). - - (* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg - * from depth (depth) by wrapping brackets around everything in the - * succedent and repopulating *) - Definition brakify {ec} (j:PCFJudg ec) : Judg := - match j with - (Σ,τ) => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil) - end. - - Definition pcf_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) - := mapOptionTreeAndFlatten (fun lt => - match lt with t @@ l => match l with - | ec'::nil => if eqd_dec ec ec' then [t] else [] - | _ => [] - end - end) t. - - Inductive MatchingJudgments {ec} : Tree ??(PCFJudg ec) -> Tree ??Judg -> Type := - | match_nil : MatchingJudgments [] [] - | match_branch : forall a b c d, MatchingJudgments a b -> MatchingJudgments c d -> MatchingJudgments (a,,c) (b,,d) - | match_leaf : - forall Σ τ lev, - MatchingJudgments - [((pcf_vars ec Σ) , τ )] - [Γ > Δ > Σ |- (mapOptionTree (HaskBrak ec) τ @@@ lev)]. - - Definition fc_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) - := mapOptionTreeAndFlatten (fun lt => - match lt with t @@ l => match l with - | ec'::nil => if eqd_dec ec ec' then [] else [t] - | _ => [] - end - end) t. - - Definition pcfjudg2judg ec (cj:PCFJudg ec) := - match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end. - - (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *) - (* Rule_PCF consists of the rules allowed in flat PCF: everything except *) - (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *) - Inductive Rule_PCF (ec:HaskTyVar Γ ★) - : forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type := - | PCF_RArrange : ∀ x y t a, Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a) - | PCF_RLit : ∀ lit , Rule_PCF ec [ ] [ ([],[_]) ] (RLit Γ Δ lit (ec::nil)) - | PCF_RNote : ∀ Σ τ n , Rule_PCF ec [(_,[_])] [(_,[_])] (RNote Γ Δ (Σ@@@(ec::nil)) τ (ec::nil) n) - | PCF_RVar : ∀ σ , Rule_PCF ec [ ] [([_],[_])] (RVar Γ Δ σ (ec::nil) ) - | PCF_RLam : ∀ Σ tx te , Rule_PCF ec [((_,,[_]),[_])] [(_,[_])] (RLam Γ Δ (Σ@@@(ec::nil)) tx te (ec::nil) ) - - | PCF_RApp : ∀ Σ Σ' tx te , - Rule_PCF ec ([(_,[_])],,[(_,[_])]) [((_,,_),[_])] - (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil)) - - | PCF_RLet : ∀ Σ Σ' σ₂ p, - Rule_PCF ec ([(_,[_])],,[((_,,[_]),[_])]) [((_,,_),[_])] - (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil)) - - | PCF_RVoid : Rule_PCF ec [ ] [([],[])] (RVoid Γ Δ ) -(*| PCF_RLetRec : ∀ Σ₁ τ₁ τ₂ , Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*) - | PCF_RJoin : ∀ Σ₁ Σ₂ τ₁ τ₂, Rule_PCF ec ([(_,_)],,[(_,_)]) [((_,,_),(_,,_))] - (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))). - (* need int/boolean case *) - Implicit Arguments Rule_PCF [ ]. - - Definition PCFRule lev h c := { r:_ & @Rule_PCF lev h c r }. - End PCF. - - Definition FCJudg Γ (Δ:CoercionEnv Γ) := - @prod (Tree ??(LeveledHaskType Γ ★)) (Tree ??(LeveledHaskType Γ ★)). - Definition fcjudg2judg {Γ}{Δ}(fc:FCJudg Γ Δ) := - match fc with - (x,y) => Γ > Δ > x |- y - end. - Coercion fcjudg2judg : FCJudg >-> Judg. - - Definition pcfjudg2fcjudg {Γ}{Δ} ec (fc:PCFJudg Γ ec) : FCJudg Γ Δ := - match fc with - (x,y) => (x @@@ (ec::nil),y @@@ (ec::nil)) - end. - - (* An organized deduction has been reorganized into contiguous blocks whose - * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth. The boolean - * indicates if non-PCF rules have been used *) - Inductive OrgR Γ Δ : Tree ??(FCJudg Γ Δ) -> Tree ??(FCJudg Γ Δ) -> Type := - - | org_fc : forall (h c:Tree ??(FCJudg Γ Δ)) - (r:Rule (mapOptionTree fcjudg2judg h) (mapOptionTree fcjudg2judg c)), - Rule_Flat r -> - OrgR _ _ h c - - | org_pcf : forall ec h c, - ND (PCFRule Γ Δ ec) h c -> - OrgR Γ Δ (mapOptionTree (pcfjudg2fcjudg ec) h) (mapOptionTree (pcfjudg2fcjudg ec) c). - - Definition mkEsc Γ Δ ec (h:Tree ??(PCFJudg Γ ec)) - : ND Rule - (mapOptionTree (brakify Γ Δ) h) - (mapOptionTree (pcfjudg2judg Γ Δ ec) h). - apply nd_replicate; intros. - destruct o; simpl in *. - induction t0. - destruct a; simpl. - apply nd_rule. - apply REsc. - apply nd_id. - apply (Prelude_error "mkEsc got multi-leaf succedent"). - Defined. - - Definition mkBrak Γ Δ ec (h:Tree ??(PCFJudg Γ ec)) - : ND Rule - (mapOptionTree (pcfjudg2judg Γ Δ ec) h) - (mapOptionTree (brakify Γ Δ) h). - apply nd_replicate; intros. - destruct o; simpl in *. - induction t0. - destruct a; simpl. - apply nd_rule. - apply RBrak. - apply nd_id. - apply (Prelude_error "mkBrak got multi-leaf succedent"). - Defined. - - (* - Definition Partition {Γ} ec (Σ:Tree ??(LeveledHaskType Γ ★)) := - { vars:(_ * _) | - fc_vars ec Σ = fst vars /\ - pcf_vars ec Σ = snd vars }. - *) - - Definition pcfToND Γ Δ : forall ec h c, - ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c). - intros. - eapply (fun q => nd_map' _ q X). - intros. - destruct X0. - apply nd_rule. - apply x. - Defined. - - Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) := - { ndr_eqv := fun a b f g => (pcfToND _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }. - Admitted. - - (* - * An intermediate representation necessitated by Coq's termination - * conditions. This is basically a tree where each node is a - * subproof which is either entirely level-1 or entirely level-0 - *) - Inductive Alternating : Tree ??Judg -> Type := - - | alt_nil : Alternating [] - - | alt_branch : forall a b, - Alternating a -> Alternating b -> Alternating (a,,b) - - | alt_fc : forall h c, - Alternating h -> - ND Rule h c -> - Alternating c - - | alt_pcf : forall Γ Δ ec h c h' c', - MatchingJudgments Γ Δ h h' -> - MatchingJudgments Γ Δ c c' -> - Alternating h' -> - ND (PCFRule Γ Δ ec) h c -> - Alternating c'. - - Require Import Coq.Logic.Eqdep. -(* - Lemma magic a b c d ec e : - ClosedSIND(Rule:=Rule) [a > b > c |- [d @@ (ec :: e)]] -> - ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@ (ec :: nil)]]. - admit. - Defined. - - Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ]. - - refine ( - fix orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] := - let case_main := tt in _ - with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c := - (match c as C return C=c -> Alternating C with - | T_Leaf None => fun _ => alt_nil - | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _ - | T_Branch b1 b2 => let case_branch := tt in fun eqpf => _ - end (refl_equal _)) - with orgify_pcf Γ Δ ec pcfj j (m:MatchingJudgments Γ Δ pcfj j) - (pf:ClosedSIND (mapOptionTree (pcfjudg2judg Γ Δ ec) pcfj)) {struct pf} : Alternating j := - let case_pcf := tt in _ - for orgify_fc'). - - destruct case_main. - inversion pf; subst. - set (alt_fc _ _ (orgify_fc _ X) (nd_rule X0)) as backup. - refine (match X0 as R in Rule H C return - match C with - | T_Leaf (Some (Γ > Δ > Σ |- τ)) => - h=H -> Alternating [Γ > Δ > Σ |- τ] -> Alternating [Γ > Δ > Σ |- τ] - | _ => True - end - with - | RBrak Σ a b c n m => let case_RBrak := tt in fun pf' backup => _ - | REsc Σ a b c n m => let case_REsc := tt in fun pf' backup => _ - | _ => fun pf' x => x - end (refl_equal _) backup). - clear backup0 backup. - - destruct case_RBrak. - rename c into ec. - set (@match_leaf Σ0 a ec n [b] m) as q. - set (orgify_pcf Σ0 a ec _ _ q) as q'. - apply q'. - simpl. - rewrite pf' in X. - apply magic in X. - apply X. - - destruct case_REsc. - apply (Prelude_error "encountered Esc in wrong side of mkalt"). - - destruct case_leaf. - apply orgify_fc'. - rewrite eqpf. - apply pf. - - destruct case_branch. - rewrite <- eqpf in pf. - inversion pf; subst. - apply no_rules_with_multiple_conclusions in X0. - inversion X0. - exists b1. exists b2. - auto. - apply (alt_branch _ _ (orgify_fc _ X) (orgify_fc _ X0)). - - destruct case_pcf. - Admitted. - - Definition pcfify Γ Δ ec : forall Σ τ, - ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] - -> ND (PCFRule Γ Δ ec) [] [(Σ,τ)]. - - refine (( - fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn} - : ND (PCFRule Γ Δ ec) [] [(Σ,τ)] := - (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with - | cnd_weak => let case_nil := tt in _ - | cnd_rule h c cnd' r => let case_rule := tt in _ - | cnd_branch _ _ c1 c2 => let case_branch := tt in _ - end (refl_equal _)))). - intros. - inversion H. - intros. - destruct c; try destruct o; inversion H. - destruct j. - Admitted. -*) - (* any proof in organized form can be "dis-organized" *) - (* - Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c. - intros. - induction X. - apply nd_rule. - apply r. - eapply nd_comp. - (* - apply (mkEsc h). - eapply nd_comp; [ idtac | apply (mkBrak c) ]. - apply pcfToND. - apply n. - *) - Admitted. - Definition unOrgND Γ Δ h c : ND (OrgR Γ Δ) h c -> ND Rule h c := nd_map (unOrgR Γ Δ). - *) - - Hint Constructors Rule_Flat. - - Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)]. - admit. - Defined. - - Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([(a,b)],,[(b,c)]) [(a,c)]. - intros. - destruct b. - destruct o. - destruct c. - destruct o. - - (* when the cut is a single leaf and the RHS is a single leaf: *) - eapply nd_comp. - eapply nd_prod. - apply nd_id. - apply (PCF_Arrange [h] ([],,[h]) [h0]). - apply RuCanL. - eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ]. - apply nd_rule. - (* - set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q. - exists q. - apply (PCF_RLet _ [] a h0 h). - apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]"). - apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]"). - apply (Prelude_error "cut rule invoked with [a|=[]] [[]|=c]"). - apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]"). - *) - Admitted. - - Instance PCF_sequents Γ Δ lev ec : @SequentND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ ec) := - { snd_cut := PCF_cut Γ Δ lev }. - apply Build_SequentND. - intros. - induction a. - destruct a; simpl. - apply nd_rule. - exists (RVar _ _ _ _). - apply PCF_RVar. - apply nd_rule. - exists (RVoid _ _ ). - apply PCF_RVoid. - eapply nd_comp. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply (nd_prod IHa1 IHa2). - apply nd_rule. - exists (RJoin _ _ _ _ _ _). - apply PCF_RJoin. - admit. - Defined. - - Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((a,,b),(a,,c))]. - eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ]. - eapply nd_prod; [ apply snd_initial | apply nd_id ]. - apply nd_rule. - set (@PCF_RJoin Γ Δ lev a b a c) as q'. - refine (existT _ _ _). - apply q'. - Admitted. - - Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((b,,a),(c,,a))]. - eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ]. - eapply nd_prod; [ apply nd_id | apply snd_initial ]. - apply nd_rule. - set (@PCF_RJoin Γ Δ lev b a c a) as q'. - refine (existT _ _ _). - apply q'. - Admitted. - - Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ lev) _ := - { cnd_expand_left := fun a b c => PCF_left Γ Δ lev c a b - ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }. - - intros; apply nd_rule. unfold PCFRule. simpl. - exists (RArrange _ _ _ _ _ (RCossa _ _ _)). - apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x). - - intros; apply nd_rule. unfold PCFRule. simpl. - exists (RArrange _ _ _ _ _ (RAssoc _ _ _)). - apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x). - - intros; apply nd_rule. unfold PCFRule. simpl. - exists (RArrange _ _ _ _ _ (RCanL _)). - apply (PCF_RArrange _ _ lev ([],,a) _ _). - - intros; apply nd_rule. unfold PCFRule. simpl. - exists (RArrange _ _ _ _ _ (RCanR _)). - apply (PCF_RArrange _ _ lev (a,,[]) _ _). - - intros; apply nd_rule. unfold PCFRule. simpl. - exists (RArrange _ _ _ _ _ (RuCanL _)). - apply (PCF_RArrange _ _ lev _ ([],,a) _). - - intros; apply nd_rule. unfold PCFRule. simpl. - exists (RArrange _ _ _ _ _ (RuCanR _)). - apply (PCF_RArrange _ _ lev _ (a,,[]) _). - Defined. - - Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev). - admit. - Defined. - - Definition OrgPCF_ContextND_Relation Γ Δ lev - : @ContextND_Relation _ _ _ _ _ (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev) (OrgPCF_SequentND_Relation Γ Δ lev). - admit. - Defined. - - (* 5.1.3 *) - Instance PCF Γ Δ lev : ProgrammingLanguage := - { pl_cnd := PCF_sequent_join Γ Δ lev - ; pl_eqv := OrgPCF_ContextND_Relation Γ Δ lev - }. - - Definition SystemFCa_cut Γ Δ : forall a b c, ND (OrgR Γ Δ) ([(a,b)],,[(b,c)]) [(a,c)]. - intros. - destruct b. - destruct o. - destruct c. - destruct o. - - (* when the cut is a single leaf and the RHS is a single leaf: *) - (* - eapply nd_comp. - eapply nd_prod. - apply nd_id. - eapply nd_rule. - set (@org_fc) as ofc. - set (RArrange Γ Δ _ _ _ (RuCanL [l0])) as rule. - apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [_])). - auto. - eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ]. - apply nd_rule. - destruct l. - destruct l0. - assert (h0=h2). admit. - subst. - apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2). - auto. - auto. - *) - admit. - apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[]]"). - apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[x,,y]]"). - apply (Prelude_error "systemfc rule invoked with [a|=[]] [[]|=c]"). - apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]"). - Defined. - - Instance SystemFCa_sequents Γ Δ : @SequentND _ (OrgR Γ Δ) _ _ := - { snd_cut := SystemFCa_cut Γ Δ }. - apply Build_SequentND. - intros. - induction a. - destruct a; simpl. - (* - apply nd_rule. - destruct l. - apply org_fc with (r:=RVar _ _ _ _). - auto. - apply nd_rule. - apply org_fc with (r:=RVoid _ _ ). - auto. - eapply nd_comp. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply (nd_prod IHa1 IHa2). - apply nd_rule. - apply org_fc with (r:=RJoin _ _ _ _ _ _). - auto. - admit. - *) - admit. - admit. - admit. - admit. - Defined. - - Definition SystemFCa_left Γ Δ a b c : ND (OrgR Γ Δ) [(b,c)] [((a,,b),(a,,c))]. - admit. - (* - eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ]. - eapply nd_prod; [ apply snd_initial | apply nd_id ]. - apply nd_rule. - apply org_fc with (r:=RJoin Γ Δ a b a c). - auto. - *) - Defined. - - Definition SystemFCa_right Γ Δ a b c : ND (OrgR Γ Δ) [(b,c)] [((b,,a),(c,,a))]. - admit. - (* - eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ]. - eapply nd_prod; [ apply nd_id | apply snd_initial ]. - apply nd_rule. - apply org_fc with (r:=RJoin Γ Δ b a c a). - auto. - *) - Defined. - - Instance SystemFCa_sequent_join Γ Δ : @ContextND _ _ _ _ (SystemFCa_sequents Γ Δ) := - { cnd_expand_left := fun a b c => SystemFCa_left Γ Δ c a b - ; cnd_expand_right := fun a b c => SystemFCa_right Γ Δ c a b }. - (* - intros; apply nd_rule. simpl. - apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))). - auto. - - intros; apply nd_rule. simpl. - apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto. - - intros; apply nd_rule. simpl. - apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto. - - intros; apply nd_rule. simpl. - apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto. - - intros; apply nd_rule. simpl. - apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto. - - intros; apply nd_rule. simpl. - apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto. - *) - admit. - admit. - admit. - admit. - admit. - admit. - Defined. - - Instance OrgFC Γ Δ : @ND_Relation _ (OrgR Γ Δ). - Admitted. - - Instance OrgFC_SequentND_Relation Γ Δ : SequentND_Relation (SystemFCa_sequent_join Γ Δ) (OrgFC Γ Δ). - admit. - Defined. - - Definition OrgFC_ContextND_Relation Γ Δ - : @ContextND_Relation _ _ _ _ _ (SystemFCa_sequent_join Γ Δ) (OrgFC Γ Δ) (OrgFC_SequentND_Relation Γ Δ). - admit. - Defined. - - (* 5.1.2 *) - Instance SystemFCa Γ Δ : @ProgrammingLanguage (LeveledHaskType Γ ★) _ := - { pl_eqv := OrgFC_ContextND_Relation Γ Δ - ; pl_snd := SystemFCa_sequents Γ Δ - }. - -End HaskProofStratified. diff --git a/src/PCF.v b/src/PCF.v index 16dceef..00ffd77 100644 --- a/src/PCF.v +++ b/src/PCF.v @@ -90,30 +90,9 @@ Section PCF. [((pcf_vars ec Σ) , τ )] [Γ > Δ > Σ |- (mapOptionTree (HaskBrak ec) τ @@@ lev)]. - Definition fc_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) - := mapOptionTreeAndFlatten (fun lt => - match lt with t @@ l => match l with - | ec'::nil => if eqd_dec ec ec' then [] else [t] - | _ => [] - end - end) t. - - Definition FCJudg := - @prod (Tree ??(LeveledHaskType Γ ★)) (Tree ??(LeveledHaskType Γ ★)). - Definition fcjudg2judg (fc:FCJudg) := - match fc with - (x,y) => Γ > Δ > x |- y - end. - Coercion fcjudg2judg : FCJudg >-> Judg. - Definition pcfjudg2judg ec (cj:PCFJudg ec) := match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end. - Definition pcfjudg2fcjudg ec (fc:PCFJudg ec) : FCJudg := - match fc with - (x,y) => (x @@@ (ec::nil),y @@@ (ec::nil)) - end. - (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *) (* Rule_PCF consists of the rules allowed in flat PCF: everything except *) (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *) @@ -171,13 +150,6 @@ Section PCF. apply (Prelude_error "mkBrak got multi-leaf succedent"). Defined. - (* - Definition Partition {Γ} ec (Σ:Tree ??(LeveledHaskType Γ ★)) := - { vars:(_ * _) | - fc_vars ec Σ = fst vars /\ - pcf_vars ec Σ = snd vars }. - *) - Definition pcfToND Γ Δ : forall ec h c, ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c). intros. @@ -192,120 +164,6 @@ Section PCF. { ndr_eqv := fun a b f g => (pcfToND _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }. Admitted. - (* - * An intermediate representation necessitated by Coq's termination - * conditions. This is basically a tree where each node is a - * subproof which is either entirely level-1 or entirely level-0 - *) - Inductive Alternating : Tree ??Judg -> Type := - - | alt_nil : Alternating [] - - | alt_branch : forall a b, - Alternating a -> Alternating b -> Alternating (a,,b) - - | alt_fc : forall h c, - Alternating h -> - ND Rule h c -> - Alternating c - - | alt_pcf : forall Γ Δ ec h c h' c', - MatchingJudgments Γ Δ h h' -> - MatchingJudgments Γ Δ c c' -> - Alternating h' -> - ND (PCFRule Γ Δ ec) h c -> - Alternating c'. - - Require Import Coq.Logic.Eqdep. -(* - Lemma magic a b c d ec e : - ClosedSIND(Rule:=Rule) [a > b > c |- [d @@ (ec :: e)]] -> - ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@ (ec :: nil)]]. - admit. - Defined. - - Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ]. - - refine ( - fix orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] := - let case_main := tt in _ - with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c := - (match c as C return C=c -> Alternating C with - | T_Leaf None => fun _ => alt_nil - | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _ - | T_Branch b1 b2 => let case_branch := tt in fun eqpf => _ - end (refl_equal _)) - with orgify_pcf Γ Δ ec pcfj j (m:MatchingJudgments Γ Δ pcfj j) - (pf:ClosedSIND (mapOptionTree (pcfjudg2judg Γ Δ ec) pcfj)) {struct pf} : Alternating j := - let case_pcf := tt in _ - for orgify_fc'). - - destruct case_main. - inversion pf; subst. - set (alt_fc _ _ (orgify_fc _ X) (nd_rule X0)) as backup. - refine (match X0 as R in Rule H C return - match C with - | T_Leaf (Some (Γ > Δ > Σ |- τ)) => - h=H -> Alternating [Γ > Δ > Σ |- τ] -> Alternating [Γ > Δ > Σ |- τ] - | _ => True - end - with - | RBrak Σ a b c n m => let case_RBrak := tt in fun pf' backup => _ - | REsc Σ a b c n m => let case_REsc := tt in fun pf' backup => _ - | _ => fun pf' x => x - end (refl_equal _) backup). - clear backup0 backup. - - destruct case_RBrak. - rename c into ec. - set (@match_leaf Σ0 a ec n [b] m) as q. - set (orgify_pcf Σ0 a ec _ _ q) as q'. - apply q'. - simpl. - rewrite pf' in X. - apply magic in X. - apply X. - - destruct case_REsc. - apply (Prelude_error "encountered Esc in wrong side of mkalt"). - - destruct case_leaf. - apply orgify_fc'. - rewrite eqpf. - apply pf. - - destruct case_branch. - rewrite <- eqpf in pf. - inversion pf; subst. - apply no_rules_with_multiple_conclusions in X0. - inversion X0. - exists b1. exists b2. - auto. - apply (alt_branch _ _ (orgify_fc _ X) (orgify_fc _ X0)). - - destruct case_pcf. - Admitted. - - Definition pcfify Γ Δ ec : forall Σ τ, - ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] - -> ND (PCFRule Γ Δ ec) [] [(Σ,τ)]. - - refine (( - fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn} - : ND (PCFRule Γ Δ ec) [] [(Σ,τ)] := - (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with - | cnd_weak => let case_nil := tt in _ - | cnd_rule h c cnd' r => let case_rule := tt in _ - | cnd_branch _ _ c1 c2 => let case_branch := tt in _ - end (refl_equal _)))). - intros. - inversion H. - intros. - destruct c; try destruct o; inversion H. - destruct j. - Admitted. -*) - Hint Constructors Rule_Flat. Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)].