HyPre.pre_ni.StateSimulation
From HyPre Require Export
MultiStep
ListExtra.
Import ListNotations.
Lemma prove_trace_by_lockstep {St Psrc Ptgt : Type}
(sim_rel : Psrc * St -> Ptgt * St -> Prop) (step_src : Psrc * St -> Psrc * St) (step_tgt : Ptgt * St -> Ptgt * St) p_src p_tgt i
(Hp : sim_rel (p_src,i) (p_tgt,i))
(Hst : forall a α,
sim_rel a α
-> sim_rel (step_src a) (step_tgt α))
: forall (a : list (Psrc * St)) (α : list (Ptgt * St)) (b : Psrc * St)
(β : list (Ptgt * St)),
Forall2 sim_rel a α ->
multi_step' step_src (p_src, i) (| b :: a |) = b :: a ->
multi_step' step_tgt (p_tgt, i) (| β ++ α |) = β ++ α ->
(fun _ _ => 1) i (| a |) = | β | -> Forall2 sim_rel (b :: a) (β ++ α).
Proof.
intros.
cbn in H2.
destruct β;cbn in H2;[congruence|].
destruct β;cbn in H2;[|congruence].
cbn in *.
econstructor.
- destruct a,α. all: inversion H.
+ cbn in H0,H1.
inversion H0; inversion H1.
eapply Hp.
+ subst.
setoid_rewrite length_cons in H0.
setoid_rewrite length_cons in H1.
setoid_rewrite multi_step_S2 in H0.
setoid_rewrite multi_step_S2 in H1.
inversion H0; inversion H1.
eapply Hst.
* unfold multi_step_hd.
rewrite H5.
rewrite H9.
cbn.
assumption.
(* * unfold multi_step_hd.
rewrite H5.
cbn.
eapply multi_step_multi_trace.
cbn.
rewrite (PeanoNat.Nat.sub_0_r).
eapply H5.*)
- assumption.
Qed.
From HyPre Require Export
Semantics
VectorList.
Import VectorListNotations.
Section with_st.
Context {SrcSt TgtSt Input : Type}.
Context (state_rel : SrcSt -> TgtSt -> Prop).
Context (step_src : SrcSt -> SrcSt).
Context (step_tgt : TgtSt -> TgtSt).
Context (p_src : Input -> SrcSt) (p_tgt : Input -> TgtSt).
Context (t_sync_state (*t_next_state*) : SrcSt -> nat).
Fixpoint lift_tsync' (s : SrcSt) (n : nat)
:= match n with
| 0 => t_sync_state s
| S n => lift_tsync' (step_src s) n
end.
Definition lift_tsync (i : Input) (n : nat)
:= match n with
| 0 => 1 (* don't stall at input *)
| S n => lift_tsync' (p_src i) n
end.
(* this definition enforces that is never related to some non-empty trace *)
Inductive lift_state_rel (i : Input) : list SrcSt -> list TgtSt -> Prop :=
| LSRNil : lift_state_rel i [] []
| LSRSingle : state_rel (p_src i) (p_tgt i) -> lift_state_rel i [p_src i] [p_tgt i]
| LSRCons a a0 al α b β β0 βαl : a = a0 :: al
-> β ++ α = β0 :: βαl
-> (|β|) = t_sync_state a0
-> state_rel b β0
-> lift_state_rel i a α
-> lift_state_rel i (b :: a) (β ++ α).
Lemma lift_state_rel_cons_impl_cons (i : Input) a a0 α
: lift_state_rel i (a0 :: a) α -> exists α0 αl, α = α0 :: αl.
(* there is no way to construct lift_state_rel where only the right part is empty*)
Proof.
inversion 1; subst.
- exists (p_tgt i), []. reflexivity.
- do 2 eexists. exact H3.
Qed.
Lemma lift_state_rel_cons (i : Input) a α a0 α0
: lift_state_rel i (a0 :: a) (α0 :: α) -> state_rel a0 α0.
Proof.
intros.
dependent destruction H;cbn;eauto.
rewrite H0 in x.
dependent destruction x.
assumption.
Qed.
Lemma multi_step_hd_step2 {X : Type} (step : X -> X) (x : X) (n : nat)
: multi_step_hd step x (S n) = multi_step_hd step (step x) n.
Proof.
clear.
revert x.
induction n;intros.
- cbn in *.
reflexivity.
- rewrite multi_step_hd_step.
rewrite IHn.
rewrite multi_step_hd_step.
reflexivity.
Qed.
Lemma lift_tsync_tsync_state (i : Input) a0 a
(Hsem : multi_step_hd step_src (p_src i) (|a|) = a0)
: lift_tsync i (| a0 :: a|) = t_sync_state a0.
Proof.
cbn.
clear - Hsem.
revert a0 Hsem.
generalize (p_src i).
clear.
induction a;intros.
- cbn.
cbn in Hsem.
subst a0.
reflexivity.
- destruct a0.
+ cbn.
cbn in Hsem.
rewrite <-Hsem.
reflexivity.
+ cbn in Hsem.
rewrite multi_step_hd_step2 in Hsem.
cbn.
eapply IHa in Hsem.
rewrite <-Hsem.
cbn.
reflexivity.
Qed.
Lemma cons_rcons_len {X : Type} (x y : X) (xl yl : list X)
: x :: xl = yl :r: y -> |xl| = |yl|.
Proof.
revert x y yl.
induction xl;intros.
- destruct yl;cbn in *;try congruence.
destruct yl;cbn in *;try congruence.
- destruct yl;[cbn in H;congruence| ].
cbn.
f_equal.
cbn in H.
dependent destruction H.
eapply IHxl;eauto.
Qed.
Lemma multi_step_middle {X : Type} (step : X -> X) (x0 x1 : X) (xl yl : list X) (n : nat)
: n = |yl| + (|xl|)
-> multi_step step x0 n = yl ++ x1 :: xl
-> multi_step_hd step x1 (|yl|) = multi_step_hd step x0 n.
Proof.
revert x0 x1 xl yl.
induction n;intros x0 x1 xl yl Hn Hmulti.
- destruct xl,yl;cbn in Hn; try congruence.
cbn in Hmulti.
inversion Hmulti.
cbn.
reflexivity.
- unfold multi_step_hd.
rewrite multi_step_S2.
cbn.
destruct yl.
+ rewrite multi_step_S2 in Hmulti.
cbn in *.
inversion Hmulti.
reflexivity.
+ rewrite length_cons.
rewrite multi_step_S2.
cbn.
f_equal.
eapply IHn with (xl:=xl);eauto.
rewrite multi_step_S2 in Hmulti.
cbn in Hmulti.
inversion Hmulti.
reflexivity.
Qed.
Lemma prove_trace_by_tsync s t i
(Hseq : s = p_src i)
(Hteq : t = p_tgt i)
(Hp : state_rel s t)
(Hst : forall a α,
state_rel a α
-> state_rel (step_src a) (multi_step_hd step_tgt α (t_sync_state a)))
: forall (a : list SrcSt) (α : list TgtSt) (b : SrcSt) (β : list TgtSt),
lift_state_rel i a α
-> multi_step' step_src s (| b :: a |) = b :: a
-> multi_step' step_tgt t (| β ++ α |) = β ++ α
-> lift_tsync i (|a|) = (| β |)
-> lift_state_rel i (b :: a) (β ++ α).
Proof.
intros ? ? ? ? Hrel Hsrc Htgt Hsync.
destruct a.
- dependent destruction Hrel.
cbn in Hsync.
destruct β;[cbn in Hsync;congruence| ].
destruct β;[ |cbn in Hsync;congruence].
cbn.
rewrite app_nil_r in Htgt.
cbn in Hsrc,Htgt.
dependent destruction Hsrc.
dependent destruction Htgt.
econstructor;eauto.
- destruct (β ++ α) eqn:E.
{
exfalso.
eapply app_eq_nil in E.
destructH.
subst α.
inversion Hrel.
rewrite H3 in H1.
congruence.
}
rewrite <-E.
econstructor;eauto.
+ rewrite <-Hsync.
eapply lift_tsync_tsync_state;eauto.
rewrite length_cons in Hsrc.
rewrite length_cons in Hsrc.
unfold multi_step' in Hsrc.
rewrite multi_step_S2 in Hsrc.
inversion Hsrc.
subst s.
subst b.
unfold multi_step_hd.
rewrite H1.
cbn.
reflexivity.
+ cbn in Hsrc,Htgt.
rewrite <-multi_step_S in Hsrc.
rewrite multi_step_S2 in Hsrc.
rewrite lift_tsync_tsync_state in Hsync.
dependent destruction Hrel.
* eapply Hst in H.
cbn in Hsync.
cbn in Hsrc.
subst s t.
dependent destruction Hsrc.
rewrite Hsync in H.
unfold multi_step_hd in H.
symmetry in E.
eapply cons_rcons_len in E.
rewrite E in Htgt.
rewrite Htgt in H.
cbn in H.
assumption.
* eapply Hst in H2.
dependent destruction Hsrc.
setoid_rewrite <-multi_step_S in x.
unfold multi_step_hd.
setoid_rewrite x.
cbn.
rewrite Hsync in H2.
rewrite multi_step_middle with (n:=|l|) (x0:=t) (xl:=βαl) in H2.
-- unfold multi_step_hd in H2.
rewrite Htgt in H2.
cbn in H2.
assumption.
-- clear - H0 E.
eapply f_equal with (f:=@length _) in H0.
eapply f_equal with (f:=@length _) in E.
rewrite app_length in H0.
rewrite app_length in E.
rewrite app_length in E.
cbn in H0,E.
lia.
-- rewrite Htgt.
rewrite <-H0.
symmetry.
assumption.
* inversion Hsrc.
subst s.
subst b.
unfold multi_step_hd.
rewrite H1.
cbn.
reflexivity.
Qed.
End with_st.
MultiStep
ListExtra.
Import ListNotations.
Lemma prove_trace_by_lockstep {St Psrc Ptgt : Type}
(sim_rel : Psrc * St -> Ptgt * St -> Prop) (step_src : Psrc * St -> Psrc * St) (step_tgt : Ptgt * St -> Ptgt * St) p_src p_tgt i
(Hp : sim_rel (p_src,i) (p_tgt,i))
(Hst : forall a α,
sim_rel a α
-> sim_rel (step_src a) (step_tgt α))
: forall (a : list (Psrc * St)) (α : list (Ptgt * St)) (b : Psrc * St)
(β : list (Ptgt * St)),
Forall2 sim_rel a α ->
multi_step' step_src (p_src, i) (| b :: a |) = b :: a ->
multi_step' step_tgt (p_tgt, i) (| β ++ α |) = β ++ α ->
(fun _ _ => 1) i (| a |) = | β | -> Forall2 sim_rel (b :: a) (β ++ α).
Proof.
intros.
cbn in H2.
destruct β;cbn in H2;[congruence|].
destruct β;cbn in H2;[|congruence].
cbn in *.
econstructor.
- destruct a,α. all: inversion H.
+ cbn in H0,H1.
inversion H0; inversion H1.
eapply Hp.
+ subst.
setoid_rewrite length_cons in H0.
setoid_rewrite length_cons in H1.
setoid_rewrite multi_step_S2 in H0.
setoid_rewrite multi_step_S2 in H1.
inversion H0; inversion H1.
eapply Hst.
* unfold multi_step_hd.
rewrite H5.
rewrite H9.
cbn.
assumption.
(* * unfold multi_step_hd.
rewrite H5.
cbn.
eapply multi_step_multi_trace.
cbn.
rewrite (PeanoNat.Nat.sub_0_r).
eapply H5.*)
- assumption.
Qed.
From HyPre Require Export
Semantics
VectorList.
Import VectorListNotations.
Section with_st.
Context {SrcSt TgtSt Input : Type}.
Context (state_rel : SrcSt -> TgtSt -> Prop).
Context (step_src : SrcSt -> SrcSt).
Context (step_tgt : TgtSt -> TgtSt).
Context (p_src : Input -> SrcSt) (p_tgt : Input -> TgtSt).
Context (t_sync_state (*t_next_state*) : SrcSt -> nat).
Fixpoint lift_tsync' (s : SrcSt) (n : nat)
:= match n with
| 0 => t_sync_state s
| S n => lift_tsync' (step_src s) n
end.
Definition lift_tsync (i : Input) (n : nat)
:= match n with
| 0 => 1 (* don't stall at input *)
| S n => lift_tsync' (p_src i) n
end.
(* this definition enforces that is never related to some non-empty trace *)
Inductive lift_state_rel (i : Input) : list SrcSt -> list TgtSt -> Prop :=
| LSRNil : lift_state_rel i [] []
| LSRSingle : state_rel (p_src i) (p_tgt i) -> lift_state_rel i [p_src i] [p_tgt i]
| LSRCons a a0 al α b β β0 βαl : a = a0 :: al
-> β ++ α = β0 :: βαl
-> (|β|) = t_sync_state a0
-> state_rel b β0
-> lift_state_rel i a α
-> lift_state_rel i (b :: a) (β ++ α).
Lemma lift_state_rel_cons_impl_cons (i : Input) a a0 α
: lift_state_rel i (a0 :: a) α -> exists α0 αl, α = α0 :: αl.
(* there is no way to construct lift_state_rel where only the right part is empty*)
Proof.
inversion 1; subst.
- exists (p_tgt i), []. reflexivity.
- do 2 eexists. exact H3.
Qed.
Lemma lift_state_rel_cons (i : Input) a α a0 α0
: lift_state_rel i (a0 :: a) (α0 :: α) -> state_rel a0 α0.
Proof.
intros.
dependent destruction H;cbn;eauto.
rewrite H0 in x.
dependent destruction x.
assumption.
Qed.
Lemma multi_step_hd_step2 {X : Type} (step : X -> X) (x : X) (n : nat)
: multi_step_hd step x (S n) = multi_step_hd step (step x) n.
Proof.
clear.
revert x.
induction n;intros.
- cbn in *.
reflexivity.
- rewrite multi_step_hd_step.
rewrite IHn.
rewrite multi_step_hd_step.
reflexivity.
Qed.
Lemma lift_tsync_tsync_state (i : Input) a0 a
(Hsem : multi_step_hd step_src (p_src i) (|a|) = a0)
: lift_tsync i (| a0 :: a|) = t_sync_state a0.
Proof.
cbn.
clear - Hsem.
revert a0 Hsem.
generalize (p_src i).
clear.
induction a;intros.
- cbn.
cbn in Hsem.
subst a0.
reflexivity.
- destruct a0.
+ cbn.
cbn in Hsem.
rewrite <-Hsem.
reflexivity.
+ cbn in Hsem.
rewrite multi_step_hd_step2 in Hsem.
cbn.
eapply IHa in Hsem.
rewrite <-Hsem.
cbn.
reflexivity.
Qed.
Lemma cons_rcons_len {X : Type} (x y : X) (xl yl : list X)
: x :: xl = yl :r: y -> |xl| = |yl|.
Proof.
revert x y yl.
induction xl;intros.
- destruct yl;cbn in *;try congruence.
destruct yl;cbn in *;try congruence.
- destruct yl;[cbn in H;congruence| ].
cbn.
f_equal.
cbn in H.
dependent destruction H.
eapply IHxl;eauto.
Qed.
Lemma multi_step_middle {X : Type} (step : X -> X) (x0 x1 : X) (xl yl : list X) (n : nat)
: n = |yl| + (|xl|)
-> multi_step step x0 n = yl ++ x1 :: xl
-> multi_step_hd step x1 (|yl|) = multi_step_hd step x0 n.
Proof.
revert x0 x1 xl yl.
induction n;intros x0 x1 xl yl Hn Hmulti.
- destruct xl,yl;cbn in Hn; try congruence.
cbn in Hmulti.
inversion Hmulti.
cbn.
reflexivity.
- unfold multi_step_hd.
rewrite multi_step_S2.
cbn.
destruct yl.
+ rewrite multi_step_S2 in Hmulti.
cbn in *.
inversion Hmulti.
reflexivity.
+ rewrite length_cons.
rewrite multi_step_S2.
cbn.
f_equal.
eapply IHn with (xl:=xl);eauto.
rewrite multi_step_S2 in Hmulti.
cbn in Hmulti.
inversion Hmulti.
reflexivity.
Qed.
Lemma prove_trace_by_tsync s t i
(Hseq : s = p_src i)
(Hteq : t = p_tgt i)
(Hp : state_rel s t)
(Hst : forall a α,
state_rel a α
-> state_rel (step_src a) (multi_step_hd step_tgt α (t_sync_state a)))
: forall (a : list SrcSt) (α : list TgtSt) (b : SrcSt) (β : list TgtSt),
lift_state_rel i a α
-> multi_step' step_src s (| b :: a |) = b :: a
-> multi_step' step_tgt t (| β ++ α |) = β ++ α
-> lift_tsync i (|a|) = (| β |)
-> lift_state_rel i (b :: a) (β ++ α).
Proof.
intros ? ? ? ? Hrel Hsrc Htgt Hsync.
destruct a.
- dependent destruction Hrel.
cbn in Hsync.
destruct β;[cbn in Hsync;congruence| ].
destruct β;[ |cbn in Hsync;congruence].
cbn.
rewrite app_nil_r in Htgt.
cbn in Hsrc,Htgt.
dependent destruction Hsrc.
dependent destruction Htgt.
econstructor;eauto.
- destruct (β ++ α) eqn:E.
{
exfalso.
eapply app_eq_nil in E.
destructH.
subst α.
inversion Hrel.
rewrite H3 in H1.
congruence.
}
rewrite <-E.
econstructor;eauto.
+ rewrite <-Hsync.
eapply lift_tsync_tsync_state;eauto.
rewrite length_cons in Hsrc.
rewrite length_cons in Hsrc.
unfold multi_step' in Hsrc.
rewrite multi_step_S2 in Hsrc.
inversion Hsrc.
subst s.
subst b.
unfold multi_step_hd.
rewrite H1.
cbn.
reflexivity.
+ cbn in Hsrc,Htgt.
rewrite <-multi_step_S in Hsrc.
rewrite multi_step_S2 in Hsrc.
rewrite lift_tsync_tsync_state in Hsync.
dependent destruction Hrel.
* eapply Hst in H.
cbn in Hsync.
cbn in Hsrc.
subst s t.
dependent destruction Hsrc.
rewrite Hsync in H.
unfold multi_step_hd in H.
symmetry in E.
eapply cons_rcons_len in E.
rewrite E in Htgt.
rewrite Htgt in H.
cbn in H.
assumption.
* eapply Hst in H2.
dependent destruction Hsrc.
setoid_rewrite <-multi_step_S in x.
unfold multi_step_hd.
setoid_rewrite x.
cbn.
rewrite Hsync in H2.
rewrite multi_step_middle with (n:=|l|) (x0:=t) (xl:=βαl) in H2.
-- unfold multi_step_hd in H2.
rewrite Htgt in H2.
cbn in H2.
assumption.
-- clear - H0 E.
eapply f_equal with (f:=@length _) in H0.
eapply f_equal with (f:=@length _) in E.
rewrite app_length in H0.
rewrite app_length in E.
rewrite app_length in E.
cbn in H0,E.
lia.
-- rewrite Htgt.
rewrite <-H0.
symmetry.
assumption.
* inversion Hsrc.
subst s.
subst b.
unfold multi_step_hd.
rewrite H1.
cbn.
reflexivity.
Qed.
End with_st.