sampled_streams.v
(* FILE: SAMPLED_STREAMS/sampled_streams.v _ Sylvain Boulmé _ LIP6 _ Spring 2001 *)
(* Coq V6.3.1 *)
(* HINTS: we consider here a discrete time. *)
(* Our system has a "global" clock. *)
(* We define "streams" which are sampled on subclocks *)
(* (called "local clocks") of this global clock. *)
(* We want to show that such sampled streams are natural *)
(* to express with dependent types. *)
Implicit Arguments On.
Require Export Streams.
Require Export Bool.
(* Some preliminaries on eq_dep (see the file EqD.v) *)
(* We RELY here on the standard AXIOM "eq_rec_eq" of Eqdep.v *)
Require Export EqD.
(* BEGIN PRELIMINARIES *)
Lemma
leb_refl: (b:bool)(leb b b).
Proof.
Intros b; Case b; Simpl; Auto.
Qed.
Lemma
leb_false_2: (b:bool)(leb b false)->b=false.
Proof.
Intros b; Elim b; Simpl; Auto.
Qed.
Lemma
leb_true_2: (b:bool)(leb b true).
Proof.
Intros b; Elim b; Simpl; Auto.
Qed.
Lemma
leb_antisym: (b1,b2:bool)(leb b1 b2)->(leb b2 b1)->b1=b2.
Proof.
Intros b1 b2; Case b1; Case b2; Simpl; Auto.
Qed.
Hints Resolve leb_refl leb_antisym leb_true_2: sampled_str.
Lemma
leb_trans: (b1,b2,b3:bool)(leb b1 b2)->(leb b2 b3)->(leb b1 b3).
Proof.
Intros b1 b2 b3; Case b1; Case b2; Case b3; Simpl; Auto.
Qed.
Lemma
EqSt_inv: (A:Set; s1,s2:(Stream A))(EqSt s1 s2)->(hd s1)=(hd s2)/\(EqSt (tl s1) (tl s2)).
Proof.
Intros A s1 s2 H; Case H; Auto.
Qed.
Lemma
unfold_Str:(A:Set; x:(Stream A))x=(Cons (hd x) (tl x)).
Proof.
Intros A x; Case x; Simpl; Auto.
Qed.
Scheme and_indd:= Induction for and Sort Prop.
Section Fun_power.
Variable A:Set.
Variable f: A->A.
Fixpoint
funPower[n:nat]: A -> A :=
[x]Cases n of
O => x | (S m) => (funPower m (f x))
end.
Lemma
funPower_commut:
(n:nat; x:A)(f (funPower n x))=(funPower (S n) x).
Proof.
Intros n; Elim n; Simpl; Auto.
Qed.
End Fun_power.
Hints Resolve EqSt_reflex sym_EqSt:sampled_str.
(* END PRELIMINARIES *)
(* BEGIN DEFINITION *)
(* A sampled stream is a "stream" of "samplElts" *)
Inductive
samplElt[A:Set]: bool -> Set :=
None: (samplElt A false)
| Any: A -> (samplElt A true)
| Fail: (samplElt A true) (* initialization error *).
Definition
clock:=(Stream bool).
(* Clocks are Streams of booleans *)
(* "true" corresponds to a "tic" *)
(* "false" corresponds to a delay *)
(* Set of sampled Streams *)
CoInductive
samplStr[A:Set]: clock -> Set :=
sp_cons: (c:clock)(samplElt A (hd c))->(samplStr A (tl c))->(samplStr A c).
Section Sampled_streams_def.
Variable A : Set. (* the set of elt in sampled streams *)
Definition
samplElt_true_invS:
(P:(samplElt A true)->Set)
((a:A)(P (Any a)))->(P (Fail A))->(x:(samplElt A true))(P x)
:= [P;P_any;P_fail;x]
<[b; y:(samplElt A b)]
(<[b:bool](samplElt A b)->Set>if b then P else [_]unit y)>
Cases x of
| (Any a) => (P_any a)
| Fail => P_fail
| _ => tt
end.
Definition
samplElt_false_invS:
(P:(samplElt A false)->Set)(P (None A))->(x:(samplElt A false))(P x)
:= [P;P_none;x]
<[b; y:(samplElt A b)]
(<[b:bool](samplElt A b)->Set>
if b then [_]unit else P y)>Cases x of
| None => P_none
| _ => tt
end.
Lemma
samplElt_true_inv:
(P:(samplElt A true)->Prop)
((a:A)(P (Any a)))->(P (Fail A))->(x:(samplElt A true))(P x).
Proof.
Intros P H1 H2 x;
Change (([b:bool]<[b:bool](samplElt A b)->Prop>
if b then [x](P x) else [_]True) true x);
Case x; Simpl; Auto.
Qed.
Lemma
samplElt_false_inv:
(P:(samplElt A false)->Prop)
(P (None A))->(x:(samplElt A false))(P x).
Proof.
Intros P H x;
Change (([b:bool]<[b:bool](samplElt A b)->Prop>
if b then [_]True else [x](P x)) false x);
Case x; Simpl; Auto.
Qed.
(* Generics destructors *)
Definition
sp_hd :=
[c:clock; x: (samplStr A c)]
<[c:clock; x: (samplStr A c)](samplElt A (hd c))>
Cases x of (sp_cons _ a _) => a end.
Definition
sp_tl :=
[c:clock; x: (samplStr A c)]
<[c:clock; x: (samplStr A c)](samplStr A (tl c))>
Cases x of (sp_cons _ _ s) => s end.
Lemma
unfold_samplStr :
(c:clock; s:(samplStr A c))
s=(sp_cons (sp_hd s) (sp_tl s)).
Proof.
Intros c x; Case x; Simpl; Auto.
Qed.
(* Equality on Streams *)
CoInductive
sp_eq: (c1,c2:clock)(samplStr A c1)->(samplStr A c2)->Prop :=
sp_eq_proof :
(c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
(sp_hd s1)==<(samplElt A)>(sp_hd s2) (* syntax for "eq_dep". see EqD.v *)
->(sp_eq (sp_tl s1) (sp_tl s2))->(sp_eq s1 s2).
Lemma
sp_eq_refl: (c:clock; s:(samplStr A c))(sp_eq s s).
Proof.
Cofix sp_eq_refl; Intros c s; Constructor 1; Simpl; Auto with eqD.
Qed.
Lemma
sp_eq_inv:
(c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
(sp_eq s1 s2)->(sp_hd s1)==<(samplElt A)>(sp_hd s2)/\(sp_eq (sp_tl s1) (sp_tl s2)).
Proof.
Intros c1 c2 s1 s2 H1; Case H1; Auto.
Qed.
Lemma
sp_eq_sym: (c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
(sp_eq s1 s2)->(sp_eq s2 s1).
Proof.
Cofix sp_eq_sym; Intros c1 c2 s1 s2 H1;
Case (sp_eq_inv H1); Constructor 1; Simpl; Auto with eqD.
Qed.
Lemma
sp_eq_trans: (c1,c2,c3:clock; s1:(samplStr A c1); s2:(samplStr A c2); s3:(samplStr A c3))
(sp_eq s1 s2)->(sp_eq s2 s3)->(sp_eq s1 s3).
Proof.
Cofix sp_eq_trans; Intros c1 c2 c3 s1 s2 s3 H1 H2;
Case (sp_eq_inv H1); Case (sp_eq_inv H2);
Constructor 1.
Apply eq_dep_trans with y:=(sp_hd s2); Auto.
Apply sp_eq_trans with s2:=(sp_tl s2); Auto.
Qed.
Lemma
sp_eq_EqSt_clock:
(c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
(sp_eq s1 s2)->(EqSt c1 c2).
Proof.
Cofix sp_eq_EqSt_clock.
Intros c1 c2 s1 s2 H; Case (sp_eq_inv H); Constructor 1; Simpl; EAuto.
Apply eq_dep_eq_param with P:=(samplElt A) x:=(sp_hd s1) y:=(sp_hd s2);
Auto.
Qed.
(* Coercion on samplStr As w.r.t. equality on clocks *)
CoFixpoint
clock_coerce: (c1,c2:clock)(EqSt c1 c2)->(samplStr A c1)->(samplStr A c2)
:= [c1,c2; H; s]
Cases (EqSt_inv H) of
(conj H1 H2) =>
(sp_cons
(eq_rec ? ? (samplElt A) (sp_hd s) ? H1)
(clock_coerce H2 (sp_tl s)))
end.
Theorem
sp_eq_clock_coerce:
(c1,c2:clock; H:(EqSt c1 c2); s:(samplStr A c1))
(sp_eq s (clock_coerce H s)).
Proof.
Cofix sp_eq_clock_coerce; Intros c1 c2 H s; Constructor 1; Simpl;
Pattern (EqSt_inv H); Apply and_indd; Auto.
Intros H1 H2; Pattern (hd c2) H1; Apply eq_indd; Simpl; Auto with eqD.
Qed.
End Sampled_streams_def.
(* END DEFINITION *)
Hints Resolve sp_eq_refl sp_eq_sym: sampled_str.
CoInductive
clock_inf: clock -> clock -> Prop :=
clock_inf_proof:
(c1,c2:clock)
(leb (hd c1) (hd c2))->
(clock_inf (tl c1) (tl c2))->(clock_inf c1 c2).
Hints Resolve clock_inf_proof: sampled_str.
Lemma
clock_inf_inv:
(c1,c2:clock)(clock_inf c1 c2)->(leb (hd c1) (hd c2))/\(clock_inf (tl c1) (tl c2)).
Proof.
Intros c1 c2 H; Case H; Simpl; Auto.
Qed.
Lemma
clock_inf_refl: (c1,c2:clock)(EqSt c1 c2)->(clock_inf c1 c2).
Proof.
Cofix clock_inf_refl; Intros c1 c2 H; Case (EqSt_inv H);
Constructor 1; Simpl; Auto.
Rewrite H0; Auto with sampled_str.
Qed.
Hints Resolve clock_inf_refl: sampled_str.
Lemma
clock_inf_antisym: (c1,c2:clock)(clock_inf c1 c2)->(clock_inf c2 c1)->(EqSt c1 c2).
Proof.
Cofix clock_inf_antisym; Intros c1 c2 H1 H2; Case (clock_inf_inv H1); Case (clock_inf_inv H2);
Constructor 1; Simpl; Auto with sampled_str.
Qed.
Hints Resolve clock_inf_antisym: sampled_str.
Lemma
clock_inf_trans: (c1,c2,c3:clock)(clock_inf c1 c2)->(clock_inf c2 c3)->(clock_inf c1 c3).
Proof.
Cofix clock_inf_trans; Intros c1 c2 c3 H1 H2; Case (clock_inf_inv H1);
Case (clock_inf_inv H2); Constructor 1.
Apply leb_trans with b2:=(hd c2); Auto.
Apply clock_inf_trans with c2:=(tl c2); Auto.
Qed.
Section Sampled_streams_props.
Variable A:Set.
(* BEGIN nth elt of samplStr As *)
(* nth power of tl for clocks *)
Fixpoint
clock_nth_tl [n:nat] : clock->clock :=
[c:clock] Cases n of
O => c
|(S m) => (tl (clock_nth_tl m c))
end.
Definition
clock_nth : nat->clock->bool :=
[n:nat][s:clock](hd (clock_nth_tl n s)).
Lemma
clock_tl_nth_tl :
(n:nat; c:clock)
(tl (clock_nth_tl n c))=(clock_nth_tl n (tl c)).
Proof.
Fix 1; Intros n; Case n; Simpl; Auto.
Intros m c'; Rewrite <- clock_tl_nth_tl; Auto.
Qed.
(* nth power of sp_tl for samplStr As *)
Fixpoint
sp_nth_tl [n:nat] :
(c:clock)(samplStr A c)->(samplStr A (clock_nth_tl n c)) :=
[c:clock; s:(samplStr A c)]
<[n:nat](samplStr A (clock_nth_tl n c))>Cases n of
O => s
|(S m) => (sp_tl (sp_nth_tl m s))
end.
Definition
sp_nth :
(n:nat; c:clock)(samplStr A c)-> (samplElt A (clock_nth n c)) :=
[n;c;s](sp_hd (sp_nth_tl n s)).
Lemma
sp_tl_nth_tl :
(n:nat; c:clock; s:(samplStr A c))
(sp_tl (sp_nth_tl n s)) ==<samplStr A> (sp_nth_tl n (sp_tl s)).
Proof.
Induction n; Simpl; Auto with eqD.
Qed.
Hints Resolve sp_tl_nth_tl: sampled_str.
Lemma
sp_nth_tl_plus: (n,m:nat; c:clock; s: (samplStr A c))
(sp_nth_tl n (sp_nth_tl m s))==<samplStr A>(sp_nth_tl (plus n m) s).
Proof.
Induction n; Simpl; Intros; Auto with eqD sampled_str.
Qed.
Lemma
sp_nth_plus: (n,m:nat; c:clock; s: (samplStr A c))
(sp_nth n (sp_nth_tl m s))==<(samplElt A)>(sp_nth (plus n m) s).
Proof.
Intros n m c s; Unfold clock_nth sp_nth.
Pattern (clock_nth_tl (plus n m) c) (sp_nth_tl (plus n m) s);
Apply eq_dep_ind_l with x:=(sp_nth_tl n (sp_nth_tl m s)); Auto with eqD.
Apply sp_nth_tl_plus.
Qed.
Hints Resolve sp_nth_plus: sampled_str.
(* An equivalent way to define sp_eq *)
Lemma
sp_eq_sp_nth :
(n:nat; c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
(sp_eq s1 s2)->(sp_nth n s1)==<(samplElt A)>(sp_nth n s2).
Proof.
Unfold clock_nth sp_nth; Induction n; Simpl.
Intros c1 c2 s1 s2 H; Case (sp_eq_inv H); Auto.
Intros m HR c1 c2 s1 s2 H; Case (sp_eq_inv H); Intros.
Pattern (tl (clock_nth_tl m c1)) (sp_tl (sp_nth_tl m s1));
Apply eq_dep_ind_l with x:=(sp_nth_tl m (sp_tl s1)); Auto with sampled_str eqD.
Pattern (tl (clock_nth_tl m c2)) (sp_tl (sp_nth_tl m s2));
Apply eq_dep_ind_l with x:=(sp_nth_tl m (sp_tl s2)); Auto with sampled_str eqD.
Qed.
Lemma
sp_nth_sp_eq :
(c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
((n:nat)(sp_nth n s1)==<(samplElt A)>(sp_nth n s2))
->(sp_eq s1 s2).
Proof.
Unfold clock_nth sp_nth; Cofix sp_nth_sp_eq; Intros c1 c2 s1 s2 H; Constructor 1.
Apply (H O).
Apply sp_nth_sp_eq; Intros n.
Pattern (clock_nth_tl n (tl c1)) (sp_nth_tl n (sp_tl s1));
Apply eq_dep_ind_l with x:=(sp_tl (sp_nth_tl n s1)); Auto with sampled_str eqD.
Pattern (clock_nth_tl n (tl c2)) (sp_nth_tl n (sp_tl s2));
Apply eq_dep_ind_l with x:=(sp_tl (sp_nth_tl n s2)); Auto with sampled_str eqD.
Apply (H (S n)).
Qed.
Hints Resolve sp_eq_sp_nth sp_nth_sp_eq: sampled_str.
(* END nth elt of samplStr As *)
(* BEGIN Wellformation of samplStr As *)
(* a wellformed stream has no "Fail" elt *)
Definition
is_no_Fail: (b:bool)(samplElt A b)->Prop
:= [b;s] Cases s of
| Fail => False
| _ => True
end.
CoInductive
sp_wf: (c:clock)(samplStr A c) -> Prop :=
sp_wf_proof: (c:clock; s:(samplStr A c))
(is_no_Fail (sp_hd s))->(sp_wf (sp_tl s))->(sp_wf s).
Lemma
sp_wf_inv: (c:clock; s:(samplStr A c))(sp_wf s)->
(is_no_Fail (sp_hd s))/\(sp_wf (sp_tl s)).
Proof.
Intros c s H; Case H; Auto.
Qed.
(* END Wellformation of samplStr As *)
Require Arith.
(* BEGIN "Partial wellformation" (on the n first elts) *)
CoInductive
loc_nfstwf: (n:nat; c:clock)(samplStr A c)->Prop :=
| loc_nfstwf_O:
(c:clock; s:(samplStr A c))(loc_nfstwf O s)
| loc_nfstwf_false:
(n:nat; c:clock; s:(samplStr A c))
(hd c)=false -> (loc_nfstwf n (sp_tl s))->(loc_nfstwf n s)
| loc_nfstwf_true:
(n:nat; c:clock; s:(samplStr A c))
(hd c)=true ->
(is_no_Fail (sp_hd s))
->(loc_nfstwf n (sp_tl s))->(loc_nfstwf (S n) s).
Hints Resolve loc_nfstwf_O loc_nfstwf_false loc_nfstwf_true: sampled_str.
Lemma
loc_nfstwf_S_n_inv:
(P:Prop; n: nat; c: clock; s:(samplStr A c))
(loc_nfstwf (S n) s) ->
((hd c)=false -> (loc_nfstwf (S n) (sp_tl s)) -> P)
->((hd c)=true -> (is_no_Fail (sp_hd s)) -> (loc_nfstwf n (sp_tl s)) -> P)
-> P.
Proof.
Intros P n c s H;
Change ([m:nat]<[m:nat]Prop>Cases m of
O => True
| (S n) =>
((hd c)=false->(loc_nfstwf (S n) (sp_tl s))->P)
->((hd c)=true
->(is_no_Fail (sp_hd s))
->(loc_nfstwf n (sp_tl s))
->P)
->P end (S n)).
Case H; Simpl; Auto.
Intros n0; Case n0; Simpl; Auto.
Qed.
Lemma
loc_nfstwf_is_no_Fail:
(n:nat; c: clock; s:(samplStr A c))
(loc_nfstwf (S n) s) -> (is_no_Fail (sp_hd s)).
Proof.
Intros n c s H; Apply loc_nfstwf_S_n_inv with n:=n s:=s; Auto.
Intros H1 H2; Generalize s.
Rewrite (unfold_Str c); Rewrite H1.
Intros s'; Pattern (sp_hd s'); Apply samplElt_false_inv; Simpl; Auto.
Qed.
Lemma
loc_nfstwf_false_inv:
(n: nat; c: clock; s:(samplStr A c))
(hd c)=false ->
(loc_nfstwf n s) -> (loc_nfstwf n (sp_tl s)).
Proof.
Intros n; Case n; Auto with sampled_str.
Intros m c s H1 H2; Apply loc_nfstwf_S_n_inv with n:=m s:=s; Auto.
Intros H3; Rewrite H1 in H3; Discriminate H3.
Qed.
Lemma
loc_nfstwf_S_n_true_inv:
(n: nat; c: clock; s:(samplStr A c))
(hd c)=true ->
(loc_nfstwf (S n) s) -> (loc_nfstwf n (sp_tl s)).
Proof.
Intros n c s H1 H2; Apply loc_nfstwf_S_n_inv with n:=n s:=s; Auto.
Intros H3; Rewrite H1 in H3; Discriminate H3.
Qed.
Hints Resolve loc_nfstwf_false_inv loc_nfstwf_S_n_true_inv: sampled_str.
Lemma
loc_nfstwf_true_inv:
(n: nat; c: clock; s:(samplStr A c))
(hd c)=true ->
(loc_nfstwf n s) -> (loc_nfstwf (pred n) (sp_tl s)).
Proof.
Intros n c s H1; Case n; Simpl; Auto with sampled_str.
Qed.
Hints Resolve loc_nfstwf_true_inv: sampled_str.
Lemma
eq_false_dec:(b:bool){ b=false } +{ b=true}.
Intros b; Case b; Simpl; Auto.
Qed.
Definition
pseudo_S:=[n:nat; b:bool]if b then (S n) else n.
Definition
pseudo_pred:=[n:nat; b:bool]if b then (pred n) else n.
Lemma
pseudo_pred_S:(n:nat; b:bool)n=(pseudo_pred (pseudo_S n b) b).
Proof.
Intros n b; Case b; Simpl; Auto.
Qed.
Lemma
pseudo_S_pred:(n:nat; b:bool)(S n)=(pseudo_S (pseudo_pred (S n) b) b).
Proof.
Intros n b; Case b; Simpl; Auto.
Qed.
Lemma
pseudo_pred_S_eq:(n:nat; b:bool)(pseudo_pred (S n) b)=(pseudo_S n (negb b)).
Proof.
Intros n b; Case b; Simpl; Auto.
Qed.
Lemma
pseudo_S_O_discr: (n:nat; b:bool)O=(pseudo_S n b) -> n=O /\ b=false.
Proof.
Intros n b; Case b; Simpl; Auto.
Intros H; Discriminate H.
Qed.
Lemma
pseudo_S_le:(b:bool; n1,n2:nat)(le n1 n2)->(le n1 (pseudo_S n2 b)).
Proof.
Intros b; Case b; Simpl; Auto with arith.
Qed.
Lemma
pseudo_pred_le:(b:bool; n1,n2:nat)(le n1 n2)->(le n1 (pseudo_pred (S n2) b)).
Proof.
Intros; Rewrite pseudo_pred_S_eq; Apply pseudo_S_le; Auto.
Qed.
Hints Resolve pseudo_pred_le pseudo_S_le: sp_aux.
Lemma
loc_nfstwf_inv:
(n:nat; c: clock; s:(samplStr A c))
(loc_nfstwf n s) -> (loc_nfstwf (pseudo_pred n (hd c)) (sp_tl s)).
Proof.
Intros n c s H; Case (eq_false_dec (hd c)); Intro H1; Rewrite H1; Simpl; Auto with sampled_str.
Qed.
Lemma
loc_nfstwf_S_n_n:
(n:nat; c: clock; s:(samplStr A c))
(loc_nfstwf (S n) s) -> (loc_nfstwf n s).
Proof.
Cofix loc_nfstwf_S_n_n; Intros n; Case n.
Intros; Apply loc_nfstwf_O.
Intros n0 c s H; Case (eq_false_dec (hd c)).
Intros H1; Apply loc_nfstwf_false; Auto with sampled_str.
Intros H1; Apply loc_nfstwf_true; Auto with sampled_str.
EApply loc_nfstwf_is_no_Fail; EAuto.
Qed.
Hints Resolve loc_nfstwf_S_n_n: sampled_str.
Lemma
loc_nfstwf_n_le:
(n,m:nat; c: clock; s:(samplStr A c))
(loc_nfstwf n s)->(le m n)->(loc_nfstwf m s).
Proof.
Intros n m c s H1 H; Generalize c s H1; Elim H; Simpl; Auto with sampled_str.
Qed.
Lemma
loc_nfstwf_S_n_n_tl:
(n:nat; c: clock; s:(samplStr A c))
(loc_nfstwf (S n) s) -> (loc_nfstwf n (sp_tl s)).
Proof.
Intros n c s H; Case (eq_false_dec (hd c)); Auto with sampled_str.
Qed.
Hints Resolve loc_nfstwf_S_n_n_tl: sampled_str.
Lemma
loc_nfstwf_sp_eq:
(n:nat; c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
(sp_eq s1 s2)->(loc_nfstwf n s1)->(loc_nfstwf n s2).
Proof.
Cofix loc_nfstwf_sp_eq.
Intros n c1 c2 s1 s2 H1 H2; Case (eq_false_dec (hd c2)).
Intros H3; Apply loc_nfstwf_false; Auto.
Apply loc_nfstwf_sp_eq with s1:=(sp_tl s1).
Case H1; Auto.
Apply loc_nfstwf_false_inv; Auto.
Rewrite <- H3; Case (EqSt_inv (sp_eq_EqSt_clock H1)); Auto.
Intros H3; Generalize H2; Case n.
Intros; Apply loc_nfstwf_O.
Intros n' H2'; Apply loc_nfstwf_true; Auto.
Pattern (hd c2) (sp_hd s2); Apply eq_dep_ind_l with x:=(sp_hd s1).
Apply loc_nfstwf_is_no_Fail with n:=n'; Auto.
Case H1; Auto.
Apply loc_nfstwf_sp_eq with s1:=(sp_tl s1).
Case H1; Auto.
Apply loc_nfstwf_S_n_true_inv; Auto.
Rewrite <- H3; Case (EqSt_inv (sp_eq_EqSt_clock H1)); Auto.
Qed.
Lemma
loc_nfstwf_nth:
(n:nat; c:clock; s:(samplStr A c))
(loc_nfstwf (S n) s)->(is_no_Fail (sp_nth n s)).
Proof.
Intros n; Elim n.
Intros; Apply loc_nfstwf_is_no_Fail with n:=O s:=s; Auto.
Unfold clock_nth sp_nth; Intros m HR c s; Intros H1.
Apply loc_nfstwf_S_n_inv with n:=(S m) s:=s; Simpl; Auto.
Intros; Pattern (tl (clock_nth_tl m c)) (sp_tl (sp_nth_tl m s)).
Apply eq_dep_ind_l with x:=(sp_nth_tl m (sp_tl s)); Auto with sampled_str eqD.
Intros; Pattern (tl (clock_nth_tl m c)) (sp_tl (sp_nth_tl m s)).
Apply eq_dep_ind_l with x:=(sp_nth_tl m (sp_tl s)); Auto with sampled_str eqD.
Qed.
Hints Resolve loc_nfstwf_nth: sampled_str.
Lemma
loc_nfstwf_lt_is_no_Fail:
(n:nat; c:clock; s:(samplStr A c))
(loc_nfstwf n s)->(m:nat)(lt m n)->(is_no_Fail (sp_nth m s)).
Proof.
Unfold lt; Intros n; Elim n.
Intros c s H1 m H2; Inversion H2.
Intros n' HR c s H1 m H2; Inversion H2; Auto with sampled_str.
Qed.
Lemma
loc_nfstwf_sp_wf:
(c:clock; s:(samplStr A c))((n:nat)(loc_nfstwf n s))->(sp_wf s).
Proof.
Cofix loc_nfstwf_sp_wf.
Intros c s H; Constructor 1.
Apply loc_nfstwf_is_no_Fail with n:=(S O); Auto.
Apply loc_nfstwf_sp_wf; Auto with sampled_str.
Qed.
Lemma
sp_wf_loc_nfstwf:
(c:clock; s:(samplStr A c))(sp_wf s)->(n:nat)(loc_nfstwf n s).
Proof.
Cofix sp_wf_loc_nfstwf.
Intros c s H n; Case (sp_wf_inv H); Case (eq_false_dec (hd c)); Intros.
Apply loc_nfstwf_false; Auto.
Case n.
Apply loc_nfstwf_O.
Intros; Apply loc_nfstwf_true; Auto.
Qed.
Hints Resolve sp_wf_loc_nfstwf loc_nfstwf_sp_wf: sampled_str.
(* END "Partial wellformation" (on the n first elts) *)
Fixpoint
glob2loc[n:nat]: clock -> nat :=
[c:clock]Cases n of
O => O
| (S m) => (pseudo_S (glob2loc m (tl c)) (hd c))
end.
Lemma
glob2loc_clock_nth:
(n:nat; c:clock)
(glob2loc (S n) c) =
(pseudo_S (glob2loc n c) (clock_nth n c)).
Proof.
Intros n; Elim n.
Simpl; Auto.
Unfold clock_nth; Intros m HR c.
Simpl; Rewrite (clock_tl_nth_tl m c);
Case (hd c); Simpl.
Cut
(S (glob2loc (S m) (tl c)))
=(S (pseudo_S (glob2loc m (tl c))
(hd (clock_nth_tl m (tl c))))); Auto.
Case (hd (clock_nth_tl m (tl c))); Simpl; Auto.
Apply HR with c:=(tl c).
Qed.
Lemma
glob2loc_S_le:
(n:nat; c:clock)
(le (glob2loc (S n) c) (S (glob2loc n c))).
Proof.
Intros n c; Rewrite glob2loc_clock_nth;
Case (clock_nth n c); Simpl; Auto.
Qed.
Lemma
glob2loc_le:
(n:nat; c:clock)
(le (glob2loc n c) n).
Proof.
Intros n; Elim n; Simpl; Auto.
Intros m HR c; Case (hd c); Simpl; Auto with arith.
Qed.
Hints Resolve glob2loc_le: sampled_str.
Lemma
glob2loc_preserves_le:
(n,m:nat)(le n m)->(c:clock)(le (glob2loc n c) (glob2loc m c)).
Proof.
Intros n; Elim n; Simpl; Auto with arith.
Intros n0 HR m H1 c; Inversion H1; Simpl; Auto.
Case (hd c); Simpl; Auto with arith.
Qed.
Lemma
loc_nfstwf_lt_is_no_Fail_strong:
(n:nat; c:clock; s:(samplStr A c))
(loc_nfstwf (glob2loc n c) s)
->(m:nat)(lt m n)->(is_no_Fail (sp_nth m s)).
Proof.
Intros n; Elim n.
Simpl; Intros c s H1 m H2; Inversion_clear H2.
Intros n0 HR c s H1 m H2; Inversion_clear H2.
Generalize HR H1; Case n0; Unfold clock_nth sp_nth; Simpl.
Generalize s; Clear HR H1 s; Rewrite (unfold_Str c); Case (hd c).
Simpl; Intros; Apply loc_nfstwf_is_no_Fail with n:=O s:=s; Auto.
Simpl; Intros; Pattern (sp_hd s); Apply samplElt_false_inv; Simpl; Auto.
Clear HR H1; Intros n1 HR H1; Simpl.
Pattern (tl (clock_nth_tl n1 c)) (sp_tl (sp_nth_tl n1 s));
Apply eq_dep_ind_l with x:=(sp_nth_tl n1 (sp_tl s)); Auto with sampled_str eqD.
Apply HR; Auto.
Case (eq_false_dec (hd c)); Intros H2; Rewrite H2 in H1; Simpl in H1;
Auto with sampled_str.
Apply HR; Auto.
Rewrite glob2loc_clock_nth in H1; Case (eq_false_dec (clock_nth n0 c)); Intros H2;
Rewrite H2 in H1; Auto with sampled_str.
Qed.
CoInductive
locle: nat->nat->clock->clock->Prop :=
| locle_O: (n:nat; c1,c2:clock)(locle O n c1 c2)
| locle_S: (n1,m1,n2,m2:nat; c1,c2:clock)
(le m1 (pseudo_S n1 (hd c1))) ->
m2=(pseudo_S n2 (hd c2)) ->
(le n1 n2)->
(leb (hd c1) (hd c2))->
(locle n1 n2 (tl c1) (tl c2))->(locle m1 m2 c1 c2).
Lemma
locle_le:
(n1,n2:nat; c1,c2:clock)
(locle n1 n2 c1 c2)->(le n1 n2).
Proof.
Intros n1 n2 c1 c2 H; Case H; Auto with arith.
Intros n1' m1 n2' m2 c1' c2' H1 H2 H3 H4 H5;
Rewrite H2; Generalize H1 H4; Case (hd c1'); Simpl.
Intros H6 H7; Rewrite H7; Simpl; Apply le_trans with m:=(S n1'); Auto with arith.
Intros; Apply le_trans with m:=n2'.
EApply le_trans; EAuto.
Case (hd c2'); Simpl; Auto.
Qed.
Hints Resolve locle_le: sp_aux.
Lemma
locle_S_false_false:
(n1,n2:nat; c1,c2:clock)
(hd c1)=false ->
(hd c2)=false ->
(locle n1 n2 (tl c1) (tl c2))->(locle n1 n2 c1 c2).
Proof.
Intros n1 n2 c1 c2 H1 H2 H3; Apply locle_S with n1:=n1 n2:=n2; Auto;
Try (Rewrite H1); Try (Rewrite H2); Simpl; Auto.
EApply locle_le; EAuto.
Qed.
Lemma
locle_S_false_true:
(n1,n2:nat; c1,c2:clock)
(hd c1)=false ->
(hd c2)=true ->
(locle n1 n2 (tl c1) (tl c2))->(locle n1 (S n2) c1 c2).
Proof.
Intros n1 n2 c1 c2 H1 H2 H3; Apply locle_S with n1:=n1 n2:=n2; Auto;
Try (Rewrite H1); Try (Rewrite H2); Simpl; Auto.
EApply locle_le; EAuto.
Qed.
Lemma
locle_S_true_true:
(n1,n2:nat; c1,c2:clock)
(hd c1)=true ->
(hd c2)=true ->
(locle n1 n2 (tl c1) (tl c2))->(locle (S n1) (S n2) c1 c2).
Proof.
Intros n1 n2 c1 c2 H1 H2 H3; Apply locle_S with n1:=n1 n2:=n2; Auto;
Try (Rewrite H1); Try (Rewrite H2); Simpl; Auto.
EApply locle_le; EAuto.
Qed.
Hints Resolve locle_O locle_S_false_false locle_S_false_true locle_S_true_true : sp_aux.
Lemma
locle_le_1: (n1,m1,n2:nat; c1,c2:clock)(locle n1 n2 c1 c2)->(le m1 n1)->(locle m1 n2 c1 c2).
Proof.
Intros n1 m1 n2 c1 c2 H; Case H; Clear H n1 n2 c1 c2.
Intros n c1 c2 H; Inversion H; Auto with sp_aux.
Intros; EApply locle_S; EAuto.
EApply le_trans; EAuto.
Qed.
Lemma
locle_le_2: (n1,n2,m2:nat; c1,c2:clock)(locle n1 n2 c1 c2)->(le n2 m2)->(locle n1 m2 c1 c2).
Proof.
Cofix locle_le_2.
Intros n1 n2 m2 c1 c2 H; Case H; Clear H n1 n2 c1 c2.
Intros; Auto with sp_aux.
Intros n1 m1 n2 m3 c1 c2 H1 H2 H3 H4 H5 H6; Case H6.
Intros; EApply locle_S; EAuto.
Intros m2' H7; Apply locle_S with n1:=n1 n2:=(pseudo_pred (S m2') (hd c2)) ; Auto.
Rewrite <- pseudo_S_pred; Auto.
Apply le_trans with m:=m3.
Rewrite H2; Auto with sp_aux.
Auto with sp_aux.
Apply locle_le_2 with n1:=n1 n2:=n2; Auto.
Generalize H7; Rewrite H2; Case (hd c2); Simpl; Auto with arith.
Qed.
Lemma
locle_glob2loc_le: (n,m:nat; c:clock)
(le n (glob2loc m c))->(locle n m c (const true)).
Proof.
Cofix locle_glob2loc_le.
Intros n m c; Case n; Simpl.
Intros; Apply locle_O.
Intros n0; Case m; Simpl.
Intro H; Inversion H.
Intros m0 H.
Apply locle_S with n1:=(pseudo_pred (S n0) (hd c))
n2:=m0; Simpl; Auto.
Rewrite <- pseudo_S_pred; Auto.
Generalize H; Case (hd c); Simpl;
Intros; Apply le_trans with m:=(glob2loc m0 (tl c));
Auto with sampled_str arith.
Intros; Case (hd c); Simpl; Auto.
Apply locle_glob2loc_le; Generalize H; Case (hd c); Simpl;
Auto with sampled_str arith.
Qed.
Lemma
glob2loc_le_locle: (m,n:nat; c:clock)
(locle n m c (const true))->(le n (glob2loc m c)).
Proof.
Intros m; Elim m.
Intros n c H; Generalize (locle_le H); Intro H'; Inversion H'; Auto with arith.
Intros m0 HR n c H; Inversion_clear H; Auto with arith.
Simpl; Apply le_trans with m:=(pseudo_S n1 (hd c)); Auto.
Simpl in H1; Injection H1; Intro H5; Rewrite <- H5 in H4.
Case (hd c); Simpl; Auto with arith.
Qed.
Lemma
glob2loc_clock_inf: (n:nat; c1,c2:clock)
(clock_inf c1 c2)->(le (glob2loc n c1) (glob2loc n c2)).
Proof.
Intros n; Elim n; Simpl; Auto.
Intros m HR c1 c2 H; Inversion_clear H.
Generalize H0; Case (hd c2); Simpl; Case (hd c1); Simpl; Auto with arith.
Intro H; Discriminate H.
Qed.
Lemma
locle_clock_inf: (n:nat; c1,c2:clock)
(clock_inf c1 c2)->(locle (glob2loc n c1) (glob2loc n c2) c1 c2).
Proof.
Cofix locle_clock_inf; Intros n; Case n; Simpl.
Intros; Apply locle_O.
Intros n0 c1 c2 H;
Apply locle_S with n1:=(glob2loc n0 (tl c1))
n2:=(glob2loc n0 (tl c2)); Inversion_clear H; Auto.
Apply glob2loc_clock_inf; Auto.
Qed.
Lemma
locle_trans:(n1,n2,n3:nat; c1,c2,c3:clock)
(locle n1 n2 c1 c2)->(locle n2 n3 c2 c3)->(locle n1 n3 c1 c3).
Proof.
Cofix locle_trans.
Intros n1; Case n1.
Intros; Apply locle_O.
Intros n1' n2 n3 c1 c2 c3 H1 H2; Generalize H1; Case H2.
Intros n2' c2' c3' H; Generalize (locle_le H); Intro H'; Inversion H'.
Intros n2' m2' n3' m3' c2' c3' h1 h2 h3 h4 h5 h6;
Apply locle_S with n1:=(pseudo_pred (S n1') (hd c1))
n2:=n3'; Auto.
Rewrite <- pseudo_S_pred; Auto.
Inversion_clear h6; Rewrite H0 in h1.
Apply le_trans with m:=n2'; Auto.
Apply le_trans with m:=n4; Auto.
Apply le_trans with m:=n0; Auto.
Generalize H; Case (hd c1); Auto with arith.
Generalize h1; Case (hd c2'); Auto with arith.
Inversion_clear h6; EApply leb_trans; EAuto.
Apply locle_trans with n2:=n2' c2:=(tl c2'); Auto.
Inversion_clear h6.
Apply locle_le_1 with n1:=n0.
Apply locle_le_2 with n2:=n4; Auto.
Generalize h1; Rewrite H0; Case (hd c2'); Simpl; Auto with arith.
Generalize H; Case (hd c1); Auto with arith.
Qed.
Lemma
locle_glob2loc_trans:
(n1,n2,m:nat; c1,c2:clock)
(locle n1 n2 c1 c2)->(le n2 (glob2loc m c2))->(le n1 (glob2loc m c1)).
Proof.
Intros n1 n2 m c1 c2 H1 H2; Apply glob2loc_le_locle;
Apply locle_trans with n2:=n2 c2:=c2; Auto.
Apply locle_glob2loc_le; Auto.
Qed.
Require Omega.
Lemma
locle_S_S: (n1,n2:nat; c1,c2:clock)(locle (S n1) (S n2) c1 c2)->(locle n1 n2 c1 c2).
Proof.
Cofix locle_S_S; Intros n1 n2 c1 c2; Case n1.
Intros; Apply locle_O.
Intros n1'; Case n2.
Intros H1; Generalize (locle_le H1); Intros H2; Inversion H2. Inversion H0.
Intros n2' H1.
Apply locle_S with n1:=(pseudo_pred (S n1') (hd c1))
n2:=(pseudo_pred (S n2') (hd c2)).
Rewrite <- pseudo_S_pred; Auto.
Rewrite <- pseudo_S_pred; Auto.
Inversion_clear H1; Generalize H H3; Case (hd c1); Simpl.
Intros H5 H6; Rewrite H6 in H0; Simpl in H0; Rewrite H6; Simpl; Omega.
Intros H5 H6; Generalize H0; Case (hd c2); Simpl; Intros; Omega.
Inversion_clear H1; Auto.
Apply locle_S_S; Inversion_clear H1; Generalize H H3; Case (hd c1); Simpl.
Intros H5 H6; Rewrite H6 in H0; Rewrite H6; Simpl; Simpl in H0; Injection H0;
Clear H0; Intro H0; Rewrite H0; Apply locle_le_1 with n1:=n0; Auto with arith.
Intros H5 H6; Generalize H0; Case (hd c2); Simpl; Intros H7.
Injection H7; Clear H7; Intro H7; Rewrite H7; EApply locle_le_1; EAuto.
Rewrite H7; EApply locle_le_1; EAuto.
Qed.
(* BEGIN Bottom order for samplStr A *)
(* Flat order for samplElts *)
Definition
flat_ord :=[b1,b2:bool; x:(samplElt A b1); y:(samplElt A b2)]
Cases x of
| Fail => True (* b1=b2 *)
| _ => x==<(samplElt A)>y
end.
Lemma
flat_ord_inv_leb: (b1,b2:bool; x:(samplElt A b1); y:(samplElt A b2))
(flat_ord x y)->(leb b2 b1).
Proof.
Intros b1 b2 x y; Case x; Simpl; Auto with sampled_str.
Intros; Rewrite <- eq_dep_eq_param with P:=(samplElt A) x:=(None A) y:=y; Simpl; Auto.
Qed.
(*
Lemma flat_ord_inv_b: (b1,b2:bool; x:(samplElt A b1); y:(samplElt A b2))
(flat_ord x y)->b1=b2.
Proof.
Intros b1 b2 x; Case x; Simpl; Auto; Intros; EApply eq_dep_eq_param with P:=(samplElt A); EAuto.
Qed.
*)
Lemma
flat_ord_is_no_Fail: (b1,b2:bool; x:(samplElt A b1); y:(samplElt A b2))
(flat_ord x y)->(is_no_Fail x)->(is_no_Fail y).
Proof.
Intros b1 b2 x y; Case x; Case y; Simpl; Auto.
Intros H; Inversion_clear H.
Intros a H; Inversion_clear H.
Qed.
Lemma
flat_ord_refl:(b1,b2:bool; x:(samplElt A b1); y:(samplElt A b2))
x==<(samplElt A)>y -> (flat_ord x y).
Proof.
Intros b1 b2 x y H; Case H; Simpl; Auto with sampled_str.
Case x; Simpl; Auto with eqD.
Qed.
Lemma
flat_ord_antisym:(b1,b2:bool; x:(samplElt A b1); y:(samplElt A b2))
(flat_ord x y)->(flat_ord y x)->x==<(samplElt A)>y.
Proof.
Intros b1 b2 x; Case x; Simpl; Auto with eqD.
Intros y; Case y; Simpl; Auto with eqD.
Qed.
Lemma
flat_ord_trans:(b1,b2,b3:bool; x:(samplElt A b1); y:(samplElt A b2); z:(samplElt A b3))
(flat_ord x y)->(flat_ord y z)->(flat_ord x z).
Proof.
Intros b1 b2 b3 x; Case x; Simpl; Auto.
Intros y z H; Pattern b2 y;
Apply eq_dep_ind_l with x:=(None A); Simpl; Auto with eqD.
Intros a y z H; Pattern b2 y;
Apply eq_dep_ind_l with x:=(Any a); Simpl; Auto with eqD.
(* Intros y z H; Generalize y; Rewrite <- H.
Intros y'; Pattern y'; Apply samplElt_true_inv; Simpl; Auto.
Intros; Apply eq_dep_eq_param with P:=(samplElt A) x:=(Any a) y:=z; Auto.*)
Qed.
Hints Resolve flat_ord_refl flat_ord_antisym: sampled_str.
(* Bottom order on the n first elts *)
Definition
sp_inf:=
[n:nat; c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2)]
(m:nat)(le m n)->(flat_ord (sp_nth m s1) (sp_nth m s2)).
Lemma
sp_inf_refl:
(c:clock; s:(samplStr A c))(n:nat)(sp_inf n s s).
Proof.
Unfold sp_inf; Auto with sampled_str.
Qed.
Lemma
sp_inf_trans:
(c1,c2,c3:clock; s1:(samplStr A c1); s2:(samplStr A c2); s3:(samplStr A c3))
(n:nat)(sp_inf n s1 s2)->(sp_inf n s2 s3)->(sp_inf n s1 s3).
Proof.
Unfold sp_inf; Intros c1 c2 c3 s1 s2 s3 n H1 H2 m H;
Apply flat_ord_trans with y:= (sp_nth m s2); Auto.
Qed.
Lemma
sp_inf_proof_O:
(c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
(flat_ord (sp_hd s1) (sp_hd s2))->(sp_inf O s1 s2).
Proof.
Unfold sp_inf; Intros c1 c2 s1 s2 H m H1; Inversion H1;
Unfold sp_nth; Simpl; Auto with sampled_str.
Qed.
Lemma
sp_inf_O_inv:
(c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
(sp_inf O s1 s2)->(flat_ord (sp_hd s1) (sp_hd s2)).
Proof.
Unfold sp_inf; Intros c1 c2 s1 s2 H; Apply H with m:=O; Auto with arith.
Qed.
Lemma
sp_inf_proof_S_n:
(n:nat;c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
(flat_ord (sp_hd s1) (sp_hd s2))->(sp_inf n (sp_tl s1) (sp_tl s2))->(sp_inf (S n) s1 s2).
Proof.
Unfold sp_inf clock_nth sp_nth; Intros n c1 c2 s1 s2 H HR m; Case m; Simpl; Auto with arith.
Intros m0 H1;
Pattern (tl (clock_nth_tl m0 c1)) (sp_tl (sp_nth_tl m0 s1));
Apply eq_dep_ind_l with x:=(sp_nth_tl m0 (sp_tl s1)); Auto with eqD sampled_str;
Pattern (tl (clock_nth_tl m0 c2)) (sp_tl (sp_nth_tl m0 s2));
Apply eq_dep_ind_l with x:=(sp_nth_tl m0 (sp_tl s2)); Auto with eqD arith sampled_str.
Qed.
Lemma
sp_inf_S_n_inv:
(n:nat;c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
(sp_inf (S n) s1 s2)->(flat_ord (sp_hd s1) (sp_hd s2))/\(sp_inf n (sp_tl s1) (sp_tl s2)).
Proof.
Unfold sp_inf clock_nth sp_nth; Intros n c1 c2 s1 s2 H; Constructor 1.
Apply H with m:=O; Auto with arith.
Intros m H'.
Pattern (clock_nth_tl m (tl c1)) (sp_nth_tl m (sp_tl s1));
Apply eq_dep_ind_l with x:=(sp_tl (sp_nth_tl m s1)); Auto with arith sampled_str eqD.
Pattern (clock_nth_tl m (tl c2)) (sp_nth_tl m (sp_tl s2));
Apply eq_dep_ind_l with x:=(sp_tl (sp_nth_tl m s2)); Auto with arith sampled_str eqD.
Apply H with m:=(S m); Auto with arith.
Qed.
Lemma
sp_inf_loc_nfstwf:
(n,p:nat; c1:clock; s1:(samplStr A c1))(loc_nfstwf (glob2loc n c1) s1)->
(c2:clock; s2:(samplStr A c2))(sp_inf n s1 s2)->p=(glob2loc n c2)->(loc_nfstwf p s2).
Proof.
Cofix sp_inf_loc_nfstwf.
Intros n p; Case p; Simpl.
Intros; Apply loc_nfstwf_O.
Clear p; Intro p; Case n; Simpl.
Intros c1 s1 H1 c2 s2 H2 H3; Inversion H3.
Intros n0 c1 s1 H1 c2 s2 H2 H3; Case (sp_inf_S_n_inv H2); Intros H5 H6;
Generalize (flat_ord_inv_leb H5); Intros H7; Case (eq_false_dec (hd c2)).
Intros H4; Apply loc_nfstwf_false.
Auto.
Apply sp_inf_loc_nfstwf with n:=n0 s1:=(sp_tl s1); Auto.
Case (eq_false_dec (hd c1)); Intro H8; Rewrite H8 in H1; Simpl in H1; Auto with sampled_str.
Rewrite H4 in H3; Auto.
Intros H4; Apply loc_nfstwf_true.
Auto.
Apply flat_ord_is_no_Fail with x:=(sp_hd s1); Auto;
Rewrite H4 in H7; Simpl in H7; Rewrite H7 in H1;
Apply loc_nfstwf_is_no_Fail with n:=(glob2loc n0 (tl c1)); Auto.
Apply sp_inf_loc_nfstwf with n:=n0 s1:=(sp_tl s1); Auto.
Rewrite H4 in H7; Simpl in H7; Rewrite H7 in H1; Apply loc_nfstwf_S_n_true_inv; Auto.
Rewrite H4 in H3; Auto.
Qed.
Lemma
sp_inf_loc_nfstwf_ext:
(n:nat; c1:clock; s1:(samplStr A c1))(loc_nfstwf (S n) s1)->
(c2:clock; s2:(samplStr A c2))
(sp_inf n s1 s2)->
(m:nat)(le m n)->(sp_nth m s1)==<(samplElt A)>(sp_nth m s2).
Proof.
Unfold sp_inf; Intros n c1 s1 H1 c2 s2 H2 m H3;
Generalize (H2 m H3); LApply (loc_nfstwf_lt_is_no_Fail H1 5!m); Auto with arith.
Generalize (clock_nth m c1) (sp_nth m s1) (clock_nth m c2) (sp_nth m s2).
Intros b x; Case x; Simpl; Auto.
Intros b' y H; Elim H.
Qed.
Lemma
sp_inf_S_n:
(n:nat; c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
(sp_inf (S n) s1 s2)->(sp_inf n s1 s2).
Proof.
Unfold sp_inf sp_nth; Intros n c1 c2 s1 s2 H1 m H2; Auto with arith.
Qed.
Lemma
sp_nth_tl_inf:
(n,m:nat; c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
(sp_inf (plus n m) s1 s2)->
(sp_inf n (sp_nth_tl m s1) (sp_nth_tl m s2)).
Proof.
Unfold sp_inf; Intros n m c1 c2 s1 s2 H m0 H0.
Pattern (clock_nth m0 (clock_nth_tl m c1)) (sp_nth m0 (sp_nth_tl m s1));
Apply eq_dep_ind_l with x:=(sp_nth (plus m0 m) s1); Auto with arith sampled_str eqD.
Pattern (clock_nth m0 (clock_nth_tl m c2)) (sp_nth m0 (sp_nth_tl m s2));
Apply eq_dep_ind_l with x:=(sp_nth (plus m0 m) s2); Auto with arith sampled_str eqD.
Qed.
Lemma
sp_inf_le_eq_refl:
(c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2); n:nat)
((m:nat)(le m n)->(sp_nth m s1)==<(samplElt A)>(sp_nth m s2))
->(sp_inf n s1 s2).
Proof.
Unfold sp_inf; Intros c1 c2 s1 s2 n H m H1.
Pattern (clock_nth m c2) (sp_nth m s2);
Apply eq_dep_ind_l with x:=(sp_nth m s1); Auto with arith sampled_str eqD.
Qed.
Lemma
sp_inf_sp_eq:
(c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))(sp_eq s1 s2)->(n:nat)(sp_inf n s1 s2).
Proof.
Unfold sp_inf; Intros; Auto with sampled_str.
Qed.
Hints Resolve sp_inf_sp_eq sp_inf_proof_O sp_inf_proof_S_n sp_inf_S_n
sp_inf_refl sp_inf_O_inv sp_inf_S_n_inv : sampled_str.
Lemma
sp_inf_wf_eq:
(c1,c2:clock; s1:(samplStr A c1); s2:(samplStr A c2))
((n:nat)(sp_inf n s1 s2))->(sp_wf s1)->(sp_eq s1 s2).
Proof.
Intros; Apply sp_nth_sp_eq; Intros n; Apply sp_inf_loc_nfstwf_ext with n:=n; Auto with
sampled_str arith.
Qed.
(* Miminum elt for the "Bottom" order *)
Definition
elt_fail :=
[b:bool]<(samplElt A)>Cases b of true => (Fail A) | false => (None A) end.
CoFixpoint
undef: (c:clock)(samplStr A c) :=
[c:clock](sp_cons (elt_fail (hd c)) (undef (tl c))).
Lemma
undef_min: (n:nat; c:clock; s:(samplStr A c))(sp_inf n (undef c) s).
Proof.
Intros n; Elim n.
Intros c s; Apply sp_inf_proof_O; Simpl; Case (sp_hd s); Simpl; Auto.
Intros m HR c s; Apply sp_inf_proof_S_n; Simpl; Auto.
Case (sp_hd s); Simpl; Auto.
Qed.
Hints Resolve undef_min: sampled_str.
(* END "Bottom" order for samplStr A *)
(* BEGIN a concatenation function for samplStr As *)
Fixpoint
sp_app_n[c:clock; s1: (samplStr A c); n:nat]:
(samplStr A (clock_nth_tl n c)) -> (samplStr A c)
:=
<[n:nat](samplStr A (clock_nth_tl n c))->(samplStr A c)>Cases n of
O => [s2]s2
| (S m) => [s2](sp_app_n s1 (sp_cons (sp_nth m s1) s2))
end.
Lemma
sp_app_nth_tl:
(n:nat; c:clock; s1: (samplStr A c); s2:(samplStr A (clock_nth_tl n c)))
(sp_nth_tl n (sp_app_n s1 s2))=s2.
Proof.
Intros n; Elim n; Simpl; Auto.
Intros m HR c' s1 s2; Rewrite HR; Auto.
Qed.
Lemma
sp_nth_app_lt:
(n,m:nat; c:clock; s1: (samplStr A c); s2:(samplStr A (clock_nth_tl m c)))
(lt n m)->(sp_nth n (sp_app_n s1 s2))=(sp_nth n s1).
Proof.
Intros n m; Generalize n; Clear n; Elim m; Simpl.
Intros n c s1 s2 H; Inversion H.
Unfold sp_nth; Intros m' HR n c s1 s2 H; Inversion_clear H.
Rewrite sp_app_nth_tl; Simpl; Auto.
Rewrite HR; Auto with arith.
Qed.
Lemma
sp_app_eq_1:
(n:nat; c:clock; s1,s2: (samplStr A c); s3:(samplStr A (clock_nth_tl n c)))
((m:nat)(lt m n)->(sp_nth m s1) = (sp_nth m s2))
->(sp_app_n s1 s3)=(sp_app_n s2 s3).
Proof.
Intros n; Elim n; Simpl; Auto.
Intros m HR c s1 s2 s3 H; Rewrite H; Auto with arith.
Qed.
Lemma
sp_app_sp_inf_1:
(n:nat;c:clock; s1:(samplStr A c); s2:(samplStr A (clock_nth_tl (S n) c)))
(sp_inf n s1 (sp_app_n s1 s2)).
Proof.
Unfold sp_inf; Intros; Rewrite sp_nth_app_lt; Auto with arith sampled_str.
Qed.
(* END a concatenation function for samplStr As *)
Fixpoint
glob_nfstwf [n:nat]:(c:clock)(samplStr A c)->Prop :=
[c; s]
Cases n of
| O => True
| (S m) => (is_no_Fail (sp_hd s)) /\ (glob_nfstwf m (sp_tl s))
end.
Lemma
glob_nfstwf_p1:(c:clock; s:(samplStr A c))(glob_nfstwf O s).
Simpl; Auto.
Qed.
Lemma
glob_nfstwf_p2:(n:nat; c:clock; s:(samplStr A c))
(is_no_Fail (sp_hd s))->(glob_nfstwf n (sp_tl s))->(glob_nfstwf (S n) s).
Intros n c s; Simpl; Auto.
Qed.
Hints Resolve glob_nfstwf_p2: sampled_str.
Lemma
glob_nfstwf_S_n_n:
(n:nat; c:clock; s:(samplStr A c))
(glob_nfstwf (S n) s)->(glob_nfstwf n s).
Proof.
Intros n; Elim n.
Simpl; Auto.
Intros m HR c s H1; Apply glob_nfstwf_p2; Case H1; Auto.
Qed.
Hints Resolve glob_nfstwf_S_n_n: sampled_str.
Lemma
glob_nfstwf_n_le:
(n,m:nat; c: clock; s:(samplStr A c))
(glob_nfstwf n s)->(le m n)->(glob_nfstwf m s).
Proof.
Intros n m c s H1 H; Generalize c s H1; Elim H; Simpl; Auto with sampled_str.
Qed.
Lemma
sp_wf_glob_nfstwf:
(c:clock; s:(samplStr A c))(sp_wf s)->(n:nat)(glob_nfstwf n s).
Proof.
Intros c s H n; Generalize c s H; Elim n; Clear H s c.
Simpl; Auto.
Intros m HR c s H; Case H; Auto with sampled_str.
Qed.
Lemma
glob_nfstwf_sp_wf:
(c:clock; s:(samplStr A c))((n:nat)(glob_nfstwf n s))->(sp_wf s).
Proof.
Cofix glob_nfstwf_sp_wf.
Intros c s H; Constructor 1.
Case (H (S O)); Simpl; Auto.
Apply glob_nfstwf_sp_wf.
Intros n; Case (H (S n)); Auto.
Qed.
(*
Lemma glob_nfstwf_nth:
(n:nat; c:clock; s:(samplStr A c))
(glob_nfstwf (S n) s)->(is_no_Fail (sp_nth n s)).
Simpl; Intros n c s H; Case H; Generalize c s; Elim n; Auto.
Unfold sp_nth; Simpl; Auto.
Unfold sp_nth; Intros m HR c' s'; Simpl; Intros H1 H2; Case H2; Intros.
Change ([s0:clock; s1:(samplStr A s0)](is_no_Fail 1!(hd s0) (sp_hd s1))
(tl (clock_nth_tl m c')) (sp_tl (sp_nth_tl m s'))).
Apply eq_dep_ind_l with x:=(sp_nth_tl m (sp_tl s')); Auto with sampled_str eqD
.
Change (is_no_Fail 1!(clock_nth ? ?) (sp_hd (sp_nth_tl m (sp_tl s')))).
Auto.
Qed.
*)
Lemma
loc_nfstwf_glob_nfstwf:
(n:nat; c:clock; s:(samplStr A c))
(loc_nfstwf (glob2loc n c) s)
->(glob_nfstwf n s).
Proof.
Intros n; Elim n; Simpl; Auto.
Intros m HR c; Rewrite (unfold_Str c); Case (hd c);
Simpl; Intros s H; Constructor 1; Auto.
Apply loc_nfstwf_is_no_Fail with
n:=(glob2loc m (tl c))
s:=s; Auto.
Apply HR; Apply loc_nfstwf_S_n_true_inv with s:=s; Simpl; Auto.
Pattern (sp_hd s); Apply samplElt_false_inv; Simpl; Auto.
Apply HR; Apply loc_nfstwf_false_inv with s:=s; Simpl; Auto.
Qed.
Lemma
glob_nfstwf_loc_nfstwf:
(n:nat; c:clock; s:(samplStr A c))
(glob_nfstwf n s)->(loc_nfstwf (glob2loc n c) s).
Proof.
Cut (n,m:nat; c:clock; s:(samplStr A c))
(glob_nfstwf n s)
->m=(glob2loc n c)
->(loc_nfstwf m s); EAuto.
Cofix glob_nfstwf_loc_nfstwf; Intros n; Case n; Simpl.
Intros m c s H H0; Rewrite H0; Apply loc_nfstwf_O.
Intros n' m c s H H0; Case (eq_false_dec (hd c)).
Intros H1; Apply loc_nfstwf_false.
Auto.
Apply glob_nfstwf_loc_nfstwf with n:=n'.
Case H; Auto.
Rewrite H0; Rewrite H1; Simpl; Auto.
Intros H1; Generalize H0; Case m.
Intros; Apply loc_nfstwf_O.
Intros m' H'; Apply loc_nfstwf_true.
Auto.
Case H; Auto.
Apply glob_nfstwf_loc_nfstwf with n:=n'.
Case H; Auto.
Rewrite H1 in H'; Simpl in H'.
Injection H'; Auto.
Qed.
Hints Resolve glob2loc_S_le glob2loc_preserves_le: sampled_str.
Require Peano_dec.
Fixpoint
loc2glob_x[n:nat; c:clock; m,k:nat]: nat :=
Cases k of
| O => (minus m k)
| (S x) =>
Cases (eq_nat_dec n (glob2loc (minus m (S x)) c)) of
| (left _) => (minus m (S x))
| (right _) => (loc2glob_x n c m x)
end
end.
Definition
loc2glob:=[n:nat; c:clock; m:nat](loc2glob_x n c m m).
Lemma
minus_le_pred:(n,m:nat)(le (S m) n)->(S (minus n (S m)))=(minus n m).
Proof.
Intros n; Elim n; Simpl; Auto.
Intros m H; Inversion H.
Intros n' HR m; Case m; Simpl.
Intros; Rewrite <- minus_n_O; Auto.
Auto with arith.
Qed.
Lemma
loc2glob_x_prop:(c:clock; n,m,k:nat)
(le k m) ->
(le n (glob2loc m c)) ->
(le (glob2loc (minus m k) c) n) ->
(glob2loc (loc2glob_x n c m k) c)=n.
Proof.
Intros c n m k; Elim k.
Simpl; Rewrite <- minus_n_O; Auto with arith.
Intros k' HR H1 H2 H3; Simpl; Case
(eq_nat_dec n (glob2loc (minus m (S k')) c)).
Auto.
Intros H'; Apply HR; Auto with arith.
Inversion H3.
Case H'; Auto.
Apply le_trans with m:=(S (glob2loc (minus m (S k')) c));
Auto with arith.
Rewrite <- (minus_le_pred H1); Auto with sampled_str.
Qed.
Lemma
loc2glob_prop:(c:clock; n,m:nat)
(le n (glob2loc m c)) ->
(glob2loc (loc2glob n c m) c)=n.
Proof.
Unfold loc2glob; Intros; Apply loc2glob_x_prop; Auto;
Rewrite <- minus_n_n; Auto with arith.
Qed.
Lemma
loc2glob_x_inv_le:(c:clock; n,m,k:nat)
(le k m) -> (le (minus m k) n) ->
(le (loc2glob_x (glob2loc n c) c m k) n).
Proof.
Intros c n m k; Elim k; Simpl; Auto.
Intros k' HR H1 H2;
Case (eq_nat_dec (glob2loc n c)
(glob2loc (minus m (S k')) c)); Auto.
Intros H; Apply HR; Auto with arith.
Inversion H2.
Case H; Rewrite H0; Auto.
Rewrite <- (minus_le_pred H1); Auto with arith.
Qed.
Lemma
loc2glob_inv_le:
(c:clock; n,m:nat)(le (loc2glob (glob2loc n c) c m) n).
Proof.
Unfold loc2glob; Intros; Apply loc2glob_x_inv_le.
Auto with arith.
Rewrite <- minus_n_n; Auto with arith.
Qed.
Lemma
loc2glob_x_le:(c:clock; n,m,k:nat)
(le k m)->
(le (minus m k) (loc2glob_x n c m k)).
Proof.
Intros c n m k; Elim k; Simpl; Auto.
Intros k' HR H1; Case (eq_nat_dec n (glob2loc (minus m (S k')) c));
Auto with arith.
Intro H; Apply le_trans with m:=(minus m k'); Auto with arith.
Rewrite <- (minus_le_pred H1); Auto with arith.
Qed.
Lemma
loc2glob_x_le':(c:clock; n,m,k:nat)
(le (loc2glob_x n c m k) m).
Proof.
Intros c n m k; Elim k; Simpl.
Rewrite <- minus_n_O; Auto.
Intros n0 HR; Case (eq_nat_dec n (glob2loc (minus m (S n0)) c)); Simpl; Auto.
Intros; Omega.
Qed.
Lemma
loc2glob_le:(c:clock; n,m:nat)(le (loc2glob n c m) m).
Proof.
Intros c n m; Unfold loc2glob; Apply loc2glob_x_le'.
Qed.
Hints Resolve loc2glob_le: sampled_str.
Lemma
loc2glob_x_S_m_eq:(c:clock; n,m,k:nat)
(le k m) ->
(le n (glob2loc m c)) ->
(le (glob2loc (minus m k) c) n) ->
(loc2glob_x n c m k)=(loc2glob_x n c (S m) (S k)).
Proof.
Intros c n m k; Elim k; Simpl.
Rewrite <- minus_n_O; Simpl.
Intros H1 H2 H3; Case (eq_nat_dec n (glob2loc m c)); Auto.
Intros H4; Case H4; Auto with arith.
Intros k' HR H1 H2; Generalize HR; Clear HR.
Rewrite <- (minus_le_pred H1); Intros HR H3.
Case (eq_nat_dec n (glob2loc (minus m (S k')) c)); Auto.
Intro H4; Apply HR; Auto with arith.
Apply le_trans with m:=(S (glob2loc (minus m (S k')) c)); Auto with sampled_str.
Omega.
Qed.
Lemma
loc2glob_S_m_eq:(c:clock; n,m:nat)
(le n (glob2loc m c)) ->
(loc2glob n c m)=(loc2glob n c (S m)).
Proof.
Unfold loc2glob; Intros; Apply loc2glob_x_S_m_eq; Auto.
Rewrite <- minus_n_n; Auto with arith.
Qed.
Lemma
loc2glob_x_n_S_lt:(c:clock; n,m,k:nat)
(le k m) ->
(le (glob2loc (minus m k) c) n) ->
(lt n (glob2loc m c)) ->
(lt (loc2glob_x n c m k) (loc2glob_x (S n) c m k)).
Proof.
Intros c n m k; Elim k; Simpl; Auto.
Rewrite <- minus_n_O; Intros H1 H2 H3; Case (lt_not_le n (glob2loc m c));
Auto.
Intros k' HR H1 H2 H3;
Case (eq_nat_dec (S n) (glob2loc (minus m (S k')) c)).
Intro H; Rewrite <- H in H2; Case (le_Sn_n n); Auto.
Intro H; Case (eq_nat_dec n (glob2loc (minus m (S k')) c)).
Intros H0; Apply lt_le_trans with m:=(minus m k').
Rewrite <- (minus_le_pred H1); Auto with arith.
Apply loc2glob_x_le; Auto with arith.
Intros H'; Apply HR; Auto with arith.
Inversion H2.
Case H'; Auto.
Rewrite <- (minus_le_pred H1);
Apply le_trans with m:=(S (glob2loc (minus m (S k')) c));
Auto with arith sampled_str.
Qed.
Lemma
loc2glob_S_lt:
(c:clock; n,m:nat)
(lt n (glob2loc m c))
->(lt (loc2glob n c m) (loc2glob (S n) c m)).
Proof.
Unfold loc2glob; Intros; Apply loc2glob_x_n_S_lt; Auto.
Rewrite <- minus_n_n; Simpl; Auto with arith.
Qed.
Lemma
loc2glob_O:(c:clock; m:nat)
(loc2glob O c m)=O.
Proof.
Unfold loc2glob; Intros c m; Case m; Simpl; Auto with arith.
Intros m'; Rewrite <- (minus_n_n m'); Simpl; Case (eq_nat_dec O O); Auto.
Intro H; Case H; Auto.
Qed.
Lemma
loc2glob_x_tl_true :
(c:clock; n,m,k:nat)
(hd c)=true->
(le k m) ->
(loc2glob_x (S n) c (S m) k)=
(S (loc2glob_x n (tl c) m k)).
Proof.
Intros c n m k H2; Elim k.
Simpl; Rewrite <- minus_n_O; Simpl; Auto.
Simpl; Intros k' HR H3.
Rewrite <- (minus_le_pred H3); Simpl; Rewrite H2; Simpl.
Case (eq_nat_dec n (glob2loc (minus m (S k')) (tl c))).
Intro H5; Rewrite <- H5; Case (eq_nat_dec (S n) (S n)); Auto.
Intro H; Case H; Auto.
Intro H5; Case (eq_nat_dec (S n) (S (glob2loc (minus m (S k')) (tl c)))).
Intro H6; Case H5; Auto with arith.
Intros; Apply HR; Auto with arith.
Qed.
Lemma
loc2glob_tl_true :
(c:clock; n,m:nat)
(hd c)=true->
(loc2glob (S n) c (S m))=(S (loc2glob n (tl c) m)).
Proof.
Intros c n m H1; Unfold loc2glob; Simpl.
Rewrite <- (minus_n_n m); Simpl.
Case (eq_nat_dec (S n) (0)).
Intro H; Discriminate H.
Intros; Apply loc2glob_x_tl_true; Auto with arith.
Qed.
End Sampled_streams_props.
Hints Resolve loc_nfstwf_O loc_nfstwf_false loc_nfstwf_true: sampled_str.
Hints Resolve sp_wf_loc_nfstwf loc_nfstwf_sp_wf: sampled_str.
Hints Resolve sp_inf_proof_O sp_inf_proof_S_n sp_inf_S_n
sp_inf_refl sp_inf_O_inv sp_inf_sp_eq: sampled_str.
Hints Resolve loc2glob_le: sampled_str.
Hints Resolve glob2loc_S_le glob2loc_preserves_le: sampled_str.
Section nfstwf_conversion.
Hints Resolve loc_nfstwf_false_inv loc_nfstwf_S_n_n_tl: sampled_str.
Hints Resolve loc_nfstwf_glob_nfstwf glob_nfstwf_loc_nfstwf : sampled_str.
Variable A,B:Set.
Lemma
nfstwf_function_convert:
(c: clock; f: (samplStr A c) -> (samplStr B c); n:nat)
((m:nat; s:(samplStr A c))
(le m (glob2loc n c))->(loc_nfstwf m s)->(loc_nfstwf m (f s)))
->(m:nat; s:(samplStr A c))
(le m n)
->(glob_nfstwf m s)->(glob_nfstwf m (f s)).
Proof.
Auto with sampled_str.
Qed.
Lemma
nfstwf_function_convert_inf:
(c1,c2: clock; f: (samplStr A c1) -> (samplStr B c2); n:nat)
((m:nat; s:(samplStr A c1))
(le m (glob2loc n c2))->
((k:nat)(locle k m c1 c2)->(loc_nfstwf k s))
->(loc_nfstwf m (f s)))
->(m:nat; s:(samplStr A c1))
(le m n)
->(glob_nfstwf m s)->(glob_nfstwf m (f s)).
Proof.
Intros c1 c2 f n H m s H0 H1; Apply loc_nfstwf_glob_nfstwf.
Apply H; Auto with sampled_str.
Intros k H2; Rewrite <- (loc2glob_prop 1!c1 2!k 3!m).
Apply glob_nfstwf_loc_nfstwf.
Apply glob_nfstwf_n_le with n:=m; Auto with sampled_str.
Apply locle_glob2loc_trans with n2:=(glob2loc m c2) c2:=c2; Auto.
Qed.
Lemma
nfstwf_function_convert_sup:
(c1,c2: clock; f: (samplStr A c1) -> (samplStr B c2); n:nat)
(clock_inf c2 c1)->
((m,k:nat; s:(samplStr A c1))
(le m (glob2loc n c1))->
(loc_nfstwf m s)->
(locle k m c2 c1)
->(loc_nfstwf k (f s)))
->(m:nat; s:(samplStr A c1))
(le m n)
->(glob_nfstwf m s)->(glob_nfstwf m (f s)).
Proof.
Intros c1 c2 f n H' H m s H0 H1; Apply loc_nfstwf_glob_nfstwf.
Apply H with m:=(glob2loc m c1); Auto with sampled_str.
Apply locle_clock_inf; Auto.
Qed.
Lemma
nfstwf_function_convert_S:
(c: clock; f: (samplStr A c) -> (samplStr B c); n:nat)
((m:nat; s:(samplStr A c))
(le (S m) (glob2loc (S n) c))->(loc_nfstwf m s)->(loc_nfstwf (S m) (f s)))
->(m:nat; s:(samplStr A c))
(le m n)
->(glob_nfstwf m s)->(glob_nfstwf (S m) (f s)).
Proof.
Intros c f n H1 m s H2 H3.
Apply loc_nfstwf_glob_nfstwf.
Case (O_or_S (glob2loc (S m) c)).
Intros H; Case H; Intros m_l H4; Rewrite <- H4.
Apply H1.
Rewrite H4; Auto with arith sampled_str.
Rewrite <- (loc2glob_prop 1!c 2!m_l 3!m).
Apply glob_nfstwf_loc_nfstwf; Apply glob_nfstwf_n_le with n:=m;
Auto with sampled_str.
Apply le_S_n; Rewrite H4; Auto with sampled_str.
Intro H4; Rewrite <- H4; Simpl; Auto with sampled_str.
Qed.
Lemma
nfstwf_function_convert_S_recip:
(c: clock; f: (samplStr A c) -> (samplStr B c); n:nat)
((m:nat; s:(samplStr A c))
(lt m n)->(glob_nfstwf m s)->(glob_nfstwf (S m) (f s)))
->(m:nat; s:(samplStr A c))
(le (S m) (glob2loc n c))
->(loc_nfstwf m s)->(loc_nfstwf (S m) (f s)).
Proof.
Cut (c: clock; f: (samplStr A c) -> (samplStr B c); n:nat)
((m:nat; s:(samplStr A c))
(lt m n)->(glob_nfstwf m s)->(glob_nfstwf (S m) (f s)))
->(m:nat; s:(samplStr A c); t:(samplStr B c))
(le (S m) (glob2loc n c))
->(loc_nfstwf m s)->t=(f s)->(loc_nfstwf (S m) t).
EAuto.
Cofix foo; Intros c f n H1 m s t Hl H2 H3; Case (eq_false_dec (hd c)).
Intros H4; Apply loc_nfstwf_false; Auto.
Apply foo with f:=[x:(samplStr A (tl c))](sp_tl (f (sp_cons (sp_hd s) x)))
s:=(sp_tl s) n:=(pred n); Auto with sampled_str.
Intros m' s' Hl' H; Case (H1 (S m') (sp_cons (sp_hd s) s')); Auto.
Generalize Hl Hl'; Case n; Simpl; Auto with arith.
Intro H'; Inversion H'.
Apply glob_nfstwf_p2; Simpl; Auto.
Generalize (sp_hd s); Rewrite H4; Intros x; Pattern x;
Apply samplElt_false_inv; Simpl; Auto.
Generalize Hl; Case n; Simpl.
Intro H'; Inversion H'.
Rewrite H4; Simpl; Auto with arith.
Rewrite <- unfold_samplStr; Rewrite H3; Auto.
Intros H4; Apply loc_nfstwf_true; Auto.
Rewrite H3; Case (H1 O s); Simpl; Auto with arith.
Generalize Hl; Case n; Simpl; Auto with arith.
Intro H'; Inversion H'.
Generalize Hl H2; Case m; Simpl; Auto with sampled_str.
Intros m1 Hl' H2';
Apply foo with f:=[x:(samplStr A (tl c))](sp_tl (f (sp_cons (sp_hd s) x)))
s:=(sp_tl s) n:=(loc2glob (S m1) (tl c) (pred n)) ; Auto with sampled_str.
Intros m' s' H5 H6; Case (H1 (S m') (sp_cons (sp_hd s) s')); Auto.
Generalize Hl' H5; Case n; Simpl.
Intro H7; Inversion H7.
Rewrite H4; Simpl; Intros n' h1 h2.
Apply lt_n_S; Apply lt_le_trans with m:=(loc2glob (S m1) (tl c) n');
Auto with sampled_str.
Apply glob_nfstwf_p2; Simpl; Auto.
Apply loc_nfstwf_is_no_Fail with n:=m1; Auto.
Rewrite loc2glob_prop; Auto.
Generalize Hl'; Case n; Simpl.
Intro H7; Inversion H7.
Rewrite H4; Simpl; Auto with arith.
Rewrite <- unfold_samplStr; Rewrite H3; Auto.
Qed.
Theorem
rec0_nfstwf_inc_loc2glob:
(c: clock; f: (samplStr A c) -> (samplStr B c))
((n:nat; s:(samplStr A c))
(loc_nfstwf n s)->(loc_nfstwf (S n) (f s)))
->(n:nat; s:(samplStr A c))(glob_nfstwf n s)->(glob_nfstwf (S n) (f s)).
Proof.
Intros c f H1 n s H2; Apply nfstwf_function_convert_S with n:=n; Auto.
Qed.
Theorem
rec0_nfstwf_inc_glob2loc:
(c: clock; f: (samplStr A c) -> (samplStr B c))
((n:nat; s:(samplStr A c))
(glob_nfstwf n s)->(glob_nfstwf (S n) (f s)))
->(n:nat; s:(samplStr A c))(loc_nfstwf n s)->(loc_nfstwf (S n) (f s)).
Proof.
Cut (c: clock; f: (samplStr A c) -> (samplStr B c))
((n:nat; s:(samplStr A c))
(glob_nfstwf n s)->(glob_nfstwf (S n) (f s)))
->(n:nat; s:(samplStr A c); t:(samplStr B c))
(loc_nfstwf n s)->t=(f s)->(loc_nfstwf (S n) t).
EAuto.
Cofix foo; Intros c f H1 n s t H2 H3; Case (eq_false_dec (hd c)).
Intros H4; Apply loc_nfstwf_false; Auto.
Apply foo with f:=[x:(samplStr A (tl c))](sp_tl (f (sp_cons (sp_hd s) x)))
s:=(sp_tl s); Auto with sampled_str.
Intros m s' H; Case (H1 (S m) (sp_cons (sp_hd s) s')); Auto.
Apply glob_nfstwf_p2; Simpl; Auto.
Generalize (sp_hd s); Rewrite H4; Intros x; Pattern x;
Apply samplElt_false_inv; Simpl; Auto.
Rewrite <- unfold_samplStr; Rewrite H3; Auto.
Intros H4; Apply loc_nfstwf_true; Auto.
Rewrite H3; Case (H1 O s); Simpl; Auto.
Generalize H2; Case n; Simpl; Auto with sampled_str.
Intros n1 H5;
Apply foo with f:=[x:(samplStr A (tl c))](sp_tl (f (sp_cons (sp_hd s) x)))
s:=(sp_tl s); Auto with sampled_str.
Intros m s' H6; Case (H1 (S m) (sp_cons (sp_hd s) s')); Auto.
Apply glob_nfstwf_p2; Simpl; Auto.
Apply loc_nfstwf_is_no_Fail with n:=n1; Auto.
Rewrite <- unfold_samplStr; Rewrite H3; Auto.
Qed.
End nfstwf_conversion.
Implicit Arguments Off.
05/07/101, 15:43