### sp_rec.v

(* FILE: SAMPLED_STREAMS/sp_rec.v _ Sylvain Boulmé _ LIP6 _ Spring 2001 *)
(* Coq V6.3.1 *)
Implicit Arguments On.

Require Export sampled_streams.
Require Arith.

Section SP_rec.

Hints Resolve sp_tl_nth_tl: sampled_str.
Hints Resolve sp_eq_sp_nth sp_nth_sp_eq: sampled_str.
Hints Resolve loc_nfstwf_S_n_n loc_nfstwf_S_n_n_tl loc_nfstwf_nth: sampled_str.
Hints Resolve undef_min: sampled_str.

Variable A:Set.

Section Rec1.

(* HINTS: We build now a recursion operator for building *)
(* using "length-fail-preserving" functions,             *)
(*   which are "partial wellformness increasing"         *)

(* BEGIN hypothesis *)

Variable B: Set.

Variable C: B -> clock. (* we work at constant clock. *)

Variable F1: ((x:B)(samplStr A (C x))) -> (x:B)(samplStr A (C x)).

Variable P: B -> Prop.

Hypothesis F1_lfp:
(s1,s2:(x:B)(samplStr A (C x)); n:nat)
((x:B)(P x)->(sp_inf n (s1 x) (s2 x)))->(x:B)(P x)->(sp_inf n (F1 s1 x) (F1 s2 x)).

Hypothesis F1_nfstwf_inc:
(n:nat; s:(x:B)(samplStr A (C x)))
((x:B)(P x)->(loc_nfstwf n (s x)))
->(x:B)(P x)->(loc_nfstwf (S n) (F1 s x)).

(* END hypothesis *)

(* nth power of F1 *)
Lemma powerF1_loc_nfstwf:(n:nat;x:B)(P x)->
(
loc_nfstwf n (funPower F1 n [z:B](undef A (C z)) x)).
Proof.
Intros n; Elim n; Auto with sampled_str.
Intros; Rewrite <- funPower_commut ; Auto.
Qed.

Lemma powerF1_lfp:
(n,m:nat; s1,s2:(x:B)(
samplStr A (C x)))
((x:B)(P x)->(sp_inf m (s1 x) (s2 x)))->
(x:B)(P x)->(sp_inf m (funPower F1 n s1 x) (funPower F1 n s2 x)).
Proof.
Intros n; Elim n; Simpl; Auto.
Qed.

Lemma powerF1_increases:
(n,m:nat; x:B)(P x)->
(
sp_inf m (funPower F1 n [z:B](undef A (C z)) x) (funPower F1 (S n) [z:B](undef A (C z)) x)).
Proof.
Intros; Simpl; Apply powerF1_lfp; Auto with sampled_str.
Qed.

Hints Resolve powerF1_loc_nfstwf powerF1_increases: sampled_str.

Lemma powerF1_nth: (n,m:nat; x:B)(le n m)->(P x)->
(
sp_nth n (funPower F1 (S m) [z:B](undef A (C z)) x))
=(sp_nth n (funPower F1 (S (S m)) [z:B](undef A (C z)) x)).
Proof.
Intros n m x H H'; Apply eq_dep_eq with P:=(samplElt A);
Apply sp_inf_loc_nfstwf_ext with n:=m; Auto with sampled_str.
Qed.

Section Rec1_ext.

(* An extensionality property for the fixpoint "r0" we are trying to build *)

Variable r1: (x:B)(samplStr A (C x)).
Hypothesis r1_inv: (x:B)(P x)->(sp_eq (r1 x) (F1 r1 x)).

Lemma r1_prop:(n,m:nat;x:B)(P x)->(sp_inf m (funPower F1 n [z:B](undef A (C z)) x) (r1 x)).
Proof.
Intros n; Elim n.
Simpl; Auto with sampled_str.
Intros n' HR m x H'; Rewrite <- funPower_commut.
Apply sp_inf_trans with s2:=(F1 r1 x); Auto with sampled_str.
Qed.

Theorem r1_ext: (n:nat; x:B)(P x)->(sp_nth n (r1 x))=(sp_nth n (funPower F1 (S n) [z:B](undef A (C z)) x)).
Proof.
Intros n x H; Symmetry; Apply eq_dep_eq with P:=(samplElt A); Apply sp_inf_loc_nfstwf_ext with n:=n;
Auto with sampled_str arith.
Apply r1_prop; Auto.
Qed.

End Rec1_ext.

Local sp_app_powerF1_undef:
(n:nat; s:(x:B)(samplStr A (clock_nth_tl (S n) (C x))); x:B)(P x)->
(sp_app_n (funPower F1 n [z:B](undef A (C z)) x)
(sp_cons (sp_nth n (funPower F1 (S n) [z:B](undef A (C z)) x)) (s x)))
= (sp_app_n (funPower F1 (S n) [z:B](undef A (C z)) x) (s x)).
Proof.
Intros n s x H'; Simpl; Apply sp_app_eq_1.
Intros m H;
Change (sp_nth m (funPower F1 n [z:B](undef A (C z)) x))
=(sp_nth m (funPower F1 (S n) [z:B](undef A (C z)) x));
Inversion_clear H; Apply powerF1_nth; Auto with arith.
Qed.

CoFixpoint rec1_tmp: (n:nat)((x:B)(samplStr A (C x)))
->(x:B)(samplStr A (clock_nth_tl n (C x))):=
[n; s]
let s'=(F1 s) in [x](sp_cons (sp_nth n (s' x)) (rec1_tmp (S n) s' x)).

Local rec1_tmp_power:
(n:nat; x:B)(rec1_tmp n (funPower F1 n [z:B](undef A (C z))) x)
=(sp_cons (sp_nth n (funPower F1 (S n) [z:B](undef A (C z)) x))
(rec1_tmp (S n) (funPower F1 (S n) [z:B](undef A (C z))) x)).
Proof.
Intros n x; Rewrite (unfold_samplStr (rec1_tmp n (funPower F1 n [z:B](undef A (C z))) x)); Simpl;
Rewrite funPower_commut; Auto.
Qed.

Require Refine.

Lemma rec1_tmp_S_n_m: (n,m:nat; x:B)
(
sp_nth (S n) (rec1_tmp m (funPower F1 m [z:B](undef A (C z))) x))
==<(samplElt A)> (sp_nth n (rec1_tmp (S m) (funPower F1 (S m) [z:B](undef A (C z))) x)).
Proof.
Intros n0 m x; Rewrite rec1_tmp_power.
Unfold clock_nth sp_nth; Simpl.
Apply eq_dep_map_eq_dep with F:=(sp_hd 1!A);
Refine (sp_tl_nth_tl n0 ?).
Qed.

Lemma rec1_tmp_wf:
(n:nat; x:B)(P x)->(
sp_wf (rec1_tmp n (funPower F1 n [z:B](undef A (C z))) x)).
Proof.
Cofix rec1_tmp_wf.
Intros n x H; Rewrite rec1_tmp_power; Constructor 1; Unfold sp_hd sp_tl.
Apply loc_nfstwf_lt_is_no_Fail with n:=(S n) m:=n s:=(funPower F1 (S n) [z:B](undef A (C z)) x);
Auto with sampled_str.
Apply rec1_tmp_wf with n:=(S n) x:=x; Auto.
Qed.

Local rec1_tmp_lemma_aux:
(n:nat; x:B)(P x)->
(flat_ord (sp_nth n (F1 (funPower F1 n [z:B](undef A (C z))) x))
(sp_nth n (F1 [y:B](sp_app_n (funPower F1 n [z:B](undef A (C z)) y)
(rec1_tmp n (funPower F1 n [z:B](undef A (C z))) y)) x))).
Proof.
Intros n x H;
LApply (F1_lfp 1!(funPower F1 n [z:B](undef A (C z)))
2![y:B](sp_app_n (funPower F1 n [z:B](undef A (C z)) y)
(rec1_tmp n (funPower F1 n [z:B](undef A (C z))) y)) 3!n).
Unfold sp_inf; Auto with arith.
Clear H x; Unfold sp_inf; Intros x H' m H; Case H.
Unfold sp_nth; Rewrite sp_app_nth_tl; Rewrite rec1_tmp_power; Simpl.
Change (flat_ord (sp_nth m (funPower F1 m [z:B](undef A (C z)) x))
(sp_nth m (funPower F1 (S m) [z:B](undef A (C z)) x))).
Generalize (powerF1_increases m 2!m); Unfold sp_inf; Auto with arith.
Intros; Generalize sp_app_sp_inf_1; Unfold sp_inf; Auto with arith.
Qed.

Local rec1_tmp_lemma:
(n,m:nat; x:B)(P x)->
(sp_inf n (rec1_tmp m (funPower F1 m [z:B](undef A (C z))) x)
(sp_nth_tl m (F1 [y:B](sp_app_n (funPower F1 m [z:B](undef A (C z)) y)
(rec1_tmp m (funPower F1 m [z:B](undef A (C z))) y))
x))).
Proof.
Intros n; Elim n; Simpl.
Intros m x H; Apply sp_inf_proof_O; Simpl; Exact (rec1_tmp_lemma_aux m H).
Intros n0 HR m x H; Apply sp_inf_proof_S_n; Simpl.
Exact (rec1_tmp_lemma_aux m H).
Rewrite funPower_commut;
Apply sp_inf_trans with s2:=
(sp_nth_tl (S m)
(F1
[y:B]
(sp_app_n (funPower F1 (S m) [z:B](undef A (C z)) y)
(rec1_tmp (S m) (funPower F1 (S m) [z:B](undef A (C z))) y)) x)).
Exact (HR (S m) ? H).
Apply sp_nth_tl_inf with n:=n0 m:=(S m)
s2:=(F1
[y:B]
(sp_app_n (funPower F1 m [z:B](undef A (C z)) y)
(rec1_tmp m (funPower F1 m [z:B](undef A (C z))) y)) x);
Apply F1_lfp; Auto.
Intros; Rewrite rec1_tmp_power with n:=m; Auto.
Rewrite sp_app_powerF1_undef; Auto with sampled_str.
Qed.

(** fixpoint operator **)
Definition rec1:(x:B)(samplStr A (C x)) :=[y:B](rec1_tmp O [x:B](undef A (C x)) y).

Lemma rec1_wf: (x:B)(P x)->(sp_wf (rec1 x)).
Proof.
Intros x H; Unfold rec1; Apply rec1_tmp_wf with n:=O x:=x; Auto.
Qed.

Theorem rec1_inv: (x:B)(P x)->(sp_eq (rec1 x) (F1 rec1 x)).
Proof.
Intros; Apply sp_inf_wf_eq.
Intros n; Unfold rec1; Generalize (rec1_tmp_lemma 1!n O); Simpl; Auto.
Apply rec1_wf; Auto.
Qed.

Theorem rec1_uniq: (r1:(x:B)(samplStr A (C x)))
((x:B)(P x)->(sp_eq (r1 x) (F1 r1 x)))
->(x:B)(P x)->(sp_eq (rec1 x) (r1 x)).
Proof.
Intros r H H' x; Apply sp_nth_sp_eq; Intros n.
Rewrite (r1_ext rec1_inv); Auto; Rewrite (r1_ext H); Auto.
Qed.

End Rec1.

Section Rec1_lfp.

Variable B : Set.

Variable C: B -> clock.

Variable F1,F2: ((x:B)(samplStr A (C x))) -> (x:B)(samplStr A (C x)).

Variable n:nat.

Hypothesis F1_inf_F2:
(s1,s2:(x:B)(samplStr A (C x)))
((x:B)(sp_inf n (s1 x) (s2 x)))
->(x:B)(sp_inf n (F1 s1 x) (F2 s2 x)).

Lemma power_F1_F2_inf:
(m:nat; s1,s2:(x:B)(
samplStr A (C x)))
((x:B)(sp_inf n (s1 x) (s2 x)))
->(x:B)(sp_inf n (funPower F1 m s1 x) (funPower F2 m s2 x)).
Proof.
Intros m; Elim m; Simpl; Auto with sampled_str.
Qed.

Hints Resolve rec1_tmp_S_n_m: sampled_str.

Lemma rec1_tmp_lfp:
(m:nat; x:B)(le m n)->
(
sp_inf (minus n m)
(rec1_tmp F1 m (funPower F1 m [z:B](undef A ?)) x)
(rec1_tmp F2 m (funPower F2 m [z:B](undef A ?)) x)).
Proof.
Unfold sp_inf; Intros m x H m0; Generalize m x H; Elim m0; Clear H m m0 x.
Intros m x H; Unfold clock_nth sp_nth; Simpl.
LApply (F1_inf_F2 1!(funPower F1 m [z:B](undef A ?))
2!(funPower F2 m [z:B](undef A ?))).
Unfold sp_inf clock_nth; EAuto.
Intros; Apply power_F1_F2_inf; Auto with sampled_str.
Intros n0 HR m x H1; Inversion H1.
Rewrite <- minus_n_n; Intros H2; Inversion H2.
Rewrite <- minus_Sn_m; Auto; Intros H2;
Pattern (clock_nth (S n0) (clock_nth_tl m (C x)))
(sp_nth (S n0) (rec1_tmp F1 m (funPower F1 m [z:B](undef A (C z))) x))
(sp_nth (S n0) (rec1_tmp F2 m (funPower F2 m [z:B](undef A (C z))) x));
Apply eq_dep_ind_l2 with x1:=(sp_nth n0 (rec1_tmp F1 (S m) (funPower F1 (S m) [z:B](undef A (C z))) x)) x2:=(sp_nth n0 (rec1_tmp F2 (S m) (funPower F2 (S m) [z:B](undef A (C z))) x));
Auto with eqD sampled_str.
Apply HR.
Rewrite <- H0; Auto with arith.
Rewrite <- H0; Auto with arith.
Qed.

Theorem rec1_lfp:
(x:B)(
sp_inf n (rec1 F1 x) (rec1 F2 x)).
Proof.
Intros x; LApply (rec1_tmp_lfp 1!O x); Auto with arith.
Rewrite <- minus_n_O; Auto.
Qed.

End Rec1_lfp.

Section Rec1_loc_nfstwf.

Variable B : Set.

Variable C: B -> clock.

Variable F1: ((x:B)(samplStr A (C x))) -> (x:B)(samplStr A (C x)).

Variable P: B -> Prop.

Variable n:nat.

Hypothesis F1_nfstwf_inc_limited:
(m:nat; s:(x:B)(samplStr A (C x)))
(lt m n)->
((x:B)(P x)->(loc_nfstwf m (s x)))
->(x:B)(P x)->(loc_nfstwf (S m) (F1 s x)).

Lemma powerF1_loc_nfstwf_limited:
(m:nat; x:B)(P x)->(le m n)->
(
loc_nfstwf m (funPower F1 m [z:B](undef A ?) x)).
Proof.
Intros m; Elim m.
Simpl; Auto with sampled_str.
Intros; Rewrite <- funPower_commut; Auto with arith sampled_str.
Qed.

Hypothesis F1_lfp:
(s1,s2:(x:B)(samplStr A (C x)); n:nat)
((x:B)(P x)->(sp_inf n (s1 x) (s2 x)))->(x:B)(P x)->(sp_inf n (F1 s1 x) (F1 s2 x)).

Lemma powerF1_increases_le:
(k1,k2:nat)(le k1 k2)->(m:nat; x:B)(P x)->
(
sp_inf m (funPower F1 k1 [z:B](undef A (C z)) x) (funPower F1 k2 [z:B](undef A (C z)) x)).
Proof.
Intros k1 k2 H; Elim H; Auto with sampled_str.
Intros k2' H1 HR m x H2;
Apply sp_inf_trans with s2:=(funPower F1 k2' [z:B](undef A (C z)) x); Auto.
Apply powerF1_increases with F1:=F1 P:=P; Auto.
Qed.

Lemma powerF1_loc_nfstwf_lim:
(m:nat; x:B)(P x)->(le (
glob2loc m (C x)) n)->
(loc_nfstwf (glob2loc m (C x)) (funPower F1 m [z:B](undef A ?) x)).
Proof.
Intros m x H1 H2; Apply sp_inf_loc_nfstwf with n:=m s1:=(funPower F1 (glob2loc m (C x)) [z:B](undef A ?) x);
Auto.
Apply powerF1_loc_nfstwf_limited; Auto.
Apply powerF1_increases_le; Auto.
Apply glob2loc_le.
Qed.

Require Omega.

Lemma rec1_tmp_loc_nfstwf:
(m,k:nat; x:B)(P x)->(le (plus m (
glob2loc k (C x))) n)->
(s:(z:B)(samplStr A (C z)))
s=(funPower F1 k [z:B](undef A ?))
->(loc_nfstwf m (rec1_tmp F1 k s x)).
Proof.
Cofix rec1_tmp_loc_nfstwf; Intros m; Case m.
Intros; Apply loc_nfstwf_O.
Intros n0 k x H1 H2 s H3; Case (eq_false_dec (clock_nth k (C x))).
Intros H4; Apply loc_nfstwf_false.
Exact H4.
Apply rec1_tmp_loc_nfstwf with m:=(S n0) x:=x k:=(S k) s:=(F1 s); Auto.
Rewrite glob2loc_clock_nth; Rewrite H4; Auto.
Rewrite <- funPower_commut; Rewrite H3; Auto.
Intros H4; Apply loc_nfstwf_true; Simpl.
Exact H4.
Rewrite H3; Rewrite funPower_commut;
Apply loc_nfstwf_lt_is_no_Fail_strong with n:=(S k) m:=k
s:=(funPower F1 (S k) [z:B](undef A (C z)) x); Auto with arith.
Apply powerF1_loc_nfstwf_lim; Auto.
Rewrite glob2loc_clock_nth; Rewrite H4; Simpl; Omega.
Apply rec1_tmp_loc_nfstwf with m:=n0 x:=x k:=(S k) s:=(F1 s); Auto.
Rewrite glob2loc_clock_nth; Rewrite H4; Simpl; Omega.
Rewrite <- funPower_commut; Rewrite H3; Auto.
Qed.

Theorem rec1_loc_nfstwf:
(x:B)(P x)->(
loc_nfstwf n (rec1 F1 x)).
Proof.
Intros; Unfold rec1; Apply rec1_tmp_loc_nfstwf with k:=O x:=x; Auto.
Simpl; Omega.
Qed.

End Rec1_loc_nfstwf.

Section Rec0.

Variable c: clock.

Variable F0: (samplStr A c) -> (samplStr A c).

Hypothesis F0_lfp:
(s1,s2:(samplStr A c); n:nat)
(sp_inf n s1 s2)->(sp_inf n (F0 s1) (F0 s2)).

Hypothesis F0_nfstwf_inc:
(n:nat; s:(samplStr A c))
(glob_nfstwf n s)->(glob_nfstwf (S n) (F0 s)).

Lemma F0_loc_nfstwf_inc:
(n:nat; s:(
samplStr A c))
(loc_nfstwf n s)->(loc_nfstwf (S n) (F0 s)).
Proof.
Intros; Apply rec0_nfstwf_inc_glob2loc with f:=F0; Auto.
Qed.

Hints Resolve F0_loc_nfstwf_inc: sampled_str.

Definition rec0:=(rec1 2![x:unit]c [f:unit->(samplStr A c); x:unit](F0 (f x)) tt).

Lemma rec0_wf: (sp_wf rec0).
Unfold rec0; Apply rec1_wf with
C:=[x:unit]c
F1:=[f:unit->(samplStr A c); x:unit](F0 (f x))
x:=tt
P:=[_:unit]True;
Auto with sampled_str.
Qed.

Theorem rec0_inv: (sp_eq rec0 (F0 rec0)).
Unfold rec0; Apply rec1_inv with
C:=[x:unit]c
F1:=[f:unit->(samplStr A c); x:unit](F0 (f x))
x:=tt
P:=[_:unit]True;
Auto with sampled_str.
Qed.

Theorem rec0_uniq: (r0:(samplStr A c))(sp_eq r0 (F0 r0))->(sp_eq rec0 r0).
Unfold rec0; Intros r0 H; Apply rec1_uniq with
C:=[x:unit]c
F1:=[f:unit->(samplStr A c); x:unit](F0 (f x))
x:=tt
r1:=[_:unit]r0
P:=[_:unit]True;
Auto with sampled_str.
Qed.

End Rec0.

Section Rec0_props.

Variable c: clock.

Theorem rec0_lfp:
(F1,F2:(
samplStr A c)->(samplStr A c); n:nat)
((s1,s2:(samplStr A c))
(sp_inf n s1 s2)->(sp_inf n (F1 s1) (F2 s2)))
->(sp_inf n (rec0 F1) (rec0 F2)).
Proof.
Intros F1 F2 H n.
Unfold rec0; Apply rec1_lfp with
C:=[x:unit]c
F1:=[f:unit->(samplStr A c); x:unit](F1 (f x))
F2:=[f:unit->(samplStr A c); x:unit](F2 (f x))
x:=tt;
Auto.
Qed.

Theorem rec0_loc_nfstwf:
(F0:(
samplStr A c)->(samplStr A c); n:nat)
((m:nat; s:(samplStr A c))
(lt m n)->(loc_nfstwf m s)->(loc_nfstwf (S m) (F0 s)))
->((s1,s2:(samplStr A c); m:nat)
(sp_inf m s1 s2)->(sp_inf m (F0 s1) (F0 s2)))
->(loc_nfstwf n (rec0 F0)).
Proof.
Intros F0 n H1 H2.
Unfold rec0; Apply rec1_loc_nfstwf with
C:=[x:unit]c
F1:=[f:unit->(samplStr A c); x:unit](F0 (f x))
x:=tt
n:=n
P:=[_:unit]True;
Auto.
Qed.

Require Peano_dec.

Theorem rec0_glob_nfstwf:
(F0:(
samplStr A c)->(samplStr A c); n:nat)
((m:nat; s:(samplStr A c))
(lt m n)->(glob_nfstwf m s)->(glob_nfstwf (S m) (F0 s)))
->((s1,s2:(samplStr A c); m:nat)
(sp_inf m s1 s2)->(sp_inf m (F0 s1) (F0 s2)))
->(glob_nfstwf n (rec0 F0)).
Proof.
Intros F0 n H1 H2; Apply loc_nfstwf_glob_nfstwf;
Apply rec0_loc_nfstwf; Auto.
Intros; Apply nfstwf_function_convert_S_recip with f:=F0 n:=n; Auto.
Qed.

End Rec0_props.

End SP_rec.

Grammar command command1 :=
sp_rec0_ex [ "<" command(\$c) ">rec0" ] -> [<<(rec0 2!\$c)>>].

Implicit Arguments Off.

05/07/101, 15:45