.
Opaque switch_scope.
induction blk using block_ind2;
intros *
Hsubin Hsubnin Hsubat Hnsub Hnsubl Hsub Hsubl Hincl Hnd1 Hnd2 Hat Hdomub Hdomlb Hsc Hdomub1 Hbck Hnl3 LD Hnd3 Hgood Hwt Hwc Hsem Hmmap;
inv LD;
inv Hnl3;
inv Hnd3;
inv Hgood;
inv Hwt;
inv Hwc;
inv Hsem;
simpl in *;
repeat inv_bind.
-
constructor.
eapply subclock_equation_sem with (
H:=
Hi);
eauto.
-
econstructor;
eauto.
+
eapply subclock_exp_sem with (
H:=
Hi);
eauto.
+
eapply Hnsub;
eauto.
apply Env.Props.P.F.not_find_in_iff.
intros contra.
eapply Hsubnin;
eauto.
+
eapply Hnsubl;
eauto.
apply Env.Props.P.F.not_find_in_iff.
intros contra.
eapply Hsubnin;
eauto.
-
econstructor;
eauto.
1:{
eapply subclock_exp_sem with (
H:=
Hi);
eauto using change_last,
sem_var_refines. }
intros k.
eapply switch_blocks_sem'
with (Γ
ty:=Γ
ty) (
Hi:=
mask_hist k r Hi)
in H0;
eauto.
1-4:(
intros *
Hfind Hv;
eapply sem_var_mask_inv in Hv as (?&
Hv&
Heq);
rewrite Heq;
eapply sem_var_mask;
eauto).
+
apply dom_ub_map;
auto.
+
apply dom_lb_map;
auto.
+
eapply sc_vars_mask in Hsc;
eauto.
+
apply dom_ub_map;
auto.
+
eapply sem_clock_mask;
eauto.
-
destruct (
partition _ _)
eqn:
Hpart.
apply partition_Partition in Hpart.
repeat inv_bind.
destruct x.
repeat inv_bind.
rename x into subs.
assert (
sem_clock (
var_history Hi)
bs ck (
abstract_clock sc))
as Hsemck.
{
take (
sem_exp_ck _ _ _ _ _)
and eapply sc_exp in it;
eauto.
rewrite H14 in it;
simpl in *.
now inv it. }
repeat rewrite subclock_exp_typeof,
H8 in *;
simpl in *.
repeat rewrite subclock_exp_clockof,
H14 in *;
simpl in *.
assert (
sem_clock (
var_history Hi')
bs' (
subclock_clock bck sub ck) (
abstract_clock sc))
as Hsemck'.
{
eapply subclock_clock_sem. 3,4:
eauto. 1,2:
intros *;
rewrite 2
sem_var_history;
eauto using sem_var_refines. }
assert (
incl (
l ++
filter (
fun '(
_,
ann) =>
ann.(
clo) ==
b ck)
l0) Γ
ck)
as Hincl1.
{
apply Partition_Permutation in Hpart.
rewrite Hpart.
apply incl_app; [
solve_incl_app|
apply incl_appr,
incl_filter',
incl_refl]. }
assert (
NoDupMembers (
l ++
filter (
fun '(
_,
ann) =>
ann.(
clo) ==
b ck)
l0))
as Hnd'.
{
apply Partition_Permutation in Hpart.
rewrite Hpart in Hnd2.
apply NoDupMembers_app;
eauto using NoDupMembers_app_l,
NoDupMembers_app_r,
NoDupMembers_filter.
intros ?
Hinm1 Hinm2.
eapply NoDupMembers_app_InMembers in Hnd2;
eauto.
eapply Hnd2,
filter_InMembers';
eauto. }
assert (
Forall (
fun '(
x,
_) =>
forall vs,
sem_var Hi (
Var x)
vs ->
abstract_clock vs ≡
abstract_clock sc)
(
filter (
fun '(
_,
ann) =>
ann.(
clo) ==
b ck)
l0 ++
l))
as Hsc'.
{
eapply Forall_forall;
intros (?&?)
Hin *
Hv.
rewrite Permutation_app_comm in Hincl1.
eapply Hsc in Hv. 2:
apply Hincl1 in Hin;
eauto with senv.
assert (
clo a =
ck);
subst. 2:
eapply sem_clock_det;
eauto.
apply in_app_iff in Hin as [
Hin|
Hin].
-
apply filter_In in Hin as (?&
Hin').
rewrite equiv_decb_equiv in Hin';
inv Hin';
auto.
-
assert (
Is_defined_in (
Var i0) (
Bswitch ec branches))
as Hdef.
{
eapply vars_defined_Is_defined_in.
eapply Partition_Forall1,
Forall_forall in Hpart;
eauto;
simpl in *.
apply PSF.mem_2;
auto. }
inv Hdef.
simpl_Exists.
simpl_Forall.
repeat inv_branch.
simpl_Exists.
simpl_Forall.
take (
Syn.Is_defined_in _ _)
and eapply wc_block_Is_defined_in in it;
eauto.
eapply InMembers_In in it as (?&
Hin').
take (
forall x ck,
HasClock _ _ _ ->
_)
and edestruct it as (
Hck&
_);
eauto with senv.
inv Hck.
eapply NoDupMembers_det with (
t:=
a)
in H1;
eauto.
congruence.
eapply Hincl1;
auto using in_or_app.
}
assert (
Forall (
fun '(
x,
_) =>
forall vs,
sem_var Hi (
Last x)
vs ->
abstract_clock vs ≡
abstract_clock sc)
(
filter (
fun '(
_,
ann) =>
isSome (
causl_last ann)) (
filter (
fun '(
_,
ann) =>
ann.(
clo) ==
b ck)
l0 ++
l)))
as Hscl'.
{
eapply Forall_forall;
intros (?&?)
Hin *
Hv.
simpl_In.
rewrite Permutation_app_comm in Hincl1.
eapply Hsc in Hv.
2:{
apply Hincl1 in Hin0;
eauto with senv. }
2:{
apply Partition_Permutation in Hpart.
rewrite Hpart.
econstructor.
rewrite in_app_iff in *.
destruct Hin0;
simpl_In;
eauto.
destruct a,
causl_last0;
simpl in *;
congruence. }
assert (
clo a =
ck);
subst. 2:
eapply sem_clock_det;
eauto.
apply in_app_iff in Hin0 as [
Hin|
Hin].
-
apply filter_In in Hin as (?&
Hin').
rewrite equiv_decb_equiv in Hin';
inv Hin';
auto.
-
assert (
Is_defined_in (
Var i0) (
Bswitch ec branches))
as Hdef.
{
eapply vars_defined_Is_defined_in.
eapply Partition_Forall1,
Forall_forall in Hpart;
eauto;
simpl in *.
apply PSF.mem_2;
auto. }
inv Hdef.
simpl_Exists.
simpl_Forall.
repeat inv_branch.
simpl_Exists.
simpl_Forall.
take (
Syn.Is_defined_in _ _)
and eapply wc_block_Is_defined_in in it;
eauto.
eapply InMembers_In in it as (?&
Hin').
take (
forall x ck,
HasClock _ _ _ ->
_)
and edestruct it as (
Hck&
_);
eauto with senv.
inv Hck.
eapply NoDupMembers_det with (
t:=
a)
in H1;
eauto.
congruence.
eapply Hincl1;
auto using in_or_app.
}
assert (
forall x,
InMembers x (
l ++
filter (
fun '(
_,
ann) =>
ann.(
clo) ==
b ck)
l0) ->
Forall (
fun '(
_,
sub,
_,
_,
_,
_) =>
Env.In x sub)
subs)
as Hinsubs.
{
intros ?
Hinm.
eapply mmap_values,
Forall2_ignore1 in H6;
eauto.
eapply Forall_impl; [|
eapply H6];
intros (((?&?)&?)&?) ((?&?)&?&?&?&?);
repeat inv_bind.
apply Env.In_from_list,
fst_InMembers.
erewrite map_map,
map_ext,
map_app, ?
new_idents_old, <-
map_app;
eauto. 2:
intros ((?&?)&(?&?));
auto.
now rewrite <-
fst_InMembers,
Permutation_app_comm. }
assert (
sem_exp_ck G2 Hi'
bs' (
subclock_exp bck sub subl ec) [
sc])
as Hsem.
{
eapply subclock_exp_sem with (
H:=
Hi);
eauto using change_last,
sem_var_refines. }
assert (
Hcond:=
H0).
eapply cond_eq_sem in H0 as (
Hi1&
Hv1&
Hsem1&
Href1&
Hdom1&
Hdoml1&
Hsc1);
eauto.
assert (
dom_ub (
Hi' +
Hi1) (Γ
ty ++
st_senv x1))
as Hdomub1'.
{
split;
intros ?
Hin;
apply FEnv.union_In in Hin as [
Hin|
Hin];
try apply Hdomub1 in Hin.
-
eapply IsVar_incl; [|
eauto].
eapply incl_appr',
incl_map,
st_follows_incl;
eauto using cond_eq_st_follows.
-
eapply Hdom1,
cond_eq_incl in Hin; [|
eauto].
apply IsVar_app,
or_intror,
IsVar_fst.
unfold st_senv,
senv_of_tyck.
solve_In.
-
eapply IsLast_incl; [|
eauto].
eapply incl_appr',
incl_map,
st_follows_incl;
eauto using cond_eq_st_follows.
-
eapply Hdoml1 in Hin as [].
}
assert (
Hni:=
H6).
eapply new_idents_sem with (
bs':=
bs')
in H6 as (
Hi2&
Href2&
Hdom2&
Hdoml2&
Hv2&
Hl2&
Hsc2);
eauto with fresh.
2:{
eapply Sem.sem_clock_refines;
eauto using var_history_refines. }
2:
take (
wt_streams [
_] [
_])
and inv it;
auto.
constructor.
eapply Sscope with (
Hi':=
Hi1 +
Hi2);
eauto. 3:
rewrite ?
Forall_app;
repeat split.
split.
+
intros.
rewrite FEnv.union_In,
Hdom1,
Hdom2,
IsVar_senv_of_decls,
InMembers_app.
apply or_iff_compat_r.
erewrite fst_InMembers,
map_map,
map_ext.
reflexivity.
intros;
destruct_conjs;
auto.
+
intros.
rewrite FEnv.union_In,
senv_of_decls_app,
IsLast_app.
split; [
intros [
In|
In]|
intros [
In|
In]]. 3,4:
clear -
In;
inv In;
simpl_In;
congruence.
1,2:
exfalso.
eapply Hdoml1;
eauto.
eapply Hdoml2;
eauto.
+
simpl_app.
apply sc_vars_app.
*
intros *
Hinm1 Hinm2.
rewrite fst_InMembers in Hinm1,
Hinm2.
specialize (
st_valid_NoDup x2)
as Hvalid'.
apply new_idents_st_ids'
in Hni.
apply cond_eq_st_ids in Hcond.
rewrite Hni,
Hcond in Hvalid'.
simpl_app.
simpl_In.
eapply NoDup_app_r,
NoDup_app_In in Hvalid'. 2:
solve_In.
eapply Hvalid'.
solve_In.
auto.
*
eapply sc_vars_refines.
1:{
rewrite FEnv.union_assoc;
eauto using EqStrel_Reflexive. }
3:{
erewrite map_map,
map_ext;
eauto.
intros (?&?&?);
auto. }
--
intros *
Hin1 Hin2.
erewrite IsVar_fst, 2
map_map,
map_ext, <-
fst_InMembers in Hin1.
2:
intros;
destruct_conjs;
auto.
apply fst_InMembers,
Hdom1 in Hin1.
apply FEnv.union_In;
auto.
--
intros *
L.
clear -
L.
inv L.
simpl_In.
congruence.
*
clear -
Hsc2.
eapply sc_vars_morph. 4:
eauto. 3:
reflexivity.
2:
symmetry;
apply FEnv.union_assoc;
auto using EqStrel_Reflexive.
erewrite 2
flat_map_concat_map,
concat_map,
map_map,
map_ext;
eauto.
intros;
destruct_conjs;
auto.
erewrite map_map,
map_ext;
eauto.
intros;
destruct_conjs;
auto.
+
simpl_Forall.
assert (
Is_defined_in (
Var i0) (
Bswitch ec branches))
as Hdef.
{
eapply vars_defined_Is_defined_in.
eapply Partition_Forall1,
Forall_forall in Hpart;
eauto;
simpl in *.
apply PSF.mem_2;
auto. }
assert (
exists vs,
sem_var Hi (
Var i0)
vs)
as (
vs&
Hi0).
{
eapply sem_block_defined in Hdef;
eauto.
-
inv Hdef.
esplit;
econstructor;
eauto.
reflexivity.
-
econstructor;
eauto.
take (
typeof ec =
_)
and now rewrite it. }
inv Hdef.
simpl_Exists.
simpl_Forall.
repeat inv_branch.
simpl_Exists.
simpl_Forall.
take (
Is_defined_in _ _)
and eapply wc_block_Is_defined_in,
InMembers_In in it as (?&
Hin1);
eauto.
assert (
HasClock Γ'
i0 x5.(
clo))
as Hck by eauto with senv.
eapply H16 in Hck as (
Hin'&?);
subst.
inv Hin'.
eapply sem_block_ck_morph; [
symmetry;
eapply FEnv.union_assoc,
EqStrel_Reflexive| | |];
simpl;
try reflexivity.
eapply merge_defs_sem with (
Hi:=
Hi);
eauto using Sem.sem_var_refines.
*
rewrite <-
H10.
replace (
map fst (
map _ subs))
with (
map fst branches).
reflexivity.
clear -
Hni.
apply mmap_values in Hni.
induction Hni as [|(?&?) (((?&?)&?)&?)];
simpl;
auto.
destruct H as (?&?&?);
repeat inv_bind.
f_equal;
auto.
*
take (
wt_streams [
_] [
_])
and inv it;
auto.
*
eapply sem_clock_det in Hsemck;
eauto.
destruct Hsc as (
Hsc&
_).
eapply Hsc;
eauto with senv.
*
simpl_Forall.
eapply Hv2;
eauto.
assert (
Env.In i0 t0)
as Henvin.
{
eapply Forall_forall in Hinsubs;
eauto. 2:
eapply InMembers_app;
left;
eauto using In_InMembers.
simpl in *;
auto. }
inv Henvin.
unfold rename_var,
Env.MapsTo in *.
rewrite H24 in *;
auto.
+
eapply CS.mmap2_values'
in H20.
assert (
st_follows x1 x2)
as Hfollows2.
{
eapply mmap_st_follows;
eauto.
simpl_Forall;
destruct_conjs;
repeat inv_bind.
repeat (
etransitivity;
eauto using new_idents_st_follows). }
assert (
Hf:=
Hni).
eapply mmap_values,
Forall3_ignore3'
with (
zs:=
x3)
in Hf.
2:{
eapply Forall3_length in H20 as (?&?);
congruence. }
2:
eapply mmap_length in Hni;
eauto.
2:{
intros;
destruct_conjs.
take (
branch _)
and destruct it.
repeat inv_bind.
eapply mmap_st_follows;
eauto.
simpl_Forall;
eauto using switch_block_st_follows. }
eapply Forall3_Forall3 in Hf; [|
eapply H20].
clear H20.
eapply Forall_concat,
Forall_forall;
intros ?
Hin1.
eapply Forall3_ignore12,
Forall_forall in Hf as ((?&?)&?&
Hin2&
Hin3&(?&?&
Hfollows&?)&?&?&?);
eauto;
repeat inv_bind.
simpl_Forall.
repeat inv_branch.
repeat inv_bind.
take (
In _ (
_ ++
_))
and rewrite ?
in_app_iff in it.
destruct it as [|[
Hin|
Hin]];
simpl_Forall.
*{
eapply sem_block_ck_morph; [
symmetry;
eapply FEnv.union_assoc,
EqStrel_Reflexive| | |];
simpl;
try reflexivity.
assert (
Forall (
wc_block G1 (
map (
fun '(
x,
ann0) => (
x,
ann_with_clock ann0 Cbase)) (
l ++
filter (
fun '(
_,
ann0) =>
clo ann0 ==
b ck)
l0)))
blks)
as Hwc'.
{
simpl_Forall.
eapply wc_block_incl; [| |
eauto].
+
intros *
Hin.
apply H16 in Hin as (
Hin&?);
subst.
inv Hin;
econstructor;
solve_In.
2:{
apply Partition_Permutation in Hpart.
rewrite Hpart in H25.
rewrite in_app_iff in *.
destruct H25;
eauto;
right;
solve_In.
apply equiv_decb_refl. }
simpl;
eauto.
auto.
+
intros *
Hin.
assert (
HasClock Γ
ck x16 ck)
as Ck.
{
inv Hin.
edestruct H16;
eauto with senv. }
eapply H18 in Hin.
inv Hin.
inv Ck.
eapply NoDupMembers_det in H25;
eauto;
subst.
apply Partition_Permutation in Hpart.
rewrite Hpart,
in_app_iff in H30.
rewrite map_app,
IsLast_app.
destruct H30 as [
Hin|
Hin]; [
left|
right];
econstructor;
solve_In.
2:
apply equiv_decb_refl.
1,2:
destruct e0;
simpl in *;
auto.
}
eapply switch_blocks_sem'
with (
ls:=
map (
fun _ => [])
blks) (Γ
ty:=Γ
ty) (
bs:=
fwhenb e bs sc)
(
Hi:=
restrict (
fwhen_hist e Hi sc) (
map (
fun '(
x,
ann0) => (
x,
ann_with_clock ann0 Cbase)) (
l ++
filter (
fun '(
_,
ann) =>
ann.(
clo) ==
b ck)
l0)))
in H0.
simpl_Forall;
eauto.
all:
eauto.
-
intros ?
Hin.
rewrite ?
Env.In_from_list, ?
fst_InMembers in Hin.
rewrite fst_InMembers.
destruct Hin.
+
erewrite map_map,
map_ext,
map_app, <-2
new_idents_old, <-
map_app,
Permutation_app_comm;
eauto.
solve_In.
intros;
destruct_conjs;
auto.
+
simpl_In.
eapply new_idents_In_inv in H21 as (?&
In&
_);
eauto.
setoid_rewrite Permutation_app_comm.
solve_In.
-
intros *
_ In.
apply in_concat in In as (?&?&
In).
simpl_In.
inv In.
-
repeat (
take (
new_idents _ _ _ _ _ _ =
_)
and apply new_idents_prefixed in it).
intros * [
Hfind|
Hfind];
apply Env.from_list_find_In in Hfind;
simpl_In.
+
apply in_app_iff in Hin as [|];
simpl_Forall;
eauto.
+
simpl_Forall.
eauto.
-
intros ??
Hfind Hv.
eapply Sem.sem_var_restrict_inv in Hv as (
Hin&
_).
exfalso.
apply Env.Props.P.F.not_find_in_iff in Hfind.
apply Hfind,
Env.In_from_list.
rewrite fst_InMembers.
erewrite vars_of_senv_Var,
IsVar_fst,
map_map,
map_ext,
map_app, <-2
new_idents_old, <-
map_app,
Permutation_app_comm in Hin;
eauto.
erewrite map_map,
map_ext;
eauto. 1,2:
intros;
destruct_conjs;
auto.
-
intros ??
Hfind Hv.
eapply Sem.sem_var_restrict_inv in Hv as (
Hin&
_).
exfalso.
apply Env.Props.P.F.not_find_in_iff in Hfind.
apply Hfind,
Env.In_from_list.
rewrite fst_InMembers.
erewrite vars_of_senv_Last in Hin.
erewrite map_map,
map_ext,
new_idents_old;
eauto.
2:
intros;
destruct_conjs;
auto.
inv Hin.
rewrite Permutation_app_comm.
solve_In.
destruct a;
simpl in *.
destruct causl_last0;
simpl;
auto;
congruence.
-
intros ???
Hfind Hv.
eapply Sem.sem_var_restrict_inv in Hv as (
_&
Hv).
eapply sem_var_fwhen_inv in Hv as (?&
Hv&
Heq).
rewrite Heq;
eauto.
-
intros ???
Hfind Hv.
eapply Sem.sem_var_restrict_inv in Hv as (
_&
Hv).
eapply sem_var_fwhen_inv in Hv as (?&
Hv&
Heq).
rewrite Heq;
eauto.
-
etransitivity; [|
eauto].
erewrite map_map,
map_ext.
apply incl_map;
eauto.
intros (?&?);
auto.
-
clear -
Hnd'.
erewrite fst_NoDupMembers,
map_map,
map_ext, <-
fst_NoDupMembers;
auto.
intros (?&?);
auto.
-
simpl_Forall;
auto.
-
split;
intros ?
In;
eapply dom_ub_map;
eauto.
1,2:
eapply FEnv.restrict_In in In as (?&?);
eauto.
-
split;
intros ?
In;
apply FEnv.restrict_In;
(
split; [
apply FEnv.map_in_iff,
Hdomlb|
try apply vars_of_senv_Var;
try apply vars_of_senv_Last]).
1:
eapply IsVar_incl;
eauto. 3:
eapply IsLast_incl;
eauto.
1,2:
clear -
In;
inv In;
econstructor;
solve_In.
1,2:
clear -
In;
inv In;
eapply in_map_iff in H as ((?&?)&?&?);
inv_equalities;
econstructor;
eauto;
solve_In.
-
split.
+
intros *
Hck Hv.
inv Hck.
simpl_In.
eapply Forall_forall in Hsc'. 2:
rewrite Permutation_app_comm;
eauto.
simpl in *.
apply Sem.sem_var_restrict_inv in Hv as (
_&
Hv).
apply sem_var_fwhen_inv in Hv as (?&
Hv&
Hwhen).
constructor.
rewrite Hwhen,
ac_fwhen,
Hsc';
eauto.
apply fwhenb_both_slower;
eauto using ac_slower,
sc_slower,
ac_aligned.
+
intros *
Hck Hl Hv.
inv Hck.
inv Hl.
simpl_In.
eapply NoDupMembers_det in Hin0;
eauto;
subst.
eapply Forall_forall in Hscl'.
2:{
rewrite Permutation_app_comm.
solve_In.
simpl.
destruct causl_last;
simpl;
auto. }
simpl in *.
apply Sem.sem_var_restrict_inv in Hv as (
_&
Hv).
apply sem_var_fwhen_inv in Hv as (?&
Hv&
Hwhen).
constructor.
rewrite Hwhen,
ac_fwhen,
Hscl';
eauto.
apply fwhenb_both_slower;
eauto using ac_slower,
sc_slower,
ac_aligned.
-
split;
intros ?
Hin;
apply FEnv.union_In in Hin as [
Hin|
Hin].
+
eapply Hdomub1'
in Hin.
eapply IsVar_incl;
eauto.
eapply incl_appr',
incl_map,
st_follows_incl.
etransitivity;
eauto.
+
apply Hdom2 in Hin.
eapply IsVar_app,
or_intror,
IsVar_incl; [
eapply incl_map,
st_follows_incl;
eauto|].
eapply new_idents_st_ids'
in Hni.
erewrite IsVar_fst,
map_map,
map_ext.
setoid_rewrite Hni. 2:
intros;
destruct_conjs;
auto.
apply in_app_iff,
or_intror;
auto.
apply fst_InMembers in Hin.
clear -
Hin.
solve_In.
auto.
+
eapply Hdomub1'
in Hin.
eapply IsLast_incl;
eauto.
eapply incl_appr',
incl_map,
st_follows_incl.
etransitivity;
eauto.
+
exfalso.
eapply Hdoml2;
eauto.
-
eapply sem_clock_Con_when;
eauto using Sem.sem_clock_refines,
var_history_refines.
+
take (
wt_streams [
_] [
_])
and inv it;
auto.
+
eapply sc_slower;
eauto using ac_aligned.
+
eapply sem_var_history,
sem_var_refines;
eauto.
-
simpl_Forall.
auto.
-
simpl_Forall.
eapply sem_block_restrict;
eauto.
+
unfold wc_env.
simpl_Forall.
take (
In _ (
idck _))
and clear -
it.
simpl_In.
constructor.
+
take (
when_hist _ _ _ _)
and apply when_hist_fwhen_hist in it;
eauto using sem_block_refines.
}
*{
simpl_In.
simpl_Forall.
assert (
InMembers i0 (
filter (
fun '(
_,
ann) =>
ann.(
clo) ==
b ck)
l0))
as Hin.
{
eapply new_idents_In_inv in H6 as (?&?&?);
eauto using In_InMembers. }
apply InMembers_In in Hin as (?&
Hin).
assert (
exists vs,
sem_var Hi (
Var i0)
vs)
as (
vs&
Hv).
{
assert (
FEnv.In (
Var i0)
Hi)
as (?&?). 2:
do 2
econstructor;
eauto;
reflexivity.
eapply Hdomlb,
IsVar_incl,
IsVar_app,
or_intror;
eauto.
clear -
Hin.
econstructor.
solve_In. }
eapply Forall_forall in Hsc';
eauto using in_or_app;
simpl in *.
eapply sem_block_ck_morph; [
symmetry;
eapply FEnv.union_assoc,
EqStrel_Reflexive| | |];
simpl;
try reflexivity.
eapply when_free_sem;
eauto using Sem.sem_var_refines.
-
take (
wt_streams [
_] [
_])
and inv it;
auto.
-
eapply Sem.sem_var_refines; [|
eapply rename_var_sem;
eauto].
etransitivity;
eauto.
-
eapply Hv2;
eauto.
apply Env.find_In_from_list.
+
apply in_map_iff;
do 2
esplit;
eauto using in_or_app.
auto.
+
erewrite fst_NoDupMembers,
map_map,
map_ext,
map_app, 2
new_idents_old, <-
map_app, <-
fst_NoDupMembers. 2,3:
eauto.
now rewrite Permutation_app_comm.
intros ((?&?)&(?&?));
auto.
}
*{
simpl_In.
assert (
InMembers i0 (
filter (
fun '(
_,
ann) =>
isSome (
causl_last ann)) (
filter (
fun '(
_,
ann) =>
clo ann ==
b ck)
l0 ++
l)))
as Hin.
{
eapply new_idents_In_inv in H21 as (?&?&?);
eauto using In_InMembers. }
apply InMembers_In in Hin as (?&
Hin).
assert (
exists vs,
sem_var Hi (
Last i0)
vs)
as (
vs&
Hv).
{
assert (
FEnv.In (
Last i0)
Hi)
as (?&?). 2:
do 2
econstructor;
eauto;
reflexivity.
eapply Hdomlb,
IsLast_incl;
eauto.
rewrite Permutation_app_comm.
econstructor;
simpl_In.
eauto.
edestruct causl_last;
simpl in *;
congruence. }
eapply Forall_forall in Hscl';
eauto using in_or_app;
simpl in *.
eapply sem_block_ck_morph; [
symmetry;
eapply FEnv.union_assoc,
EqStrel_Reflexive| | |];
simpl;
try reflexivity.
eapply when_freel_sem;
eauto using Sem.sem_var_refines.
-
take (
wt_streams [
_] [
_])
and inv it;
auto.
-
eapply Hl2;
eauto.
apply Env.find_In_from_list.
+
apply in_map_iff;
do 2
esplit;
eauto using in_or_app.
auto.
+
erewrite fst_NoDupMembers,
map_map,
map_ext,
new_idents_old, <-
fst_NoDupMembers. 2:
eauto.
apply NoDupMembers_filter.
now rewrite Permutation_app_comm.
intros ((?&?)&(?&?));
auto.
}
+
simpl_Forall.
constructor.
eapply sem_equation_refines;
eauto.
rewrite FEnv.union_assoc;
eauto using EqStrel_Reflexive.
-
constructor.
eapply switch_scope_sem with (Γ
ty:=Γ
ty);
eauto.
intros.
simpl in *.
inv_VarsDefined.
eapply switch_blocks_sem'
with (Γ
ty:=Γ
ty0);
eauto.
+
intros *
In1.
rewrite Hperm;
eauto.
Transparent switch_scope.
Qed.