Module sp

Set Implicit Arguments.

Require Export sampled_streams.
Require Arith.

Section SP_rec.

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

Variable A: Set.

Section Rec1.

Variable B: Set.

Variable C: B -> clock.

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

Variable P: B -> Prop.

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

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

Lemma powerF1_loc_nfstwf :
  forall (n: nat) (x: B), P x ->
     loc_nfstwf n (funPower F1 n (fun (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 :
  forall (n m: nat) (s1 s2: forall (x: B), samplStr A (C x)),
    (forall (x: B), P x -> sp_inf m (s1 x) (s2 x)) ->
      forall (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 :
forall (n m: nat) (x: B), P x ->
sp_inf m (funPower F1 n (fun (z: B) => undef A (C z)) x) (funPower F1 (S n) (fun (z: B) => undef A (C z)) x).

Proof.

intros; simpl; apply powerF1_lfp; auto with sampled_str.
Qed.

Hint Resolve powerF1_loc_nfstwf powerF1_increases : sampled_str.

Lemma powerF1_nth :
  forall (n m: nat) (x: B), le n m -> P x ->
    sp_nth n (funPower F1 (S m) (fun (z: B) => undef A (C z)) x)
   = sp_nth n (funPower F1 (S (S m)) (fun (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.

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

Lemma r1_prop :
forall (n m: nat) (x: B),
P x -> sp_inf m (funPower F1 n (fun (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 :
forall (n: nat) (x: B), P x ->
sp_nth n (r1 x) = sp_nth n (funPower F1 (S n) (fun (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.

Let sp_app_powerF1_undef :
  forall (n: nat) (s: forall (x: B), samplStr A (clock_nth_tl (S n) (C x))) (x: B),
    P x ->
     sp_app_n (funPower F1 n (fun (z: B) => undef A (C z)) x) _
               (sp_cons _ (sp_nth n (funPower F1 (S n) (fun (z: B) => undef A (C z)) x)) (s x))
     = sp_app_n (funPower F1 (S n) (fun (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 (fun (z: B) => undef A (C z)) x)
             = sp_nth m (funPower F1 (S n) (fun (z: B) => undef A (C z)) x));
     inversion_clear H; apply powerF1_nth; auto with arith.
Qed.

CoFixpoint rec1_tmp (n: nat) (s: forall (x: B), samplStr A (C x)) :
     forall (x: B), samplStr A (clock_nth_tl n (C x)) :=
  let s' := F1 s in fun x => sp_cons _ (sp_nth n (s' x)) (rec1_tmp (S n) s' x).

Let rec1_tmp_power :
  forall (n: nat) (x: B), rec1_tmp n (funPower F1 n (fun (z: B) => undef A (C z))) x
      = sp_cons _ (sp_nth n (funPower F1 (S n) (fun (z: B) => undef A (C z)) x))
                (rec1_tmp (S n) (funPower F1 (S n) (fun (z: B) => undef A (C z))) x).

Proof.

intros n x; rewrite (unfold_samplStr (rec1_tmp n (funPower F1 n (fun (z: B) => undef A (C z))) x)); simpl;
rewrite funPower_commut; auto.
Qed.

Lemma rec1_tmp_S_n_m :
  forall (n m: nat) (x: B),
    sp_nth (S n) (rec1_tmp m (funPower F1 m (fun (z: B) => undef A (C z))) x)
    ==<< samplElt A >> sp_nth n (rec1_tmp (S m) (funPower F1 (S m) (fun (z: B) => undef A (C z))) x).

Proof.

   intros n0 m x; rewrite rec1_tmp_power.
   unfold sp_nth; simpl.
   apply eq_dep_map_eq_dep with (F := sp_hd (A := A)) (y := sp_nth_tl n0
       (rec1_tmp (S m) (funPower F1 m (F1 (fun z : B => undef A (C z)))) x))
       (x := sp_tl
       (sp_nth_tl n0
          (sp_cons (clock_nth_tl m (C x))
             (sp_hd
                (sp_nth_tl m
                   (funPower F1 m (F1 (fun z : B => undef A (C z))) x)))
             (rec1_tmp (S m)
                (funPower F1 m (F1 (fun z : B => undef A (C z)))) x))));
   refine (sp_tl_nth_tl n0 _).
Qed.

Lemma rec1_tmp_wf :
forall (n: nat) (x: B), P x ->
sp_wf (rec1_tmp n (funPower F1 n (fun (z: B) => undef A (C z))) x).

Proof.

  cofix rec1_tmp_wf.
  intros n x H; rewrite rec1_tmp_power; constructor 1; unfold sp_tl.
  apply loc_nfstwf_lt_is_no_Fail with (n := S n) (m := n) (s := funPower F1 (S n) (fun (z: B) => undef A (C z)) x);
   auto with sampled_str.
  apply rec1_tmp_wf with (n := S n) (x := x); auto.
Qed.

Let rec1_tmp_lemma_aux :
  forall (n: nat) (x: B), P x ->
    flat_ord (sp_nth n (F1 (funPower F1 n (fun (z: B) => undef A (C z))) x))
       (sp_nth n (F1 (fun (y: B) => sp_app_n (funPower F1 n (fun (z: B) => undef A (C z)) y)
                                _ (rec1_tmp n (funPower F1 n (fun (z: B) => undef A (C z))) y)) x)).

Proof.

intros n x H.
    lapply (F1_lfp (funPower F1 n (fun (z: B) => undef A (C z)))
            (fun (y: B) => sp_app_n (funPower F1 n (fun (z: B) => undef A (C z)) y)
                             _ (rec1_tmp n (funPower F1 n (fun (z: B) => undef A (C z))) y)) (n := 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 (fun (z: B) => undef A (C z)) x))
                       (sp_nth m (funPower F1 (S m) (fun (z: B) => undef A (C z)) x))).
      generalize (powerF1_increases m (m := m)); unfold sp_inf; auto with arith.
    intros; generalize sp_app_sp_inf_1; unfold sp_inf; auto with arith.
Qed.

Let rec1_tmp_lemma :
  forall (n m: nat) (x: B), P x ->
     sp_inf n (rec1_tmp m (funPower F1 m (fun (z: B) => undef A (C z))) x)
                           (sp_nth_tl m (F1 (fun (y: B) => sp_app_n (funPower F1 m (fun (z: B) => undef A (C z)) y)
                                                           _ (rec1_tmp m (funPower F1 m (fun (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
           (fun (y: B) => sp_app_n (funPower F1 (S m) (fun (z: B) => undef A (C z)) y)
              _ (rec1_tmp (S m) (funPower F1 (S m) (fun (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
           (fun (y: B) => sp_app_n (funPower F1 m (fun (z: B) => undef A (C z)) y)
              _ (rec1_tmp m (funPower F1 m (fun (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 (y: B) : samplStr A (C y) :=
rec1_tmp O (fun (x: B) => undef A (C x)) y.

Lemma rec1_wf :
forall (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 :
forall (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 (n := n) O); simpl; auto.
  apply rec1_wf; auto.
Qed.

Theorem rec1_uniq :
  forall (r1: forall (x: B), samplStr A (C x)),
    (forall (x: B), P x -> sp_eq (r1 x) (F1 r1 x))
     -> forall (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: (forall (x: B), samplStr A (C x)) -> forall (x: B), samplStr A (C x).

Variable n: nat.

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

Lemma power_F1_F2_inf :
  forall (m: nat) (s1 s2: forall (x: B), samplStr A (C x)),
    (forall (x: B), sp_inf n (s1 x) (s2 x))
    -> forall (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.

Hint Resolve rec1_tmp_S_n_m : sampled_str.

Lemma rec1_tmp_lfp :
  forall (m: nat) (x: B), le m n ->
      sp_inf (minus n m)
                 (rec1_tmp _ F1 m (funPower F1 m (fun (z: B) => undef A _)) x)
                 (rec1_tmp _ F2 m (funPower F2 m (fun (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 sp_nth; simpl.
  lapply (F1_inf_F2 (funPower F1 m (fun (z: B) => undef A _))
                    (funPower F2 m (fun (z: B) => undef A _))).
  unfold sp_inf; intros; apply (H0 x m H).
  intros; apply power_F1_F2_inf; auto with sampled_str.
  intros n0 HR m x H1; inversion H1.
  rewrite <- Minus.minus_n_n; intros H2; inversion H2.
  rewrite <- Minus.minus_Sn_m; auto; intros H2.
  apply eq_dep_ind_l2 with (x1 := sp_nth n0 (rec1_tmp C F1 (S m) (funPower F1 (S m) (fun (z: B) => undef A (C z))) x)) (x2 := sp_nth n0 (rec1_tmp C F2 (S m) (funPower F2 (S m) (fun (z: B) => undef A (C z))) x))
    (y1 := sp_nth (S n0) (rec1_tmp C F1 m (funPower F1 m (fun (z: B) => undef A (C z))) x))
    (y2 := sp_nth (S n0) (rec1_tmp C F2 m (funPower F2 m (fun (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 :
forall (x: B), sp_inf n (rec1 _ F1 x) (rec1 _ F2 x).

Proof.

intros x; lapply (rec1_tmp_lfp (m := O) x); auto with arith.
rewrite <- Minus.minus_n_O; auto.
Qed.

End Rec1_lfp.

Section Rec1_loc_nfstwf.

Variable B: Set.

Variable C: B -> clock.

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

Variable P: B -> Prop.

Variable n: nat.

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

Lemma powerF1_loc_nfstwf_limited :
  forall (m: nat) (x: B), P x -> le m n ->
  loc_nfstwf m (funPower F1 m (fun (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 :
  forall (s1 s2: forall (x: B), samplStr A (C x)) (n: nat),
    (forall (x: B), P x -> sp_inf n (s1 x) (s2 x)) ->
    forall (x: B), P x -> sp_inf n (F1 s1 x) (F1 s2 x).

Lemma powerF1_increases_le :
  forall (k1 k2: nat), le k1 k2 -> forall (m: nat) (x: B), P x ->
    sp_inf m (funPower F1 k1 (fun (z: B) => undef A (C z)) x) (funPower F1 k2 (fun (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' (fun (z: B) => undef A (C z)) x); auto.
   apply powerF1_increases with (F1 := F1) (P := P); auto.
Qed.

Lemma powerF1_loc_nfstwf_lim :
forall (m: nat) (x: B), P x -> le (glob2loc m (C x)) n ->
loc_nfstwf (glob2loc m (C x)) (funPower F1 m (fun (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)) (fun (z: B) => undef A _) x);
  auto.
  apply powerF1_loc_nfstwf_limited; auto.
  apply powerF1_increases_le; auto.
  apply glob2loc_le.
Qed.

Require Import Lia.

Lemma rec1_tmp_loc_nfstwf :
  forall (m k: nat) (x: B), P x -> le (plus m (glob2loc k (C x))) n ->
   forall (s: forall (z: B), samplStr A (C z)),
   s = funPower F1 k (fun (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) (fun (z: B) => undef A (C z)) x); auto with arith.
      apply powerF1_loc_nfstwf_lim; auto.
      rewrite glob2loc_clock_nth; rewrite H4; simpl; lia.
      apply rec1_tmp_loc_nfstwf with (m := n0) (x := x) (k := S k) (s := F1 s); auto.
      rewrite glob2loc_clock_nth; rewrite H4; simpl; lia.
      rewrite <- funPower_commut; rewrite H3; auto.
Qed.

Theorem rec1_loc_nfstwf :
forall (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; lia.
Qed.

End Rec1_loc_nfstwf.

Section Rec0.

Variable c: clock.

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

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

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

Lemma F0_loc_nfstwf_inc :
  forall (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.

Hint Resolve F0_loc_nfstwf_inc : sampled_str.

Definition rec0 :=
rec1 (fun (x: unit) => c) (fun (f: unit-> samplStr A c) (x: unit) => F0 (f x)) tt.

Lemma rec0_wf : sp_wf rec0.

Proof.

  unfold rec0; apply rec1_wf with
     (C := fun (x: unit) => c)
     (F1 := fun (f: unit-> samplStr A c) (x: unit) => F0 (f x))
     (x := tt)
     (P := fun (_: unit) => True);
   auto with sampled_str.
Qed.

Theorem rec0_inv : sp_eq rec0 (F0 rec0).

Proof.

  unfold rec0; apply rec1_inv with
     (C := fun (x: unit) => c)
     (F1 := fun (f: unit-> samplStr A c) (x: unit) => F0 (f x))
     (x := tt)
     (P := fun (_: unit) => True);
   auto with sampled_str.
Qed.

Theorem rec0_uniq :
forall (r0: samplStr A c), sp_eq r0 (F0 r0) -> sp_eq rec0 r0.

Proof.

  unfold rec0; intros r0 H; apply rec1_uniq with
     (C:= fun (x: unit) => c)
     (F1:= fun (f: unit-> samplStr A c) (x: unit) => F0 (f x))
     (x := tt)
     (r1 := fun (_: unit) => r0)
     (P := fun (_: unit) => True);
   auto with sampled_str.
Qed.

End Rec0.

Section Rec0_props.

Variable c: clock.

Theorem rec0_lfp :
  forall (F1 F2: samplStr A c -> samplStr A c) (n: nat),
    (forall (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 := fun (x: unit) => c)
     (F1 := fun (f: unit-> samplStr A c) (x: unit) => F1 (f x))
     (F2 := fun (f: unit -> samplStr A c) (x: unit) => F2 (f x))
     (x := tt);
   auto.
Qed.

Theorem rec0_loc_nfstwf :
  forall (F0: samplStr A c -> samplStr A c) (n: nat),
    (forall (m: nat) (s: samplStr A c),
      lt m n -> loc_nfstwf m s -> loc_nfstwf (S m) (F0 s))
    -> (forall (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 := fun (x: unit) => c)
     (F1 := fun (f: unit-> samplStr A c) (x: unit) => F0 (f x))
     (x := tt)
     (n := n)
     (P:= fun (_: unit) => True);
   auto.
Qed.

Require Peano_dec.

Theorem rec0_glob_nfstwf :
  forall (F0: samplStr A c -> samplStr A c) (n: nat),
    (forall (m: nat) (s: samplStr A c),
      lt m n -> glob_nfstwf m s -> glob_nfstwf (S m) (F0 s))
    -> (forall (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.

Notation "'<' c '>rec0' " := (rec0 (c := c)) (at level 100).

Unset Implicit Arguments.

Module sp_rec