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 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
  | simErr (σ1 σ1´:S) (σ2:S´)
    : result σ1´ = None
      → star2 step σ1 nil σ1´
      → normal2 step σ1´
      → sim σ1 σ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.

Lemma sim_refl {S} `{StateType S} (σ:S)
      : sim σ σ.

Inductive sim_gen
          {S} `{StateType S} {S´} `{StateType S´} (r: S → S´ → Prop) : S → S´ → Prop :=
  | sim´Silent (σ1 σ1´:S) (σ2 σ2´:S´) :
      plus2 step σ1 nil σ1´
      → plus2 step σ2 nil σ2´
      → r σ1´ σ2´
      → sim_gen r σ1 σ2
  | sim´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´)
      → sim_gen r pσ1 pσ2
  | sim´Err (σ1 σ1´:S) (σ2:S´)
    : result σ1´ = None
      → star2 step σ1 nil σ1´
      → normal2 step σ1´
      → sim_gen r σ1 σ2
  | sim´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´
      → sim_gen r σ1 σ2.


Hint Constructors sim_gen.

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

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

Lemma sim_gen_mon {S} `{StateType S} {S´} `{StateType S´}
: monotone2 (@sim_gen S _ S´ _).


Hint Resolve sim_gen_mon : paco.

Lemma sim_sim´ {S} `{StateType S} {S´} `{StateType S´} (σ1:S) (σ2:S´)
: sim σ1 σ2 → sim´ σ1 σ2.

Lemma sim´_sim {S} `{StateType S} {S´} `{StateType S´} (σ1:S) (σ2:S´)
: sim´ σ1 σ2 → sim σ1 σ2.

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

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

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

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

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

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

Lemma sim´_activated {S1} `{StateType S1} (σ1:S1)
      {S2} `{StateType S2} (σ2:S2)
: activated σ1
  → sim´ σ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 (sim_gen (S´:=S2)) bot2 σ1´´ σ2´´))
           ∧
           ( ∀ (evt : event) (σ2´´ : S2),
               step σ2´ evt σ2´´ →
               ∃ σ1´ : S1,
                 step σ1 evt σ1´ ∧
                 (paco2 (sim_gen (S´:=S2)) bot2 σ1´ σ2´´)).

Lemma sim´_activated_2 {S1} `{StateType S1} (σ1:S1)
      {S2} `{StateType S2} (σ2:S2)
: activated σ1
  → sim´ σ2 σ1
  → ∃ σ2´, star2 step σ2 nil σ2´ ∧
           (activated σ2´ ∧
           ( ∀ (evt : event) (σ1´´ : S1),
               step σ1 evt σ1´´ →
               ∃ σ2´´ : S2,
                 step σ2´ evt σ2´´ ∧
                 (paco2 (sim_gen (S´:=S1)) bot2 σ2´´ σ1´´))
           ∧
           ( ∀ (evt : event) (σ2´´ : S2),
               step σ2´ evt σ2´´ →
               ∃ σ1´ : S1,
                 step σ1 evt σ1´ ∧
                 (paco2 (sim_gen (S´:=S1)) bot2 σ2´´ σ1´))
           ∨ (normal2 step σ2´ ∧ result σ2´ = None)).

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

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.

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

Module I.

Class SimRelation (A:Type) := {
    ParamRel : A→ list var → list var → Prop;
    ArgRel : onv val → onv val → A→ list val → list val → Prop;
    BlockRel : A→ I.block → I.block → Prop;
    RelsOK : ∀ E E´ a Z Z´ VL VL´, ParamRel a Z Z´ → ArgRel E E´ a VL VL´ → length Z = length VL ∧ length Z´ = length VL´
}.

Inductive simB (r:rel2 I.state (fun _ : I.state ⇒ I.state)) {A} (AR:SimRelation A) : I.labenv → I.labenv → A → I.block → I.block → Prop :=
| simBI a L L´ Z Z´ s s´
  : ParamRel a Z Z´
    → BlockRel a (I.blockI Z s) (I.blockI Z´ s´)
    → (∀ E E´ Y Y´ Yv Y´v,
         omap (exp_eval E) Y = Some Yv
         → omap (exp_eval E´) Y´ = Some Y´v
         → ArgRel E E´ a Yv Y´v
         → paco2 (@sim_gen I.state _ I.state _) r (L, E, stmtApp (LabI 0) Y)
                        (L´, E´, stmtApp (LabI 0) Y´))
    → simB r AR L L´ a (I.blockI Z s) (I.blockI Z´ s´).

Definition simL´ (r:rel2 I.state (fun _ : I.state ⇒ I.state))
           {A} AR (AL:list A) L L´ := AIR5 (simB r AR) L L´ AL L L´.

Definition fexteq´
           {A} AR (a:A) (AL:list A) Z s Z´ s´ :=
  ∀ E E´ VL VL´ L L´ (r:rel2 I.state (fun _ : I.state ⇒ I.state)),
    ArgRel E E´ a VL VL´
    → simL´ r AR AL L L´
    → ParamRel a Z Z´
    → paco2 (@sim_gen I.state _ I.state _) r (L, E[Z <-- List.map Some VL], s)
            (L´, E´[Z´ <-- List.map Some VL´], s´).

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

Lemma subst_lemma A AR (a:A) AL s s´ V V´ Z Z´ L1 L2 t t´
: fexteq´ AR a (a::AL) Z s Z´ s´
  → ParamRel a Z Z´
  → BlockRel a (I.blockI Z s) (I.blockI Z´ s´)
  → simL´ bot2 AR AL L1 L2
  → (∀ r (L L´ : list I.block),
       simL´ r AR (a :: AL) L L´ →
       sim´r r (L, V, t) (L´, V´, t´))
  → sim´ (I.blockI Z s :: L1, V, t)
         (I.blockI 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´ r AR AL L L´
  → fexteq´ AR a (a::AL) Z s Z´ s´
  → ParamRel a Z Z´
  → BlockRel a (I.blockI Z s) (I.blockI Z´ s´)
  → ArgRel E E´ a Yv Y´v
  → sim´r r
            (I.blockI Z s :: L, E [Z <-- List.map Some Yv], s)
            (I.blockI Z´ s´ :: L´, E´ [Z´ <-- List.map Some Y´v], s´).

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

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

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

Lemma sim_drop_shift r l L E Y L´ E´ Y´
: sim´r (S:=I.state) (S´:=I.state) r (drop (labN l) L, E, stmtApp (LabI 0) Y)
        (drop (labN l) L´, E´, stmtApp (LabI 0) Y´)
  → sim´r (S:=I.state) (S´:=I.state) r (L, E, stmtApp l Y)
          (L´, E´, stmtApp l Y´).

End I.


Instance sim_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 sim_progeq r AR) L1 L2 AL L1´ L2´
  → (∀ x0 x1 : F.state, r x0 x1 → r0 x0 x1)
  → L1 = L1´
  → L2 = L2´
  → AIR5 (simB sim_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´ sim_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´ sim_progeq bot2 AR AL L1 L2
  → (∀ r (L L´ : list F.block),
       simL´ sim_progeq r AR (a :: AL) L L´ →
       sim´r r (L, V, t) (L´, V´, t´))
  → sim´ (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´ sim_progeq r AR AL L L´
  → fexteq´ sim_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
  → sim´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´ sim_progeq r AR AL L L´
  → fexteq´ sim_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´ sim_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 sim_drop_shift r l L E Y L´ E´ Y´
: sim´r (S:=F.state) (S´:=F.state) r (drop (labN l) L, E, stmtApp (LabI 0) Y)
        (drop (labN l) L´, E´, stmtApp (LabI 0) Y´)
  → sim´r (S:=F.state) (S´:=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 simSilent; [ eapply plus2O; single_step
                              | eapply plus2O; single_step
                              | ].

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

Ltac err_step := eapply simErr;
               try eapply star2_refl; try get_functional; try subst;
                [ try reflexivity
                | 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 simExtern;
    [ eapply star2_refl
    | eapply star2_refl
    | try step_activated
    | try step_activated
    | intros ? ? STEP; inv STEP
    | intros ? ? STEP; inv STEP
    ].