From: Adam Megacz Date: Thu, 26 May 2011 03:55:29 +0000 (-0700) Subject: add new Where rule, eliminate unnecessary ga_swaps in the Skolemizer X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=b83e779e742413ca84df565263dafbdf9f79920a add new Where rule, eliminate unnecessary ga_swaps in the Skolemizer --- diff --git a/examples/Demo.hs b/examples/Demo.hs index 4e7f599..afedde6 100644 --- a/examples/Demo.hs +++ b/examples/Demo.hs @@ -1,13 +1,23 @@ {-# OPTIONS_GHC -XModalTypes -fcoqpass -dcore-lint #-} module Demo (demo) where -demo con mer = <[ ~~mer ~~(con (2::Int)) ~~(con (12::Int)) ]> +--demo con mer = <[ ~~mer ~~(con (2::Int)) ~~(con (12::Int)) ]> -- demo const mult = <[ let q = ~~(const (1::Int)) in ~~mult q q ]> ---demo const mult = --- <[ let twelve = ~~(const (12::Int)) --- in ~~mult (~~mult twelve twelve) (~~mult twelve twelve) ]> +demo const mult = + <[ let twelve = ~~(const (12::Int)) + in let four = ~~(const (4::Int)) + in ~~mult four twelve ]> + +{- +demo const mult = + <[ let twelve = ~~(const (12::Int)) + in let twelvea = twelve + four = ~~(const (4::Int)) + twelveb = twelve + in ~~mult (~~mult twelvea four) (~~mult twelveb twelveb) ]> +-} {- demo const mult = demo' 3 diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 5be5280..6364a5a 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -235,14 +235,14 @@ Section core2proof. Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} : ND Rule [ Γ > Δ > Σ |- [a ---> s @@ lev ] ] - [ Γ > Δ > Σ,,[a @@ lev] |- [ s @@ lev ] ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ [a@@lev] Σ a s lev) ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. + [ Γ > Δ > [a @@ lev],,Σ |- [ s @@ lev ] ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. + apply nd_id. apply nd_rule. apply RVar. - apply nd_id. Defined. Definition fToC1 {Γ}{Δ}{a}{s}{lev} : @@ -251,13 +251,13 @@ Section core2proof. intro pf. eapply nd_comp. apply pf. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ]. apply curry. Defined. Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} : ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) @@ lev ] ] -> - ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s @@ lev ] ]. + ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s @@ lev ] ]. intro pf. eapply nd_comp. eapply pf. @@ -267,7 +267,8 @@ Section core2proof. eapply nd_comp. eapply nd_rule. eapply RArrange. - eapply RCanL. + eapply RCanR. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. apply curry. Defined. diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index a5f4261..308e669 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -371,8 +371,8 @@ Section HaskFlattener. ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] -> ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. @@ -380,141 +380,117 @@ Section HaskFlattener. apply X. eapply nd_rule. eapply RArrange. - apply RuCanL. - Defined. - - Definition postcompose' : ∀ Γ Δ ec lev a b c Σ, - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> - ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ]. - intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. - eapply nd_comp; [ idtac - | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod. - apply X. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ]. - apply ga_comp. - Defined. + apply RuCanR. + Defined. Definition precompose Γ Δ ec : forall a x y z lev, ND Rule [ Γ > Δ > a |- [@ga_mk _ ec y z @@ lev] ] [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ]. intros. - eapply nd_comp. - apply nd_rlecnac. - eapply nd_comp. - eapply nd_prod. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. + apply nd_prod. apply nd_id. - eapply ga_comp. - - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ]. - - apply nd_rule. - apply RLet. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + apply ga_comp. Defined. - Definition precompose' : ∀ Γ Δ ec lev a b c Σ, - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] -> - ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ]. - intros. - eapply nd_comp. - apply X. - apply precompose. - Defined. + Definition precompose' Γ Δ ec : forall a b x y z lev, + ND Rule + [ Γ > Δ > a,,b |- [@ga_mk _ ec y z @@ lev] ] + [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z @@ lev] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCossa ]. + apply precompose. + Defined. - Definition postcompose : ∀ Γ Δ ec lev a b c, - ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] -> - ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ]. - intros. - eapply nd_comp. - apply postcompose'. - apply X. - apply nd_rule. - apply RArrange. - apply RCanL. - Defined. + Definition postcompose_ Γ Δ ec : forall a x y z lev, + ND Rule + [ Γ > Δ > a |- [@ga_mk _ ec x y @@ lev] ] + [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z @@ lev] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. + apply nd_prod. + apply nd_id. + apply ga_comp. + Defined. - Definition firstify : ∀ Γ Δ ec lev a b c Σ, - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ]. + Definition postcompose Γ Δ ec : forall x y z lev, + ND Rule [] [ Γ > Δ > [] |- [@ga_mk _ ec x y @@ lev] ] -> + ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z @@ lev] ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod. + eapply nd_comp; [ idtac | eapply postcompose_ ]. apply X. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ]. - apply ga_first. Defined. - Definition secondify : ∀ Γ Δ ec lev a b c Σ, - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ]. + Definition first_nd : ∀ Γ Δ ec lev a b c Σ, + ND Rule [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] + [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. - apply X. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ]. - apply ga_second. + apply nd_id. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ]. + apply ga_first. Defined. - Lemma ga_unkappa : ∀ Γ Δ ec l z a b Σ, - ND Rule - [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ] - [Γ > Δ > Σ,,[@ga_mk Γ ec z a @@ l] |- [@ga_mk Γ ec z b @@ l] ]. + Definition firstify : ∀ Γ Δ ec lev a b c Σ, + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ]. intros. - set (ga_comp Γ Δ ec l z a b) as q. - - set (@RLet Γ Δ) as q'. - set (@RLet Γ Δ [@ga_mk _ ec z a @@ l] Σ (@ga_mk _ ec z b) (@ga_mk _ ec a b) l) as q''. eapply nd_comp. - Focus 2. - eapply nd_rule. - eapply RArrange. - apply RExch. - - eapply nd_comp. - Focus 2. - eapply nd_rule. - apply q''. + apply X. + apply first_nd. + Defined. - idtac. - clear q'' q'. - eapply nd_comp. - apply nd_rlecnac. + Definition second_nd : ∀ Γ Δ ec lev a b c Σ, + ND Rule + [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] + [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. - apply q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ]. + apply ga_second. Defined. - Lemma ga_unkappa' : ∀ Γ Δ ec l a b Σ x, - ND Rule - [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ] - [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ]. + Definition secondify : ∀ Γ Δ ec lev a b c Σ, + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod. - apply ga_first. - - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod. - apply postcompose. - apply ga_uncancell. - apply precompose. + eapply nd_comp. + apply X. + apply second_nd. Defined. - Lemma ga_kappa' : ∀ Γ Δ ec l a b Σ x, - ND Rule - [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ] - [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ]. - apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)"). - Defined. + Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ x, + ND Rule + [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ] + [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply ga_first. + + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply postcompose. + apply ga_uncancell. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + apply precompose. + Defined. (* useful for cutting down on the pretty-printed noise @@ -559,17 +535,17 @@ Section HaskFlattener. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. eapply nd_comp; [ idtac | eapply nd_rule; apply - (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ]. + (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. apply r2'. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply - (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. eapply nd_prod. apply r1'. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. apply ga_comp. Defined. @@ -630,7 +606,7 @@ Section HaskFlattener. apply RuCanR. apply RAssoc. apply RCossa. - apply RExch. + apply RExch. (* TO DO: check for all-leaf trees here *) apply RWeak. apply RCont. apply RLeft; auto. @@ -648,29 +624,32 @@ Section HaskFlattener. intro pfa. intro pfb. apply secondify with (c:=a) in pfb. - eapply nd_comp. - Focus 2. + apply firstify with (c:=[]) in pfa. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. eapply nd_comp; [ eapply nd_llecnac | idtac ]. - eapply nd_prod. - apply pfb. - clear pfb. - apply postcompose'. - eapply nd_comp. + apply nd_prod. apply pfa. clear pfa. - apply boost. + + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. - apply precompose'. + eapply nd_comp; [ idtac | eapply postcompose_ ]. apply ga_uncancelr. - apply nd_id. + + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply precompose ]. + apply pfb. Defined. Definition arrange_brak : forall Γ Δ ec succ t, ND Rule - [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),, - [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil] |- [t @@ nil]] + [Γ > Δ > + [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],, + mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t @@ nil]] [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]]. + intros. unfold drop_lev. set (@arrange' _ succ (levelMatch (ec::nil))) as q. @@ -682,6 +661,7 @@ Section HaskFlattener. apply y. idtac. clear y q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. simpl. eapply nd_comp; [ apply nd_llecnac | idtac ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. @@ -778,8 +758,9 @@ Section HaskFlattener. Definition arrange_esc : forall Γ Δ ec succ t, ND Rule [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]] - [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),, - [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil] |- [t @@ nil]]. + [Γ > Δ > + [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],, + mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t @@ nil]]. intros. set (@arrange _ succ (levelMatch (ec::nil))) as q. set (@drop_lev Γ (ec::nil) succ) as q'. @@ -803,7 +784,7 @@ Section HaskFlattener. simpl. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ]. set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''. - eapply nd_comp; [ idtac | eapply nd_rule; apply q'' ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. clear q''. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. @@ -812,15 +793,15 @@ Section HaskFlattener. eapply RComp; [ idtac | apply RCanR ]. apply RLeft. apply (@arrange_empty_tree _ _ _ _ e). - + eapply nd_comp. eapply nd_rule. eapply (@RVar Γ Δ t nil). apply nd_rule. apply RArrange. eapply RComp. - apply RuCanL. - apply RRight. + apply RuCanR. + apply RLeft. apply RWeak. (* eapply decide_tree_empty. @@ -873,52 +854,45 @@ Section HaskFlattener. reflexivity. Qed. - Lemma tree_of_nothing : forall Γ ec t a, - Arrange (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) a. + Lemma tree_of_nothing : forall Γ ec t, + Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) []. intros. - induction t; try destruct o; try destruct a0. + induction t; try destruct o; try destruct a. simpl. drop_simplify. simpl. - apply RCanR. + apply RId. simpl. - apply RCanR. + apply RId. + eapply RComp; [ idtac | apply RCanL ]. + eapply RComp; [ idtac | eapply RLeft; apply IHt2 ]. Opaque drop_lev. simpl. Transparent drop_lev. + idtac. drop_simplify. - simpl. - eapply RComp. - eapply RComp. - eapply RAssoc. - eapply RRight. + apply RRight. apply IHt1. - apply IHt2. Defined. - Lemma tree_of_nothing' : forall Γ ec t a, - Arrange a (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))). + Lemma tree_of_nothing' : forall Γ ec t, + Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))). intros. - induction t; try destruct o; try destruct a0. + induction t; try destruct o; try destruct a. simpl. drop_simplify. simpl. - apply RuCanR. + apply RId. simpl. - apply RuCanR. + apply RId. + eapply RComp; [ apply RuCanL | idtac ]. + eapply RComp; [ eapply RRight; apply IHt1 | idtac ]. Opaque drop_lev. simpl. Transparent drop_lev. + idtac. drop_simplify. - simpl. - eapply RComp. - Focus 2. - eapply RComp. - Focus 2. - eapply RCossa. - Focus 2. - eapply RRight. - apply IHt1. + apply RLeft. apply IHt2. Defined. @@ -989,6 +963,7 @@ Section HaskFlattener. | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _ | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _ + | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _ | RJoin Γ p lri m x q => let case_RJoin := tt in _ | RVoid _ _ => let case_RVoid := tt in _ | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _ @@ -1130,22 +1105,51 @@ Section HaskFlattener. repeat take_simplify. simpl. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''. + eapply nd_comp. eapply nd_prod; [ idtac | apply nd_id ]. eapply boost. - apply ga_second. + apply (ga_first _ _ _ _ _ _ Σ₂'). - eapply nd_comp. - eapply nd_prod. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + apply nd_prod. apply nd_id. + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanL | idtac ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch (* okay *)]. + apply precompose. + + destruct case_RWhere. + simpl. + destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ]. + repeat take_simplify. + repeat drop_simplify. + simpl. + + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''. + eapply nd_comp. - eapply nd_rule. - eapply RArrange. - apply RCanR. - eapply precompose. + eapply nd_prod; [ eapply nd_id | idtac ]. + eapply (first_nd _ _ _ _ _ _ Σ₃'). + eapply nd_comp. + eapply nd_prod; [ eapply nd_id | idtac ]. + eapply (second_nd _ _ _ _ _ _ Σ₁'). + eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ]. + apply nd_prod; [ idtac | apply nd_id ]. + eapply nd_comp; [ idtac | eapply precompose' ]. apply nd_rule. - apply RLet. + apply RArrange. + apply RLeft. + apply RCanL. destruct case_RVoid. simpl. @@ -1242,11 +1246,15 @@ Section HaskFlattener. set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest. set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args. unfold empty_tree. - eapply nd_comp; [ eapply nd_rule; eapply RArrange; apply tree_of_nothing | idtac ]. - refine (ga_unkappa' Γ Δ (v2t ec) nil _ _ _ _ ;; _). + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing | idtac ]. + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanR | idtac ]. + refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _). + eapply nd_comp; [ idtac | eapply arrange_brak ]. unfold succ_host. unfold succ_guest. - apply arrange_brak. + eapply nd_rule. + eapply RArrange. + apply RExch. apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported"). destruct case_SEsc. @@ -1260,7 +1268,8 @@ Section HaskFlattener. take_simplify. drop_simplify. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply tree_of_nothing' ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing' ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. simpl. rewrite take_lemma'. rewrite unlev_relev. @@ -1276,13 +1285,15 @@ Section HaskFlattener. set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host. set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; [ idtac | eapply boost ]. induction x. apply ga_id. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. simpl. apply ga_join. apply IHx1. @@ -1307,7 +1318,7 @@ Section HaskFlattener. apply IHx2. (* environment has non-empty leaves *) - apply ga_kappa'. + apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)"). (* nesting too deep *) apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported"). diff --git a/src/HaskProof.v b/src/HaskProof.v index d9c6a7e..a8b311e 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -82,9 +82,11 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := | RJoin : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ] -| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx@@l]],,[Γ>Δ> Σ₂ |- [tx--->te @@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]] +(* order is important here; we want to be able to skolemize without introducing new RExch'es *) +| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]] -| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]] +| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁ |- [σ₁@@l]],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂@@l] ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ @@l]] +| RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂@@l] ],,[Γ>Δ> Σ₂ |- [σ₁@@l]]) [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ @@l]] | RVoid : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ] @@ -99,7 +101,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]] [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]] -| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ] +| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁])@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ] | RCase : forall Γ Δ lev tc Σ avars tbranches (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }), Rule @@ -159,6 +161,7 @@ Lemma no_rules_with_multiple_conclusions : forall c h, destruct X0; destruct s; inversion e. destruct X0; destruct s; inversion e. destruct X0; destruct s; inversion e. + destruct X0; destruct s; inversion e. Qed. Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False. diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index 61b358f..61a0bdb 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -189,12 +189,13 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo" | RApp _ _ _ _ _ _ _ => "App" | RLet _ _ _ _ _ _ _ => "Let" - | RJoin _ _ _ _ _ _ => "RJoin" + | RWhere _ _ _ _ _ _ _ _ => "Where" + | RJoin _ _ _ _ _ _ => "RJoin" | RLetRec _ _ _ _ _ _ => "LetRec" | RCase _ _ _ _ _ _ _ _ => "Case" | RBrak _ _ _ _ _ _ => "Brak" | REsc _ _ _ _ _ _ => "Esc" - | RVoid _ _ => "RVoid" + | RVoid _ _ => "RVoid" end. Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool := diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index b6e8efe..6ba094e 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -524,8 +524,9 @@ Section HaskProofToStrong. | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _ | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _ - | RJoin Γ p lri m x q => let case_RJoin := tt in _ - | RVoid _ _ => let case_RVoid := tt in _ + | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := 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 _ @@ -636,42 +637,84 @@ Section HaskProofToStrong. apply ileaf in q1'. apply ileaf in q2'. simpl in *. - apply (EApp _ _ _ _ _ _ q2' q1'). + apply (EApp _ _ _ _ _ _ q1' q2'). destruct case_RLet. apply ILeaf. simpl in *; intros. destruct vars; try destruct o; inversion H. - refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)). + + refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)). apply FreshMon. + destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_ξ ξ p (((vnew, σ₂ )) :: nil)) as ξ' in *. + set (update_ξ ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. inversion X_. apply ileaf in X. apply ileaf in X0. simpl in *. - refine (X ξ vars2 _ >>>= fun X0' => _). + + refine (X ξ vars1 _ >>>= fun X0' => _). apply FreshMon. + simpl. auto. - refine (X0 ξ' (vars1,,[vnew]) _ >>>= fun X1' => _). + refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _). apply FreshMon. - rewrite H1. simpl. rewrite pf2. rewrite pf1. - rewrite H1. reflexivity. + apply FreshMon. - refine (return _). apply ILeaf. - apply ileaf in X0'. apply ileaf in X1'. + apply ileaf in X0'. simpl in *. - apply ELet with (ev:=vnew)(tv:=σ₂). + apply ELet with (ev:=vnew)(tv:=σ₁). apply X0'. apply X1'. + destruct case_RWhere. + apply ILeaf. + simpl in *; intros. + destruct vars; try destruct o; inversion H. + destruct vars2; try destruct o; inversion H2. + clear H2. + + assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto. + refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)). + apply FreshMon. + + destruct pf as [ vnew [ pf1 pf2 ]]. + set (update_ξ ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. + inversion X_. + apply ileaf in X. + apply ileaf in X0. + simpl in *. + + refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _). + apply FreshMon. + simpl. + inversion pf1. + rewrite H3. + rewrite H4. + rewrite pf2. + reflexivity. + + refine (X0 ξ vars2_1 _ >>>= fun X1' => _). + apply FreshMon. + reflexivity. + apply FreshMon. + + apply ILeaf. + apply ileaf in X0'. + apply ileaf in X1'. + simpl in *. + apply ELet with (ev:=vnew)(tv:=σ₁). + apply X1'. + apply X0'. + destruct case_RVoid. apply ILeaf; simpl; intros. refine (return _). @@ -720,11 +763,11 @@ Section HaskProofToStrong. apply (@ELetRec _ _ _ _ _ _ _ varstypes). auto. apply (@letrec_helper Γ Δ t varstypes). - rewrite <- pf2 in X1. + rewrite <- pf2 in X0. rewrite mapOptionTree_compose. - apply X1. - apply ileaf in X0. apply X0. + apply ileaf in X1. + apply X1. destruct case_RCase. apply ILeaf; simpl; intros. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index bfbdf0e..b037bb0 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -130,10 +130,10 @@ Section HaskSkolemizer. Implicit Arguments drop_arg_types_as_tree [[Γ]]. Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev, - Arrange ([tx @@ lev],, take_arg_types_as_tree te @@@ lev) + Arrange ([tx @@ lev],,take_arg_types_as_tree te @@@ lev) (take_arg_types_as_tree (tx ---> te) @@@ lev). intros. - destruct (eqd_dec ([tx],, take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))). + destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))). rewrite <- e. simpl. apply RId. @@ -152,9 +152,9 @@ Section HaskSkolemizer. Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev, Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev) - ([tx @@ lev],, take_arg_types_as_tree te @@@ lev). + ([tx @@ lev],,take_arg_types_as_tree te @@@ lev). intros. - destruct (eqd_dec ([tx],, take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))). + destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))). rewrite <- e. simpl. apply RId. @@ -184,13 +184,13 @@ Section HaskSkolemizer. | SFlat : forall h c, Rule h c -> SRule h c | SBrak : forall Γ Δ t ec Σ l, SRule - [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]] + [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]] [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]] | SEsc : forall Γ Δ t ec Σ l, SRule [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]] - [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]] + [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]] . Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) := @@ -245,10 +245,11 @@ Section HaskSkolemizer. | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _ | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _ + | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _ | RJoin Γ p lri m x q => let case_RJoin := tt in _ | RVoid _ _ => let case_RVoid := tt in _ - | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _ - | REsc Γ Δ t ec succ lev => let case_REsc := tt in _ + | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _ + | REsc Γ Δ t ec succ lev => 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 h c. @@ -347,8 +348,8 @@ Section HaskSkolemizer. apply SFlat. apply RArrange. eapply RComp. - apply RCossa. - apply RLeft. + eapply RCossa. + eapply RLeft. apply take_arrange. destruct case_RCast. @@ -383,23 +384,16 @@ Section HaskSkolemizer. rewrite H. rewrite H0. simpl. - set (@RLet Γ Δ (Σ₂,,take_arg_types_as_tree te @@@ (h :: lev)) Σ₁ (drop_arg_types_as_tree te) tx (h::lev)) as q. + eapply nd_comp. + eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ]. + eapply nd_rule. + eapply SFlat. + eapply RArrange. + eapply RLeft. + eapply take_unarrange. + eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RExch ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ]. - clear q. - apply nd_prod. - apply nd_rule. - apply SFlat. - apply RArrange. - apply RCanR. - apply nd_rule. - apply SFlat. - apply RArrange. - eapply RComp; [ idtac | eapply RAssoc ]. - apply RLeft. - eapply RComp; [ idtac | apply RExch ]. - apply take_unarrange. + eapply nd_rule; eapply SFlat; apply RWhere. destruct case_RLet. simpl. @@ -407,29 +401,48 @@ Section HaskSkolemizer. apply nd_rule. apply SFlat. apply RLet. - set (check_hof σ₂) as hof_tx. + set (check_hof σ₁) as hof_tx. destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ]. destruct a. rewrite H. rewrite H0. - set (@RLet Γ Δ (Σ₁,,(take_arg_types_as_tree σ₁ @@@ (h::lev))) Σ₂ (drop_arg_types_as_tree σ₁) σ₂ (h::lev)) as q. + + eapply nd_comp. + eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR | eapply nd_id ]. + + set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q. eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; eapply RLeft; apply RExch ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ]. - clear q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ]. apply nd_prod. + apply nd_id. + apply nd_rule. + eapply SFlat. + eapply RArrange. + eapply RCossa. + + destruct case_RWhere. + simpl. + destruct lev. apply nd_rule. apply SFlat. - apply RArrange. - apply RCanR. - eapply nd_comp; [ eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa | idtac ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ]. - apply nd_rule. - apply SFlat. - apply RArrange. + apply RWhere. + set (check_hof σ₁) as hof_tx. + destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ]. + destruct a. + rewrite H. + rewrite H0. + + eapply nd_comp. + eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RAssoc ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RLeft; eapply RAssoc ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ]. + apply nd_prod; [ idtac | eapply nd_id ]. + eapply nd_rule; apply SFlat; eapply RArrange. + eapply RComp. + eapply RCossa. apply RLeft. - eapply RExch. + eapply RCossa. destruct case_RVoid. simpl. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 9c3b041..5f3baa3 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -19,6 +19,9 @@ Section HaskStrongToProof. Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) := RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _). +Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) := + RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _). + Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b). eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ]. eapply RComp; [ idtac | apply RCossa ]. @@ -522,9 +525,9 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? | EGlobal Γ Δ ξ _ _ _ => [] | EVar Γ Δ ξ ev => [ev] | ELit Γ Δ ξ lit lev => [] - | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e2),,(expr2antecedent e1) + | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2) | ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e) - | ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev)) + | ELet Γ Δ ξ tv t lev v ev ebody => (expr2antecedent ev),,((stripOutVars (v::nil) (expr2antecedent ebody))) | EEsc Γ Δ ξ ec t lev e => expr2antecedent e | EBrak Γ Δ ξ ec t lev e => expr2antecedent e | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e @@ -535,7 +538,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e | ELetRec Γ Δ ξ l τ vars _ branches body => let branch_context := eLetRecContext branches - in let all_contexts := (expr2antecedent body),,branch_context + in let all_contexts := branch_context,,(expr2antecedent body) in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts | ECase Γ Δ ξ l tc tbranches atypes e' alts => ((fix varsfromalts (alts: @@ -598,7 +601,112 @@ Lemma stripping_nothing_is_inert reflexivity. Qed. -Definition arrangeContext +Definition factorContextLeft + (Γ:TypeEnv)(Δ:CoercionEnv Γ) + v (* variable to be pivoted, if found *) + ctx (* initial context *) + (ξ:VV -> LeveledHaskType Γ ★) + : + + (* a proof concluding in a context where that variable does not appear *) + sum (Arrange + (mapOptionTree ξ ctx ) + (mapOptionTree ξ ([],,(stripOutVars (v::nil) ctx)) )) + + (* or a proof concluding in a context where that variable appears exactly once in the left branch *) + (Arrange + (mapOptionTree ξ ctx ) + (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) )). + + induction ctx. + + refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end). + + (* nonempty leaf *) + destruct case_Some. + unfold stripOutVars in *; simpl. + unfold dropVar. + unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. + + destruct (eqd_dec v' v); subst. + + (* where the leaf is v *) + apply inr. + subst. + apply RuCanR. + + (* where the leaf is NOT v *) + apply inl. + apply RuCanL. + + (* empty leaf *) + destruct case_None. + apply inl; simpl in *. + apply RuCanR. + + (* branch *) + refine ( + match IHctx1 with + | inr lpf => + match IHctx2 with + | inr rpf => let case_Both := tt in _ + | inl rpf => let case_Left := tt in _ + end + | inl lpf => + match IHctx2 with + | inr rpf => let case_Right := tt in _ + | inl rpf => let case_Neither := tt in _ + end + end); clear IHctx1; clear IHctx2. + + destruct case_Neither. + apply inl. + simpl. + eapply RComp; [idtac | apply RuCanL ]. + exact (RComp + (* order will not matter because these are central as morphisms *) + (RRight _ (RComp lpf (RCanL _))) + (RLeft _ (RComp rpf (RCanL _)))). + + destruct case_Right. + apply inr. + unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. + fold (stripOutVars (v::nil)). + eapply RComp; [ idtac | eapply pivotContext' ]. + eapply RComp. + eapply RRight. + eapply RComp. + apply lpf. + apply RCanL. + eapply RLeft. + apply rpf. + + destruct case_Left. + apply inr. + fold (stripOutVars (v::nil)). + simpl. + eapply RComp. + eapply RLeft. + eapply RComp. + apply rpf. + simpl. + eapply RCanL. + eapply RComp; [ idtac | eapply RCossa ]. + eapply RRight. + apply lpf. + + destruct case_Both. + apply inr. + simpl. + eapply RComp; [ idtac | eapply RRight; eapply RCont ]. + eapply RComp; [ eapply RRight; eapply lpf | idtac ]. + eapply RComp; [ eapply RLeft; eapply rpf | idtac ]. + clear lpf rpf. + simpl. + apply arrangeSwapMiddle. + Defined. + +Definition factorContextRight (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) ctx (* initial context *) @@ -703,7 +811,72 @@ Definition arrangeContext Defined. (* same as before, but use RWeak if necessary *) -Definition arrangeContextAndWeaken +Definition factorContextLeftAndWeaken + (Γ:TypeEnv)(Δ:CoercionEnv Γ) + v (* variable to be pivoted, if found *) + ctx (* initial context *) + (ξ:VV -> LeveledHaskType Γ ★) : + Arrange + (mapOptionTree ξ ctx ) + (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) ). + set (factorContextLeft Γ Δ v ctx ξ) as q. + destruct q; auto. + eapply RComp; [ apply a | idtac ]. + refine (RRight _ (RWeak _)). + Defined. + +Definition factorContextLeftAndWeaken'' + (Γ:TypeEnv)(Δ:CoercionEnv Γ) + v (* variable to be pivoted, if found *) + (ξ:VV -> LeveledHaskType Γ ★) : forall ctx, + distinct (leaves v) -> + Arrange + ((mapOptionTree ξ ctx) ) + ((mapOptionTree ξ v),,(mapOptionTree ξ (stripOutVars (leaves v) ctx))). + + induction v; intros. + destruct a. + unfold mapOptionTree in *. + simpl in *. + fold (mapOptionTree ξ) in *. + intros. + set (@factorContextLeftAndWeaken) as q. + simpl in q. + apply q. + apply Δ. + + unfold mapOptionTree; simpl in *. + intros. + rewrite (@stripping_nothing_is_inert Γ); auto. + apply RuCanL. + intros. + unfold mapOptionTree in *. + simpl in *. + fold (mapOptionTree ξ) in *. + set (mapOptionTree ξ) as X in *. + + set (distinct_app _ _ _ H) as H'. + destruct H' as [H1 H2]. + + set (IHv1 (v2,,(stripOutVars (leaves v2) ctx))) as IHv1'. + + unfold X in *. + simpl in *. + rewrite <- strip_twice_lemma. + set (notin_strip_inert' v2 (leaves v1)) as q. + unfold stripOutVars in q. + rewrite q in IHv1'. + clear q. + eapply RComp; [ idtac | eapply RAssoc ]. + eapply RComp; [ idtac | eapply IHv1' ]. + clear IHv1'. + apply IHv2; auto. + auto. + auto. + Defined. + +(* same as before, but use RWeak if necessary *) +Definition factorContextRightAndWeaken (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) ctx (* initial context *) @@ -711,13 +884,13 @@ Definition arrangeContextAndWeaken Arrange (mapOptionTree ξ ctx ) (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) ). - set (arrangeContext Γ Δ v ctx ξ) as q. + set (factorContextRight Γ Δ v ctx ξ) as q. destruct q; auto. eapply RComp; [ apply a | idtac ]. refine (RLeft _ (RWeak _)). Defined. -Definition arrangeContextAndWeaken'' +Definition factorContextRightAndWeaken'' (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) (ξ:VV -> LeveledHaskType Γ ★) : forall ctx, @@ -732,7 +905,7 @@ Definition arrangeContextAndWeaken'' simpl in *. fold (mapOptionTree ξ) in *. intros. - apply arrangeContextAndWeaken. + apply factorContextRightAndWeaken. apply Δ. unfold mapOptionTree; simpl in *. @@ -833,7 +1006,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : eapply nd_comp; [ idtac | eapply nd_rule; apply z ]. clear z. - set (@arrangeContextAndWeaken'' Γ Δ pctx ξ' (expr2antecedent body,,eLetRecContext branches)) as q'. + set (@factorContextRightAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'. unfold passback in *; clear passback. unfold pctx in *; clear pctx. set (q' disti) as q''. @@ -855,7 +1028,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q. eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod; auto. rewrite ξlemma. apply q. @@ -1007,7 +1180,7 @@ Definition expr2proof : unfold mapOptionTree; simpl; fold (mapOptionTree ξ). eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ]. set (update_ξ ξ lev ((v,t1)::nil)) as ξ'. - set (arrangeContextAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx. + set (factorContextRightAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx. eapply RArrange in pfx. unfold mapOptionTree in pfx; simpl in pfx. unfold ξ' in pfx. @@ -1024,16 +1197,14 @@ Definition expr2proof : destruct case_ELet; intros; simpl in *. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. - apply pf_let. - clear pf_let. - eapply nd_comp; [ apply pf_body | idtac ]. - clear pf_body. + apply pf_let. + eapply nd_comp; [ apply pf_body | idtac ]. fold (@mapOptionTree VV). fold (mapOptionTree ξ). set (update_ξ ξ v ((lev,tv)::nil)) as ξ'. - set (arrangeContextAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n. + set (factorContextLeftAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n. unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n. unfold ξ' in n. rewrite updating_stripped_tree_is_inert in n. @@ -1102,7 +1273,7 @@ Definition expr2proof : rewrite <- (scbwv_coherent scbx l ξ). rewrite <- vec2list_map_list2vec. rewrite mapleaves'. - set (@arrangeContextAndWeaken'') as q. + set (@factorContextRightAndWeaken'') as q. unfold scbwv_ξ. set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z. unfold scbwv_varstypes in z. @@ -1110,6 +1281,7 @@ Definition expr2proof : rewrite fst_zip in z. rewrite <- z. clear z. + replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))). apply q.