Lvc.Equiv.TraceEquiv

Require Import List.
Require Export Util Var Val Exp Env Map CSet AutoIndTac IL AllInRel.
Require Export EventsActivated StateType paco Equiv Bisim Sim.

Set Implicit Arguments.

Divergence


CoInductive diverges S `{StateType S} : SProp :=
| DivergesI σ σ´
  : step σ EvtTau σ´
    → diverges σ´
    → diverges σ.

Lemma diverges_reduction_closed S `{StateType S} (σ σ´:S)
: diverges σstar2 step σ nil σ´diverges σ´.

Lemma diverges_never_activated S `{StateType S} (σ:S)
: activated σdiverges σFalse.

Lemma diverges_never_terminates S `{StateType S} (σ:S)
: normal2 step σdiverges σFalse.

Lemma bisim_sound_diverges S `{StateType S} `{StateType } (σ:S) (σ´:)
: bisim σ σ´diverges σdiverges σ´.

Lemma bisim_complete_diverges S `{StateType S} `{StateType } (σ:S) (σ´:)
: diverges σdiverges σ´bisim σ σ´.

Three equivalent notions of program equivalence

Prefix Trace Equivalence (partial traces)

A prefix is a list of extevent

Inductive extevent :=
  | EEvtExtern (evt:event)
  | EEvtTerminate (res:option val).

A relation that assigns prefixes to states

Inductive prefix {S} `{StateType S} : Slist exteventProp :=
  | producesPrefixSilent (σ:S) (σ´:S) L :
      step σ EvtTau σ´
      → prefix σ´ L
      → prefix σ L
  | producesPrefixExtern (σ:S) (σ´:S) evt L :
      activated σ
      → step σ evt σ´
      → prefix σ´ L
      → prefix σ (EEvtExtern evt::L)
  | producesPrefixTerm (σ:S) (σ´:S) r
    : result σ´ = r
      → star2 step σ nil σ´
      → normal2 step σ´
      → prefix σ (EEvtTerminate r::nil)
  | producesPrefixPrefix (σ:S)
    : prefix σ nil.

Closedness under silent reduction/expansion


Lemma prefix_star2_silent {S} `{StateType S} (σ σ´:S) L
 : star2 step σ nil σ´
   prefix σ´ Lprefix σ L.

Lemma prefix_star2_silent´ {S} `{StateType S} (σ σ´:S) L
 : star2 step σ nil σ´
   prefix σ Lprefix σ´ L.

Bisimilarity is sound for prefix inclusion


Lemma bisim_prefix´ {S} `{StateType S} {} `{StateType } (sigma:S) (σ´:)
: bisim sigma σ´ L, prefix sigma Lprefix σ´ L.

Lemma bisim_prefix {S} `{StateType S} {} `{StateType } (sigma:S) (σ´:)
  : bisim sigma σ´ L, prefix sigma L prefix σ´ L.

The only prefix is empty if and only if the state diverges


Lemma produces_only_nil_diverges S `{StateType S} (σ:S)
: ( L, prefix σ LL = nil) → diverges σ.

Lemma prefix_extevent S `{StateType S} (σ:S) evt L
: prefix σ (EEvtExtern evt::L)
  → σ´, star2 step σ nil σ´
           activated σ´
           σ´´, step σ´ evt σ´´ prefix σ´´ L.

Lemma prefix_terminates S `{StateType S} (σ:S) r L
: prefix σ (EEvtTerminate r::L)
   → σ´, star2 step σ nil σ´ normal2 step σ´ result σ´ = r L = nil.

Lemma diverges_produces_only_nil S `{StateType S} `{StateType } (σ:S)
: diverges σ → ( L, prefix σ LL = nil).

Prefix Equivalence is sound for divergence


Lemma produces_diverges S `{StateType S} `{StateType } (σ:S) (σ´:)
: ( L, prefix σ L prefix σ´ L)
  → diverges σdiverges σ´.

Several closedness properties


Lemma prefix_star_activated S `{StateType S} (σ1 σ1´ σ1´´:S) evt L
: star2 step σ1 nil σ1´
  → activated σ1´
  → step σ1´ evt σ1´´
  → prefix σ1´´ L
  → prefix σ1 (EEvtExtern evt::L).

Lemma prefix_preserved´ S `{StateType S} `{StateType } (σ1 σ1´ σ1´´:S) (σ2 σ2´ σ2´´:) evt
: ( L : list extevent, prefix σ1 L prefix σ2 L)
  → star2 step σ1 nil σ1´
  → activated σ1´
  → step σ1´ evt σ1´´
  → star2 step σ2 nil σ2´
  → activated σ2´
  → step σ2´ evt σ2´´
  → L, prefix σ1´´ Lprefix σ2´´ L.

Lemma prefix_preserved S `{StateType S} `{StateType } (σ1 σ1´ σ1´´:S) (σ2 σ2´ σ2´´:) evt
:
  ( L : list extevent, prefix σ1 L prefix σ2 L)
  → star2 step σ1 nil σ1´
  → activated σ1´
  → step σ1´ evt σ1´´
  → star2 step σ2 nil σ2´
  → activated σ2´
  → step σ2´ evt σ2´´
  → L, prefix σ1´´ L prefix σ2´´ L.

Lemma produces_silent_closed {S} `{StateType S} `{StateType } (σ1 σ1´:S) (σ2 σ2´:)
: star2 step σ1 nil σ1´
  → star2 step σ2 nil σ2´
  → ( L, prefix σ1 L prefix σ2 L)
  → ( L, prefix σ1´ L prefix σ2´ L).

Trace Equivalence (maximal traces)


CoInductive stream (A : Type) : Type :=
| sil : stream A
| sons : Astream Astream A.


CoInductive coproduces {S} `{StateType S} : Sstream exteventProp :=
| CoProducesExtern (σ σ´ σ´´:S) evt L :
    star2 step σ nil σ´
      → activated σ´
      → step σ´ evt σ´´
      → coproduces σ´´ L
      → coproduces σ (sons (EEvtExtern evt) L)
| CoProducesSilent (σ:S) :
    diverges σ
    → coproduces σ sil
| CoProducesTerm (σ:S) (σ´:S) r
  : result σ´ = r
    → star2 step σ nil σ´
    → normal2 step σ´
    → coproduces σ (sons (EEvtTerminate r) sil).

Several closedness properties

Bisimilarity is sound for maximal traces


Lemma bisim_coproduces S `{StateType S} `{StateType } (sigma:S) (σ´:)
  : bisim sigma σ´ L, coproduces sigma Lcoproduces σ´ L.

Prefix trace equivalence coincides with maximal trace equivalence.


Lemma produces_coproduces´ S `{StateType S} `{StateType } (σ:S) (σ´:)
: ( L, prefix σ L prefix σ´ L)
  → ( T, coproduces σ Tcoproduces σ´ T).

Lemma produces_coproduces S `{StateType S} `{StateType } (σ:S) (σ´:)
: ( L, prefix σ L prefix σ´ L)
  → ( T, coproduces σ T coproduces σ´ T).

Bisimilarity is complete for prefix trace equivalence.


Require Import Classical_Prop.

Lemma three_possibilities S `{StateType S} (σ:S)
: ( σ´, star2 step σ nil σ´ normal2 step σ´)
   ( σ´, star2 step σ nil σ´ activated σ´)
   diverges σ.

Lemma prefix_bisim S `{StateType S} `{StateType } (σ:S) (σ´:)
: ( L, prefix σ L prefix σ´ L)
  → bisim σ σ´.