Require Import Relations.
Require Import Wellfounded.
Require Import Coqlib.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Lia.
Local Open Scope nat_scope.
Auxiliary lemma on starN
Section starN_lemma.
Variable L:
semantics.
Local Hint Resolve starN_refl starN_step Eapp_assoc:
core.
Lemma starN_split n s t s':
starN (
step L) (
globalenv L)
n s t s' ->
forall m k,
n=
m+
k ->
exists (
t1 t2:
trace)
s0,
starN (
step L) (
globalenv L)
m s t1 s0 /\
starN (
step L) (
globalenv L)
k s0 t2 s' /\
t=
t1**
t2.
Proof.
induction 1;
cbn.
+
intros m k H;
assert (
X:
m=0);
try lia.
assert (
X0:
k=0);
try lia.
subst;
repeat (
eapply ex_intro);
intuition eauto.
+
intros m;
destruct m as [|
m'];
cbn.
-
intros k H2;
subst;
repeat (
eapply ex_intro);
intuition eauto.
-
intros k H2.
inversion H2.
exploit (
IHstarN m' k);
eauto.
intro.
destruct H3 as (
t5 &
t6 &
s0 &
H5 &
H6 &
H7).
repeat (
eapply ex_intro).
instantiate (1 :=
t6);
instantiate (1 :=
t1 **
t5);
instantiate (1 :=
s0).
intuition eauto.
subst.
auto.
Qed.
Lemma starN_tailstep n s t1 s':
starN (
step L) (
globalenv L)
n s t1 s' ->
forall (
t t2:
trace)
s'',
Step L s' t2 s'' ->
t =
t1 **
t2 ->
starN (
step L) (
globalenv L) (
S n)
s t s''.
Proof.
induction 1;
cbn.
+
intros t t1 s0;
autorewrite with trace_rewrite.
intros;
subst;
eapply starN_step;
eauto.
autorewrite with trace_rewrite;
auto.
+
intros.
eapply starN_step;
eauto.
intros;
subst;
autorewrite with trace_rewrite;
auto.
Qed.
End starN_lemma.
General scheme from a "match_states" relation
Section ForwardSimuBlock_REL.
Variable L1 L2:
semantics.
Hypothèses de la preuve
Variable dist_end_block:
state L1 ->
nat.
Hypothesis simu_mid_block:
forall s1 t s1',
Step L1 s1 t s1' -> (
dist_end_block s1)<>0 ->
t =
E0 /\
dist_end_block s1=
S (
dist_end_block s1').
Hypothesis public_preserved:
forall id,
Senv.public_symbol (
symbolenv L2)
id =
Senv.public_symbol (
symbolenv L1)
id.
Variable match_states:
state L1 ->
state L2 ->
Prop.
Hypothesis match_initial_states:
forall s1,
initial_state L1 s1 ->
exists s2,
match_states s1 s2 /\
initial_state L2 s2.
Hypothesis match_final_states:
forall s1 s2 r,
final_state L1 s1 r ->
match_states s1 s2 ->
final_state L2 s2 r.
Hypothesis final_states_end_block:
forall s1 t s1' r,
Step L1 s1 t s1' ->
final_state L1 s1' r ->
dist_end_block s1 = 0.
Hypothesis simu_end_block:
forall s1 t s1' s2,
starN (
step L1) (
globalenv L1) (
S (
dist_end_block s1))
s1 t s1' ->
match_states s1 s2 ->
exists s2',
Step L2 s2 t s2' /\
match_states s1' s2'.
Introduction d'une sémantique par bloc sur L1 appelée "memoL1"
Local Hint Resolve starN_refl starN_step:
core.
Definition follows_in_block (
head current:
state L1):
Prop :=
dist_end_block head >=
dist_end_block current
/\
starN (
step L1) (
globalenv L1) (
minus (
dist_end_block head) (
dist_end_block current))
head E0 current.
Lemma follows_in_block_step (
head previous next:
state L1):
forall t,
follows_in_block head previous ->
Step L1 previous t next -> (
dist_end_block previous)<>0 ->
follows_in_block head next.
Proof.
Lemma follows_in_block_init (
head current:
state L1):
forall t,
Step L1 head t current -> (
dist_end_block head)<>0 ->
follows_in_block head current.
Proof.
Record memostate := {
real:
state L1;
memorized:
option (
state L1);
memo_star:
forall head,
memorized =
Some head ->
follows_in_block head real;
memo_final:
forall r,
final_state L1 real r ->
memorized =
None
}.
Definition head (
s:
memostate):
state L1 :=
match memorized s with
|
None =>
real s
|
Some s' =>
s'
end.
Lemma head_followed (
s:
memostate):
follows_in_block (
head s) (
real s).
Proof.
Inductive is_well_memorized (
s s':
memostate):
Prop :=
|
StartBloc:
dist_end_block (
real s) <>
O ->
memorized s =
None ->
memorized s' =
Some (
real s) ->
is_well_memorized s s'
|
MidBloc:
dist_end_block (
real s) <>
O ->
memorized s <>
None ->
memorized s' =
memorized s ->
is_well_memorized s s'
|
ExitBloc:
dist_end_block (
real s) =
O ->
memorized s' =
None ->
is_well_memorized s s'.
Local Hint Resolve StartBloc MidBloc ExitBloc:
core.
Definition memoL1 := {|
state :=
memostate;
genvtype :=
genvtype L1;
step :=
fun ge s t s' =>
step L1 ge (
real s)
t (
real s')
/\
is_well_memorized s s' ;
initial_state :=
fun s =>
initial_state L1 (
real s) /\
memorized s =
None;
final_state :=
fun s r =>
final_state L1 (
real s)
r;
globalenv:=
globalenv L1;
symbolenv:=
symbolenv L1
|}.
Preuve des 2 forward simulations: L1 -> memoL1 et memoL1 -> L2
Lemma discr_dist_end s:
{
dist_end_block s =
O} + {
dist_end_block s <>
O}.
Proof.
Lemma memo_simulation_step:
forall s1 t s1',
Step L1 s1 t s1' ->
forall s2,
s1 = (
real s2) ->
exists s2',
Step memoL1 s2 t s2' /\
s1' = (
real s2').
Proof.
Lemma forward_memo_simulation_1:
forward_simulation L1 memoL1.
Proof.
Lemma forward_memo_simulation_2:
forward_simulation memoL1 L2.
Proof.
Lemma forward_simulation_block_rel:
forward_simulation L1 L2.
Proof.
End ForwardSimuBlock_REL.
Section ForwardSimuBlock_TRANS.
Variable L1 L2:
semantics.
Variable trans_state:
state L1 ->
state L2.
Definition equiv_on_next_step (
P Q:
Prop)
s2_a s2_b:
Prop :=
(
P -> (
forall t s',
Step L2 s2_a t s' <->
Step L2 s2_b t s')) /\ (
Q -> (
forall r, (
final_state L2 s2_a r) <-> (
final_state L2 s2_b r))).
Definition match_states s1 s2:
Prop :=
equiv_on_next_step (
exists t s1',
Step L1 s1 t s1') (
exists r,
final_state L1 s1 r)
s2 (
trans_state s1).
Lemma match_states_trans_state s1:
match_states s1 (
trans_state s1).
Proof.
Variable dist_end_block:
state L1 ->
nat.
Hypothesis simu_mid_block:
forall s1 t s1',
Step L1 s1 t s1' -> (
dist_end_block s1)<>0 ->
t =
E0 /\
dist_end_block s1=
S (
dist_end_block s1').
Hypothesis public_preserved:
forall id,
Senv.public_symbol (
symbolenv L2)
id =
Senv.public_symbol (
symbolenv L1)
id.
Hypothesis match_initial_states:
forall s1,
initial_state L1 s1 ->
exists s2,
match_states s1 s2 /\
initial_state L2 s2.
Hypothesis match_final_states:
forall s1 r,
final_state L1 s1 r ->
final_state L2 (
trans_state s1)
r.
Hypothesis final_states_end_block:
forall s1 t s1' r,
Step L1 s1 t s1' ->
final_state L1 s1' r ->
dist_end_block s1 = 0.
Hypothesis simu_end_block:
forall s1 t s1',
starN (
step L1) (
globalenv L1) (
S (
dist_end_block s1))
s1 t s1' ->
exists s2',
Step L2 (
trans_state s1)
t s2' /\
match_states s1' s2'.
Lemma forward_simulation_block_trans:
forward_simulation L1 L2.
Proof.
End ForwardSimuBlock_TRANS.
Section ForwardSimuBlock_TRANS_R.
Variable L1 L2:
semantics.
Variable trans_state_R:
state L1 ->
state L2 ->
Prop.
Definition match_states_R s1 s2:
Prop :=
exists s2',
trans_state_R s1 s2' /\
equiv_on_next_step _ (
exists t s1',
Step L1 s1 t s1') (
exists r,
final_state L1 s1 r)
s2 s2'.
Lemma match_states_trans_state_R s1 s2:
trans_state_R s1 s2 ->
match_states_R s1 s2.
Proof.
Variable dist_end_block:
state L1 ->
nat.
Hypothesis simu_mid_block:
forall s1 t s1',
Step L1 s1 t s1' -> (
dist_end_block s1)<>0 ->
t =
E0 /\
dist_end_block s1=
S (
dist_end_block s1').
Hypothesis public_preserved:
forall id,
Senv.public_symbol (
symbolenv L2)
id =
Senv.public_symbol (
symbolenv L1)
id.
Hypothesis match_initial_states:
forall s1,
initial_state L1 s1 ->
exists s2,
match_states_R s1 s2 /\
initial_state L2 s2.
Hypothesis match_final_states:
forall s1 s2 r,
final_state L1 s1 r ->
trans_state_R s1 s2 ->
final_state L2 s2 r.
Hypothesis final_states_end_block:
forall s1 t s1' r,
Step L1 s1 t s1' ->
final_state L1 s1' r ->
dist_end_block s1 = 0.
Hypothesis simu_end_block:
forall s1 t s1' s2,
starN (
step L1) (
globalenv L1) (
S (
dist_end_block s1))
s1 t s1' ->
trans_state_R s1 s2 ->
exists s2',
Step L2 s2 t s2' /\
match_states_R s1' s2'.
Lemma forward_simulation_block_trans_R:
forward_simulation L1 L2.
Proof.
eapply forward_simulation_block_rel with (
dist_end_block:=
dist_end_block) (
match_states:=
match_states_R);
try tauto.
+
intros s1 s2 r H1 (
s2' &
H2 &
H3 &
H4).
rewrite H4;
eauto.
+
intros s1 t s1' s2 H1 (
s2' &
H2 &
H2a &
H2b).
exploit simu_end_block;
eauto.
intros (
x &
Hx & (
y &
H3 &
H4 &
H5)).
repeat (
econstructor;
eauto).
rewrite H2a;
eauto.
inversion_clear H1.
eauto.
Qed.
End ForwardSimuBlock_TRANS_R.