Require Import List.
Require Export Util Var Val Exp Env Map CSet AutoIndTac IL AllInRel Bisim.

Set Implicit Arguments.

Instance SR : ProofRelation (params) := {
   ParamRel G Z Z´ := Z = Z´ ∧ Z = G;
   ArgRel V V G VL VL´ := VL = VL´ ∧ length VL = length G;
   BlockRel := fun Z b b´ ⇒ length (F.block_Z b) = length Z
                           ∧ length (F.block_Z b´) = length Z
}.
Defined.

Definition bisimeq s s´ :=
  ∀ ZL L L´ E, simL´ _ bot2 SR ZL L L´ → bisim (L, E, s) (L´, E, s´).

Definition bisimeqid s s´ :=
  ∀ (L:F.labenv) E, bisim (L, E, s) (L, E, s´).

Definition bisimeq´ r s s´ :=
  ∀ ZL L L´ E, simL´ _ r SR ZL L L´ → bisim´r r (L, E, s) (L´, E, s´).

Ltac pone_step := pfold; eapply bisim´Silent; [ eapply plus2O; single_step
                              | eapply plus2O; single_step
                              | left ].

Ltac pone_step´ := pfold; eapply bisim´Silent; [ eapply plus2O; single_step
                              | eapply plus2O; single_step
                              | right ].

Ltac pno_step := pfold; eapply bisim´Term;
               try eapply star2_refl; try get_functional; try subst;
                [ try reflexivity
                | stuck2
                | stuck2 ].

Ltac pextern_step :=
  let STEP := fresh "STEP" in
  pfold; eapply bisim´Extern;
    [ eapply star2_refl
    | eapply star2_refl
    | try step_activated
    | try step_activated
    | intros ? ? STEP; inv STEP
    | intros ? ? STEP; inv STEP
    ].

Lemma bisimeq´_refl s
: ∀ ZL L L´ E r,
    simL´ _ r SR ZL L L´
    → bisim´r r (L, E, s) (L´, E, s).

Lemma bisimeq_refl s
: bisimeq s s.

Lemma bisimeq´_bisimeqid s s´
: bisimeqid s s´
  → bisimeq s s´.

Lemma simL´_refl r L
: AIR5 (simB bisim_progeq r SR) L L (List.map F.block_Z L) L L.

Inductive stmtCtx : Type :=
| ctxExp (x : var) (e: exp) (C : stmtCtx) : stmtCtx
| ctxIfS (e : exp) (C : stmtCtx) (t : stmt) : stmtCtx
| ctxIfT (e : exp) (s : stmt) (C : stmtCtx) : stmtCtx

| ctxLetS (Z:params) (C : stmtCtx) (t : stmt) : stmtCtx
| ctxLetT (Z:params) (s : stmt) (C : stmtCtx) : stmtCtx
| ctxExtern (x : var) (f:external) (e:args) (C:stmtCtx) : stmtCtx
| ctxHole.

Fixpoint fill (ctx:stmtCtx) (s´:stmt) : stmt :=
  match ctx with
    | ctxExp x e ctx ⇒ stmtLet x e (fill ctx s´)
    | ctxIfS e ctx t ⇒ stmtIf e (fill ctx s´) t
    | ctxIfT e s ctx ⇒ stmtIf e s (fill ctx s´)
    | ctxLetS Z ctx t ⇒ stmtFun Z (fill ctx s´) t
    | ctxLetT Z s ctx ⇒ stmtFun Z s (fill ctx s´)
    | ctxExtern x f e ctx ⇒ stmtExtern x f e (fill ctx s´)
    | ctxHole ⇒ s´
  end.

Fixpoint fillC (ctx:stmtCtx) (s´:stmtCtx) : stmtCtx :=
  match ctx with
    | ctxExp x e ctx ⇒ ctxExp x e (fillC ctx s´)
    | ctxIfS e ctx t ⇒ ctxIfS e (fillC ctx s´) t
    | ctxIfT e s ctx ⇒ ctxIfT e s (fillC ctx s´)
    | ctxLetS Z ctx t ⇒ ctxLetS Z (fillC ctx s´) t
    | ctxLetT Z s ctx ⇒ ctxLetT Z s (fillC ctx s´)
    | ctxExtern x f e ctx ⇒ ctxExtern x f e (fillC ctx s´)
    | ctxHole ⇒ s´
  end.

Lemma simeq_contextual´ s s´ ctx r
: (∀ r, bisimeq´ r s s´)
  → bisimeq´ r (fill ctx s) (fill ctx s´).

Lemma fill_fillC C C´ s
  : fill (fillC C C´) s = fill C (fill C´ s).