{-# 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
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} :
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.
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.
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.
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
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.
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.
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.
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 ].
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'.
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.
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.
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.
| 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 _
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.
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.
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.
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.
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").
| 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 [] [Γ > Δ > [] |- [] ]
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
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.
| 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 :=
| 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 _
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 _).
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.
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.
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.
| 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 Γ ★) :=
| 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.
apply SFlat.
apply RArrange.
eapply RComp.
- apply RCossa.
- apply RLeft.
+ eapply RCossa.
+ eapply RLeft.
apply take_arrange.
destruct case_RCast.
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.
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.
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 ].
| 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
| 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:
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 *)
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 *)
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,
simpl in *.
fold (mapOptionTree ξ) in *.
intros.
- apply arrangeContextAndWeaken.
+ apply factorContextRightAndWeaken.
apply Δ.
unfold mapOptionTree; simpl in *.
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''.
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.
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.
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.
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.
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.
Inductive WeakExpr :=
| WEVar : WeakExprVar -> WeakExpr
| WELit : HaskLiteral -> WeakExpr
+
+(* TO DO: add a WEWhere and use the source location to detect which one the user used *)
| WELet : WeakExprVar -> WeakExpr -> WeakExpr -> WeakExpr
| WELetRec : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr -> WeakExpr
| WECast : WeakExpr -> WeakCoercion -> WeakExpr
(* natural deduction: you may duplicate conclusions *)
| nd_copy : forall h, h /⋯⋯/ (h,,h)
+ (* natural deduction: you may re-order conclusions *)
+ | nd_exch : forall x y, (x,,y) /⋯⋯/ (y,,x)
+
(* natural deduction: you may write two proof trees side by side on a piece of paper -- "proof product" *)
| nd_prod : forall {h1 h2 c1 c2}
(pf1: h1 /⋯⋯/ c1 )
apply k.
apply scnd_weak.
eapply scnd_branch; apply k.
+ inversion k; subst; auto.
inversion k; subst.
apply (scnd_branch _ _ _ (IHnd1 X) (IHnd2 X0)).
apply IHnd2.
| nd_id1 h => let case_nd_id1 := tt in _
| nd_weak1 h => let case_nd_weak := tt in _
| nd_copy h => let case_nd_copy := tt in _
+ | nd_exch x y => let case_nd_exch := tt in _
| nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
| nd_comp _ _ _ top bot => let case_nd_comp := tt in _
| nd_rule _ _ rule => let case_nd_rule := tt in _
destruct case_nd_id1. apply nd_id1.
destruct case_nd_weak. apply nd_weak.
destruct case_nd_copy. apply nd_copy.
+ destruct case_nd_exch. apply nd_exch.
destruct case_nd_prod. apply (nd_prod (nd_map _ _ lpf) (nd_map _ _ rpf)).
destruct case_nd_comp. apply (nd_comp (nd_map _ _ top) (nd_map _ _ bot)).
destruct case_nd_cancell. apply nd_cancell.
| nd_id1 h => let case_nd_id1 := tt in _
| nd_weak1 h => let case_nd_weak := tt in _
| nd_copy h => let case_nd_copy := tt in _
+ | nd_exch x y => let case_nd_exch := tt in _
| nd_prod _ _ _ _ lpf rpf => let case_nd_prod := tt in _
| nd_comp _ _ _ top bot => let case_nd_comp := tt in _
| nd_rule _ _ rule => let case_nd_rule := tt in _
destruct case_nd_id1. apply nd_id1.
destruct case_nd_weak. apply nd_weak.
destruct case_nd_copy. apply nd_copy.
+ destruct case_nd_exch. apply nd_exch.
destruct case_nd_prod. apply (nd_prod (nd_map' _ _ lpf) (nd_map' _ _ rpf)).
destruct case_nd_comp. apply (nd_comp (nd_map' _ _ top) (nd_map' _ _ bot)).
destruct case_nd_cancell. apply nd_cancell.
| nd_copy h' => rawLatexMath indent +++
rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
+ | nd_exch x y => rawLatexMath indent +++
+ rawLatexMath "\inferrule*[Left=exch]{"+++judgments2latex h+++
+ rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
| nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++
rawLatexMath "% prod " +++ eolL +++
rawLatexMath indent +++
projects / coq-hetmet.git / commitdiff