HyPre.pred.Semantics
From Coq Require Import
Classes.EquivDec
Lists.List
Lia.
From Coq Require Vector.
Import ListNotations.
Require Import VectorExtra Tac.
Require Import Equality.
Require Import VectorNat VectorList.
From HyPre Require Import PreSuffix.
Import VectorListNotations.
Import VecNatNotations.
Section with_st.
Context {Input State : Type}.
Context {state0 : State}.
Context (dec_St : forall x y : State, {x = y} + {x <> y}).
(* TODO Consider renaming into "linear semantics" *)
(* intuitively the set of traces should be a semi-lattice,
maybe this requirement translates to the hypersemantics as well *)
Class rad_semantics (sem : Input -> list State -> Prop)
:= {
rooted : forall i, sem i [];
alive : forall i, forall sl, sem i sl -> {s | sem i (s :: sl)};
deterministic : forall i, forall s1 s2 sl, sem i sl -> sem i (s1 :: sl) -> sem i (s2 :: sl) -> s1 = s2;
safe : forall i s sl, sem i (s :: sl) -> sem i sl;
}.
Section with_rad_sem.
Context (sem : Input -> list State -> Prop) {RS : rad_semantics sem}.
(* TODO Prove or assume decidability of sem *)
Lemma dec_sem (i : Input) (sl : list State) : {sem i sl} + {~ sem i sl}.
Proof.
induction sl.
- left.
eapply rooted.
- destruct IHsl.
+ specialize (alive i sl) as Ha.
exploit Ha.
destruct Ha as [x Hx].
specialize (dec_St x a).
destruct dec_St.
* subst x.
left.
assumption.
* right.
contradict n.
eapply deterministic.
1: eapply s.
1,2:assumption.
+ right.
contradict n.
eapply safe;eauto.
Qed.
Lemma n_sem_steps (n : nat) i (sl : list State) (sem_sl : sem i sl)
: {sl' : list State | sem i (sl' ++ sl) /\ length sl' = n}.
Proof.
induction n.
- econstructor. erewrite app_nil_l. eauto.
- destruct IHn.
destruct a as [Hsem Hlen].
eapply alive in Hsem.
destruct Hsem.
eapply exist with (x:=x0 :: x).
split;cbn;eauto.
Defined.
Lemma sem_prefix_containing i sl sl'
: prefix sl sl' -> sem i sl' -> sem i sl.
Proof.
intros H.
induction H.
- intros;eauto.
- intros.
eapply IHprefix.
eapply safe.
eapply H0.
Qed.
Lemma sem_safe_app
: forall i sl1 sl2, sem i (sl1 ++ sl2) -> sem i sl2.
Proof.
intros.
eapply sem_prefix_containing.
- eapply prefix_eq.
exists sl1.
reflexivity.
- assumption.
Qed.
Lemma rooted_n_sem_steps (n : nat) i
: {sl : list State | sem i sl /\ length sl = n}.
Proof.
specialize (n_sem_steps n i [] (rooted i)) as [sl' [? ?] ].
econstructor.
setoid_rewrite app_nil_r in H.
split;eauto.
Defined.
Lemma sem_leneq_eq i sl1 sl2
: sem i sl1 -> sem i sl2 -> length sl1 = length sl2 -> sl1 = sl2.
Proof.
intros Hsem1 Hsem2 Hlen.
revert dependent sl2.
induction sl1;
intros;
destruct sl2;
cbn in *.
- reflexivity.
- congruence.
- congruence.
- inversion Hlen.
eapply safe in Hsem1 as Hsem0.
specialize (IHsl1 Hsem0 sl2).
exploit IHsl1.
1: eapply safe;eauto.
subst sl2.
f_equal.
eapply deterministic;eauto.
Qed.
Definition sem_step i (sl : list State)
: State
:= match dec_sem i sl with
| left H => proj1_sig (alive i sl H)
| _ => state0
end.
Lemma construct_vec {k : nat} (i_vec : Vector.t Input k) (v : Vector.t nat k)
: {sv | Vector.Forall2 sem i_vec sv /\ vl_len sv = v}.
Proof.
dependent induction v.
- eapply exist with (x:=Vector.nil _). split;[|cbn;eauto].
eapply Vector.case0 with (v:=i_vec).
econstructor.
- dependent destruction i_vec.
destruct (IHv i_vec) as [sv [Hsem Hlen] ].
specialize (rooted_n_sem_steps h0) as [sl' [Hsem' Hlen'] ].
eapply exist with (x:=Vector.cons _ sl' _ sv).
split.
+ econstructor;eauto.
+ cbn. rewrite Hlen'. rewrite <-Hlen. reflexivity.
Defined.
Lemma construct_vec_cont {k : nat} (i_vec : Vector.t Input k) (vpre : Vector.t (list State) k) (v : Vector.t nat k)
: Vector.Forall2 sem i_vec vpre -> {sv | Vector.Forall2 sem i_vec (sv +vl+ vpre) /\ vl_len sv = v}.
Proof. (*
Lemma construct_vec_cont {k : nat} (i_vec : Vector.t Input k) (vpre : {vpre : Vector.t (list State) k | Vector.Forall2 sem i_vec vpre}) (v : Vector.t nat k)
: {sv | Vector.Forall2 sem i_vec (sv +vl+ proj1_sig vpre) /\ vl_len sv = v}.
Proof.*)
(* intro H.
specialize (construct_vec i_vec (v +vn+ vl_len vpre)) as Hsv.
destruct Hsv.*)
dependent induction v;intros H.
- eapply exist with (x:=Vector.nil _). split;[|cbn;eauto].
rewrite vec_0_nil.
eapply Vector.case0 with (v:=i_vec).
econstructor.
- dependent destruction i_vec.
dependent destruction vpre.
destruct (IHv i_vec vpre) as [sv [Hsem Hlen] ].
+ dependent destruction H. assumption.
+ specialize (n_sem_steps h1 h h0) as [sl' [Hsem' Hlen'] ].
* inversion_clear H;eauto.
* eapply exist with (x:=Vector.cons _ sl' _ sv).
split.
-- econstructor;eauto.
-- cbn. rewrite Hlen'. rewrite <-Hlen. reflexivity.
Qed.
Classes.EquivDec
Lists.List
Lia.
From Coq Require Vector.
Import ListNotations.
Require Import VectorExtra Tac.
Require Import Equality.
Require Import VectorNat VectorList.
From HyPre Require Import PreSuffix.
Import VectorListNotations.
Import VecNatNotations.
Section with_st.
Context {Input State : Type}.
Context {state0 : State}.
Context (dec_St : forall x y : State, {x = y} + {x <> y}).
(* TODO Consider renaming into "linear semantics" *)
(* intuitively the set of traces should be a semi-lattice,
maybe this requirement translates to the hypersemantics as well *)
Class rad_semantics (sem : Input -> list State -> Prop)
:= {
rooted : forall i, sem i [];
alive : forall i, forall sl, sem i sl -> {s | sem i (s :: sl)};
deterministic : forall i, forall s1 s2 sl, sem i sl -> sem i (s1 :: sl) -> sem i (s2 :: sl) -> s1 = s2;
safe : forall i s sl, sem i (s :: sl) -> sem i sl;
}.
Section with_rad_sem.
Context (sem : Input -> list State -> Prop) {RS : rad_semantics sem}.
(* TODO Prove or assume decidability of sem *)
Lemma dec_sem (i : Input) (sl : list State) : {sem i sl} + {~ sem i sl}.
Proof.
induction sl.
- left.
eapply rooted.
- destruct IHsl.
+ specialize (alive i sl) as Ha.
exploit Ha.
destruct Ha as [x Hx].
specialize (dec_St x a).
destruct dec_St.
* subst x.
left.
assumption.
* right.
contradict n.
eapply deterministic.
1: eapply s.
1,2:assumption.
+ right.
contradict n.
eapply safe;eauto.
Qed.
Lemma n_sem_steps (n : nat) i (sl : list State) (sem_sl : sem i sl)
: {sl' : list State | sem i (sl' ++ sl) /\ length sl' = n}.
Proof.
induction n.
- econstructor. erewrite app_nil_l. eauto.
- destruct IHn.
destruct a as [Hsem Hlen].
eapply alive in Hsem.
destruct Hsem.
eapply exist with (x:=x0 :: x).
split;cbn;eauto.
Defined.
Lemma sem_prefix_containing i sl sl'
: prefix sl sl' -> sem i sl' -> sem i sl.
Proof.
intros H.
induction H.
- intros;eauto.
- intros.
eapply IHprefix.
eapply safe.
eapply H0.
Qed.
Lemma sem_safe_app
: forall i sl1 sl2, sem i (sl1 ++ sl2) -> sem i sl2.
Proof.
intros.
eapply sem_prefix_containing.
- eapply prefix_eq.
exists sl1.
reflexivity.
- assumption.
Qed.
Lemma rooted_n_sem_steps (n : nat) i
: {sl : list State | sem i sl /\ length sl = n}.
Proof.
specialize (n_sem_steps n i [] (rooted i)) as [sl' [? ?] ].
econstructor.
setoid_rewrite app_nil_r in H.
split;eauto.
Defined.
Lemma sem_leneq_eq i sl1 sl2
: sem i sl1 -> sem i sl2 -> length sl1 = length sl2 -> sl1 = sl2.
Proof.
intros Hsem1 Hsem2 Hlen.
revert dependent sl2.
induction sl1;
intros;
destruct sl2;
cbn in *.
- reflexivity.
- congruence.
- congruence.
- inversion Hlen.
eapply safe in Hsem1 as Hsem0.
specialize (IHsl1 Hsem0 sl2).
exploit IHsl1.
1: eapply safe;eauto.
subst sl2.
f_equal.
eapply deterministic;eauto.
Qed.
Definition sem_step i (sl : list State)
: State
:= match dec_sem i sl with
| left H => proj1_sig (alive i sl H)
| _ => state0
end.
Lemma construct_vec {k : nat} (i_vec : Vector.t Input k) (v : Vector.t nat k)
: {sv | Vector.Forall2 sem i_vec sv /\ vl_len sv = v}.
Proof.
dependent induction v.
- eapply exist with (x:=Vector.nil _). split;[|cbn;eauto].
eapply Vector.case0 with (v:=i_vec).
econstructor.
- dependent destruction i_vec.
destruct (IHv i_vec) as [sv [Hsem Hlen] ].
specialize (rooted_n_sem_steps h0) as [sl' [Hsem' Hlen'] ].
eapply exist with (x:=Vector.cons _ sl' _ sv).
split.
+ econstructor;eauto.
+ cbn. rewrite Hlen'. rewrite <-Hlen. reflexivity.
Defined.
Lemma construct_vec_cont {k : nat} (i_vec : Vector.t Input k) (vpre : Vector.t (list State) k) (v : Vector.t nat k)
: Vector.Forall2 sem i_vec vpre -> {sv | Vector.Forall2 sem i_vec (sv +vl+ vpre) /\ vl_len sv = v}.
Proof. (*
Lemma construct_vec_cont {k : nat} (i_vec : Vector.t Input k) (vpre : {vpre : Vector.t (list State) k | Vector.Forall2 sem i_vec vpre}) (v : Vector.t nat k)
: {sv | Vector.Forall2 sem i_vec (sv +vl+ proj1_sig vpre) /\ vl_len sv = v}.
Proof.*)
(* intro H.
specialize (construct_vec i_vec (v +vn+ vl_len vpre)) as Hsv.
destruct Hsv.*)
dependent induction v;intros H.
- eapply exist with (x:=Vector.nil _). split;[|cbn;eauto].
rewrite vec_0_nil.
eapply Vector.case0 with (v:=i_vec).
econstructor.
- dependent destruction i_vec.
dependent destruction vpre.
destruct (IHv i_vec vpre) as [sv [Hsem Hlen] ].
+ dependent destruction H. assumption.
+ specialize (n_sem_steps h1 h h0) as [sl' [Hsem' Hlen'] ].
* inversion_clear H;eauto.
* eapply exist with (x:=Vector.cons _ sl' _ sv).
split.
-- econstructor;eauto.
-- cbn. rewrite Hlen'. rewrite <-Hlen. reflexivity.
Qed.
This is used to translate a synchroniser in some live simulation language
to an abstract one, operating on Vector.t nat k ...
Lemma construct_sync {k : nat} (vsync : Vector.t Input k -> Vector.t (list State) k -> Vector.t nat k)
: Vector.t Input k -> Vector.t nat k -> Vector.t nat k.
Proof.
intros i_vec v. specialize (construct_vec i_vec v) as Hvec.
destruct Hvec as [sv Hsv]. eapply vsync.
- eapply i_vec.
- eapply sv.
Defined.
: Vector.t Input k -> Vector.t nat k -> Vector.t nat k.
Proof.
intros i_vec v. specialize (construct_vec i_vec v) as Hvec.
destruct Hvec as [sv Hsv]. eapply vsync.
- eapply i_vec.
- eapply sv.
Defined.
.. with determinism this construction is unique
Definition construct_vsync {k : nat} (sync : Vector.t Input k -> Vector.t nat k -> Vector.t nat k)
: Vector.t Input k -> Vector.t (list State) k -> Vector.t nat k
:= fun iv v => sync iv (vl_len v).
(* TODO Prove construct_sync_vsync lemmas if needed
Lemma construct_sync_vsync_eq {k : nat} (sync : Vector.t Input k -> Vector.t nat k -> Vector.t nat k)
: forall v, construct_sync (construct_vsync sync) v = sync v.
(* using vecnat_ind *)
unfold construct_vsync.
Lemma construct_vsync_sync_eq {k : nat} (vsync : Vector.t Input k -> Vector.t (list State) k -> Vector.t nat k)
: forall v, construct_vsync (construct_sync vsync) v = vsync v.
Lemma construct_sync_lenvec_eq {k : nat} (vsync : Vector.t Input k -> Vector.t (list State) k -> Vector.t nat k)
: forall iv v, (construct_sync vsync) iv (vl_len v) = vsync iv v.
Proof.
intros. rewrite <-construct_vsync_sync_eq. reflexivity.
Qed.
*)
: Vector.t Input k -> Vector.t (list State) k -> Vector.t nat k
:= fun iv v => sync iv (vl_len v).
(* TODO Prove construct_sync_vsync lemmas if needed
Lemma construct_sync_vsync_eq {k : nat} (sync : Vector.t Input k -> Vector.t nat k -> Vector.t nat k)
: forall v, construct_sync (construct_vsync sync) v = sync v.
(* using vecnat_ind *)
unfold construct_vsync.
Lemma construct_vsync_sync_eq {k : nat} (vsync : Vector.t Input k -> Vector.t (list State) k -> Vector.t nat k)
: forall v, construct_vsync (construct_sync vsync) v = vsync v.
Lemma construct_sync_lenvec_eq {k : nat} (vsync : Vector.t Input k -> Vector.t (list State) k -> Vector.t nat k)
: forall iv v, (construct_sync vsync) iv (vl_len v) = vsync iv v.
Proof.
intros. rewrite <-construct_vsync_sync_eq. reflexivity.
Qed.
*)
Until
Section with_d.
Context (d : State -> bool).
Fixpoint until (n : nat) (i : Input) (sl : list State) : nat
:= match n with
| O => 1
| S n => let s := sem_step i sl in
if d s then 1 else S (until n i (s :: sl))
end.
Lemma until_gt_zero (n : nat) i (sl : list State)
: until n i sl > 0.
Proof.
revert dependent sl.
induction n;intros;cbn.
- lia.
- destruct (d _).
+ lia.
+ specialize (IHn (sem_step i sl :: sl)). lia.
Qed.
Definition vl_until {k : nat} (n : nat) (iv : Vector.t Input k)
:= Vector.map2 (until n) iv.
Definition construct_trace (n : nat) (i : Input) : list State
:= proj1_sig (rooted_n_sem_steps n i).
Definition construct_trace_sync (sync : Input -> list State -> nat)
: Input -> nat -> nat
:= fun i n => sync i (construct_trace n i).
Lemma construct_trace_len (n : nat) (i : Input)
: | construct_trace n i | = n.
Proof.
clear d state0.
unfold construct_trace,rooted_n_sem_steps,n_sem_steps.
match goal with |- length (_ (match ?x with _=>_ end)) = _
=> destruct x
end.
destruct a.
cbn.
assumption.
Qed.
Lemma construct_trace_sem (n : nat) (i : Input)
: sem i (construct_trace n i).
Proof.
clear d state0.
unfold construct_trace,rooted_n_sem_steps,n_sem_steps.
match goal with |- sem i (_ (match ?x with _=>_ end))
=> destruct x
end.
destruct a.
cbn.
rewrite app_nil_r in s.
assumption.
Qed.
Lemma construct_trace_length i t
: sem i t -> construct_trace (length t) i = t.
clear.
intros.
specialize (construct_trace_sem (|t|) i) as Q.
specialize (construct_trace_len (|t|) i) as R.
eapply sem_leneq_eq;eauto.
Qed.
(* TODO Prove construct_sync_map2 if needed
Lemma construct_sync_map2 {k : nat} (f : Input -> list State -> nat)
: forall (iv xl : Vector.t _ k),
construct_sync (Vector.map2 f) iv xl = Vector.map2 (construct_trace_sync f) iv xl.
*)
End with_d.
End with_rad_sem.
End with_st.
Context (d : State -> bool).
Fixpoint until (n : nat) (i : Input) (sl : list State) : nat
:= match n with
| O => 1
| S n => let s := sem_step i sl in
if d s then 1 else S (until n i (s :: sl))
end.
Lemma until_gt_zero (n : nat) i (sl : list State)
: until n i sl > 0.
Proof.
revert dependent sl.
induction n;intros;cbn.
- lia.
- destruct (d _).
+ lia.
+ specialize (IHn (sem_step i sl :: sl)). lia.
Qed.
Definition vl_until {k : nat} (n : nat) (iv : Vector.t Input k)
:= Vector.map2 (until n) iv.
Definition construct_trace (n : nat) (i : Input) : list State
:= proj1_sig (rooted_n_sem_steps n i).
Definition construct_trace_sync (sync : Input -> list State -> nat)
: Input -> nat -> nat
:= fun i n => sync i (construct_trace n i).
Lemma construct_trace_len (n : nat) (i : Input)
: | construct_trace n i | = n.
Proof.
clear d state0.
unfold construct_trace,rooted_n_sem_steps,n_sem_steps.
match goal with |- length (_ (match ?x with _=>_ end)) = _
=> destruct x
end.
destruct a.
cbn.
assumption.
Qed.
Lemma construct_trace_sem (n : nat) (i : Input)
: sem i (construct_trace n i).
Proof.
clear d state0.
unfold construct_trace,rooted_n_sem_steps,n_sem_steps.
match goal with |- sem i (_ (match ?x with _=>_ end))
=> destruct x
end.
destruct a.
cbn.
rewrite app_nil_r in s.
assumption.
Qed.
Lemma construct_trace_length i t
: sem i t -> construct_trace (length t) i = t.
clear.
intros.
specialize (construct_trace_sem (|t|) i) as Q.
specialize (construct_trace_len (|t|) i) as R.
eapply sem_leneq_eq;eauto.
Qed.
(* TODO Prove construct_sync_map2 if needed
Lemma construct_sync_map2 {k : nat} (f : Input -> list State -> nat)
: forall (iv xl : Vector.t _ k),
construct_sync (Vector.map2 f) iv xl = Vector.map2 (construct_trace_sync f) iv xl.
*)
End with_d.
End with_rad_sem.
End with_st.