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

Set Implicit Arguments.

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.

Lemma bisim_refl {S} `{StateType S} (σ:S)
      : bisim σ σ.

Lemma bisim_sym {S} `{StateType S} {S´} `{StateType S´} (σ:S) (σ´:S´)
      : bisim σ σ´ → bisim σ´ σ.

Inductive bisim_gen
          {S} `{StateType S} {S´} `{StateType S´} (r: S → S´ → Prop) : S → S´ → Prop :=
  | bisim´Silent (σ1 σ1´:S) (σ2 σ2´:S´) :
      plus2 step σ1 nil σ1´
      → plus2 step σ2 nil σ2´
      → r σ1´ σ2´
      → bisim_gen r σ1 σ2
  | bisim´Extern (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´ ∧ r σ1´ σ2´)
      → (∀ evt σ2´, step σ2 evt σ2´ → ∃ σ1´, step σ1 evt σ1´ ∧ r σ1´ σ2´)
      → bisim_gen r pσ1 pσ2
  | bisim´Term (σ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_gen r σ1 σ2.


Hint Constructors bisim_gen.

Definition bisim´ {S} `{StateType S} {S´} `{StateType S´} (σ1:S) (σ2:S´)
  := paco2 (@bisim_gen S _ S´ _) bot2 σ1 σ2.
Hint Unfold bisim´.

Definition bisim´r {S} `{StateType S} {S´} `{StateType S´} r (σ1:S) (σ2:S´)
  := paco2 (@bisim_gen S _ S´ _) r σ1 σ2.
Hint Unfold bisim´.

Lemma bisim_gen_mon {S} `{StateType S} {S´} `{StateType S´}
: monotone2 (@bisim_gen S _ S´ _).


Hint Resolve bisim_gen_mon : paco.

Lemma bisim_bisim´ {S} `{StateType S} {S´} `{StateType S´} (σ1:S) (σ2:S´)
: bisim σ1 σ2 → bisim´ σ1 σ2.

Lemma bisim´_bisim {S} `{StateType S} {S´} `{StateType S´} (σ1:S) (σ2:S´)
: bisim´ σ1 σ2 → bisim σ1 σ2.

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

Lemma bisim´_sym {S} `{StateType S} {S´} `{StateType S´} (σ:S) (σ´:S´)
      : bisim´ σ σ´ → bisim´ σ´ σ.

Lemma bisim´_expansion_closed {S} `{StateType S}
      (σ1 σ1´:S) {S´} `{StateType S´} (σ2 σ2´:S´) r
  : bisim´r r σ1´ σ2´
    → star2 step σ1 nil σ1´
    → star2 step σ2 nil σ2´
    → bisim´r r σ1 σ2.

Lemma bisim´_reduction_closed_1 {S} `{StateType S}
      (σ1 σ1´:S) {S´} `{StateType S´} (σ2:S´)
  : bisim´ σ1 σ2
    → star2 step σ1 nil σ1´
    → bisim´ σ1´ σ2.

Lemma bisim´_terminate {S1} `{StateType S1} (σ1 σ1´:S1)
      {S2} `{StateType S2} (σ2:S2)
: star2 step σ1 nil σ1´
  → normal2 step σ1´
  → bisim´ σ1 σ2
  → ∃ σ2´, star2 step σ2 nil σ2´ ∧ normal2 step σ2´ ∧ result σ1´ = result σ2´.

Lemma bisim´_activated {S1} `{StateType S1} (σ1:S1)
      {S2} `{StateType S2} (σ2:S2)
: activated σ1
  → bisim´ σ1 σ2
  → ∃ σ2´, star2 step σ2 nil σ2´ ∧ activated σ2´ ∧
           ( ∀ (evt : event) (σ1´´ : S1),
               step σ1 evt σ1´´ →
               ∃ σ2´´ : S2,
                 step σ2´ evt σ2´´ ∧
                 (paco2 (bisim_gen (S´:=S2)) bot2 σ1´´ σ2´´))
           ∧
           ( ∀ (evt : event) (σ2´´ : S2),
               step σ2´ evt σ2´´ →
               ∃ σ1´ : S1,
                 step σ1 evt σ1´ ∧
                 (paco2 (bisim_gen (S´:=S2)) bot2 σ1´ σ2´´)).

Lemma plus_step_activated {S1} `{StateType S1} (σ1 σ1´:S1)
      {S2} `{StateType S2} (σ2a σ2´ σ2b σ4:S2)
      {S3} `{StateType S3} (σ3 σ5:S3) (r : S1 → S3 → Prop)
      (H6:plus2 step σ2a nil σ2´)
      (H2:star2 step σ2a nil σ2b)
      (H10:star2 step σ2b nil σ4)
      (H11 : star2 step σ3 nil σ5)
      (H4 : plus2 step σ1 nil σ1´)
      (H13 : activated σ5)
      (H12 : activated σ4)
      (H7 : paco2 (bisim_gen (S´:=S2)) bot2 σ1´ σ2´)
      (H14 : ∀ (evt : event) (σ1´ : S2),
               step σ4 evt σ1´ →
               ∃ σ2´ : S3,
          step σ5 evt σ2´ ∧
          (paco2 (bisim_gen (S´:=S3)) bot2 σ1´ σ2´ ∨ bot2 σ1´ σ2´))
      (H15 : ∀ (evt : event) (σ2´ : S3),
               step σ5 evt σ2´ →
               ∃ σ1´ : S2,
                 step σ4 evt σ1´ ∧
                 (paco2 (bisim_gen (S´:=S3)) bot2 σ1´ σ2´ ∨ bot2 σ1´ σ2´))
      (CIH : ∀ (σ1 : S1) (σ2a σ2b : S2) (σ3 : S3),
               bisim´ σ1 σ2a →
               star2 step σ2a nil σ2b ∨ star2 step σ2b nil σ2a →
               bisim´ σ2b σ3 → r σ1 σ3)
: paco2 (bisim_gen (S´:=S3)) r σ1 σ3.

Lemma bisim´_zigzag {S1} `{StateType S1}
      (σ1:S1) {S2} `{StateType S2} (σ2a σ2b:S2) {S3} `{StateType S3} (σ3:S3)
  : bisim´ σ1 σ2a
    → (star2 step σ2a nil σ2b ∨ star2 step σ2b nil σ2a)
    → bisim´ σ2b σ3
    → bisim´ σ1 σ3.
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.

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.

Lemma bisim´_reduction_closed {S} `{StateType S}
      (σ1 σ1´:S) {S´} `{StateType S´} (σ2 σ2´:S´)
  : bisim´ σ1 σ2
    → star2 step σ1 nil σ1´
    → star2 step σ2 nil σ2´
    → bisim´ σ1´ σ2´.

Instance bisim_progeq : ProgramEquivalence F.state F.state.
Defined.

Lemma simL_mon (r r0:rel2 F.state (fun _ : F.state ⇒ F.state)) A AR L1 L2 (AL:list A) L1´ L2´
: AIR5 (simB bisim_progeq r AR) L1 L2 AL L1´ L2´
  → (∀ x0 x1 : F.state, r x0 x1 → r0 x0 x1)
  → L1 = L1´
  → L2 = L2´
  → AIR5 (simB bisim_progeq r0 AR) L1 L2 AL L1´ L2´.

Lemma subst_lemma A AR (a:A) AL s s´ V V´ E E´ Z Z´ L1 L2 t t´
: fexteq´ bisim_progeq AR a (a::AL) E Z s E´ Z´ s´
  → ParamRel a Z Z´
  → BlockRel a (F.blockI E Z s) (F.blockI E´ Z´ s´)
  → simL´ bisim_progeq bot2 AR AL L1 L2
  → (∀ r (L L´ : list F.block),
       simL´ bisim_progeq r AR (a :: AL) L L´ →
       paco2 (@bisim_gen F.state _ F.state _) r (L, V, t) (L´, V´, t´))
  → paco2 (@bisim_gen F.state _ F.state _) bot2 (F.blockI E Z s :: L1, V, t)
         (F.blockI E´ Z´ s´ :: L2, V´, t´).

Lemma fix_compatible r A AR (a:A) AL s s´ E E´ Z Z´ L L´ Yv Y´v
: simL´ bisim_progeq r AR AL L L´
  → fexteq´ bisim_progeq AR a (a::AL) E Z s E´ Z´ s´
  → ParamRel a Z Z´
  → BlockRel a (F.blockI E Z s) (F.blockI E´ Z´ s´)
  → ArgRel E E´ a Yv Y´v
  → bisim´r r
            (F.blockI E Z s :: L, E [Z <-- List.map Some Yv], s)
            (F.blockI E´ Z´ s´ :: L´, E´ [Z´ <-- List.map Some Y´v], s´).

Lemma simL_extension´ r A AR (a:A) AL s s´ E E´ Z Z´ L L´
: simL´ bisim_progeq r AR AL L L´
  → fexteq´ bisim_progeq AR a (a::AL) E Z s E´ Z´ s´
  → BlockRel a (F.blockI E Z s) (F.blockI E´ Z´ s´)
  → simL´ bisim_progeq r AR (a::AL) (F.blockI E Z s :: L) (F.blockI E´ Z´ s´ :: L´).

Lemma get_drop_lab0 (L:F.labenv) l blk
: get L (counted l) blk
   → get (drop (labN l) L) (counted (LabI 0)) blk.

Lemma drop_get_lab0 (L:F.labenv) l blk
: get (drop (labN l) L) (counted (LabI 0)) blk
  → get L (counted l) blk.

Lemma bisim_drop_shift r l L E Y L´ E´ Y´
: paco2 (@bisim_gen F.state _ F.state _) r (drop (labN l) L, E, stmtApp (LabI 0) Y)
        (drop (labN l) L´, E´, stmtApp (LabI 0) Y´)
  → paco2 (@bisim_gen F.state _ F.state _) r (L, E, stmtApp l Y)
          (L´, E´, stmtApp l Y´).

Ltac single_step :=
  match goal with
    | [ H : agree_on _ ?E ?E´, I : val2bool (?E ?x) = true |- step (_, ?E´, stmtIf ?x _ _) _ ] ⇒
      econstructor; eauto; rewrite <- H; eauto; cset_tac; intuition
    | [ H : agree_on _ ?E ?E´, I : val2bool (?E ?x) = false |- step (_, ?E´, stmtIf ?x _ _) _ ] ⇒
      econstructor 3; eauto; rewrite <- H; eauto; cset_tac; intuition
    | [ H : val2bool _ = false |- _ ] ⇒ econstructor 3 ; try eassumption; try reflexivity
    | [ H : step (?L, _ , stmtApp ?l _) _, H´: get ?L (counted ?l) _ |- _] ⇒
      econstructor; try eapply H´; eauto
    | [ H´: get ?L (counted ?l) _ |- step (?L, _ , stmtApp ?l _) _] ⇒
      econstructor; try eapply H´; eauto
    | _ ⇒ econstructor; eauto
  end.

Ltac one_step := eapply bisimSilent; [ eapply plus2O; single_step
                              | eapply plus2O; single_step
                              | ].

Ltac no_step := eapply bisimTerm;
               try eapply star2_refl; try get_functional; try subst;
                [ try reflexivity
                | stuck2
                | stuck2 ].

Ltac step_activated :=
  match goal with
    | [ H : omap (exp_eval ?E) ?Y = Some ?vl
        |- activated (_, ?E, stmtExtern ?x ?f ?Y ?s) ] ⇒
      eexists (ExternI f vl 0); eexists; try (now (econstructor; eauto))
  end.

Ltac extern_step :=
  let STEP := fresh "STEP" in
  eapply bisimExtern;
    [ eapply star2_refl
    | eapply star2_refl
    | try step_activated
    | try step_activated
    | intros ? ? STEP; inv STEP
    | intros ? ? STEP; inv STEP
    ].

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´) σ´´.


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


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.