ND Rule
[ Γ > Δ > Σ |- [a ---> s ]@lev ]
[ Γ > Δ > [a @@ lev],,Σ |- [ s ]@lev ].
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod.
intro pf.
eapply nd_comp.
apply pf.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
apply curry.
Defined.
eapply nd_comp.
eapply nd_rule.
eapply RArrange.
- eapply RCanR.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+ eapply ACanR.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
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 RCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod.
apply X.
eapply nd_rule.
eapply RArrange.
- apply RuCanR.
+ apply AuCanR.
Defined.
Definition precompose Γ Δ ec : forall a x y z lev,
eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod.
apply nd_id.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
apply ga_comp.
Defined.
[ Γ > Δ > 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 ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
apply precompose.
Defined.
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; eapply RArrange; eapply ACanL ].
eapply nd_comp; [ idtac | eapply postcompose_ ].
apply X.
Defined.
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 RCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod.
apply nd_id.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
apply ga_first.
Defined.
[ Γ > Δ > Σ |- [@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; eapply RArrange; eapply ACanR ].
eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod.
apply nd_id.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
apply ga_second.
Defined.
[Γ > Δ > Σ |- [@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 RArrange; eapply AExch ].
eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
apply nd_prod.
apply nd_prod.
apply postcompose.
apply ga_uncancell.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
apply precompose.
Defined.
(mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
(mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
with
- | RId a => let case_RId := tt in ga_id _ _ _ _ _
- | 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 flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
- | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
- | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
+ | AId a => let case_AId := tt in ga_id _ _ _ _ _
+ | ACanL a => let case_ACanL := tt in ga_uncancell _ _ _ _ _
+ | ACanR a => let case_ACanR := tt in ga_uncancelr _ _ _ _ _
+ | AuCanL a => let case_AuCanL := tt in ga_cancell _ _ _ _ _
+ | AuCanR a => let case_AuCanR := tt in ga_cancelr _ _ _ _ _
+ | AAssoc a b c => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _
+ | AuAssoc a b c => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _
+ | AExch a b => let case_AExch := tt in ga_swap _ _ _ _ _ _
+ | AWeak a => let case_AWeak := tt in ga_drop _ _ _ _ _
+ | ACont a => let case_ACont := tt in ga_copy _ _ _ _ _
+ | ALeft a b c r' => let case_ALeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
+ | ARight a b c r' => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
+ | AComp c b a r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
- destruct case_RComp.
+ destruct case_AComp.
set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
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; eapply RArrange; apply ACanL ].
eapply nd_comp; [ idtac | eapply nd_rule; apply
(@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 RuCanR ].
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
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 ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
apply ga_comp.
Defined.
match r as R in Arrange A B return
Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
(mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
- | RId a => let case_RId := tt in RId _
- | 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 _ (flatten _ _ r')
- | RRight a b c r' => let case_RRight := tt in RRight _ (flatten _ _ r')
- | RComp a b c r1 r2 => let case_RComp := tt in RComp (flatten _ _ r1) (flatten _ _ r2)
+ | AId a => let case_AId := tt in AId _
+ | ACanL a => let case_ACanL := tt in ACanL _
+ | ACanR a => let case_ACanR := tt in ACanR _
+ | AuCanL a => let case_AuCanL := tt in AuCanL _
+ | AuCanR a => let case_AuCanR := tt in AuCanR _
+ | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _
+ | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _
+ | AExch a b => let case_AExch := tt in AExch _ _
+ | AWeak a => let case_AWeak := tt in AWeak _
+ | ACont a => let case_ACont := tt in ACont _
+ | ALeft a b c r' => let case_ALeft := tt in ALeft _ (flatten _ _ r')
+ | ARight a b c r' => let case_ARight := tt in ARight _ (flatten _ _ r')
+ | AComp a b c r1 r2 => let case_AComp := tt in AComp (flatten _ _ r1) (flatten _ _ r2)
end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
Defined.
apply nd_rule.
apply RArrange.
induction r; simpl.
- apply RId.
- apply RCanL.
- apply RCanR.
- apply RuCanL.
- apply RuCanR.
- apply RAssoc.
- apply RCossa.
- apply RExch. (* TO DO: check for all-leaf trees here *)
- apply RWeak.
- apply RCont.
- apply RLeft; auto.
- apply RRight; auto.
- eapply RComp; [ apply IHr1 | apply IHr2 ].
+ apply AId.
+ apply ACanL.
+ apply ACanR.
+ apply AuCanL.
+ apply AuCanR.
+ apply AAssoc.
+ apply AuAssoc.
+ apply AExch. (* TO DO: check for all-leaf trees here *)
+ apply AWeak.
+ apply ACont.
+ apply ALeft; auto.
+ apply ARight; auto.
+ eapply AComp; [ apply IHr1 | apply IHr2 ].
apply flatten_arrangement.
apply r.
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 ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
eapply nd_comp; [ idtac | eapply postcompose_ ].
apply ga_uncancelr.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
eapply nd_comp; [ idtac | eapply precompose ].
apply pfb.
Defined.
apply y.
idtac.
clear y q.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
simpl.
eapply nd_comp; [ apply nd_llecnac | idtac ].
eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
destruct s.
simpl.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
clear q''.
apply nd_prod.
apply nd_rule.
apply RArrange.
- eapply RComp; [ idtac | apply RCanR ].
- apply RLeft.
+ eapply AComp; [ idtac | apply ACanR ].
+ apply ALeft.
apply (@arrangeCancelEmptyTree _ _ _ _ e).
eapply nd_comp.
eapply (@RVar Γ Δ t nil).
apply nd_rule.
apply RArrange.
- eapply RComp.
- apply RuCanR.
- apply RLeft.
- apply RWeak.
+ eapply AComp.
+ apply AuCanR.
+ apply ALeft.
+ apply AWeak.
(*
eapply decide_tree_empty.
simpl.
apply nd_rule.
apply RArrange.
- apply RLeft.
- apply RWeak.
+ apply ALeft.
+ apply AWeak.
simpl.
apply nd_rule.
unfold take_lev.
simpl.
apply RArrange.
- apply RLeft.
- apply RWeak.
+ apply ALeft.
+ apply AWeak.
apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
*)
Defined.
simpl.
drop_simplify.
simpl.
- apply RId.
+ apply AId.
simpl.
- apply RId.
- eapply RComp; [ idtac | apply RCanL ].
- eapply RComp; [ idtac | eapply RLeft; apply IHt2 ].
+ apply AId.
+ eapply AComp; [ idtac | apply ACanL ].
+ eapply AComp; [ idtac | eapply ALeft; apply IHt2 ].
Opaque drop_lev.
simpl.
Transparent drop_lev.
idtac.
drop_simplify.
- apply RRight.
+ apply ARight.
apply IHt1.
Defined.
simpl.
drop_simplify.
simpl.
- apply RId.
+ apply AId.
simpl.
- apply RId.
- eapply RComp; [ apply RuCanL | idtac ].
- eapply RComp; [ eapply RRight; apply IHt1 | idtac ].
+ apply AId.
+ eapply AComp; [ apply AuCanL | idtac ].
+ eapply AComp; [ eapply ARight; apply IHt1 | idtac ].
Opaque drop_lev.
simpl.
Transparent drop_lev.
idtac.
drop_simplify.
- apply RLeft.
+ apply ALeft.
apply IHt2.
Defined.
eapply nd_rule.
eapply RArrange.
simpl.
- apply RCanR.
+ apply ACanR.
apply boost.
simpl.
apply ga_curry.
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 *)].
+ eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)].
apply precompose.
destruct case_RWhere.
eapply nd_comp; [ idtac | eapply precompose' ].
apply nd_rule.
apply RArrange.
- apply RLeft.
- apply RCanL.
+ apply ALeft.
+ apply ACanL.
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; eapply RLeft; apply tree_of_nothing | idtac ].
- eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanR | idtac ].
+ eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ].
+ eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ].
refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
eapply nd_comp; [ idtac | eapply arrange_brak ].
unfold succ_host.
unfold succ_guest.
eapply nd_rule.
eapply RArrange.
- apply RExch.
+ apply AExch.
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; eapply RLeft; apply tree_of_nothing' ].
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
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 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 RArrange; apply AuCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
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 RCanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
simpl.
apply ga_join.
apply IHx1.
apply nd_id.
eapply nd_rule.
set (@org_fc) as ofc.
- set (RArrange Γ Δ _ _ _ (RuCanL [l0])) as rule.
- apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [_])).
+ set (RArrange Γ Δ _ _ _ (AuCanL [l0])) as rule.
+ apply org_fc with (r:=RArrange _ _ _ _ _ (AuCanL [_])).
auto.
- eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (ACanL _)) ].
apply nd_rule.
destruct l.
destruct l0.
; cnd_expand_right := fun a b c => SystemFCa_right c a b }.
(*
intros; apply nd_rule. simpl.
- apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))).
+ apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (AuAssoc _ _ _)))).
auto.
intros; apply nd_rule. simpl.
- apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AAssoc _ _ _))); auto.
intros; apply nd_rule. simpl.
- apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanL _))); auto.
intros; apply nd_rule. simpl.
- apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanR _))); auto.
intros; apply nd_rule. simpl.
- apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanL _))); auto.
intros; apply nd_rule. simpl.
- apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanR _))); auto.
*)
admit.
admit.
| RJoin : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ l, Rule ([Γ > Δ > Σ₁ |- τ₁ @l],,[Γ > Δ > Σ₂ |- τ₂ @l]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ @l ]
-(* order is important here; we want to be able to skolemize without introducing new RExch'es *)
+(* order is important here; we want to be able to skolemize without introducing new AExch'es *)
| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l]) [Γ>Δ> Σ₁,,Σ₂ |- [te]@l]
| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ ]@l]
Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
match r with
- | RLeft _ _ _ r => nd_uruleToRawLatexMath r
- | RRight _ _ _ r => nd_uruleToRawLatexMath r
- | RId _ => "Id"
- | RCanL _ => "CanL"
- | RCanR _ => "CanR"
- | RuCanL _ => "uCanL"
- | RuCanR _ => "uCanR"
- | RAssoc _ _ _ => "Assoc"
- | RCossa _ _ _ => "Cossa"
- | RExch _ _ => "Exch"
- | RWeak _ => "Weak"
- | RCont _ => "Cont"
- | RComp _ _ _ _ _ => "Comp" (* FIXME: do a better job here *)
+ | ALeft _ _ _ r => nd_uruleToRawLatexMath r
+ | ARight _ _ _ r => nd_uruleToRawLatexMath r
+ | AId _ => "Id"
+ | ACanL _ => "CanL"
+ | ACanR _ => "CanR"
+ | AuCanL _ => "uCanL"
+ | AuCanR _ => "uCanR"
+ | AAssoc _ _ _ => "Assoc"
+ | AuAssoc _ _ _ => "Cossa"
+ | AExch _ _ => "Exch"
+ | AWeak _ => "Weak"
+ | ACont _ => "Cont"
+ | AComp _ _ _ _ _ => "Comp" (* FIXME: do a better job here *)
end.
Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
match r with
- | RLeft _ _ _ r => nd_hideURule r
- | RRight _ _ _ r => nd_hideURule r
- | RCanL _ => true
- | RCanR _ => true
- | RuCanL _ => true
- | RuCanR _ => true
- | RAssoc _ _ _ => true
- | RCossa _ _ _ => true
- | RExch (T_Leaf None) b => true
- | RExch a (T_Leaf None) => true
- | RWeak (T_Leaf None) => true
- | RCont (T_Leaf None) => true
- | RComp _ _ _ _ _ => false (* FIXME: do better *)
+ | ALeft _ _ _ r => nd_hideURule r
+ | ARight _ _ _ r => nd_hideURule r
+ | ACanL _ => true
+ | ACanR _ => true
+ | AuCanL _ => true
+ | AuCanR _ => true
+ | AAssoc _ _ _ => true
+ | AuAssoc _ _ _ => true
+ | AExch (T_Leaf None) b => true
+ | AExch a (T_Leaf None) => true
+ | AWeak (T_Leaf None) => true
+ | ACont (T_Leaf None) => true
+ | AComp _ _ _ _ _ => false (* FIXME: do better *)
| _ => false
end.
Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
ujudg2exprType Γ ξ Δ H t l ->
ujudg2exprType Γ ξ Δ C t l
with
- | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
- | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
- | RId a => let case_RId := tt in _
- | RCanL a => let case_RCanL := tt in _
- | RCanR a => let case_RCanR := tt in _
- | RuCanL a => let case_RuCanL := tt in _
- | RuCanR a => let case_RuCanR := tt in _
- | RAssoc a b c => let case_RAssoc := tt in _
- | RCossa a b c => let case_RCossa := tt in _
- | RExch a b => let case_RExch := tt in _
- | RWeak a => let case_RWeak := tt in _
- | RCont a => let case_RCont := tt in _
- | RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g)
+ | ALeft h c ctx r => let case_ALeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
+ | ARight h c ctx r => let case_ARight := tt in (fun e => _) (urule2expr _ _ _ _ r)
+ | AId a => let case_AId := tt in _
+ | ACanL a => let case_ACanL := tt in _
+ | ACanR a => let case_ACanR := tt in _
+ | AuCanL a => let case_AuCanL := tt in _
+ | AuCanR a => let case_AuCanR := tt in _
+ | AAssoc a b c => let case_AAssoc := tt in _
+ | AuAssoc a b c => let case_AuAssoc := tt in _
+ | AExch a b => let case_AExch := tt in _
+ | AWeak a => let case_AWeak := tt in _
+ | ACont a => let case_ACont := tt in _
+ | AComp a b c f g => let case_AComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g)
end); clear urule2expr; intros.
- destruct case_RId.
+ destruct case_AId.
apply X.
- destruct case_RCanL.
+ destruct case_ACanL.
simpl; unfold ujudg2exprType; intros.
simpl in X.
apply (X ([],,vars)).
simpl; rewrite <- H; auto.
- destruct case_RCanR.
+ destruct case_ACanR.
simpl; unfold ujudg2exprType; intros.
simpl in X.
apply (X (vars,,[])).
simpl; rewrite <- H; auto.
- destruct case_RuCanL.
+ destruct case_AuCanL.
simpl; unfold ujudg2exprType; intros.
destruct vars; try destruct o; inversion H.
simpl in X.
apply (X vars2); auto.
- destruct case_RuCanR.
+ destruct case_AuCanR.
simpl; unfold ujudg2exprType; intros.
destruct vars; try destruct o; inversion H.
simpl in X.
apply (X vars1); auto.
- destruct case_RAssoc.
+ destruct case_AAssoc.
simpl; unfold ujudg2exprType; intros.
simpl in X.
destruct vars; try destruct o; inversion H.
apply (X (vars1_1,,(vars1_2,,vars2))).
subst; auto.
- destruct case_RCossa.
+ destruct case_AuAssoc.
simpl; unfold ujudg2exprType; intros.
simpl in X.
destruct vars; try destruct o; inversion H.
apply (X ((vars1,,vars2_1),,vars2_2)).
subst; auto.
- destruct case_RExch.
+ destruct case_AExch.
simpl; unfold ujudg2exprType ; intros.
simpl in X.
destruct vars; try destruct o; inversion H.
apply (X (vars2,,vars1)).
inversion H; subst; auto.
- destruct case_RWeak.
+ destruct case_AWeak.
simpl; unfold ujudg2exprType; intros.
simpl in X.
apply (X []).
auto.
- destruct case_RCont.
+ destruct case_ACont.
simpl; unfold ujudg2exprType ; intros.
simpl in X.
apply (X (vars,,vars)).
rewrite <- H.
auto.
- destruct case_RLeft.
+ destruct case_ALeft.
intro vars; unfold ujudg2exprType; intro H.
destruct vars; try destruct o; inversion H.
apply (fun q => e ξ q vars2 H2).
simpl.
reflexivity.
- destruct case_RRight.
+ destruct case_ARight.
intro vars; unfold ujudg2exprType; intro H.
destruct vars; try destruct o; inversion H.
apply (fun q => e ξ q vars1 H1).
simpl.
reflexivity.
- destruct case_RComp.
+ destruct case_AComp.
apply e2.
apply e1.
apply X.
destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
rewrite <- e.
simpl.
- apply RId.
+ apply AId.
unfold take_arg_types_as_tree.
Opaque take_arg_types_as_tree.
simpl.
destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
simpl.
replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
- apply RCanR.
+ apply ACanR.
apply phoas_extensionality.
reflexivity.
apply (Prelude_error "should not be possible").
destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
rewrite <- e.
simpl.
- apply RId.
+ apply AId.
unfold take_arg_types_as_tree.
Opaque take_arg_types_as_tree.
simpl.
destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
simpl.
replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
- apply RuCanR.
+ apply AuCanR.
apply phoas_extensionality.
reflexivity.
apply (Prelude_error "should not be possible").
apply nd_rule.
apply SFlat.
apply RArrange.
- apply RRight.
+ apply ARight.
apply d.
destruct case_RBrak.
rewrite H.
rewrite H0.
simpl.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply AuCanL ].
apply nd_rule.
apply SFlat.
apply RLit.
rewrite H.
rewrite H0.
simpl.
- eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].
apply nd_rule.
apply SFlat.
apply RVar.
rewrite H.
rewrite H0.
simpl.
- eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].
apply nd_rule.
apply SFlat.
apply RGlobal.
apply nd_rule.
apply SFlat.
apply RArrange.
- eapply RComp.
- eapply RCossa.
- eapply RLeft.
+ eapply AComp.
+ eapply AuAssoc.
+ eapply ALeft.
apply take_arrange.
destruct case_RCast.
rewrite H0.
simpl.
eapply nd_comp.
- eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ].
+ eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
eapply nd_rule.
eapply SFlat.
eapply RArrange.
- eapply RLeft.
+ eapply ALeft.
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 AAssoc ].
eapply nd_rule; eapply SFlat; apply RWhere.
destruct case_RLet.
rewrite H0.
eapply nd_comp.
- eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR | eapply nd_id ].
+ eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR | 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; apply AAssoc ].
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.
+ eapply AuAssoc.
destruct case_RWhere.
simpl.
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_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ].
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 RCossa.
+ eapply AComp.
+ eapply AuAssoc.
+ apply ALeft.
+ eapply AuAssoc.
destruct case_RVoid.
simpl.
apply nd_rule.
apply SFlat.
apply RVoid.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RuCanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuCanL ].
apply nd_rule.
apply SFlat.
apply RVoid.
(* where the leaf is v *)
apply inr.
subst.
- apply RuCanR.
+ apply AuCanR.
(* where the leaf is NOT v *)
apply inl.
- apply RuCanL.
+ apply AuCanL.
(* empty leaf *)
destruct case_None.
apply inl; simpl in *.
- apply RuCanR.
+ apply AuCanR.
(* branch *)
refine (
destruct case_Neither.
apply inl.
simpl.
- eapply RComp; [idtac | apply RuCanL ].
- exact (RComp
+ eapply AComp; [idtac | apply AuCanL ].
+ exact (AComp
(* order will not matter because these are central as morphisms *)
- (RRight _ (RComp lpf (RCanL _)))
- (RLeft _ (RComp rpf (RCanL _)))).
+ (ARight _ (AComp lpf (ACanL _)))
+ (ALeft _ (AComp rpf (ACanL _)))).
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.
+ eapply AComp; [ idtac | eapply pivotContext' ].
+ eapply AComp.
+ eapply ARight.
+ eapply AComp.
apply lpf.
- apply RCanL.
- eapply RLeft.
+ apply ACanL.
+ eapply ALeft.
apply rpf.
destruct case_Left.
apply inr.
fold (stripOutVars (v::nil)).
simpl.
- eapply RComp.
- eapply RLeft.
- eapply RComp.
+ eapply AComp.
+ eapply ALeft.
+ eapply AComp.
apply rpf.
simpl.
- eapply RCanL.
- eapply RComp; [ idtac | eapply RCossa ].
- eapply RRight.
+ eapply ACanL.
+ eapply AComp; [ idtac | eapply AuAssoc ].
+ eapply ARight.
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 ].
+ eapply AComp; [ idtac | eapply ARight; eapply ACont ].
+ eapply AComp; [ eapply ARight; eapply lpf | idtac ].
+ eapply AComp; [ eapply ALeft; eapply rpf | idtac ].
clear lpf rpf.
simpl.
apply arrangeSwapMiddle.
(* where the leaf is v *)
apply inr.
subst.
- apply RuCanL.
+ apply AuCanL.
(* where the leaf is NOT v *)
apply inl.
- apply RuCanR.
+ apply AuCanR.
(* empty leaf *)
destruct case_None.
apply inl; simpl in *.
- apply RuCanR.
+ apply AuCanR.
(* branch *)
refine (
destruct case_Neither.
apply inl.
- eapply RComp; [idtac | apply RuCanR ].
- exact (RComp
+ eapply AComp; [idtac | apply AuCanR ].
+ exact (AComp
(* order will not matter because these are central as morphisms *)
- (RRight _ (RComp lpf (RCanR _)))
- (RLeft _ (RComp rpf (RCanR _)))).
+ (ARight _ (AComp lpf (ACanR _)))
+ (ALeft _ (AComp rpf (ACanR _)))).
destruct case_Right.
apply inr.
fold (stripOutVars (v::nil)).
- set (RRight (mapOptionTree ξ ctx2) (RComp lpf ((RCanR _)))) as q.
+ set (ARight (mapOptionTree ξ ctx2) (AComp lpf ((ACanR _)))) as q.
simpl in *.
- eapply RComp.
+ eapply AComp.
apply q.
clear q.
clear lpf.
unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
- eapply RComp; [ idtac | apply RAssoc ].
- apply RLeft.
+ eapply AComp; [ idtac | apply AAssoc ].
+ apply ALeft.
apply rpf.
destruct case_Left.
apply inr.
unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
fold (stripOutVars (v::nil)).
- eapply RComp; [ idtac | eapply pivotContext ].
- set (RComp rpf (RCanR _ )) as rpf'.
- set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
+ eapply AComp; [ idtac | eapply pivotContext ].
+ set (AComp rpf (ACanR _ )) as rpf'.
+ set (ALeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
simpl in *.
- eapply RComp; [ idtac | apply qq ].
+ eapply AComp; [ idtac | apply qq ].
clear qq rpf' rpf.
- apply (RRight (mapOptionTree ξ ctx2)).
+ apply (ARight (mapOptionTree ξ ctx2)).
apply lpf.
destruct case_Both.
apply inr.
unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
fold (stripOutVars (v::nil)).
- eapply RComp; [ idtac | eapply copyAndPivotContext ].
+ eapply AComp; [ idtac | eapply copyAndPivotContext ].
(* order will not matter because these are central as morphisms *)
- exact (RComp (RRight _ lpf) (RLeft _ rpf)).
+ exact (AComp (ARight _ lpf) (ALeft _ rpf)).
Defined.
-(* same as before, but use RWeak if necessary *)
+(* same as before, but use AWeak if necessary *)
Definition factorContextLeftAndWeaken
(Γ:TypeEnv)(Δ:CoercionEnv Γ)
v (* variable to be pivoted, if found *)
(mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) ).
set (factorContextLeft Γ Δ v ctx ξ) as q.
destruct q; auto.
- eapply RComp; [ apply a | idtac ].
- refine (RRight _ (RWeak _)).
+ eapply AComp; [ apply a | idtac ].
+ refine (ARight _ (AWeak _)).
Defined.
Definition factorContextLeftAndWeaken''
unfold mapOptionTree; simpl in *.
intros.
rewrite (@stripping_nothing_is_inert Γ); auto.
- apply RuCanL.
+ apply AuCanL.
intros.
unfold mapOptionTree in *.
simpl in *.
unfold stripOutVars in q.
rewrite q in IHv1'.
clear q.
- eapply RComp; [ idtac | eapply RAssoc ].
- eapply RComp; [ idtac | eapply IHv1' ].
+ eapply AComp; [ idtac | eapply AAssoc ].
+ eapply AComp; [ idtac | eapply IHv1' ].
clear IHv1'.
apply IHv2; auto.
auto.
auto.
Defined.
-(* same as before, but use RWeak if necessary *)
+(* same as before, but use AWeak if necessary *)
Definition factorContextRightAndWeaken
(Γ:TypeEnv)(Δ:CoercionEnv Γ)
v (* variable to be pivoted, if found *)
(mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) ).
set (factorContextRight Γ Δ v ctx ξ) as q.
destruct q; auto.
- eapply RComp; [ apply a | idtac ].
- refine (RLeft _ (RWeak _)).
+ eapply AComp; [ apply a | idtac ].
+ refine (ALeft _ (AWeak _)).
Defined.
Definition factorContextRightAndWeaken''
unfold mapOptionTree; simpl in *.
intros.
rewrite (@stripping_nothing_is_inert Γ); auto.
- apply RuCanR.
+ apply AuCanR.
intros.
unfold mapOptionTree in *.
simpl in *.
fold X in IHv2'.
set (distinct_app _ _ _ H) as H'.
destruct H' as [H1 H2].
- set (RComp (IHv1 _ H1) (IHv2' H2)) as qq.
- eapply RComp.
+ set (AComp (IHv1 _ H1) (IHv2' H2)) as qq.
+ eapply AComp.
apply qq.
clear qq IHv2' IHv2 IHv1.
rewrite strip_swap_lemma.
rewrite strip_twice_lemma.
rewrite (notin_strip_inert' v1 (leaves v2)).
- apply RCossa.
+ apply AuAssoc.
apply distinct_swap.
auto.
Defined.
(* un-letrec-ify multi branch letrecs *)
| WELetRec mlr e => WELetRec mlr (simplifyWeakExpr e )
end.
-*)
\ No newline at end of file
+*)
(* Figure 3, production $\vdash_E$, Uniform rules *)
Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
- | RId : forall a , Arrange a a
- | RCanL : forall a , Arrange ( [],,a ) ( a )
- | RCanR : forall a , Arrange ( a,,[] ) ( a )
- | RuCanL : forall a , Arrange ( a ) ( [],,a )
- | RuCanR : forall a , Arrange ( a ) ( a,,[] )
- | RAssoc : forall a b c , Arrange (a,,(b,,c) ) ((a,,b),,c )
- | RCossa : forall a b c , Arrange ((a,,b),,c ) ( a,,(b,,c) )
- | RExch : forall a b , Arrange ( (b,,a) ) ( (a,,b) )
- | RWeak : forall a , Arrange ( [] ) ( a )
- | RCont : forall a , Arrange ( (a,,a) ) ( a )
- | RLeft : forall {h}{c} x , Arrange h c -> Arrange ( x,,h ) ( x,,c)
- | RRight : forall {h}{c} x , Arrange h c -> Arrange ( h,,x ) ( c,,x)
- | RComp : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c
+ | AId : forall a , Arrange a a
+ | ACanL : forall a , Arrange ( [],,a ) ( a )
+ | ACanR : forall a , Arrange ( a,,[] ) ( a )
+ | AuCanL : forall a , Arrange ( a ) ( [],,a )
+ | AuCanR : forall a , Arrange ( a ) ( a,,[] )
+ | AAssoc : forall a b c , Arrange (a,,(b,,c) ) ((a,,b),,c )
+ | AuAssoc : forall a b c , Arrange ((a,,b),,c ) ( a,,(b,,c) )
+ | AExch : forall a b , Arrange ( (b,,a) ) ( (a,,b) )
+ | AWeak : forall a , Arrange ( [] ) ( a )
+ | ACont : forall a , Arrange ( (a,,a) ) ( a )
+ | ALeft : forall {h}{c} x , Arrange h c -> Arrange ( x,,h ) ( x,,c)
+ | ARight : forall {h}{c} x , Arrange h c -> Arrange ( h,,x ) ( c,,x)
+ | AComp : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c
.
(* "Arrange" objects are parametric in the type of the leaves of the tree *)
Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
intros.
induction X; simpl.
- apply RId.
- 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 IHX1 | apply IHX2 ].
+ apply AId.
+ apply ACanL.
+ apply ACanR.
+ apply AuCanL.
+ apply AuCanR.
+ apply AAssoc.
+ apply AuAssoc.
+ apply AExch.
+ apply AWeak.
+ apply ACont.
+ apply ALeft; auto.
+ apply ARight; auto.
+ eapply AComp; [ apply IHX1 | apply IHX2 ].
Defined.
(* a frequently-used Arrange - swap the middle two elements of a four-element sequence *)
Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
- eapply RComp.
- apply RCossa.
- eapply RComp.
- eapply RLeft.
- eapply RComp.
- eapply RAssoc.
- eapply RRight.
- apply RExch.
- eapply RComp.
- eapply RLeft.
- eapply RCossa.
- eapply RAssoc.
+ eapply AComp.
+ apply AuAssoc.
+ eapply AComp.
+ eapply ALeft.
+ eapply AComp.
+ eapply AAssoc.
+ eapply ARight.
+ apply AExch.
+ eapply AComp.
+ eapply ALeft.
+ eapply AuAssoc.
+ eapply AAssoc.
Defined.
- (* like RExch, but works on nodes which are an Assoc away from being adjacent *)
+ (* like AExch, but works on nodes which are an Assoc away from being adjacent *)
Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
- RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
+ AComp (AComp (AuAssoc _ _ _) (ALeft a (AExch c b))) (AAssoc _ _ _).
- (* like RExch, but works on nodes which are an Assoc away from being adjacent *)
+ (* like AExch, but works on nodes which are an Assoc away from being adjacent *)
Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
- RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _).
+ AComp (AComp (AAssoc _ _ _) (ARight c (AExch b a))) (AuAssoc _ _ _).
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 ].
- eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
- apply RAssoc.
+ eapply AComp; [ idtac | apply (ALeft (a,,c) (ACont b)) ].
+ eapply AComp; [ idtac | apply AuAssoc ].
+ eapply AComp; [ idtac | apply (ARight b (pivotContext a b c)) ].
+ apply AAssoc.
Defined.
(* given any set of TreeFlags on a tree, we can Arrange all of the flagged nodes into the left subtree *)
destruct a.
simpl.
destruct (f t); simpl.
- apply RuCanL.
- apply RuCanR.
+ apply AuCanL.
+ apply AuCanR.
simpl.
- apply RuCanL.
+ apply AuCanL.
simpl in *.
- eapply RComp; [ idtac | apply arrangeSwapMiddle ].
- eapply RComp.
- eapply RLeft.
+ eapply AComp; [ idtac | apply arrangeSwapMiddle ].
+ eapply AComp.
+ eapply ALeft.
apply IHΣ2.
- eapply RRight.
+ eapply ARight.
apply IHΣ1.
Defined.
destruct a.
simpl.
destruct (f t); simpl.
- apply RCanL.
- apply RCanR.
+ apply ACanL.
+ apply ACanR.
simpl.
- apply RCanL.
+ apply ACanL.
simpl in *.
- eapply RComp; [ apply arrangeSwapMiddle | idtac ].
- eapply RComp.
- eapply RLeft.
+ eapply AComp; [ apply arrangeSwapMiddle | idtac ].
+ eapply AComp.
+ eapply ALeft.
apply IHΣ2.
- eapply RRight.
+ eapply ARight.
apply IHΣ1.
Defined.
induction q; intros.
simpl in H.
rewrite H.
- apply RId.
+ apply AId.
simpl in *.
destruct t; try destruct o; inversion H.
set (IHq1 _ H1) as x1.
set (IHq2 _ H2) as x2.
- eapply RComp.
- eapply RRight.
+ eapply AComp.
+ eapply ARight.
rewrite <- H1.
apply x1.
- eapply RComp.
- apply RCanL.
+ eapply AComp.
+ apply ACanL.
rewrite <- H2.
apply x2.
Defined.
induction q; intros.
simpl in H.
rewrite H.
- apply RId.
+ apply AId.
simpl in *.
destruct t; try destruct o; inversion H.
set (IHq1 _ H1) as x1.
set (IHq2 _ H2) as x2.
- eapply RComp.
- apply RuCanL.
- eapply RComp.
- eapply RRight.
+ eapply AComp.
+ apply AuCanL.
+ eapply AComp.
+ eapply ARight.
apply x1.
- eapply RComp.
- eapply RLeft.
+ eapply AComp.
+ eapply ALeft.
apply x2.
rewrite H.
- apply RId.
+ apply AId.
Defined.
(* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (dropT Σ₁) to (dropT Σ₂) *)
refine ((fix arrangeTake t1 t2 (arr:Arrange t1 t2) :=
match arr as R in Arrange A B return Arrange (dropT (mkFlags pred A)) (dropT (mkFlags pred B)) with
- | RId a => let case_RId := tt in RId _
- | RCanL a => let case_RCanL := tt in _
- | RCanR a => let case_RCanR := tt in _
- | RuCanL a => let case_RuCanL := tt in _
- | RuCanR a => let case_RuCanR := tt in _
- | 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 _
- | RCont a => let case_RCont := tt in _
- | RLeft a b c r' => let case_RLeft := tt in RLeft _ (arrangeTake _ _ r')
- | RRight a b c r' => let case_RRight := tt in RRight _ (arrangeTake _ _ r')
- | RComp a b c r1 r2 => let case_RComp := tt in RComp (arrangeTake _ _ r1) (arrangeTake _ _ r2)
+ | AId a => let case_AId := tt in AId _
+ | ACanL a => let case_ACanL := tt in _
+ | ACanR a => let case_ACanR := tt in _
+ | AuCanL a => let case_AuCanL := tt in _
+ | AuCanR a => let case_AuCanR := tt in _
+ | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _
+ | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _
+ | AExch a b => let case_AExch := tt in AExch _ _
+ | AWeak a => let case_AWeak := tt in _
+ | ACont a => let case_ACont := tt in _
+ | ALeft a b c r' => let case_ALeft := tt in ALeft _ (arrangeTake _ _ r')
+ | ARight a b c r' => let case_ARight := tt in ARight _ (arrangeTake _ _ r')
+ | AComp a b c r1 r2 => let case_AComp := tt in AComp (arrangeTake _ _ r1) (arrangeTake _ _ r2)
end)); clear arrangeTake; intros.
- destruct case_RCanL.
- simpl; destruct (pred None); simpl; apply RCanL.
+ destruct case_ACanL.
+ simpl; destruct (pred None); simpl; apply ACanL.
- destruct case_RCanR.
- simpl; destruct (pred None); simpl; apply RCanR.
+ destruct case_ACanR.
+ simpl; destruct (pred None); simpl; apply ACanR.
- destruct case_RuCanL.
- simpl; destruct (pred None); simpl; apply RuCanL.
+ destruct case_AuCanL.
+ simpl; destruct (pred None); simpl; apply AuCanL.
- destruct case_RuCanR.
- simpl; destruct (pred None); simpl; apply RuCanR.
+ destruct case_AuCanR.
+ simpl; destruct (pred None); simpl; apply AuCanR.
- destruct case_RWeak.
- simpl; destruct (pred None); simpl; apply RWeak.
+ destruct case_AWeak.
+ simpl; destruct (pred None); simpl; apply AWeak.
- destruct case_RCont.
- simpl; destruct (pred None); simpl; apply RCont.
+ destruct case_ACont.
+ simpl; destruct (pred None); simpl; apply ACont.
Defined.
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 AuCanL.
+ eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply ACanL ].
apply nd_rule.
(*
set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
intros; apply nd_rule. unfold PCFRule. simpl.
- exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
+ exists (RArrange _ _ _ _ _ (AuAssoc _ _ _)).
apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
intros; apply nd_rule. unfold PCFRule. simpl.
- exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
+ exists (RArrange _ _ _ _ _ (AAssoc _ _ _)).
apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
intros; apply nd_rule. unfold PCFRule. simpl.
- exists (RArrange _ _ _ _ _ (RCanL _)).
+ exists (RArrange _ _ _ _ _ (ACanL _)).
apply (PCF_RArrange _ _ lev ([],,a) _ _).
intros; apply nd_rule. unfold PCFRule. simpl.
- exists (RArrange _ _ _ _ _ (RCanR _)).
+ exists (RArrange _ _ _ _ _ (ACanR _)).
apply (PCF_RArrange _ _ lev (a,,[]) _ _).
intros; apply nd_rule. unfold PCFRule. simpl.
- exists (RArrange _ _ _ _ _ (RuCanL _)).
+ exists (RArrange _ _ _ _ _ (AuCanL _)).
apply (PCF_RArrange _ _ lev _ ([],,a) _).
intros; apply nd_rule. unfold PCFRule. simpl.
- exists (RArrange _ _ _ _ _ (RuCanR _)).
+ exists (RArrange _ _ _ _ _ (AuCanR _)).
apply (PCF_RArrange _ _ lev _ (a,,[]) _).
Defined.