Lvc.Equiv.CtxEq

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

Set Implicit Arguments.
Unset Printing Records.

Instance SR : ProofRelation (params) := {
   ParamRel G Z := Z = Z = G;
   ArgRel V V G VL VL´ := VL = VL´ length VL = length G;
   BlockRel := fun Z b length (F.block_Z b) = length Z
                            length (F.block_Z ) = length Z
}.
intros; dcr; subst; split; congruence.
Defined.

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

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

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

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 E r,
    simL´ _ r SR ZL L
    → bisim´r r (L, E, s) (, E, s).
Proof.
  unfold bisimeq; intros. general induction s.
  - case_eq (exp_eval E e); intros.
    + pone_step. eapply IHs; eauto.
    + pno_step.
  - case_eq (exp_eval E e); intros.
    case_eq (val2bool v); intros.
    + pone_step. eapply IHs1; eauto.
    + pone_step. eapply IHs2; eauto.
    + pno_step.
  - edestruct (get_dec L (counted l)) as [[b]|].
    decide (length Y = length (F.block_Z b)).
    case_eq (omap (exp_eval E) Y); intros.
    + edestruct AIR5_nth1 as [? [? [? []]]]; eauto; dcr.
      inv H7. eapply bisim_drop_shift.
      eapply paco2_mon. eapply H8; eauto.
      hnf; intuition. exploit omap_length; eauto.
      hnf in H6. hnf in H1; dcr. simpl in ×.
      get_functional. subst b. simpl in ×.
      congruence. eauto.
    + pno_step.
    + pno_step. exploit omap_length; eauto.
      get_functional; subst. congruence.
      edestruct AIR5_nth1 as [? [? [? []]]]; eauto; dcr.
      inv H6. hnf in H5; dcr. repeat get_functional; subst. simpl in ×.
      congruence.
    + pno_step.
      × edestruct AIR5_nth1 as [? [? [? []]]]; eauto; dcr.
      × edestruct AIR5_nth2 as [? [? [? []]]]; eauto; dcr. eauto.
  - pno_step.
  - case_eq (omap (exp_eval E) Y); intros.
    + pextern_step.
      × eexists; split.
        econstructor; eauto.
        left. eapply IHs; eauto.
      × eexists; split.
        econstructor; eauto.
        left. eapply IHs; eauto.
    + pno_step.
  - pone_step.
    eapply IHs2; eauto.
    eapply simL_extension´; hnf; intros; eauto.
    hnf in H; dcr; subst.
    split; simpl; eauto. intros; dcr; subst.
    eapply IHs1; eauto.
Qed.

Lemma bisimeq_refl s
: bisimeq s s.
Proof.
  hnf; intros. eapply bisim´_bisim.
  eapply bisimeq´_refl; eauto.
Qed.

Lemma bisimeq´_bisimeqid s
: bisimeqid s
  → bisimeq s .
Proof.
  intros; hnf; intros.
  hnf in H. eapply bisim_trans with (S2:=F.state).
  eapply H. eapply bisim´_bisim.
  eapply bisimeq´_refl; eauto.
Qed.

Lemma simL´_refl r L
: AIR5 (simB bisim_progeq r SR) L L (List.map F.block_Z L) L L.
Proof.
  intros.
  general induction L; simpl.
  - econstructor.
  - econstructor.
    + destruct a. econstructor; eauto; try now (clear_all; intuition).
      × intros. hnf.
        hnf in H1; dcr; subst; simpl in ×.
        exploit omap_length; eauto.
        exploit omap_length; try eapply H0; eauto.
        pone_step; eauto using get; simpl; eauto; try congruence.
        eapply paco2_mon. eapply bisim´_refl. clear_all; firstorder.
    + eapply IHL.
Qed.

Contextual Equivalence


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) (:stmt) : stmt :=
  match ctx with
    | ctxExp x e ctxstmtLet x e (fill ctx )
    | ctxIfS e ctx tstmtIf e (fill ctx ) t
    | ctxIfT e s ctxstmtIf e s (fill ctx )
    | ctxLetS Z ctx tstmtFun Z (fill ctx ) t
    | ctxLetT Z s ctxstmtFun Z s (fill ctx )
    | ctxExtern x f e ctxstmtExtern x f e (fill ctx )
    | ctxHole
  end.

Fixpoint fillC (ctx:stmtCtx) (:stmtCtx) : stmtCtx :=
  match ctx with
    | ctxExp x e ctxctxExp x e (fillC ctx )
    | ctxIfS e ctx tctxIfS e (fillC ctx ) t
    | ctxIfT e s ctxctxIfT e s (fillC ctx )
    | ctxLetS Z ctx tctxLetS Z (fillC ctx ) t
    | ctxLetT Z s ctxctxLetT Z s (fillC ctx )
    | ctxExtern x f e ctxctxExtern x f e (fillC ctx )
    | ctxHole
  end.

Lemma simeq_contextual´ s ctx r
: ( r, bisimeq´ r s )
  → bisimeq´ r (fill ctx s) (fill ctx ).
Proof.
  intros. general induction ctx; simpl; hnf; intros; eauto.
  - case_eq (exp_eval E e); intros.
    + pone_step. eapply IHctx; eauto.
    + pno_step.
  - case_eq (exp_eval E e); intros.
    case_eq (val2bool v); intros.
    + pone_step; eapply IHctx; eauto.
    + pone_step.
      eapply bisimeq´_refl; eauto.
    + pno_step.
  - case_eq (exp_eval E e); intros.
    case_eq (val2bool v); intros.
    + pone_step.
      eapply bisimeq´_refl; eauto.
    + pone_step; eapply IHctx; eauto.
    + pno_step.
  - pone_step.
    eapply bisimeq´_refl.
    eapply simL_extension´; eauto. Focus 2.
    instantiate (1:=Z). hnf; intros; simpl; eauto.
    hnf; intros. split. hnf; intros; eauto.
    intros. simpl. hnf in H1; dcr; subst.
    eapply IHctx. eapply H. eauto.
  - pone_step.
    eapply IHctx. eauto.
    eapply simL_extension´; eauto. instantiate (1:=Z).
    hnf; intros. split. hnf; intros; eauto.
    intros. simpl. hnf in H1; dcr; subst.
    eapply bisimeq´_refl. eauto.
    hnf; simpl; eauto.
  - case_eq (omap (exp_eval E) e); intros.
    + pextern_step.
      × eexists; split.
        econstructor; eauto.
        left. eapply IHctx; eauto.
      × eexists; split.
        econstructor; eauto.
        left. eapply IHctx; eauto.
    + pno_step.
  - eapply H; eauto.
Qed.

Lemma fill_fillC C s
  : fill (fillC C ) s = fill C (fill s).
Proof.
  general induction C; simpl; f_equal; eauto.
Qed.