Lvc.Equiv.NPSimEquiv

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

Relationship of bisimulation to the parametric definition

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

Lemma simp_bisim {S} `{StateType S} {S'} `{StateType S'}
  : ∀ (σ:S) (σ':S'), Sim.sim bot3 Bisim σ σ' → bisim σ σ'.
Proof.
  cofix CIH; intros.
  assert (sim_gen ( (sim_gen (S:=S) (S':=S')) bot3) Bisim σ σ').
  punfold .
  inv ; pclearbot.
  - econstructor 1; eauto.
  - econstructor 2; eauto.
    + intros. edestruct ; eauto; dcr; pclearbot; eauto.
    + intros. edestruct ; eauto; dcr; pclearbot; eauto.
  - exfalso; eauto.
  - econstructor 3; eauto.
Qed.

Transitivity

Lemma bisim_trans {} `{StateType }
      (σ1:) {} `{StateType } (σ2:) {} `{StateType } (σ3:)
  : bisim σ1 σ2
    → bisim σ2 σ3
    → bisim σ1 σ3.
Proof.
  intros. eapply simp_bisim.
  eapply bisim_simp in .
  eapply bisim_simp in .
  eapply (Sim.sim_trans ).
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 ; pfold; eauto using sim_gen.
  - econstructor 2; eauto.
    + simpl. intros; exfalso; eauto.
    + intros. edestruct ; eauto; dcr; eauto 10.
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 ( (sim_gen (S:=S) (S':=S')) bot3) t σ σ').
  punfold .
  inversion ; pclearbot.
  - econstructor 1; eauto.
  - econstructor 2; eauto.
    + intros. edestruct ; eauto; dcr; pclearbot; eauto.
  - econstructor 4; eauto.
  - econstructor 3; eauto.
Qed.

Transitivity

Lemma sim_trans {} `{StateType }
      (σ1:) {} `{StateType } (σ2:) {} `{StateType } (σ3:)
  : sim σ1 σ2
    → sim σ2 σ3
    → sim σ1 σ3.
Proof.
  intros. eapply simp_sim.
  eapply sim_simp in .
  eapply sim_simp in .
  eapply (Sim.sim_trans ).
Qed.

Arguments sim_trans [] {H} σ1 [] {} σ2 [] {} σ3 _ _.