lucid_ops.v
(* FILE: SAMPLED_STREAMS/lucid_ops.v _ Sylvain Boulmé _ LIP6 _ Spring 2001 *)
(* Coq V6.3.1 *)
Implicit Arguments On.
Require Export sampled_streams.
Section Constant_samplStr.
Variable A: Set.
Variable a: A.
Definition
elt_const: (b:bool)(samplElt A b)
:= [b]<(samplElt A)>if b then (Any a) else (None A).
CoFixpoint
sp_const : (c:clock)(samplStr A c)
:= [c](sp_cons (elt_const (hd c)) (sp_const (tl c))).
Lemma
elt_const_no_Fail: (b:bool)(is_no_Fail (elt_const b)).
Proof.
Intros b; Case b; Simpl; Auto.
Qed.
Hints Resolve elt_const_no_Fail: sampled_str.
Lemma
sp_wf_const:(c:clock)(sp_wf (sp_const c)).
Proof.
Cofix sp_wf_const; Constructor 1; Simpl; Auto with sampled_str.
Qed.
End Constant_samplStr.
Hints Resolve sp_wf_const: sampled_str sp_rec0.
Grammar command command1 :=
sp_const_ex [ "`" command($c) "`" ] -> [<<(sp_const $c ?)>>].
Section Mem_Less.
Variables A,B: Set.
CoInductive
mem_less: clock->clock->Set :=
ml_cons:
(c1,c2:clock)
((samplElt A (hd c1))->(samplElt B (hd c2)))
->(mem_less (tl c1) (tl c2))
->(mem_less c1 c2).
Definition
ml_hd :=
[c1,c2:clock; m: (mem_less c1 c2)]
<[c1,c2:clock; m: (mem_less c1 c2)](samplElt A (hd c1))->(samplElt B (hd c2))>
Cases m of (ml_cons _ _ f _) => f end.
Definition
ml_tl :=
[c1,c2:clock; m: (mem_less c1 c2)]
<[c1,c2:clock; m: (mem_less c1 c2)](mem_less (tl c1) (tl c2))>
Cases m of (ml_cons _ _ _ m') => m' end.
CoFixpoint
mem_less_apply: (c1,c2:clock)(mem_less c1 c2)->(samplStr A c1)->(samplStr B c2)
:= [c1,c2;m;x](sp_cons ((ml_hd m) (sp_hd x)) (mem_less_apply (ml_tl m) (sp_tl x))).
CoFixpoint
ml_const: ((b:bool)(samplElt A b)->(samplElt B b))->(c:clock)(mem_less c c)
:= [f; c](ml_cons (f (hd c)) (ml_const f (tl c))).
End Mem_Less.
Lemma
mem_less_id_def: (A:Set; c:clock; x:(samplStr A c))(sp_eq x (mem_less_apply (ml_const [b;a]a ?) x)).
Proof.
Cofix ml_id_def; Intros A c x; Constructor 1.
Simpl; Auto with eqD sampled_str.
Apply ml_id_def with x:=(sp_tl x).
Qed.
Hints Resolve mem_less_id_def:sampled_str.
Section Followed_By.
Variable A:Set.
(* Introduit l'elt dans le flot *)
CoFixpoint
sp_delay: (c:clock)(samplStr A c)->(samplElt A true)->(samplStr A c):=
[c]<[c0](samplStr A c0)->(samplElt A true)->(samplStr A c0)>
Cases c of (Cons hc tc) =>
<[b](samplStr A (Cons b tc))->(samplElt A true)->(samplStr A (Cons b tc))>
if hc
then
[x;a](sp_cons a (sp_delay (sp_tl x) (sp_hd x)))
else
[x;a](sp_cons (None A) (sp_delay (sp_tl x) a))
end.
Lemma
sp_delay_lfp:
(n:nat; c:clock; s1,s2:(samplStr A c); a1,a2:(samplElt A true))
(sp_inf n s1 s2)->
(flat_ord a1 a2)->
(sp_inf n (sp_delay s1 a1) (sp_delay s2 a2)).
Proof.
Intros n; Elim n; Simpl.
Intros c; Case c; Simpl; Intros b c'; Case b; Intros s1 s2 a1 a2 H1 H2;
Auto with sampled_str. Apply sp_inf_proof_O; Simpl; Auto.
Intros n0 HR c; Case c; Simpl; Intros b c'; Case b; Intros s1 s2 a1 a2 H1 H2;
Case (sp_inf_S_n_inv H1); Intros; Apply sp_inf_proof_S_n; Simpl; Auto with sampled_str.
Qed.
(*
Axiom flat_ord_true_false: (a1: (samplElt A true); a2: (samplElt A false))(flat_ord a1 a2).
Lemma sp_delay_lfp':
(n:nat; c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2); a1,a2:(samplElt A true))
(sp_inf n s1 s2)->
(flat_ord a1 a2)->(glob_nfstwf n s1)->
(sp_inf n (sp_delay s1 a1) (sp_delay s2 a2)).
Proof.
Intros n; Elim n; Simpl.
Intros c1 c2; Case c1; Case c2; Simpl; Intros b2 c2' b1 c1';
Case b1; Case b2; Intros s1 s2 a1 a2 H1 H2 H3; Apply sp_inf_proof_O; Simpl;
Auto. Apply flat_ord_true_false.
Generalize (flat_ord_inv_leb (sp_inf_O_inv H1)); Simpl; Intros H'; Discriminate H'.
Intros n0 HR c1 c2; Case c1; Case c2; Simpl; Intros b2 c2' b1 c1'; Case b1.
Case b2; Intros s1 s2 a1 a2 H1 H2 H3; Apply sp_inf_proof_S_n; Simpl; Auto.
Case (sp_inf_S_n_inv H1); Case H3; Auto.
Apply flat_ord_true_false.
Absurd true=false.
Intro H; Discriminate H;
Case H3; Case (sp_inf_S_n_inv H1); Pattern (sp_hd s1); Apply samplElt_true_inv; Simpl.
Intros a H4 h h0 h1; Exact (eq_dep_eq_param ? ? ? ? ? ? H4).
Contradiction.
Intros s1 s2 a1 a2 H1 H2 H3; Case (sp_inf_S_n_inv H1); Case H3;
Intros h1 h2 h3; Generalize (leb_false_2 (flat_ord_inv_leb h3)); Simpl;
Intro h4; Generalize s2 h3; Rewrite h4; Intros s2' h3' h5;
Apply sp_inf_proof_S_n; Simpl; Auto with sampled_str.
Qed.
*)
Lemma
sp_delay_loc_nfstwf:
(n:nat; c:clock; s:(samplStr A c); a:(samplElt A true))
(loc_nfstwf n s)->
(is_no_Fail a)->
(loc_nfstwf (S n) (sp_delay s a)).
Proof.
Cofix sp_delay_loc_nfstwf.
Intros n c; Case c; Intros b c'; Case b.
Intros s a H1 H2; Apply loc_nfstwf_true with s:=(sp_delay s a); Simpl; Auto.
Generalize H1; Case n; Auto with sampled_str.
Intros n' H1'; Apply sp_delay_loc_nfstwf.
Apply loc_nfstwf_S_n_true_inv with s:=s; Auto.
Apply loc_nfstwf_is_no_Fail with n:=n' s:=s; Auto.
Intros s a H1 H2; Apply loc_nfstwf_false with s:=(sp_delay s a); Simpl; Auto.
Apply sp_delay_loc_nfstwf; Auto.
Apply loc_nfstwf_false_inv with s:=s; Auto.
Qed.
(* sp_pre: décalage avec Fail *)
Definition
sp_pre: (c:clock)(samplStr A c)->(samplStr A c) :=
[c;s](sp_delay s (Fail A)).
CoFixpoint
sp_arrow : (c:clock)(samplStr A c)->(samplStr A c) -> (samplStr A c)
:= [c;x;y](sp_cons (sp_hd x)
(if (hd c)
then (sp_tl y)
else (sp_arrow (sp_tl x) (sp_tl y)))).
Definition
sp_fby := [c;x;y](sp_arrow 1!c x (sp_pre y)).
Lemma
sp_arrow_lfp:
(n:nat; c:clock; x1,x2:(samplStr A c); y1,y2:(samplStr A c))
(sp_inf n x1 x2)->
(sp_inf n y1 y2)->(sp_inf n (sp_arrow x1 y1) (sp_arrow x2 y2)).
Proof.
Intros n; Elim n; Simpl.
Intros c; Case c; Simpl; Intros b c'; Case b; Intros x1 x2 y1 y2 H1 H2;
Apply sp_inf_proof_O; Simpl; Auto with sampled_str; Apply sp_inf_O_inv with s1:=x1 s2:=x2; Auto.
Intros n0 HR c; Case c; Simpl; Intros b c'; Case b; Intros x1 x2 y1 y2 H1 H2;
Case (sp_inf_S_n_inv H1); Case (sp_inf_S_n_inv H2); Intros; Apply sp_inf_proof_S_n; Simpl; Auto.
Qed.
Lemma
sp_arrow_loc_nfstwf:
(n:nat; c:clock; x:(samplStr A c); y:(samplStr A c))
(loc_nfstwf n x)->
(loc_nfstwf n y)->
(loc_nfstwf n (sp_arrow x y)).
Proof.
Cofix sp_arrow_loc_nfstwf.
Intros n c; Case c; Simpl; Intros b c'; Case b; Intros x y.
Case n.
Intros H1 H2; Apply loc_nfstwf_O.
Intros m H1 H2; Apply loc_nfstwf_true; Simpl; Auto.
Apply loc_nfstwf_is_no_Fail with n:=m s:=x; Auto.
Apply loc_nfstwf_S_n_true_inv with n:=m s:=y; Simpl; Auto.
Intros H1 H2; Apply loc_nfstwf_false; Simpl; Auto.
Apply sp_arrow_loc_nfstwf.
Apply loc_nfstwf_false_inv with s:=x; Simpl; Auto.
Apply loc_nfstwf_false_inv with s:=y; Simpl; Auto.
Qed.
Lemma
sp_arrow_loc_nfstwf_1:
(c:clock; x:(samplStr A c); y:(samplStr A c))
(loc_nfstwf (S O) x)->
(loc_nfstwf (S O) (sp_arrow x y)).
Proof.
Cofix sp_arrow_loc_nfstwf_1.
Intros c; Case c; Simpl; Intros b c'; Case b; Intros x y H.
Apply loc_nfstwf_true; Simpl; Auto with sampled_str.
Apply loc_nfstwf_is_no_Fail with s:=x n:=O; Auto.
Apply loc_nfstwf_false; Simpl; Auto.
Apply sp_arrow_loc_nfstwf_1.
Apply loc_nfstwf_false_inv with s:=x; Simpl; Auto.
Qed.
Lemma
sp_arrow_ext2:
(c:clock ; x,y1,y2:(samplStr A c))
(sp_eq y1 y2)->(sp_eq (sp_arrow x y1) (sp_arrow x y2)).
Proof.
Cofix sp_arrow_ext2; Intros c; Case c; Simpl; Intros b c'; Case b; Simpl;
Constructor 1; Simpl; Auto with eqD sampled_str.
Case (sp_eq_inv H); Auto.
Apply sp_arrow_ext2; Case (sp_eq_inv H); Auto.
Qed.
Hints Resolve sp_delay_lfp sp_delay_loc_nfstwf: sampled_str.
CoFixpoint
sp_init_pre : (c:clock)(samplStr A c) -> (samplStr A c)
:= [c]<[c0](samplStr A c0)->(samplStr A c0)>
Cases c of (Cons hc tc) =>
<[b](samplStr A (Cons b tc))->(samplStr A (Cons b tc))>
if hc
then
[x](sp_delay x (sp_hd x))
else
[x](sp_cons (None A) (sp_init_pre (sp_tl x)))
end.
Lemma
sp_init_pre_lfp:
(n:nat; c:clock; x1,x2:(samplStr A c))
(sp_inf n x1 x2)->
(sp_inf n (sp_init_pre x1) (sp_init_pre x2)).
Proof.
Intros n; Elim n; Simpl.
Intros c; Case c; Simpl; Intros b c'; Case b; Intros x1 x2 H1;
Apply sp_inf_proof_O; Simpl; Auto with sampled_str; Apply sp_inf_O_inv with s1:=x1 s2:=x2; Auto.
Intros n0 HR c; Case c; Simpl; Intros b c'; Case b; Intros x1 x2 H1;
Case (sp_inf_S_n_inv H1); Intros; Apply sp_inf_proof_S_n; Simpl; Auto with sampled_str.
Qed.
Lemma
sp_init_pre_loc_nfstwf:
(n:nat; c:clock; x:(samplStr A c))
(loc_nfstwf (S n) x)->
(loc_nfstwf (S (S n)) (sp_init_pre x)).
Proof.
Cofix sp_init_pre_loc_nfstwf.
Intros n c; Case c; Simpl; Intros b c'; Case b; Intros x H.
Rewrite (unfold_samplStr (sp_init_pre x));
Change (loc_nfstwf (S (S n)) (sp_cons (sp_hd (sp_delay x (sp_hd x)))
(sp_tl (sp_delay x (sp_hd x)))));
Rewrite <- unfold_samplStr; Apply sp_delay_loc_nfstwf; Auto.
Apply loc_nfstwf_is_no_Fail with n:=n s:=x; Auto.
Apply loc_nfstwf_false; Simpl; Auto.
Apply sp_init_pre_loc_nfstwf.
Apply loc_nfstwf_false_inv with s:=x; Simpl; Auto.
Qed.
Hints Resolve sp_arrow_lfp sp_arrow_loc_nfstwf_1 sp_arrow_loc_nfstwf sp_arrow_ext2
sp_init_pre_lfp sp_init_pre_loc_nfstwf: sampled_str.
(*
CoFixpoint sp_waitfst : (c:clock)(samplStr A c) ->
((samplElt A true) -> (samplStr A c)) -> (samplStr A c)
:= [c]<[c0](samplStr A c0)->((samplElt A true)->(samplStr A c0))->(samplStr A c0)>
Cases c of (Cons hc tc) =>
<[b](samplStr A (Cons b tc))->((samplElt A true)->(samplStr A (Cons b tc)))
->(samplStr A (Cons b tc))>
if hc
then
[x;f](sp_cons (sp_hd x) (sp_tl (f (sp_hd x))))
else
[x;f](sp_cons (None A) (sp_waitfst (sp_tl x)
[a](sp_tl (f a))))
end.
Lemma sp_waitfst_lfp:
(n:nat; c:clock; s1,s2:(samplStr A c); g1,g2:((samplElt A true) -> (samplStr A c)))
(sp_inf n s1 s2)->
((a1,a2:(samplElt A true))(flat_ord a1 a2)->(sp_inf n (g1 a1) (g2 a2)))
->(sp_inf n (sp_waitfst s1 g1) (sp_waitfst s2 g2)).
Proof.
Intros n; Elim n; Simpl.
Intros c; Case c; Simpl; Intros b c'; Case b; Intros s1 s2 g1 g2 H1 H2;
Apply sp_inf_proof_O; Simpl; Auto with sampled_str.
Apply sp_inf_O_inv with s1:=s1 s2:=s2; Auto.
Intros n0 HR c; Case c; Simpl; Intros b c'; Case b; Intros s1 s2 g1 g2 H1 H2;
Case (sp_inf_S_n_inv H1); Intros H3 H4; Apply sp_inf_proof_S_n; Simpl; Auto.
Case (sp_inf_S_n_inv (H2 ? ? H3)); Auto.
Apply HR with g1:=[a:(samplElt A true)](sp_tl (g1 a))
g2:=[a:(samplElt A true)](sp_tl (g2 a)); Auto.
Intros a1 a2 H'; Case (sp_inf_S_n_inv (H2 ? ? H')); Auto.
Qed.
Lemma sp_waitfst_loc_nfstwf:
(n:nat; c:clock; s:(samplStr A c); g:((samplElt A true)->(samplStr A c)))
(loc_nfstwf n s)->
((a:(samplElt A true))(is_no_Fail a)->(loc_nfstwf n (g a)))
->(loc_nfstwf n (sp_waitfst s g)).
Proof.
Cofix sp_waitfst_loc_nfstwf.
Intros n c; Case c; Simpl; Intros b c'; Case b; Intros s g.
Case n.
Intros H1 H2; Apply loc_nfstwf_O.
Intros m H1 H2; Apply loc_nfstwf_true; Simpl; Auto.
Apply loc_nfstwf_is_no_Fail with n:=m s:=s; Auto.
Apply loc_nfstwf_S_n_true_inv with n:=m s:=(g (sp_hd s)); Simpl; Auto.
Apply H2; Apply loc_nfstwf_is_no_Fail with n:=m s:=s; Auto.
Intros H1 H2; Apply loc_nfstwf_false; Simpl; Auto.
Apply sp_waitfst_loc_nfstwf.
Apply loc_nfstwf_false_inv with s:=s; Simpl; Auto.
Intros a H3; Apply loc_nfstwf_false_inv with s:=(g a); Auto.
Qed.
Hints Resolve sp_waitfst_lfp sp_waitfst_loc_nfstwf: sampled_str.
Lemma sp_arrow_waitfst_equiv: (c:clock; x,y:(samplStr A c))
(sp_eq (sp_arrow x y) (sp_waitfst x [_]y)).
Cofix sp_arrow_waitfst_equiv; Intros c; Case c; Simpl; Intros b c'; Case b;
Constructor 1; Simpl; Auto with eqD sampled_str.
Pattern (sp_hd x); Apply samplElt_false_inv; Simpl; Auto with eqD.
Qed.
Hints Resolve sp_arrow_waitfst_equiv: sampled_str.
Hints Resolve sp_pre_elimination:sampled_str.
Lemma sp_waitfst_ext2:
(c:clock ; x:(samplStr A c); g1,g2: (samplElt A true) -> (samplStr A c))
((a:(samplElt A true))(sp_eq (g1 a) (g2 a)))
->(sp_eq (sp_waitfst x g1) (sp_waitfst x g2)).
Proof.
Cofix sp_waitfst_ext2; Intros c; Case c; Simpl; Intros b c'; Case b; Simpl;
Constructor 1; Simpl; Auto with eqD sampled_str.
Case (sp_eq_inv (H (sp_hd x))); Auto.
Apply sp_waitfst_ext2; Intros a; Case (sp_eq_inv (H a)); Auto.
Qed.
*)
End Followed_By.
Section Pre_elimination.
Variable A,B: Set.
Theorem
sp_pre_elimination:
(c1,c2:clock; g:(mem_less A B c1 c2); x:(samplStr B c2); y:(samplStr A c1);
a:A)
(clock_inf c2 c1)->
(sp_eq
(sp_arrow x (mem_less_apply g (sp_pre y)))
(sp_arrow x (mem_less_apply g (sp_delay y (Any a))))).
Proof.
Unfold sp_pre; Cofix sp_pre_elimination; Intros c1 c2; Case c2; Simpl; Intros b2 c2';
Case b2; Intros g x y a H; Constructor 1; Try (Simpl; Auto with eqD; Fail).
Case (clock_inf_inv H); Intros H1 H2; Simpl in H1;
Generalize g y; Rewrite (unfold_Str c1); Rewrite H1; Simpl.
Intros; Apply sp_eq_refl.
Generalize g y H ; Case c1; Intros hc1 tc1; Case hc1;
Intros g' y' H'; Simpl.
Apply sp_eq_refl.
Apply sp_pre_elimination with x:=(sp_tl x) g:=(ml_tl g') y:=(sp_tl y').
Simpl; Case (clock_inf_inv H'); Auto.
Qed.
Lemma
pre_init_pre:
(c1,c2:clock; g:(mem_less A B c1 c2); x:(samplStr B c2); y:(samplStr A c1))
(clock_inf c2 c1)->
(sp_eq
(sp_arrow x (mem_less_apply g (sp_pre y)))
(sp_arrow x (mem_less_apply g (sp_init_pre y)))).
Proof.
Unfold sp_pre; Cofix pre_init_pre; Intros c1 c2; Case c2; Simpl; Intros b2 c2';
Case b2; Intros g x y H; Constructor 1; Try (Simpl; Auto with eqD; Fail).
Case (clock_inf_inv H); Intros H1 H2; Simpl in H1;
Generalize g y; Rewrite (unfold_Str c1); Rewrite H1; Simpl.
Intros; Apply sp_eq_refl.
Generalize g y H ; Case c1; Intros hc1 tc1; Case hc1;
Intros g' y' H'; Simpl.
Apply sp_eq_refl.
Apply pre_init_pre with x:=(sp_tl x) g:=(ml_tl g') y:=(sp_tl y').
Simpl; Case (clock_inf_inv H'); Auto.
Qed.
End Pre_elimination.
Section Delays_prop.
Variable A: Set.
Hints Resolve sp_arrow_lfp sp_arrow_loc_nfstwf_1 sp_arrow_loc_nfstwf sp_arrow_ext2
sp_init_pre_lfp sp_init_pre_loc_nfstwf: sampled_str.
Hints Resolve pre_init_pre:sampled_str.
Lemma
sp_fby_equiv:
(c:clock; x,y:(samplStr A c))
(sp_eq (sp_fby x y) (sp_arrow x (sp_init_pre y))).
Proof.
Unfold sp_fby; Intros c x y;
Apply sp_eq_trans with
s2:=(sp_arrow x (mem_less_apply (ml_const [b;a]a ?) (sp_pre y)));
Auto with sampled_str.
Apply sp_eq_trans with
s2:=(sp_arrow x (mem_less_apply (ml_const [b;a]a ?) (sp_init_pre y)));
Auto with sampled_str.
Qed.
Hints Resolve sp_fby_equiv: sampled_str.
Lemma
sp_fby_lfp:
(n:nat; c:clock; x1,x2,y1,y2:(samplStr A c))
(sp_inf n x1 x2)->
(sp_inf n y1 y2)->
(sp_inf n (sp_fby x1 y1) (sp_fby x2 y2)).
Proof.
Intros n c x1 x2 y1 y2 H1 H2.
Apply sp_inf_trans with s2:=(sp_arrow x1 (sp_init_pre y1));
Auto with sampled_str.
Apply sp_inf_trans with s2:=(sp_arrow x2 (sp_init_pre y2));
Auto with sampled_str.
Qed.
Lemma
sp_fby_loc_nfstwf:
(n:nat; c:clock; x,y:(samplStr A c))
(loc_nfstwf (S n) x)->
(loc_nfstwf n y)->
(loc_nfstwf (S n) (sp_fby x y)).
Proof.
Intros n c x y H1 H2.
Apply loc_nfstwf_sp_eq with s1:=(sp_arrow x (sp_init_pre y));
Auto with sampled_str.
Generalize H1 H2; Case n; Simpl; Auto with sampled_str.
Qed.
Lemma
sp_fby_glob_nfstwf:
(n:nat; c:clock; x,y:(samplStr A c))
(glob_nfstwf (S n) x)->
(glob_nfstwf n y)->
(glob_nfstwf (S n) (sp_fby x y)).
Proof.
Intros n c x y H1 H2;
Apply nfstwf_function_convert_S with f:=[y](sp_fby x y) n:=n; Auto.
Intros m y' H3 H4; Apply sp_fby_loc_nfstwf; Auto with sampled_str.
Rewrite <- (loc2glob_prop 1!c 2!(S m) 3!(S n)); Auto.
Apply glob_nfstwf_loc_nfstwf; Apply glob_nfstwf_n_le with n:=(S n);
Auto with sampled_str.
Qed.
End Delays_prop.
(* Concrete syntax a la lucid *)
Infix RIGHTA 7 "fby" sp_fby.
Infix RIGHTA 7 "-->" sp_arrow.
Syntactic Definition
pre := [x](sp_pre x).
Section Extend.
Variables A,B: Set.
(*
Definition elt_extend: (b:bool)(samplElt A->B b)->(samplElt A b)->(samplElt B b)
:= [b; f]
<[b; _:(samplElt A->B b)](samplElt A b)->(samplElt B b)>
Cases f of
None => [_](None B)
| (Any vf) =>
[x](samplElt_true_invS 2
(* Any *) [vx](Any (vf vx))
(* Fail *) (Fail B)
x)
| Fail => [_](Fail ?)
end.
*)
Definition
elt_extend: (b:bool)(samplElt A->B b)->(samplElt A b)->(samplElt B b)
:= [b; f]
<[b; _:(samplElt A->B b)](samplElt A b)->(samplElt B b)>
Cases f of
| None => [_](None B)
| (Any vf) =>
[x]Cases x of
| (Any vx) => (Any (vf vx))
| Fail => (Fail ?)
| None => (Fail ?) (* unused case *)
end
| Fail => [_](Fail ?)
end.
Lemma
elt_extend_lfp:
(b1,b2:bool; f1:(samplElt A->B b1); f2:(samplElt A->B b2);
s1:(samplElt A b1); s2:(samplElt A b2))
(flat_ord f1 f2)->
(flat_ord s1 s2)->
(flat_ord (elt_extend f1 s1) (elt_extend f2 s2)).
Proof.
Intros b1 b2 f1 f2; Case f1; Case f2; Simpl; Auto.
Intros f s1 s2 H; Inversion H.
Intros s1 s2 H; Inversion H.
Intros f s1 s2 H; Inversion H.
Intros f1' f2' s1 s2 H1; Generalize (eq_dep_eq ? ? ? ? ? H1); Intro H2; Injection H2;
Intro H3; Rewrite H3; Pattern s1; Apply samplElt_true_inv;
Pattern s2; Apply samplElt_true_inv; Simpl; Auto.
Intros x y H1'; Generalize (eq_dep_eq ? ? ? ? ? H1'); Intro H2'; Injection H2';
Intro H3'; Rewrite H3'; Simpl; Auto.
Intros x H; Inversion H.
Intros f s1 s2 H; Inversion H.
Qed.
Lemma
elt_extend_is_no_Fail:
(b:bool; f:(samplElt A->B b); s:(samplElt A b))
(is_no_Fail f)->
(is_no_Fail s)->
(is_no_Fail (elt_extend f s)).
Proof.
Intros b f; Case f; Simpl; Auto.
Intros f' s; Inversion s using samplElt_true_inv;
Simpl; Auto.
Qed.
Hints Resolve elt_extend_lfp elt_extend_is_no_Fail: sampled_str.
(* extend: flot de fonctions => fonction de flots *)
CoFixpoint
sp_extend :
(c:clock)(samplStr A->B c)->(samplStr A c)->(samplStr B c)
:=
[c:clock;f;x]
(sp_cons (elt_extend (sp_hd f) (sp_hd x)) (sp_extend (sp_tl f) (sp_tl x))).
Require Refine.
Lemma
sp_extend_const:
(c:clock; f:A->B; x:A)(sp_eq (sp_extend (sp_const f c) (sp_const x c))
(sp_const (f x) c)).
Proof.
Cofix sp_extend_const.
Intros; Constructor 1.
Simpl; Case (hd c); Auto with eqD.
Refine (sp_extend_const ? ? ?).
Qed.
Lemma
sp_extend_lfp:
(n:nat; c1,c2:clock; f1:(samplStr A->B c1); f2:(samplStr A->B c2);
s1:(samplStr A c1); s2:(samplStr A c2))
(sp_inf n f1 f2)->
(sp_inf n s1 s2)->
(sp_inf n (sp_extend f1 s1) (sp_extend f2 s2)).
Proof.
Intros n; Elim n; Simpl.
Intros; Apply sp_inf_proof_O; Simpl; Auto with sampled_str.
Intros n0 HR c1 c2 f1 f2 s1 s2 H H0; Case (sp_inf_S_n_inv H);
Case (sp_inf_S_n_inv H0); Intros; Apply sp_inf_proof_S_n;
Simpl; Auto with sampled_str.
Qed.
Lemma
sp_extend_loc_nfstwf:
(n:nat; c:clock; f:(samplStr A->B c); s:(samplStr A c))
(loc_nfstwf n f)->
(loc_nfstwf n s)->
(loc_nfstwf n (sp_extend f s)).
Proof.
Cofix sp_extend_loc_nfstwf.
Intros n c f s; Case (eq_false_dec (hd c)); Intros H1.
Intros; Apply loc_nfstwf_false; Simpl; Auto.
Apply sp_extend_loc_nfstwf; Apply loc_nfstwf_false_inv; Auto.
Case n.
Intros; Apply loc_nfstwf_O.
Intros; Apply loc_nfstwf_true; Simpl; Auto.
Apply elt_extend_is_no_Fail; Apply loc_nfstwf_is_no_Fail with n:=n0; Auto.
Apply sp_extend_loc_nfstwf; Apply loc_nfstwf_S_n_true_inv; Auto.
Qed.
Hints Resolve sp_extend_lfp sp_extend_loc_nfstwf: sampled_str.
Lemma
sp_extend_glob_nfstwf:
(n:nat; c:clock; f:(samplStr A->B c); s:(samplStr A c))
(glob_nfstwf n f)->
(glob_nfstwf n s)->
(glob_nfstwf n (sp_extend f s)).
Proof.
Intros n c f s H1 H2;
Apply nfstwf_function_convert with f:=[s](sp_extend f s) n:=n; Auto.
Intros m s' H3 H4; Apply sp_extend_loc_nfstwf; Auto.
Rewrite <- (loc2glob_prop 1!c 2!m 3!n); Auto.
Apply glob_nfstwf_loc_nfstwf; Apply glob_nfstwf_n_le with n:=n; Auto
with sampled_str.
Qed.
Lemma
sp_extend_wf:
(c:clock; f:(samplStr A->B c); s:(samplStr A c))
(sp_wf f)->
(sp_wf s)->
(sp_wf (sp_extend f s)).
Proof.
Auto with sampled_str.
Qed.
CoFixpoint
ml_extend1 :
(c:clock)(samplStr A c)->(mem_less A->B B c c)
:=
[c:clock;x](ml_cons [hf](elt_extend hf (sp_hd x)) (ml_extend1 (sp_tl x))).
Lemma
sp_extend_mem_less1:(c:clock; f:(samplStr A->B c); s:(samplStr A c))
(sp_eq (sp_extend f s) (mem_less_apply (ml_extend1 s) f)).
Proof.
Cofix sp_extend_mem_less. Intros c f s; Constructor 1; Simpl; Auto with eqD sampled_str.
Qed.
CoFixpoint
ml_extend2 :
(c:clock)(samplStr A->B c)->(mem_less A B c c)
:=
[c:clock;f](ml_cons (elt_extend (sp_hd f)) (ml_extend2 (sp_tl f))).
Lemma
sp_extend_mem_less2:(c:clock; f:(samplStr A->B c); s:(samplStr A c))
(sp_eq (sp_extend f s) (mem_less_apply (ml_extend2 f) s)).
Proof.
Cofix sp_extend_mem_less. Intros c f s; Constructor 1; Simpl; Auto with eqD sampled_str.
Qed.
End Extend.
Hints Resolve sp_extend_lfp sp_extend_wf: sampled_str sp_rec0.
Hints Resolve sp_extend_loc_nfstwf: sampled_str.
Syntactic Definition
ext := [x,y](sp_extend x y).
Section Extend_prop.
Lemma
sp_extend_id:(A:Set; c:clock; f: A->A; x:(samplStr A c))
((z:A)(f z)=z) -> (sp_eq (sp_extend (sp_const f c) x) x).
Proof.
Intros A; Cofix sp_extend_id.
Intros c f x H; Constructor 1.
Simpl; Case (sp_hd x); Simpl; Intros; Try (Rewrite H); Auto with eqD.
Refine (sp_extend_id ? ? ? ?); Auto.
Qed.
Lemma
sp_extend_comp: (A,B,C:Set; c:clock; f:A->B; g:B->C; h:A->C; x:(samplStr A c))
((z:A)(g (f z))=(h z)) ->
(sp_eq (sp_extend (sp_const g c) (sp_extend (sp_const f c) x))
(sp_extend (sp_const h c) x)).
Proof.
Intros A B C; Cofix sp_extend_comp.
Intros c f g h x H; Constructor 1.
Simpl; Case (sp_hd x); Simpl; Intros; Try (Rewrite H); Auto with eqD.
Refine (sp_extend_comp ? ? ? ? ? ?); Auto.
Qed.
Variable A: Set.
Hints Resolve sp_extend_mem_less2 pre_init_pre sp_arrow_ext2
sp_arrow_lfp sp_arrow_loc_nfstwf: sampled_str.
Hints Resolve sp_init_pre_lfp sp_init_pre_loc_nfstwf: sampled_str.
Hints Resolve sp_arrow_loc_nfstwf_1: sampled_str.
Lemma
sp_arrow_extend2_pre_equiv:
(c:clock; f:(samplStr A->A c); x,y:(samplStr A c))
(sp_eq (sp_arrow x (sp_extend f (sp_pre y)))
(sp_arrow x (sp_extend f (sp_init_pre y)))).
Proof.
Intros c f x y;
Apply sp_eq_trans with
s2:=(sp_arrow x (mem_less_apply (ml_extend2 f) (sp_pre y)));
Auto with sampled_str.
Apply sp_eq_trans with
s2:=(sp_arrow x (mem_less_apply (ml_extend2 f) (sp_init_pre y)));
Auto with sampled_str.
Qed.
Hints Resolve sp_arrow_extend2_pre_equiv: sampled_str.
Lemma
sp_arrow_extend2_pre_lfp:
(n:nat; c:clock; f:(samplStr A->A c); x,y1,y2:(samplStr A c))
(sp_inf n y1 y2)->
(sp_inf n (sp_arrow x (sp_extend f (sp_pre y1)))
(sp_arrow x (sp_extend f (sp_pre y2)))).
Proof.
Intros n c f x y1 y2 H1.
Apply sp_inf_trans with s2:=(sp_arrow x (sp_extend f (sp_init_pre y1)));
Auto with sampled_str.
Apply sp_inf_trans with s2:=(sp_arrow x (sp_extend f (sp_init_pre y2)));
Auto with sampled_str.
Qed.
Lemma
sp_arrow_extend2_pre_loc_nfstwf:
(n:nat; c:clock; f:(samplStr A->A c); x,y:(samplStr A c))
(sp_wf f)->
(sp_wf x)->
(loc_nfstwf n y)->
(loc_nfstwf (S n) (sp_arrow x (sp_extend f (sp_pre y)))).
Proof.
Intros n c f x y H1 H2 H3.
Apply loc_nfstwf_sp_eq with s1:=(sp_arrow x (sp_extend f (sp_init_pre y)));
Auto with sampled_str.
Generalize H3; Case n; Simpl; Auto with sampled_str.
Qed.
Lemma
sp_arrow_extend2_pre_glob_nfstwf:
(n:nat; c:clock; f:(samplStr A->A c); x,y:(samplStr A c))
(sp_wf f)->
(sp_wf x)->
(glob_nfstwf n y)->
(glob_nfstwf (S n) (sp_arrow x (sp_extend f (sp_pre y)))).
Proof.
Intros n c f x y H1 H2 H3.
Apply rec0_nfstwf_inc_loc2glob with
f:=[y](sp_arrow x (sp_extend f (sp_pre y))); Auto.
Intros; Apply sp_arrow_extend2_pre_loc_nfstwf; Auto.
Qed.
End Extend_prop.
Section IsFstValue.
Variable A: Set.
Variable a:A.
CoInductive
is_fst_value: (c:clock)(samplStr A c)->Prop :=
| is_fst_value_false:
(c:clock; s:(samplStr A c))
(hd c)=false -> (is_fst_value (sp_tl s))->(is_fst_value s)
| is_fst_value_true:
(c:clock; s:(samplStr A c))
(sp_hd s)==<(samplElt A)>(Any a)->(is_fst_value s).
Lemma
is_fst_value_false_inv:
(c: clock; s:(samplStr A c))
(hd c)=false ->
(is_fst_value s) -> (is_fst_value (sp_tl s)).
Proof.
Intros c s H1 H2; Generalize H1; Case H2; Simpl; Auto.
Intros c' s' H3; Rewrite (eq_dep_eq_param ? ? ? ? ? ? H3).
Intros H'; Discriminate H'.
Qed.
Lemma
is_fst_value_true_inv:
(c: clock; s:(samplStr A c))
(hd c)=true ->
(is_fst_value s) -> (sp_hd s)==<(samplElt A)>(Any a).
Proof.
Intros c s H1 H2; Generalize H1; Case H2; Simpl; Auto.
Intros c' s' H3 H4 H5; Rewrite H3 in H5; Discriminate H5.
Qed.
Lemma
is_fst_value_sp_eq:
(c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
(sp_eq s1 s2)->(is_fst_value s1)->(is_fst_value s2).
Proof.
Cofix is_fst_value_sp_eq.
Intros c1 c2 s1 s2 H1 H2; Case (eq_false_dec (hd c2)).
Intros H3; Apply is_fst_value_false; Auto.
Apply is_fst_value_sp_eq with s1:=(sp_tl s1).
Case H1; Auto.
Apply is_fst_value_false_inv; Auto.
Rewrite <- H3; Case (EqSt_inv (sp_eq_EqSt_clock H1)); Auto.
Intros H3; Apply is_fst_value_true.
Pattern (hd c2) (sp_hd s2); Apply eq_dep_ind_l with x:=(sp_hd s1).
Apply is_fst_value_true_inv; Auto.
Rewrite <- H3; Case (EqSt_inv (sp_eq_EqSt_clock H1)); Auto.
Case H1; Auto.
Qed.
Lemma
is_fst_value_const: (c:clock)(is_fst_value (sp_const a c)).
Proof.
Cofix is_fst_value_const; Intros c; Case (eq_false_dec (hd c)).
Intros H; Apply is_fst_value_false; Simpl; Auto.
Intros H; Apply is_fst_value_true; Simpl; Auto.
Rewrite H; Simpl; Auto.
Qed.
Lemma
is_fst_value_sp_arrow: (c:clock; x,y:(samplStr A c))
(is_fst_value x)->(is_fst_value (sp_arrow x y)).
Proof.
Cofix is_fst_value_sp_arrow; Intros c; Case c; Intros b c'; Case b; Simpl.
Intros x y H; Apply is_fst_value_true; Simpl.
Apply is_fst_value_true_inv with s:=x; Auto.
Intros x y H; Apply is_fst_value_false; Simpl; Auto.
Apply is_fst_value_sp_arrow;
Apply is_fst_value_false_inv with s:=x; Simpl; Auto.
Qed.
End IsFstValue.
Hints Resolve is_fst_value_const is_fst_value_sp_arrow: sampled_str.
Section Sampling.
Definition
sp_not := [c:clock](sp_extend (sp_const negb c)).
Lemma
sp_not2_id:(c:clock; lc:(samplStr bool c))
(sp_eq (sp_not (sp_not lc)) lc).
Proof.
Intros c lc; Unfold sp_not;
Apply sp_eq_trans with s2:=(sp_extend (sp_const [z](negb (negb z)) c) lc).
EApply sp_extend_comp; EAuto.
Apply sp_extend_id; Intros b; Case b; Auto.
Qed.
Definition
elt_on: (b:bool)(samplElt bool b)->bool
:= [b;o]
Cases o of
None => false
| (Any x) => x
| Fail => true
end.
(*
Lemma elt_on_eq_false:(b:bool; x:(samplElt bool b))
(elt_on x)=false -> x==<(samplElt bool)>(None bool) \/ x==<(samplElt bool)>(Any false).
Proof.
Intros b x; Case x; Simpl; Auto with eqD.
Intros b0; Case b0; Auto with eqD.
Intros H; Discriminate H.
Intros H; Discriminate H.
Qed.
Lemma elt_on_eq_false_weak:(b:bool; x:(samplElt bool b))
(elt_on x)=false -> b=false \/ x==<(samplElt bool)>(Any false).
Proof.
Intros b x; Case x; Simpl; Auto with eqD.
Intros b0; Case b0; Auto with eqD.
Qed.
*)
Lemma
elt_on_eq_true:(b:bool; x:(samplElt bool b))
(elt_on x)=true -> x==<(samplElt bool)>(Any true) \/ x==<(samplElt bool)>(Fail bool).
Proof.
Intros b x; Case x; Simpl; Auto with eqD.
Intros H; Discriminate H.
Intros b0; Case b0; Auto with eqD.
Intros H; Discriminate H.
Qed.
Lemma
elt_on_eq_true_weak:(b:bool; x:(samplElt bool b))
(elt_on x)=true -> b=true.
Proof.
Intros b x; Case x; Simpl; Auto.
Qed.
Lemma
elt_on_false:(b:bool; x:(samplElt bool b))
b=false -> (elt_on x)=false.
Proof.
Intros b x; Case x; Simpl; Auto.
Intros b' H; Discriminate H.
Qed.
Hints Resolve elt_on_false: sp_aux.
CoFixpoint
sp_on: (c:clock)(samplStr bool c) -> clock
:= [c;lc](Cons (elt_on (sp_hd lc)) (sp_on (sp_tl lc))).
Lemma
sp_on_clock_inf:(c:clock; lc:(samplStr bool c))
(clock_inf (sp_on lc) c).
Proof.
Cofix sp_on_clock_inf; Intros c lc; Constructor 1; Simpl; Auto.
Case (sp_hd lc); Simpl; Auto. Intros b; Case b; Simpl; Auto.
Qed.
Variable A: Set.
Definition
elt_merge:
(b:bool; o:(samplElt bool b))
(samplElt A (elt_on o))
->(samplElt A (elt_on (elt_extend (elt_const negb b) o)))->(samplElt A b)
:=[b;o]
<[b;o](samplElt A (elt_on o))
->(samplElt A (elt_on (elt_extend (elt_const negb b) o)))->(samplElt A b)>
Cases o of
None => [x; y](None ?)
| (Any b0) =>
<[b](samplElt A b)->(samplElt A (negb b))->(samplElt A true)>
if b0 then [x; y]x else [x; y]y
| Fail => [x;y](Fail ?)
end.
Lemma
elt_merge_lfp:
(b1,b2:bool; o1:(samplElt bool b1); o2: (samplElt bool b2);
x1:(samplElt A (elt_on o1)); x2:(samplElt A (elt_on o2));
y1: (samplElt A (elt_on (elt_extend (elt_const negb ?) o1)));
y2: (samplElt A (elt_on (elt_extend (elt_const negb ?) o2))))
(flat_ord o1 o2) ->
(flat_ord x1 x2)->
(flat_ord y1 y2)->
(flat_ord (elt_merge x1 y1) (elt_merge x2 y2)).
Proof.
Intros b1 b2 o1 o2; Case o1; Case o2; Simpl; Auto; Clear o1 b1 o2 b2.
Intros b x1 x2 y1 y2 H; Inversion H.
Intros x1 x2 y1 y2 H; Inversion H.
Intros b x1 x2 y1 y2 H; Inversion H.
Intros b1 b2 x1 x2 y1 y2 H1; Generalize (eq_dep_eq ? ? ? ? ? H1); Intros H2;
Injection H2; Intro H3; Generalize x1 y1 x2 y2; Rewrite H3; Case b1; Simpl; Auto.
Intros b x1 x2 y1 y2 H1; Inversion H1.
Qed.
Lemma
elt_merge_is_no_Fail:
(b:bool; o:(samplElt bool b); x:(samplElt A (elt_on o));
y: (samplElt A (elt_on (elt_extend (elt_const negb b) o))))
(is_no_Fail o)->
(is_no_Fail x)->
(is_no_Fail y)->
(is_no_Fail (elt_merge x y)).
Proof.
Intros b o; Case o; Simpl; Auto; Clear o b.
Intros b x1; Case x1; Simpl; Auto.
Qed.
Lemma
elt_merge_true:
(b:bool; o:(samplElt bool b); x:(samplElt A (elt_on o));
y: (samplElt A (elt_on (elt_extend (elt_const negb b) o))))
o==<(samplElt bool)>(Any true)
->(is_no_Fail x)->
(is_no_Fail (elt_merge x y)).
Proof.
Intros b o x y H; Generalize x y;
Pattern b o; Apply eq_dep_ind_l with x:=(Any true); Simpl; Auto with eqD.
Qed.
Hints Resolve elt_merge_lfp elt_merge_is_no_Fail: sampled_str.
CoFixpoint
sp_merge :
(c:clock; lc:(samplStr bool c))
(samplStr A (sp_on lc))
->(samplStr A (sp_on (sp_not lc)))
->(samplStr A c)
:= [c;lc;x;y](sp_cons (elt_merge (sp_hd x) (sp_hd y))
(sp_merge (sp_tl x) (sp_tl y))).
Lemma
sp_merge_lfp:
(n:nat; c1,c2:clock; lc1:(samplStr bool c1); lc2: (samplStr bool c2);
s1:(samplStr A (sp_on lc1)); s2:(samplStr A (sp_on lc2));
t1:(samplStr A (sp_on (sp_not lc1))); t2:(samplStr A (sp_on (sp_not lc2))))
(sp_inf n lc1 lc2) ->
(sp_inf n s1 s2)->
(sp_inf n t1 t2)->
(sp_inf n (sp_merge s1 t1) (sp_merge s2 t2)).
Proof.
Intros n; Elim n; Simpl.
Intros; Apply sp_inf_proof_O; Simpl; Apply elt_merge_lfp; Auto with sampled_str.
Apply sp_inf_O_inv with c1:=(sp_on lc1) c2:=(sp_on lc2); Auto.
Apply sp_inf_O_inv with c1:=(sp_on (sp_not lc1)) c2:=(sp_on (sp_not lc2)); Auto.
Intros n0 HR c1 c2 lc1 lc2 x1 x2 s1 s2 H H0 H1; Case (sp_inf_S_n_inv H);
Case (sp_inf_S_n_inv H0); Case (sp_inf_S_n_inv H1); Intros; Apply sp_inf_proof_S_n; Simpl;
Auto with sampled_str.
Qed.
Hints Resolve locle_O locle_S_false_false locle_S_false_true
locle_S_true_true: sp_aux.
Hints Resolve loc_nfstwf_O loc_nfstwf_false_inv loc_nfstwf_S_n_n_tl: sp_aux.
Lemma
sp_merge_loc_nfstwf:
(n:nat; c:clock; lc:(samplStr bool c); s:(samplStr A (sp_on lc));
t:(samplStr A (sp_on (sp_not lc))))
(loc_nfstwf n lc)->
((m:nat)(locle m n (sp_on lc) c)->(loc_nfstwf m s))
->((m:nat)(locle m n (sp_on (sp_not lc)) c) -> (loc_nfstwf m t))
-> (loc_nfstwf n (sp_merge s t)).
Proof.
Cofix sp_merge_loc_nfstwf.
Intros n; Case n.
Intros; Apply loc_nfstwf_O.
Intros n0 c lc s t H1 H2 H3; Case (eq_false_dec (hd c)).
Intros H4; Apply loc_nfstwf_false; Simpl; Auto.
Apply sp_merge_loc_nfstwf; Auto with sp_aux.
Intros; Apply loc_nfstwf_false_inv with s:=s; Simpl; Auto with sp_aux.
Apply H2; Apply locle_S_false_false; Simpl; Auto with sp_aux.
Intros; Apply loc_nfstwf_false_inv with s:=t; Simpl; Auto with sp_aux.
Apply H3; Apply locle_S_false_false; Simpl; Auto with sp_aux.
Intros H4; Apply loc_nfstwf_true; Simpl; Auto.
Apply elt_merge_is_no_Fail.
Apply loc_nfstwf_is_no_Fail with n:=n0; Auto.
Case (eq_false_dec (elt_on (sp_hd lc))).
Generalize (sp_hd s); Simpl; Generalize (elt_on (sp_hd lc));
Intros b x H5; Generalize x; Rewrite H5;
Intros y; Pattern y; Apply samplElt_false_inv; Simpl; Auto.
Intros H5; Apply loc_nfstwf_is_no_Fail with n:=O s:=s; Auto with sp_aux.
Case (eq_false_dec (elt_on (sp_hd (sp_not lc)))).
Generalize (sp_hd t); Simpl;
Generalize (elt_on (elt_extend (elt_const negb (hd c)) (sp_hd lc)));
Intros b x H5; Generalize x; Rewrite H5;
Intros y; Pattern y; Apply samplElt_false_inv; Simpl; Auto.
Simpl; Intros H5; Apply loc_nfstwf_is_no_Fail with n:=O s:=t; Auto with sp_aux.
Apply sp_merge_loc_nfstwf; Auto with sp_aux.
Intros m H5; Case (eq_false_dec (elt_on (sp_hd lc))).
Intros; Apply loc_nfstwf_false_inv with s:=s; Auto with sp_aux.
Intros; Apply loc_nfstwf_S_n_n_tl with s:=s; Auto with sp_aux.
Intros m H5; Case (eq_false_dec (elt_on (sp_hd (sp_not lc)))).
Intros H6; Apply loc_nfstwf_false_inv with s:=t; Auto with sp_aux.
Simpl; Intros; Apply loc_nfstwf_S_n_n_tl with s:=t; Simpl; Auto with sp_aux.
Qed.
Lemma
sp_merge_glob_nfstwf:
(n:nat; c:clock; lc:(samplStr bool c); s:(samplStr A (sp_on lc));
t:(samplStr A (sp_on (sp_not lc))))
(glob_nfstwf n lc)->
(glob_nfstwf n s)->
(glob_nfstwf n t)->
(glob_nfstwf n (sp_merge s t)).
Proof.
Intros n c lc s t H1 H2 H3;
Apply nfstwf_function_convert_inf with
f:=[t](sp_merge s t) n:=n; Auto.
Intros m t' H4 H5; Apply sp_merge_loc_nfstwf; Auto.
Rewrite <- (loc2glob_prop 1!c 2!m 3!n); Auto.
Apply glob_nfstwf_loc_nfstwf.
Apply glob_nfstwf_n_le with n:=n; Auto with sampled_str.
Intros m' H6; Rewrite <- (loc2glob_prop 1!(sp_on lc) 2!m' 3!n); Auto.
Apply glob_nfstwf_loc_nfstwf;
Apply glob_nfstwf_n_le with n:=n; Auto with sampled_str.
Apply locle_glob2loc_trans with n2:=m c2:=c; Auto.
Qed.
Lemma
sp_merge_loc_nfstwf_weak:
(n:nat; c:clock; lc:(samplStr bool c); s:(samplStr A (sp_on lc));
t:(samplStr A (sp_on (sp_not lc))))
(loc_nfstwf n lc)->
(loc_nfstwf n s)->
(loc_nfstwf n t)->
(loc_nfstwf n (sp_merge s t)).
Proof.
Cofix sp_merge_loc_nfstwf_weak.
Intros n; Case n.
Intros; Apply loc_nfstwf_O.
Intros n0 c lc s t H1 H2 H3; Case (eq_false_dec (hd c)).
Intros H4; Apply loc_nfstwf_false; Simpl; Auto.
Apply sp_merge_loc_nfstwf_weak.
Apply loc_nfstwf_false_inv ; Simpl; Auto.
Apply loc_nfstwf_false_inv with s:=s; Simpl; Auto.
Generalize (sp_hd lc); Rewrite H4; Intros s';
Pattern s'; Apply samplElt_false_inv; Simpl; Auto.
Apply loc_nfstwf_false_inv with s:=t; Simpl; Auto.
Generalize (sp_hd lc); Rewrite H4; Intros s';
Pattern s'; Apply samplElt_false_inv; Simpl; Auto.
Intros H4; Apply loc_nfstwf_true; Simpl; Auto.
Apply elt_merge_is_no_Fail.
Apply loc_nfstwf_is_no_Fail with n:=n0; Auto.
Apply loc_nfstwf_is_no_Fail with n:=n0 s:=s; Auto.
Apply loc_nfstwf_is_no_Fail with n:=n0 s:=t; Auto.
Apply sp_merge_loc_nfstwf_weak.
Apply loc_nfstwf_S_n_n_tl; Auto.
Apply loc_nfstwf_S_n_n_tl with s:=s; Auto.
Apply loc_nfstwf_S_n_n_tl with s:=t; Auto.
Qed.
Lemma
sp_merge_true_loc_nfstwf:
(n:nat; c:clock; lc:(samplStr bool c); s:(samplStr A (sp_on lc));
t:(samplStr A (sp_on (sp_not lc))))
(is_fst_value true lc)->
(loc_nfstwf (S n) lc)->
(loc_nfstwf (S n) s)->
(loc_nfstwf n t)->
(loc_nfstwf (S n) (sp_merge s t)).
Proof.
Cofix sp_merge_true_loc_nfstwf.
Intros n c lc s t H H1 H2 H3; Case (eq_false_dec (hd c)).
Intros H4 ; Apply loc_nfstwf_false; Simpl; Auto.
Apply sp_merge_true_loc_nfstwf.
Apply is_fst_value_false_inv ; Auto.
Apply loc_nfstwf_false_inv ; Simpl; Auto.
Apply loc_nfstwf_false_inv with s:=s; Simpl; Auto.
Generalize (sp_hd lc); Rewrite H4; Intros s';
Pattern s'; Apply samplElt_false_inv; Simpl; Auto.
Apply loc_nfstwf_false_inv with s:=t; Simpl; Auto.
Generalize (sp_hd lc); Rewrite H4; Intros s';
Pattern s'; Apply samplElt_false_inv; Simpl; Auto.
Intros H4; Apply loc_nfstwf_true; Simpl; Auto.
Apply elt_merge_true.
Apply is_fst_value_true_inv ; Auto.
Apply loc_nfstwf_is_no_Fail with n:=n s:=s; Auto.
Apply sp_merge_loc_nfstwf_weak.
Apply loc_nfstwf_S_n_n_tl; Auto.
Apply loc_nfstwf_S_n_n_tl with s:=s; Auto.
Apply loc_nfstwf_false_inv with s:=t; Simpl; Auto.
Pattern (hd c) (sp_hd lc);
Apply eq_dep_ind_l with x:=(Any true); Auto.
Apply eq_dep_sym; Apply is_fst_value_true_inv; Auto.
Qed.
Hints Resolve sp_merge_lfp sp_merge_loc_nfstwf_weak: sampled_str.
Lemma
sp_merge_wf:
(c:clock; lc:(samplStr bool c); s:(samplStr A (sp_on lc));
t:(samplStr A (sp_on (sp_not lc))))
(sp_wf lc)->
(sp_wf s)->(sp_wf t)->
(sp_wf (sp_merge s t)).
Proof.
Auto with sampled_str.
Qed.
Definition
elt_when : (b:bool;o:(samplElt bool b))(samplElt A b)->(samplElt A (elt_on o))
:= [b;o]<[b;o:(samplElt bool b)](samplElt A b)->(samplElt A (elt_on o))>Cases o of
None => [x](None ?)
| (Any b0) => [x:(samplElt A true)]<(samplElt A)>if b0 then x else (None ?)
| Fail => [x](Fail ?)
end.
Lemma
elt_when_lfp:
(b1,b2:bool; o1:(samplElt bool b1); o2:(samplElt bool b2); x1:(samplElt A b1); x2:(samplElt A b2))
(flat_ord o1 o2)->
(flat_ord x1 x2)->
(flat_ord (elt_when o1 x1) (elt_when o2 x2)).
Proof.
Intros b1 b2 o1 o2; Case o1; Case o2; Simpl; Auto; Clear o1 b1 o2 b2.
Intros b x1 x2 H; Inversion H.
Intros x1 x2 H; Inversion H.
Intros b x1 x2 H; Inversion H.
Intros b1 b2 x1 x2 H1; Generalize (eq_dep_eq ? ? ? ? ? H1); Intros H2;
Injection H2; Intro H3; Generalize x1 x2; Rewrite H3; Case b1; Simpl; Auto.
Intros b x1 x2 H; Inversion H.
Qed.
Lemma
elt_when_is_no_Fail:
(b:bool; o:(samplElt bool b); x:(samplElt A b))
(is_no_Fail o)->
(is_no_Fail x)->
(is_no_Fail (elt_when o x)).
Proof.
Intros b o; Case o; Simpl; Auto; Clear o b.
Intros b'; Case b'; Simpl; Auto.
Qed.
Hints Resolve elt_when_lfp elt_when_is_no_Fail: sampled_str.
CoFixpoint
sp_when:
(c:clock; lc:(samplStr bool c))(samplStr A c)
->(samplStr A (sp_on lc)):=
[c;lc;x](sp_cons 2!(sp_on lc) (elt_when (sp_hd lc) (sp_hd x))
(sp_when (sp_tl lc) (sp_tl x))).
Lemma
sp_when_lfp:
(n:nat; c1,c2:clock; lc1:(samplStr bool c1); lc2:(samplStr bool c2);
s1:(samplStr A c1); s2:(samplStr A c2))
(sp_inf n lc1 lc2) ->
(sp_inf n s1 s2) ->
(sp_inf n (sp_when lc1 s1) (sp_when lc2 s2)).
Proof.
Intros n; Elim n.
Intros; Apply sp_inf_proof_O; Simpl; Auto with sampled_str.
Intros n0 HR c1 c2 lc1 lc2 s1 s2 H1 H2; Case (sp_inf_S_n_inv H1); Case (sp_inf_S_n_inv H2); Intros;
Apply sp_inf_proof_S_n; Simpl; Auto with sampled_str.
Qed.
Lemma
elt_when_true: (b:bool;o:(samplElt bool b); x:(samplElt A b))
o==<(samplElt bool)>(Any true)
-> (elt_when o x)==<(samplElt A)>x.
Proof.
Intros b o x H; Generalize x.
Pattern b o; Apply eq_dep_ind_l with x:=(Any true); Simpl; Auto with eqD.
Qed.
Hints Resolve elt_when_true: sampled_str.
Require Arith.
Lemma
sp_when_loc_nfstwf:
(n,m:nat; c:clock; lc:(samplStr bool c); s:(samplStr A c))
(loc_nfstwf n lc) -> (loc_nfstwf n s)
-> (locle m n (sp_on lc) c)
-> (loc_nfstwf m (sp_when lc s)).
Proof.
Cofix sp_when_loc_nfstwf.
Intros n m; Case m.
Intros; Apply loc_nfstwf_O.
Intros n0 c lc s H1 H2 H3; Case (eq_false_dec (elt_on (sp_hd lc))).
Intros H4; Apply loc_nfstwf_false; Simpl; Auto.
Apply sp_when_loc_nfstwf with n:=(pseudo_pred n (hd c)).
Case (eq_false_dec (hd c)); Intros H5; Rewrite H5; Simpl; Auto with sp_aux;
Generalize H1; Case n; Simpl; Auto with sp_aux.
Case (eq_false_dec (hd c)); Intros H5; Rewrite H5; Simpl; Auto with sp_aux;
Generalize H2; Case n; Simpl; Auto with sp_aux.
Inversion_clear H3; Simpl in H; Simpl in H5; Rewrite H4 in H; Simpl in H.
Rewrite H0; Rewrite <- pseudo_pred_S.
EApply locle_le_1; EAuto.
Intros H4; Apply loc_nfstwf_true; Simpl; Auto.
Inversion_clear H3; Rewrite (elt_on_eq_true_weak H4) in H0;
Simpl in H0; Case (elt_on_eq_true H4).
Intros; Pattern (elt_on (sp_hd lc)) (elt_when (sp_hd lc) (sp_hd s)).
Apply eq_dep_ind_l with x:=(sp_hd s); Simpl; Auto with sampled_str eqD.
Intros; Apply loc_nfstwf_is_no_Fail with n:=n2; Auto; Rewrite <- H0; Auto.
Intros; Absurd (is_no_Fail (sp_hd lc)).
Pattern (hd c) (sp_hd lc); Apply eq_dep_ind_l with x:=(Fail bool); Simpl; Auto with eqD.
Intros; Apply loc_nfstwf_is_no_Fail with n:=n2; Auto; Rewrite <- H0; Auto.
Apply sp_when_loc_nfstwf with n:=(pred n).
Generalize H1; Case n; Simpl; Auto with sp_aux.
Generalize H2; Case n; Simpl; Auto with sp_aux.
Inversion_clear H3; Simpl in H; Simpl in H5; Rewrite H4 in H; Simpl in H.
Rewrite H0; Rewrite (elt_on_eq_true_weak H4); Simpl.
EApply locle_le_1; EAuto with arith.
Qed.
Lemma
sp_when_glob_nfstwf:
(n:nat; c:clock; lc:(samplStr bool c); s:(samplStr A c))
(glob_nfstwf n lc) ->
(glob_nfstwf n s) -> (glob_nfstwf n (sp_when lc s)).
Proof.
Intros n c lc s H1 H2; Apply nfstwf_function_convert_sup
with f:=[s](sp_when lc s) n:=n; Auto.
Apply sp_on_clock_inf.
Intros m k s' H3 H4 H5; Apply sp_when_loc_nfstwf with n:=m; Auto.
Rewrite <- (loc2glob_prop 1!c 2!m 3!n); Auto.
Apply glob_nfstwf_loc_nfstwf;
Apply glob_nfstwf_n_le with n:=n; Auto with sampled_str.
Qed.
Lemma
sp_when_wf:
(c:clock; lc:(samplStr bool c); s:(samplStr A c))
(sp_wf lc)->(sp_wf s)->(sp_wf (sp_when lc s)).
Proof.
Cofix sp_merge_wf.
Intros c ls s H1 H2; Case (sp_wf_inv H1); Case (sp_wf_inv H2);
Constructor 1;Simpl; Auto with sampled_str.
Qed.
End Sampling.
Hints Resolve sp_merge sp_when_wf: sampled_str sp_rec0.
Syntactic Definition
merge := [c,s1,s2](sp_merge 3!c s1 s2).
Syntactic Definition
swp_when := [s,c](sp_when c s).
Infix RIGHTA 7 "when" swp_when.
Hints Resolve sp_fby_lfp sp_merge_lfp sp_when_lfp : sp_rec0.
Hints Resolve sp_fby_loc_nfstwf
sp_extend_loc_nfstwf sp_merge_loc_nfstwf_weak : sampled_str.
Hints Resolve sp_when_glob_nfstwf sp_fby_glob_nfstwf
sp_extend_glob_nfstwf sp_merge_glob_nfstwf : sp_rec0.
Hints Resolve sp_wf_glob_nfstwf glob_nfstwf_sp_wf: sp_rec0.
Section IF.
Variable A: Set.
Definition
If:= [b:bool; x,y:A]if b then x else y.
Definition
sp_if:=
[c:clock; lc:(samplStr bool c); x,y:(samplStr A c)]
(sp_extend (sp_extend (sp_extend (sp_const If ?) lc) x) y).
Lemma
sp_if_lfp:
(n:nat; c:clock; lc1,lc2:(samplStr bool c); s1,s2,t1,t2:(samplStr A c))
(sp_inf n lc1 lc2) ->
(sp_inf n s1 s2)->
(sp_inf n t1 t2)->
(sp_inf n (sp_if lc1 s1 t1) (sp_if lc2 s2 t2)).
Proof.
Unfold sp_if; Auto with sampled_str.
Qed.
Lemma
sp_if_loc_nfstwf:
(n:nat; c:clock; lc:(samplStr bool c); s1,s2:(samplStr A c))
(loc_nfstwf n lc)->
(loc_nfstwf n s1)->
(loc_nfstwf n s2)->
(loc_nfstwf n (sp_if lc s1 s2)).
Proof.
Unfold sp_if; Auto with sampled_str.
Qed.
Lemma
sp_if_glob_nfstwf:
(n:nat; c:clock; lc:(samplStr bool c); s1,s2:(samplStr A c))
(glob_nfstwf n lc)->
(glob_nfstwf n s1)->
(glob_nfstwf n s2)->
(glob_nfstwf n (sp_if lc s1 s2)).
Proof.
Unfold sp_if; Auto with sp_rec0.
Qed.
Lemma
if_equiv:
(c:clock; lc:(samplStr bool c); x,y:(samplStr A c))
(sp_wf x)-> (sp_wf y)->
(sp_eq (sp_if lc x y)
(sp_merge (sp_when lc x)
(sp_when (sp_not lc) y))).
Proof.
Cofix if_equiv;
Intros c lc x y H1 H2; Constructor 1.
Simpl; Rewrite (unfold_samplStr x) in H1; Rewrite (unfold_samplStr y) in H2;
Generalize lc x y H1 H2; Case c; Clear H2 H1 y x lc c; Intros b s;
Case b; Intros lc; Pattern (sp_hd lc).
Apply samplElt_true_inv; Simpl; Auto with eqD.
Intros a x y; Case a; Simpl; Pattern (sp_hd x); Apply samplElt_true_inv; Simpl; Auto with eqD;
Pattern (sp_hd y); Apply samplElt_true_inv; Simpl; Auto with eqD;
Intros a0 H1 H2.
Case (sp_wf_inv H2); Simpl; Intros H3; Elim H3.
Case (sp_wf_inv H1); Simpl; Intros H3; Elim H3.
Apply samplElt_false_inv; Simpl; Auto with eqD.
Case (sp_wf_inv H2); Case (sp_wf_inv H1); Intros;
Apply if_equiv with lc:=(sp_tl lc) x:=(sp_tl x) y:=(sp_tl y);
Auto.
Qed.
Lemma
if_false_equiv:
(c:clock;x,y:(samplStr A c))
(sp_wf x)->(sp_eq y (sp_if (sp_const false ?) x y)).
Proof.
Cofix if_false_equiv.
Intros c x y; Constructor 1.
Simpl; Case (sp_wf_inv H); Generalize (sp_hd x); Case (sp_hd y); Simpl; Auto with eqD.
Intros a s; Pattern s; Apply samplElt_true_inv; Simpl; Auto.
Intros H'; Elim H'.
Intros s; Pattern s; Apply samplElt_true_inv; Simpl; Auto.
Apply if_false_equiv with x:=(sp_tl x) y:=(sp_tl y); Case (sp_wf_inv H); Auto.
Qed.
Lemma
const_decal_eq:
(A:Set ; c:clock;a:A)(sp_eq (sp_const a c) (sp_delay (sp_const a c) (Any a))).
Proof.
Intros A'; Cofix const_decal_eq.
Intros c a; Constructor 1.
Case c; Intros b c'; Case b; Simpl; Auto with eqD.
Case c; Intros b c'; Case b; Apply const_decal_eq with c:=c' a:=a.
Qed.
Hints Resolve const_decal_eq sp_if_lfp sp_if_loc_nfstwf: sampled_str.
Lemma
arrow_equiv: (c:clock;x,y:(samplStr A c))
(sp_wf x)->(sp_wf y)->
(sp_eq (sp_arrow x y) (sp_if (`true` fby `false`) x y)).
Proof.
Cofix arrow_equiv;
Intros c x y H1 H2; Constructor 1.
Simpl; Case (sp_wf_inv H2); Generalize (sp_hd y); Case (sp_hd x); Simpl; Auto with eqD.
Intros a s; Pattern s; Apply samplElt_true_inv; Simpl; Auto.
Intros H'; Elim H'.
Case (sp_wf_inv H1); Case (sp_wf_inv H2); Generalize x y;
Case c; Intros b c0; Case b; Clear b H1 H2 y x c.
Intros x y H1 H2 H3 H4;
Change (sp_eq (sp_tl y)
(sp_if (sp_delay (sp_const false c0) (Any false)) (sp_tl x) (sp_tl y))).
Apply sp_eq_trans with s2:=(sp_if (sp_const false c0) (sp_tl x) (sp_tl y)).
Apply if_false_equiv; Auto.
Apply sp_inf_wf_eq; Auto with sampled_str.
Intros x y H1 H2 H3 H4; Apply arrow_equiv with x:=(sp_tl x) y:=(sp_tl y); Auto.
Qed.
End IF.
Hints Resolve sp_if_lfp: sampled_str sp_rec0.
Hints Resolve sp_if_loc_nfstwf: sampled_str.
Hints Resolve sp_if_glob_nfstwf : sp_rec0.
(*
Section Reseting.
Variable A: Set.
CoFixpoint sp_whilenot:(c:clock)(samplStr bool c)->(samplStr bool c)
:= [c,lc]Cases (sp_hd lc) of
| None => (sp_cons None (sp_whilenot (sp_tl lc)))
| (Any b) => if b then (sp_cons (Any false) (sp_const false (tl c)))
else (sp_cons (Any true) (sp_whilenot (tl c)))
| Fail => (undef ? ?)
end.
Definition repeat_until:=
[c:clock; lc:(samplStr bool c)](sp_arrow (sp_const true) (sp_whilenot lc))
Variable f: (c:clock)(samplStr A c)->(samplStr A c).
CoFixpoint sp_reset_aux: (c:clock)(samplStr A c)->(samplStr bool c)->(samplStr A c)->(samplStr A c)
:=[c;x;lc;acc]
(sp_cons (sp_hd acc)
(sp_reset_aux (sp_tl x) (sp_tl lc)
Cases (sp_hd (sp_tl lc)) of
| None => (sp_tl acc)
| (Any b) => if b then (f (sp_tl x)) else (sp_tl acc)
| Fail => (undef ? ?)
end)).
Definition sp_reset:=
[c:clock; x:(samplStr A c); lc]
let acc = (f x) (* faux !! *)
in (sp_arrow acc (sp_reset_aux x lc acc)).
End Reseting.
*)
Implicit Arguments Off.
23/06/101, 15:38