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