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} : S → Prop :=
| 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} S´ `{StateType S´} (σ:S) (σ´:S´)
: bisim σ σ´ → diverges σ → diverges σ´.

Lemma bisim_complete_diverges S `{StateType S} S´ `{StateType S´} (σ:S) (σ´: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} : S → list extevent → Prop :=
  | 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 σ´ L → prefix σ L.

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

Bisimilarity is sound for prefix inclusion

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

Lemma bisim_prefix {S} `{StateType S} {S´} `{StateType S´} (sigma:S) (σ´: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 σ L → L = 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} S´ `{StateType S´} (σ:S)
: diverges σ → (∀ L, prefix σ L → L = nil).

Prefix Equivalence is sound for divergence

Lemma produces_diverges S `{StateType S} S´ `{StateType S´} (σ:S) (σ´: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} S´ `{StateType S´} (σ1 σ1´ σ1´´:S) (σ2 σ2´ σ2´´:S´) 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 prefix_preserved S `{StateType S} S´ `{StateType S´} (σ1 σ1´ σ1´´:S) (σ2 σ2´ σ2´´:S´) 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} S´ `{StateType S´} (σ1 σ1´:S) (σ2 σ2´:S´)
: 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 : A → stream A → stream A.

CoInductive coproduces {S} `{StateType S} : S → stream extevent → Prop :=
| 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

Lemma coproduces_reduction_closed_step S `{StateType S} (σ σ´:S) L
: coproduces σ L → step σ EvtTau σ´ → coproduces σ´ L.

Lemma coproduces_reduction_closed S `{StateType S} (σ σ´:S) L
: coproduces σ L → star2 step σ nil σ´ → coproduces σ´ L.

Bisimilarity is sound for maximal traces

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

Prefix trace equivalence coincides with maximal trace equivalence.

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

Lemma produces_coproduces S `{StateType S} S´ `{StateType S´} (σ:S) (σ´: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} S´ `{StateType S´} (σ:S) (σ´:S´)
: (∀ L, prefix σ L ↔ prefix σ´ L)
  → bisim σ σ´.