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 = 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
}.
intros; dcr; subst; split; congruence.
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).
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 s´
: bisimeqid s s´
→ bisimeq s 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.
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 = 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
}.
intros; dcr; subst; split; congruence.
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).
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 s´
: bisimeqid s s´
→ bisimeq s 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.
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´).
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 C´ s
: fill (fillC C C´) s = fill C (fill C´ s).
Proof.
general induction C; simpl; f_equal; eauto.
Qed.