# Lvc.Equiv.NonParametricBiSim

Require Import List paco2.
Require Import Util IL.
Require Export SmallStepRelations StateType Sim.

Set Implicit Arguments.
Unset Printing Records.

# Non-parametric Definitions of Simulation and Bisimulation

## Bisimulation

A characterization of bisimulation equivalence on states; works only for internally deterministic semantics.

CoInductive bisim {S} `{StateType S} {S'} `{StateType S'} : S S' Prop :=
| BisimSilent (σ1 σ1':S) (σ2 σ2':S') :
plus2 step σ1 nil σ1'
plus2 step σ2 nil σ2'
bisim σ1' σ2'
bisim σ1 σ2
| BisimExtern (pσ1 σ1:S) (pσ2 σ2:S') :
star2 step pσ1 nil σ1
star2 step pσ2 nil σ2
activated σ1
activated σ2
( evt σ1', step σ1 evt σ1' σ2', step σ2 evt σ2' bisim σ1' σ2')
( evt σ2', step σ2 evt σ2' σ1', step σ1 evt σ1' bisim σ1' σ2')
bisim pσ1 pσ2
| BisimTerm (σ1 σ1':S) (σ2 σ2':S')
: result σ1' = result σ2'
star2 step σ1 nil σ1'
star2 step σ2 nil σ2'
normal2 step σ1'
normal2 step σ2'
bisim σ1 σ2.

Arguments bisim [S] {H} [S'] {H0} _ _.

### Bisimulation is an reflexive and symmetric

Lemma bisim_refl {S} `{StateType S} (σ:S)
: bisim σ σ.
Proof.
revert σ. cofix.
intros. destruct (step_dec σ) as [[[] []]|].
- eapply BisimExtern; intros; eauto using star2_refl; eexists; eauto.
- eapply BisimSilent; eauto using plus2O.
- eapply BisimTerm; eauto using star2_refl.
Qed.

Lemma bisim_sym {S} `{StateType S} {S'} `{StateType S'} (σ:S) (σ':S')
: bisim σ σ' bisim σ' σ.
Proof.
revert σ σ'. cofix; intros.
inv H1.
- eapply BisimSilent; eauto.
- eapply BisimExtern; eauto; intros.
edestruct H7; eauto; dcr. eexists; eauto.
edestruct H6; eauto; dcr. eexists; eauto.
- eapply BisimTerm; eauto using star2_refl.
Qed.

## Relationship of bisimulation to the parametric definition

Lemma bisim_simp t {S} `{StateType S} {S'} `{StateType S'}
: (σ:S) (σ':S'), bisim σ σ' sim bot3 t σ σ'.
Proof.
pcofix CIH; intros. invt bisim; pfold; eauto using sim_gen.
- econstructor 2; eauto.
+ intros. edestruct H6; eauto; dcr; eauto.
+ intros. edestruct H7; eauto; dcr; eauto.
Qed.

Lemma simp_bisim {S} `{StateType S} {S'} `{StateType S'}
: (σ:S) (σ':S'), sim bot3 Bisim σ σ' bisim σ σ'.
Proof.
cofix CIH; intros.
assert (sim_gen (paco3 (sim_gen (S:=S) (S':=S')) bot3 \3/ bot3) Bisim σ σ').
punfold H1.
inv H2; pclearbot.
- econstructor 1; eauto.
- econstructor 2; eauto.
+ intros. edestruct H7; eauto; dcr; pclearbot; eauto.
+ intros. edestruct H8; eauto; dcr; pclearbot; eauto.
- econstructor 3; eauto.
Qed.

### Transitivity

Lemma bisim_trans {S1} `{StateType S1}
(σ1:S1) {S2} `{StateType S2} (σ2:S2) {S3} `{StateType S3} (σ3:S3)
: bisim σ1 σ2
bisim σ2 σ3
bisim σ1 σ3.
Proof.
intros. eapply simp_bisim.
eapply bisim_simp in H2.
eapply bisim_simp in H3.
eapply (Sim.sim_trans H2 H3).
Qed.

## Simulation

CoInductive sim {S} `{StateType S} {S'} `{StateType S'} : S S' Prop :=
| SimSilent (σ1 σ1':S) (σ2 σ2':S') :
plus2 step σ1 nil σ1'
plus2 step σ2 nil σ2'
sim σ1' σ2'
sim σ1 σ2
| SimExtern (pσ1 σ1:S) (pσ2 σ2:S') :
star2 step pσ1 nil σ1
star2 step pσ2 nil σ2
activated σ1
activated σ2
( evt σ1', step σ1 evt σ1' σ2', step σ2 evt σ2' sim σ1' σ2')
( evt σ2', step σ2 evt σ2' σ1', step σ1 evt σ1' sim σ1' σ2')
sim pσ1 pσ2
| SimTerm (σ1 σ1':S) (σ2 σ2':S')
: result σ1' = result σ2'
star2 step σ1 nil σ1'
star2 step σ2 nil σ2'
normal2 step σ1'
normal2 step σ2'
sim σ1 σ2
| SimErr (σ1 σ1':S) (σ2:S')
: result σ1' = None
star2 step σ1 nil σ1'
normal2 step σ1'
sim σ1 σ2.

Arguments bisim [S] {H} [S'] {H0} _ _.

### Simulation is an reflexive

Lemma sim_refl {S} `{StateType S} (σ:S)
: sim σ σ.
Proof.
revert σ. cofix.
intros. destruct (step_dec σ) as [[[] []]|].
- eapply SimExtern; intros; eauto using star2_refl; eexists; eauto.
- eapply SimSilent; eauto using plus2O.
- eapply SimTerm; eauto using star2_refl.
Qed.

## Relationship of simulation to the parametric definition

Lemma sim_simp {S} `{StateType S} {S'} `{StateType S'}
: (σ:S) (σ':S'), sim σ σ' Sim.sim bot3 Sim σ σ'.
Proof.
pcofix CIH; intros. inv H2; pfold; eauto using sim_gen.
- econstructor 2; eauto.
+ intros. edestruct H6; eauto; dcr; eauto.
+ intros. edestruct H7; eauto; dcr; eauto.
Qed.

Lemma simp_sim t {S} `{StateType S} {S'} `{StateType S'}
: (σ:S) (σ':S'), Sim.sim bot3 t σ σ' sim σ σ'.
Proof.
cofix CIH; intros.
assert (sim_gen (paco3 (sim_gen (S:=S) (S':=S')) bot3 \3/ bot3) t σ σ').
punfold H1.
inversion H2; pclearbot.
- econstructor 1; eauto.
- econstructor 2; eauto.
+ intros. edestruct H7; eauto; dcr; pclearbot; eauto.
+ intros. edestruct H8; eauto; dcr; pclearbot; eauto.
- econstructor 4; eauto.
- econstructor 3; eauto.
Qed.

### Transitivity

Lemma sim_trans {S1} `{StateType S1}
(σ1:S1) {S2} `{StateType S2} (σ2:S2) {S3} `{StateType S3} (σ3:S3)
: sim σ1 σ2
sim σ2 σ3
sim σ1 σ3.
Proof.
intros. eapply simp_sim.
eapply sim_simp in H2.
eapply sim_simp in H3.
eapply (Sim.sim_trans H2 H3).
Qed.

Arguments sim_trans [S1] {H} σ1 [S2] {H0} σ2 [S3] {H1} σ3 _ _.

Receptive and determinate according to CompCertTSO (Sevcík 2013)

Definition same_call (e e':extern) := extern_fnc e = extern_fnc e' extern_args e = extern_args e'.

Definition receptive S `{StateType S} :=
σ σ' ext, step σ (EvtExtern ext) σ'
ext', same_call ext ext' σ'', step σ (EvtExtern ext') σ''.

Arguments receptive S [H].

Definition determinate S `{StateType S} :=
σ σ' σ'' ext ext', step σ (EvtExtern ext) σ'
step σ (EvtExtern ext') σ'' same_call ext ext'.

Arguments determinate S [H].

Lemma bisimExternDet {S} `{StateType S} {S'} `{StateType S'} (pσ1:S) (pσ2:S') (σ1:S) (σ2:S')
(RCPT:receptive S) (DET:determinate S')
: star2 step pσ1 nil σ1
star2 step pσ2 nil σ2
activated σ1
( evt σ1', step σ1 evt σ1' σ2', step σ2 evt σ2' bisim σ1' σ2')
bisim pσ1 pσ2.
Proof.
intros.
econstructor 2; eauto.
- inv H3. dcr. edestruct H4; eauto. firstorder.
- intros. inv H3. dcr. exploit H4; eauto; dcr.
destruct evt.
+ exploit DET. eauto. eapply H5.
exploit RCPT; eauto. dcr.
exploit H4. eapply H11. dcr.
eexists; split. eapply H11.
exploit step_externally_determined. Focus 3.
instantiate (2:=σ2') in H8. rewrite H8. eapply H14.
eauto. eauto.
+ exfalso. exploit step_internally_deterministic; eauto; dcr. congruence.
Qed.