.
Opaque switch_scope.
induction blk using block_ind2;
intros *
Hnl1 Hnl2 Hsubin Hsub Hsubat Hnsub Hincl Hnd1 Hnd2 Hat Hdomub Hdomlb Hsc Hdomub1 Hbck Hnl3 Hnd3 Hgood Hwt Hwc Hsem Hmmap;
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 using change_last.
-
econstructor;
eauto.
1:{
eapply subclock_exp_sem with (
H:=
Hi);
eauto using change_last. }
intros k.
eapply switch_blocks_sem'
with (Γ
ty:=Γ
ty) (
Hi:=
mask_hist k r Hi)
in H0;
eauto.
+
intros ???
Hfind Hv.
eapply sem_var_mask_inv in Hv as (?&
Hv&
Heq).
rewrite Heq.
eapply sem_var_mask;
eauto.
+
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.
{
eapply sc_exp in H15;
eauto.
rewrite H12 in H15;
simpl in H15.
now inv H15. }
repeat rewrite subclock_exp_typeof,
H6 in *;
simpl in *.
repeat rewrite subclock_exp_clockof,
H12 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. }
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 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 H4;
eauto.
eapply Forall_impl; [|
eapply H4];
intros (((?&?)&?)&?) ((?&?)&?&?&?&?);
repeat inv_bind.
apply Env.In_from_list,
fst_InMembers.
erewrite map_map,
map_ext,
map_app, 2
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 ec) [
sc])
as Hsem.
{
eapply subclock_exp_sem with (
H:=
Hi);
eauto using change_last. }
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:=
H4).
eapply new_idents_sem with (
bs':=
bs')
in H4 as (
Hi2&
Href2&
Hdom2&
Hdoml2&
Hv2&
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. 4:
repeat 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.
+
apply Forall_app;
split;
simpl_Forall. 2:
simpl_In. 1,2:
constructor.
+
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 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 i0 _)
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 H14 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 <-
H8.
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 t)
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 H23 in *;
auto.
+
eapply CS.mmap2_values'
in H18.
assert (
st_follows x1 x2)
as Hfollows2.
{
eapply mmap_st_follows;
eauto.
simpl_Forall;
destruct_conjs;
repeat inv_bind.
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 H18 as (?&?);
congruence. }
2:
eapply mmap_length in Hni;
eauto.
2:{
intros (?&?) (((?&?)&?)&?) ????;
repeat inv_bind.
destruct b;
repeat inv_bind.
eapply mmap_st_follows;
eauto.
simpl_Forall;
eauto using switch_block_st_follows. }
eapply Forall3_Forall3 in Hf; [|
eapply H18].
clear H18.
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 apply in_app_iff in it as [|
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 H14 in Hin as (
Hin&?);
subst.
inv Hin;
econstructor;
solve_In.
2:{
apply Partition_Permutation in Hpart.
rewrite Hpart in H22.
rewrite in_app_iff in *.
destruct H22;
eauto;
right;
solve_In.
apply equiv_decb_refl. }
simpl;
eauto.
auto.
+
intros *
Hin.
apply H16,
Hnl2 in Hin as []. }
eapply switch_blocks_sem'
with (Γ
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 *
Hla.
eapply Hnl2.
inv Hla.
simpl_In.
eapply IsLast_incl;
eauto with senv.
-
intros ?
Hin.
apply Env.In_from_list in Hin.
rewrite fst_InMembers in Hin.
rewrite fst_InMembers.
erewrite map_map,
map_ext,
map_app, <-2
new_idents_old, <-
map_app,
Permutation_app_comm;
eauto.
erewrite map_map,
map_ext in Hin;
eauto.
intros ((?&?)&(?&?));
auto.
intros (?&?);
auto.
-
intros *
Hfind.
apply Env.from_list_find_In in Hfind.
simpl_In.
repeat (
take (
new_idents _ _ _ _ _ _ =
_)
and apply new_idents_prefixed in it).
apply in_app_iff in Hin as [|];
simpl_Forall;
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.
-
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.
-
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.
2:{
intros Hca.
exfalso.
inv Hca.
simpl_In.
apply Hincl1 in Hin.
eapply Hnl2;
econstructor;
eauto. }
intros 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.
-
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.
+
exfalso.
apply FEnv.union_In in Hin as [
Hin|
Hin]; [|
eapply Hdoml1;
eauto].
apply Hdomub1,
IsLast_app in Hin as [
Hin|
Hin]; [
eapply Hnl1;
eauto|].
clear -
Hin.
inv Hin.
simpl_In.
congruence.
+
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.
eapply sem_block_restrict;
eauto.
+
unfold wc_env.
simpl_Forall.
take (
In _ (
idck _))
and clear -
it.
simpl_In.
constructor.
+
apply when_hist_fwhen_hist in H19;
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 H4 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_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.
eapply switch_blocks_sem'
with (Γ
ty:=Γ
ty0);
eauto.
Transparent switch_scope.
Qed.