Set Implicit Arguments.

Require Export sampled_streams.

Section Constant_samplStr.

Variable A: Set.

Variable a: A.

Definition elt_const (b: bool) : samplElt A b :=
  if b return samplElt A b then Any a else None A.

CoFixpoint sp_const (c:clock) : samplStr A c :=
  sp_cons _ (elt_const (hd c)) (sp_const (tl c)).

Lemma elt_const_no_Fail :
  forall (b: bool), is_no_Fail (elt_const b).
Proof.
  intros b; case b; simpl; auto.
Qed.

Hint Resolve elt_const_no_Fail : sampled_str.

Lemma sp_wf_const :
  forall (c: clock), sp_wf (sp_const c).
Proof.
  cofix sp_wf_const; constructor 1; simpl; auto with sampled_str.
Qed.

End Constant_samplStr.

Hint Resolve sp_wf_const : sampled_str sp_rec0.

Notation " '`' c '`' " := (sp_const c _) (at level 100).

Section Mem_Less.

Variables A B: Set.

CoInductive mem_less : clock -> clock -> Set :=
  | ml_cons : forall (c1 c2: clock),
     (samplElt A (hd c1) -> samplElt B (hd c2))
        -> mem_less (tl c1) (tl c2)
          -> mem_less c1 c2.

Definition ml_hd (c1 c2: clock) (m: mem_less c1 c2) :=
  match m as m' in mem_less c1' c2' return samplElt A (hd c1') -> samplElt B (hd c2') with
    | ml_cons _ _ f _ => f
  end.

Definition ml_tl (c1 c2: clock) (m: mem_less c1 c2) :=
  match m as m' in mem_less c1' c2' return mem_less (tl c1') (tl c2') with
    | ml_cons _ _ _ m' => m'
  end.

CoFixpoint mem_less_apply (c1 c2: clock) (m: mem_less c1 c2) (x: samplStr A c1) : samplStr B c2 :=
  sp_cons _ ((ml_hd m) (sp_hd x)) (mem_less_apply (ml_tl m) (sp_tl x)).

CoFixpoint ml_const : (forall (b: bool), samplElt A b -> samplElt B b) -> forall (c: clock), mem_less c c :=
  fun f c =>
     ml_cons _ _ (f (hd c)) (ml_const f (tl c)).

End Mem_Less.

Lemma mem_less_id_def :
  forall (A: Set) (c: clock) (x: samplStr A c),
      sp_eq x (mem_less_apply (ml_const (fun b a => a) _) x).
Proof.
  cofix ml_id_def; intros A c x; constructor 1.
    simpl; auto with eqD sampled_str.
    apply ml_id_def with (x := sp_tl x).
Qed.

Hint Resolve mem_less_id_def : sampled_str.

Section Followed_By.

Variable A: Set.

CoFixpoint sp_delay (c: clock) : samplStr A c -> samplElt A true -> samplStr A c :=
  match c as c0 return samplStr A c0 -> samplElt A true -> samplStr A c0 with
    | Cons hc tc => if hc as b return samplStr A (Cons b tc) -> samplElt A true -> samplStr A (Cons b tc)
         then (fun x a => sp_cons (Cons true tc) a (sp_delay (sp_tl x) (sp_hd x)))
         else (fun x a => sp_cons (Cons false tc) (None A) (sp_delay (sp_tl x) a))
  end.

Lemma sp_delay_lfp :
  forall (n: nat) (c: clock) (s1 s2: samplStr A c) (a1 a2: samplElt A true),
    sp_inf n s1 s2 -> flat_ord a1 a2 -> sp_inf n (sp_delay s1 a1) (sp_delay s2 a2).
Proof.
  intros n; elim n; simpl.
    intros c; case c; simpl; intros b c'; case b; intros s1 s2 a1 a2 H1 H2;
    auto with sampled_str. apply sp_inf_proof_O; simpl; auto.
    intros n0 HR c; case c; simpl; intros b c'; case b; intros s1 s2 a1 a2 H1 H2;
    case (sp_inf_S_n_inv H1); intros; apply sp_inf_proof_S_n; simpl; auto with sampled_str.
Qed.


Lemma sp_delay_loc_nfstwf :
  forall (n: nat) (c: clock) (s: samplStr A c) (a: samplElt A true),
      loc_nfstwf n s -> is_no_Fail a -> loc_nfstwf (S n) (sp_delay s a).
Proof.
  cofix sp_delay_loc_nfstwf.
  intros n c; case c; intros b c'; case b.
  intros s a H1 H2; apply loc_nfstwf_true with (s := sp_delay s a); simpl; auto.
  generalize H1; case n; auto with sampled_str.
  intros n' H1'; apply sp_delay_loc_nfstwf.
    apply loc_nfstwf_S_n_true_inv with (s := s); auto.
    apply loc_nfstwf_is_no_Fail with (n := n') (s := s); auto.
  intros s a H1 H2; apply loc_nfstwf_false with (s := sp_delay s a); simpl; auto.
  apply sp_delay_loc_nfstwf; auto.
  apply loc_nfstwf_false_inv with (s := s); auto.
Qed.

Definition sp_pre (c: clock) (s: samplStr A c) : samplStr A c :=
  sp_delay s (Fail A).

CoFixpoint sp_arrow (c: clock) (x y: samplStr A c) : samplStr A c :=
  sp_cons _ (sp_hd x)
              (if (hd c)
               then (sp_tl y)
               else (sp_arrow (sp_tl x) (sp_tl y))).

Definition sp_fby c x y := sp_arrow (c := c) x (sp_pre y).

Lemma sp_arrow_lfp :
  forall (n: nat) (c: clock) (x1 x2: samplStr A c) (y1 y2: samplStr A c),
    sp_inf n x1 x2 ->
      sp_inf n y1 y2 -> sp_inf n (sp_arrow x1 y1) (sp_arrow x2 y2).
Proof.
  intros n; elim n; simpl.
  intros c; case c; simpl; intros b c'; case b; intros x1 x2 y1 y2 H1 H2;
 apply sp_inf_proof_O; simpl; auto with sampled_str; apply sp_inf_O_inv with (s1 := x1) (s2 := x2); auto.
  intros n0 HR c; case c; simpl; intros b c'; case b; intros x1 x2 y1 y2 H1 H2;
  case (sp_inf_S_n_inv H1); case (sp_inf_S_n_inv H2); intros; apply sp_inf_proof_S_n; simpl; auto.
Qed.

Lemma sp_arrow_loc_nfstwf :
  forall (n: nat) (c: clock) (x: samplStr A c) (y: samplStr A c),
    loc_nfstwf n x -> loc_nfstwf n y -> loc_nfstwf n (sp_arrow x y).
Proof.
  cofix sp_arrow_loc_nfstwf.
  intros n c; case c; simpl; intros b c'; case b; intros x y.
  case n.
   intros H1 H2; apply loc_nfstwf_O.
   intros m H1 H2; apply loc_nfstwf_true; simpl; auto.
    apply loc_nfstwf_is_no_Fail with (n := m) (s := x); auto.
    apply loc_nfstwf_S_n_true_inv with (n := m) (s := y); simpl; auto.
  intros H1 H2; apply loc_nfstwf_false; simpl; auto.
  apply sp_arrow_loc_nfstwf.
    apply loc_nfstwf_false_inv with (s := x); simpl; auto.
    apply loc_nfstwf_false_inv with (s := y); simpl; auto.
Qed.

Lemma sp_arrow_loc_nfstwf_1 :
  forall (c: clock) (x: samplStr A c) (y: samplStr A c),
    loc_nfstwf (S O) x -> loc_nfstwf (S O) (sp_arrow x y).
Proof.
  cofix sp_arrow_loc_nfstwf_1.
  intros c; case c; simpl; intros b c'; case b; intros x y H.
    apply loc_nfstwf_true; simpl; auto with sampled_str.
    apply loc_nfstwf_is_no_Fail with (s := x) (n := O); auto.
  apply loc_nfstwf_false; simpl; auto.
  apply sp_arrow_loc_nfstwf_1.
    apply loc_nfstwf_false_inv with (s := x); simpl; auto.
Qed.

Lemma sp_arrow_ext2 :
  forall (c: clock) (x y1 y2: samplStr A c),
    sp_eq y1 y2 -> sp_eq (sp_arrow x y1) (sp_arrow x y2).
Proof.
  cofix sp_arrow_ext2; intros c; case c; simpl; intros b c'; case b; simpl;
   constructor 1; simpl; auto with eqD sampled_str.
   case (sp_eq_inv H); auto.
   apply sp_arrow_ext2; case (sp_eq_inv H); auto.
Qed.

Hint Resolve sp_delay_lfp sp_delay_loc_nfstwf : sampled_str.

CoFixpoint sp_init_pre (c: clock) : samplStr A c -> samplStr A c :=
  match c as c0 return samplStr A c0 -> samplStr A c0 with
    | Cons hc tc => if hc as b return samplStr A (Cons b tc) -> samplStr A (Cons b tc)
         then (fun x => sp_delay x (sp_hd x))
         else (fun x => sp_cons (Cons false tc) (None A) (sp_init_pre (sp_tl x)))
    end.

Lemma sp_init_pre_lfp :
  forall (n: nat) (c: clock) (x1 x2: samplStr A c),
    sp_inf n x1 x2 -> sp_inf n (sp_init_pre x1) (sp_init_pre x2).
Proof.
  intros n; elim n; simpl.
  intros c; case c; simpl; intros b c'; case b; intros x1 x2 H1;
  apply sp_inf_proof_O; simpl; auto with sampled_str; apply sp_inf_O_inv with (s1 := x1) (s2 := x2); auto.
  intros n0 HR c; case c; simpl; intros b c'; case b; intros x1 x2 H1;
  case (sp_inf_S_n_inv H1); intros; apply sp_inf_proof_S_n; simpl; auto with sampled_str.
Qed.

Lemma sp_init_pre_loc_nfstwf :
  forall (n: nat) (c: clock) (x: samplStr A c),
    loc_nfstwf (S n) x -> loc_nfstwf (S (S n)) (sp_init_pre x).
Proof.
  cofix sp_init_pre_loc_nfstwf.
  intros n c; case c; simpl; intros b c'; case b; intros x H.
    rewrite (unfold_samplStr (sp_init_pre x));
     change (loc_nfstwf (S (S n)) (sp_cons _ (sp_hd (sp_delay x (sp_hd x)))
                                     (sp_tl (sp_delay x (sp_hd x)))));
     rewrite <- unfold_samplStr; apply sp_delay_loc_nfstwf; auto.
     apply loc_nfstwf_is_no_Fail with (n := n) (s := x); auto.
  apply loc_nfstwf_false; simpl; auto.
  apply sp_init_pre_loc_nfstwf.
    apply loc_nfstwf_false_inv with (s := x); simpl; auto.
Qed.

Hint Resolve sp_arrow_lfp sp_arrow_loc_nfstwf_1 sp_arrow_loc_nfstwf sp_arrow_ext2
   sp_init_pre_lfp sp_init_pre_loc_nfstwf : sampled_str.


End Followed_By.

Section Pre_elimination.

Variable A B: Set.

Theorem sp_pre_elimination :
  forall (c1 c2: clock) (g: mem_less A B c1 c2) (x: samplStr B c2)
           (y: samplStr A c1) (a: A),
   clock_inf c2 c1 ->
     sp_eq
        (sp_arrow x (mem_less_apply g (sp_pre y)))
        (sp_arrow x (mem_less_apply g (sp_delay y (Any a)))).
Proof.
 unfold sp_pre; cofix sp_pre_elimination; intros c1 c2; case c2; simpl; intros b2 c2';
 case b2; intros g x y a H; constructor 1; try (simpl; auto with eqD; fail).
 case (clock_inf_inv H); intros H1 H2; simpl in H1;
 generalize g y; rewrite (unfold_Str c1); rewrite H1; simpl.
 intros; apply sp_eq_refl.
 generalize g y H ; case c1; intros hc1 tc1; case hc1;
 intros g' y' H'; simpl.
  apply sp_eq_refl.
  apply sp_pre_elimination with (x := sp_tl x) (g := ml_tl g') (y := sp_tl y').
  simpl; case (clock_inf_inv H'); auto.
Qed.

Lemma pre_init_pre :
  forall (c1 c2: clock) (g: mem_less A B c1 c2) (x: samplStr B c2)
       (y: samplStr A c1),
   clock_inf c2 c1 ->
     sp_eq
        (sp_arrow x (mem_less_apply g (sp_pre y)))
        (sp_arrow x (mem_less_apply g (sp_init_pre y))).
Proof.
 unfold sp_pre; cofix pre_init_pre; intros c1 c2; case c2; simpl; intros b2 c2';
 case b2; intros g x y H; constructor 1; try (simpl; auto with eqD; fail).
 case (clock_inf_inv H); intros H1 H2; simpl in H1;
 generalize g y; rewrite (unfold_Str c1); rewrite H1; simpl.
 intros; apply sp_eq_refl.
 generalize g y H ; case c1; intros hc1 tc1; case hc1;
 intros g' y' H'; simpl.
  apply sp_eq_refl.
  apply pre_init_pre with (x := sp_tl x) (g := ml_tl g') (y := sp_tl y').
  simpl; case (clock_inf_inv H'); auto.
Qed.

End Pre_elimination.

Section Delays_prop.

Variable A: Set.

Hint Resolve sp_arrow_lfp sp_arrow_loc_nfstwf_1 sp_arrow_loc_nfstwf sp_arrow_ext2
   sp_init_pre_lfp sp_init_pre_loc_nfstwf : sampled_str.

Hint Resolve pre_init_pre : sampled_str.

Lemma sp_fby_equiv :
  forall (c: clock) (x y: samplStr A c),
    sp_eq (sp_fby x y) (sp_arrow x (sp_init_pre y)).
Proof.
  unfold sp_fby; intros c x y;
  apply sp_eq_trans with
    (s2 := sp_arrow x (mem_less_apply (ml_const (fun b a => a) _) (sp_pre y)));
  auto with sampled_str.
  apply sp_eq_trans with
    (s2 := sp_arrow x (mem_less_apply (ml_const (fun b a => a) _) (sp_init_pre y)));
  auto with sampled_str.
Qed.

Hint Resolve sp_fby_equiv : sampled_str.

Lemma sp_fby_lfp :
  forall (n: nat) (c: clock) (x1 x2 y1 y2: samplStr A c),
    sp_inf n x1 x2 ->
       sp_inf n y1 y2 ->
       sp_inf n (sp_fby x1 y1) (sp_fby x2 y2).
Proof.
  intros n c x1 x2 y1 y2 H1 H2.
  apply sp_inf_trans with (s2 := sp_arrow x1 (sp_init_pre y1));
   auto with sampled_str.
  apply sp_inf_trans with (s2 := sp_arrow x2 (sp_init_pre y2));
   auto with sampled_str.
Qed.

Lemma sp_fby_loc_nfstwf :
  forall (n: nat) (c: clock) (x y: samplStr A c),
    loc_nfstwf (S n) x ->
      loc_nfstwf n y ->
       loc_nfstwf (S n) (sp_fby x y).
Proof.
  intros n c x y H1 H2.
  apply loc_nfstwf_sp_eq with (s1 := sp_arrow x (sp_init_pre y));
  auto with sampled_str.
  generalize H1 H2; case n; simpl; auto with sampled_str.
Qed.

Lemma sp_fby_glob_nfstwf :
  forall (n: nat) (c: clock) (x y: samplStr A c),
    glob_nfstwf (S n) x ->
      glob_nfstwf n y ->
       glob_nfstwf (S n) (sp_fby x y).
Proof.
  intros n c x y H1 H2;
   apply nfstwf_function_convert_S with (f := fun y => sp_fby x y) (n := n); auto.
  intros m y' H3 H4; apply sp_fby_loc_nfstwf; auto with sampled_str.
  assert (glob2loc (loc2glob (S m) c (S n)) c = S m).
  apply loc2glob_prop; auto.
  rewrite <- H.
  apply glob_nfstwf_loc_nfstwf; apply glob_nfstwf_n_le with (n := S n);
  auto with sampled_str.
Qed.

End Delays_prop.


Infix "fby" := sp_fby (at level 100, right associativity).
Infix "-->" := sp_arrow (at level 100, right associativity).

Notation pre := sp_pre.

Section Extend.

Variables A B: Set.


Definition elt_extend (b: bool) (f: samplElt (A -> B) b) : samplElt A b -> samplElt B b :=
  match f as f0 in samplElt _ b return samplElt A b -> samplElt B b with
    | None _ => fun _: samplElt A false => None B
    | Any vf => fun x => match x with
      | Any vx => Any (vf vx)
      | Fail _ => Fail B
      | None _ => Fail B
    end
    | Fail _ => fun _ => Fail _
  end.

Lemma elt_extend_lfp :
  forall (b1 b2: bool) (f1: samplElt (A -> B) b1) (f2: samplElt (A -> B) b2)
         (s1: samplElt A b1) (s2: samplElt A b2),
    flat_ord f1 f2 -> flat_ord s1 s2 ->
           flat_ord (elt_extend f1 s1) (elt_extend f2 s2).
Proof.
  intros b1 b2 f1 f2; case f1; case f2; simpl; auto.
    intros f s1 s2 H; inversion H.
    intros s1 s2 H; inversion H.
    intros f s1 s2 H; inversion H.
    intros f1' f2' s1 s2 H1; generalize (eq_dep_eq _ _ _ _ _ H1); intro H2; injection H2;
    intro H3; rewrite H3; pattern s1; apply samplElt_true_inv;
    pattern s2; apply samplElt_true_inv; simpl; auto.
     intros x y H1'; generalize (eq_dep_eq _ _ _ _ _ H1'); intro H2'; injection H2';
     intro H3'; rewrite H3'; simpl; auto.
     intros x H; inversion H.
    intros f s1 s2 H; inversion H.
Qed.

Lemma elt_extend_is_no_Fail :
  forall (b: bool) (f: samplElt (A -> B) b) (s: samplElt A b),
    is_no_Fail f -> is_no_Fail s -> is_no_Fail (elt_extend f s).
Proof.
  intros b f; case f; simpl; auto.
  intros f' s; inversion s using samplElt_true_inv;
    simpl; auto.
Qed.

Hint Resolve elt_extend_lfp elt_extend_is_no_Fail : sampled_str.

CoFixpoint sp_extend (c: clock) (f: samplStr (A -> B) c) (x: samplStr A c) : samplStr B c :=
    sp_cons _ (elt_extend (sp_hd f) (sp_hd x)) (sp_extend (sp_tl f) (sp_tl x)).

Lemma sp_extend_const :
  forall (c: clock) (f: A->B) (x: A),
       sp_eq (sp_extend (sp_const f c) (sp_const x c)) (sp_const (f x) c).
Proof.
  cofix sp_extend_const.
  intros; constructor 1.
    simpl; case (hd c); auto with eqD.
    refine (sp_extend_const _ _ _).
Qed.

Lemma sp_extend_lfp :
  forall (n: nat) (c1 c2: clock) (f1: samplStr (A -> B) c1)
             (f2: samplStr (A -> B) c2) (s1: samplStr A c1) (s2: samplStr A c2),
    sp_inf n f1 f2 -> sp_inf n s1 s2 ->
         sp_inf n (sp_extend f1 s1) (sp_extend f2 s2).
Proof.
  intros n; elim n; simpl.
  intros; apply sp_inf_proof_O; simpl; auto with sampled_str.
  intros n0 HR c1 c2 f1 f2 s1 s2 H H0; case (sp_inf_S_n_inv H);
  case (sp_inf_S_n_inv H0); intros; apply sp_inf_proof_S_n;
  simpl; auto with sampled_str.
Qed.

Lemma sp_extend_loc_nfstwf :
  forall (n: nat) (c: clock) (f: samplStr (A -> B) c) (s: samplStr A c),
    loc_nfstwf n f -> loc_nfstwf n s -> loc_nfstwf n (sp_extend f s).
Proof.
  cofix sp_extend_loc_nfstwf.
  intros n c f s; case (eq_false_dec (hd c)); intros H1.
  intros; apply loc_nfstwf_false; simpl; auto.
   apply sp_extend_loc_nfstwf; apply loc_nfstwf_false_inv; auto.
  case n.
   intros; apply loc_nfstwf_O.
   intros; apply loc_nfstwf_true; simpl; auto.
    apply elt_extend_is_no_Fail; apply loc_nfstwf_is_no_Fail with (n := n0); auto.
   apply sp_extend_loc_nfstwf; apply loc_nfstwf_S_n_true_inv; auto.
Qed.

Hint Resolve sp_extend_lfp sp_extend_loc_nfstwf : sampled_str.

Lemma sp_extend_glob_nfstwf :
  forall (n: nat) (c: clock) (f: samplStr (A -> B) c) (s: samplStr A c),
    glob_nfstwf n f -> glob_nfstwf n s -> glob_nfstwf n (sp_extend f s).
Proof.
  intros n c f s H1 H2;
  apply nfstwf_function_convert with (f := fun s => sp_extend f s) (n := n); auto.
  intros m s' H3 H4; apply sp_extend_loc_nfstwf; auto.
  assert (glob2loc (loc2glob m c n) c = m).
  apply loc2glob_prop; auto.
  rewrite <- H.
  apply glob_nfstwf_loc_nfstwf; apply glob_nfstwf_n_le with (n := n); auto
  with sampled_str.
Qed.

Lemma sp_extend_wf :
  forall (c: clock) (f: samplStr (A -> B) c) (s: samplStr A c),
    sp_wf f -> sp_wf s -> sp_wf (sp_extend f s).
Proof.
  auto with sampled_str.
Qed.

CoFixpoint ml_extend1 (c: clock) (x: samplStr A c) : mem_less (A -> B) B c c :=
  ml_cons _ _ (fun hf => elt_extend hf (sp_hd x)) (ml_extend1 (sp_tl x)).

Lemma sp_extend_mem_less1 :
  forall (c: clock) (f: samplStr (A -> B) c) (s: samplStr A c),
        sp_eq (sp_extend f s) (mem_less_apply (ml_extend1 s) f).
Proof.
  cofix sp_extend_mem_less. intros c f s; constructor 1; simpl; auto with eqD sampled_str.
Qed.

CoFixpoint ml_extend2 (c: clock) (f: samplStr (A -> B) c) : mem_less A B c c :=
  ml_cons _ _ (elt_extend (sp_hd f)) (ml_extend2 (sp_tl f)).

Lemma sp_extend_mem_less2 :
  forall (c: clock) (f: samplStr (A -> B) c) (s: samplStr A c),
        sp_eq (sp_extend f s) (mem_less_apply (ml_extend2 f) s).
Proof.
  cofix sp_extend_mem_less. intros c f s; constructor 1; simpl; auto with eqD sampled_str.
Qed.

End Extend.

Hint Resolve sp_extend_lfp sp_extend_wf : sampled_str sp_rec0.
Hint Resolve sp_extend_loc_nfstwf : sampled_str.

Notation ext := sp_extend.

Section Extend_prop.

Lemma sp_extend_id :
  forall (A: Set) (c: clock) (f: A -> A) (x: samplStr A c),
       (forall (z: A), f z = z) -> sp_eq (sp_extend (sp_const f c) x) x.
Proof.
  intros A; cofix sp_extend_id.
  intros c f x H; constructor 1.
  simpl; case (sp_hd x); simpl; intros; try (rewrite H); auto with eqD.
  refine (sp_extend_id _ _ _ _); auto.
Qed.

Lemma sp_extend_comp :
  forall (A B C: Set) (c: clock) (f: A -> B) (g: B -> C) (h: A -> C)
        (x: samplStr A c),
   (forall (z: A), g (f z) = h z) ->
   sp_eq (sp_extend (sp_const g c) (sp_extend (sp_const f c) x))
         (sp_extend (sp_const h c) x).
Proof.
  intros A B C; cofix sp_extend_comp.
  intros c f g h x H; constructor 1.
  simpl; case (sp_hd x); simpl; intros; try (rewrite H); auto with eqD.
  refine (sp_extend_comp _ _ _ _ _ _); auto.
Qed.

Variable A: Set.

Hint Resolve sp_extend_mem_less2 pre_init_pre sp_arrow_ext2
  sp_arrow_lfp sp_arrow_loc_nfstwf : sampled_str.
Hint Resolve sp_init_pre_lfp sp_init_pre_loc_nfstwf : sampled_str.
Hint Resolve sp_arrow_loc_nfstwf_1 : sampled_str.

Lemma sp_arrow_extend2_pre_equiv :
  forall (c: clock) (f: samplStr (A -> A) c) (x y: samplStr A c),
    sp_eq (sp_arrow x (sp_extend f (sp_pre y)))
           (sp_arrow x (sp_extend f (sp_init_pre y))).
Proof.
  intros c f x y;
  apply sp_eq_trans with
    (s2 := sp_arrow x (mem_less_apply (ml_extend2 f) (sp_pre y)));
  auto with sampled_str.
  apply sp_eq_trans with
    (s2 := sp_arrow x (mem_less_apply (ml_extend2 f) (sp_init_pre y)));
  auto with sampled_str.
Qed.

Hint Resolve sp_arrow_extend2_pre_equiv : sampled_str.

Lemma sp_arrow_extend2_pre_lfp :
  forall (n: nat) (c: clock) (f: samplStr (A -> A) c) (x y1 y2: samplStr A c),
      sp_inf n y1 y2 ->
          sp_inf n (sp_arrow x (sp_extend f (sp_pre y1)))
                    (sp_arrow x (sp_extend f (sp_pre y2))).
Proof.
  intros n c f x y1 y2 H1.
  apply sp_inf_trans with (s2 := sp_arrow x (sp_extend f (sp_init_pre y1)));
   auto with sampled_str.
  apply sp_inf_trans with (s2 := sp_arrow x (sp_extend f (sp_init_pre y2)));
   auto with sampled_str.
Qed.

Lemma sp_arrow_extend2_pre_loc_nfstwf :
  forall (n: nat) (c: clock) (f: samplStr (A -> A) c) (x y: samplStr A c),
    sp_wf f -> sp_wf x -> loc_nfstwf n y ->
          loc_nfstwf (S n) (sp_arrow x (sp_extend f (sp_pre y))).
Proof.
  intros n c f x y H1 H2 H3.
  apply loc_nfstwf_sp_eq with (s1 := sp_arrow x (sp_extend f (sp_init_pre y)));
   auto with sampled_str.
  generalize H3; case n; simpl; auto with sampled_str.
Qed.

Lemma sp_arrow_extend2_pre_glob_nfstwf :
  forall (n: nat) (c: clock) (f: samplStr (A -> A) c) (x y: samplStr A c),
    sp_wf f -> sp_wf x -> glob_nfstwf n y ->
          glob_nfstwf (S n) (sp_arrow x (sp_extend f (sp_pre y))).
Proof.
  intros n c f x y H1 H2 H3.
  apply rec0_nfstwf_inc_loc2glob with
   (f := fun y => sp_arrow x (sp_extend f (sp_pre y))); auto.
  intros; apply sp_arrow_extend2_pre_loc_nfstwf; auto.
Qed.

End Extend_prop.

Section IsFstValue.

Variable A: Set.

Variable a: A.

CoInductive is_fst_value : forall (c: clock), samplStr A c -> Prop :=
 | is_fst_value_false:
    forall (c: clock) (s: samplStr A c),
      hd c = false -> is_fst_value (sp_tl s) -> is_fst_value s
 | is_fst_value_true:
    forall (c: clock) (s: samplStr A c),
      (sp_hd s ==<< samplElt A >> Any a) -> is_fst_value s.

Lemma is_fst_value_false_inv :
  forall (c: clock) (s: samplStr A c),
   hd c = false -> is_fst_value s -> is_fst_value (sp_tl s).
Proof.
  intros c s H1 H2; generalize H1; case H2; simpl; auto.
  intros c' s' H3.
  assert (hd c' = true).
  apply eq_dep_eq_param with (x := sp_hd s') (y := Any a); auto.
  rewrite H.
  intros H'; discriminate H'.
Qed.

Lemma is_fst_value_true_inv :
  forall (c: clock) (s: samplStr A c),
    hd c = true -> is_fst_value s -> (sp_hd s ==<< samplElt A >> Any a).
Proof.
  intros c s H1 H2; generalize H1; case H2; simpl; auto.
  intros c' s' H3 H4 H5; rewrite H3 in H5; discriminate H5.
Qed.

Lemma is_fst_value_sp_eq :
  forall (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
      sp_eq s1 s2 -> is_fst_value s1 -> is_fst_value s2.
Proof.
  cofix is_fst_value_sp_eq.
  intros c1 c2 s1 s2 H1 H2; case (eq_false_dec (hd c2)).
   intros H3; apply is_fst_value_false; auto.
     apply is_fst_value_sp_eq with (s1 := sp_tl s1).
     case H1; auto.
     apply is_fst_value_false_inv; auto.
     rewrite <- H3; case (EqSt_inv (sp_eq_EqSt_clock H1)); auto.
   intros H3; apply is_fst_value_true.
   apply eq_dep_ind_l with (x := sp_hd s1) (y := sp_hd s2)
          (P := fun (b: bool) (z: samplElt A b) => z ==<< samplElt A >> Any a).
        apply is_fst_value_true_inv; auto.
         rewrite <- H3; case (EqSt_inv (sp_eq_EqSt_clock H1)); auto.
        case H1; auto.
Qed.

Lemma is_fst_value_const :
  forall (c: clock), is_fst_value (sp_const a c).
Proof.
  cofix is_fst_value_const; intros c; case (eq_false_dec (hd c)).
   intros H; apply is_fst_value_false; simpl; auto.
   intros H; apply is_fst_value_true; simpl; auto.
   rewrite H; simpl; auto.
Qed.

Lemma is_fst_value_sp_arrow :
  forall (c: clock) (x y: samplStr A c),
         is_fst_value x -> is_fst_value (sp_arrow x y).
Proof.
  cofix is_fst_value_sp_arrow; intros c; case c; intros b c'; case b; simpl.
    intros x y H; apply is_fst_value_true; simpl.
      apply is_fst_value_true_inv with (s := x); auto.
    intros x y H; apply is_fst_value_false; simpl; auto.
     apply is_fst_value_sp_arrow;
     apply is_fst_value_false_inv with (s := x); simpl; auto.
Qed.

End IsFstValue.

Hint Resolve is_fst_value_const is_fst_value_sp_arrow : sampled_str.

Section Sampling.

Definition sp_not (c: clock) := sp_extend (sp_const negb c).

Lemma sp_not2_id :
  forall (c: clock) (lc: samplStr bool c),
        sp_eq (sp_not (sp_not lc)) lc.
Proof.
  intros c lc; unfold sp_not;
   apply sp_eq_trans with (s2 := sp_extend (sp_const (fun z => negb (negb z)) c) lc).
   eapply sp_extend_comp; eauto.
   apply sp_extend_id; intros b; case b; auto.
Qed.

Definition elt_on (b:bool) (o: samplElt bool b) : bool :=
  match o with
    | None _ => false
    | Any x => x
    | Fail _ => true
  end.


Lemma elt_on_eq_true :
  forall (b: bool) (x: samplElt bool b),
     elt_on x = true -> (x ==<< samplElt bool >> Any true) \/ (x ==<< samplElt bool >> Fail bool).
Proof.
  intros b x; case x; simpl; auto with eqD.
   intros H; discriminate H.
   intros b0; case b0; auto with eqD.
   intros H; discriminate H.
Qed.

Lemma elt_on_eq_true_weak :
  forall (b: bool) (x: samplElt bool b),
       elt_on x = true -> b = true.
Proof.
  intros b x; case x; simpl; auto.
Qed.

Lemma elt_on_false :
  forall (b: bool) (x: samplElt bool b),
       b = false -> elt_on x = false.
Proof.
  intros b x; case x; simpl; auto.
  intros b' H; discriminate H.
Qed.

Hint Resolve elt_on_false : sp_aux.

CoFixpoint sp_on (c:clock) (lc: samplStr bool c) : clock :=
  Cons (elt_on (sp_hd lc)) (sp_on (sp_tl lc)).

Lemma sp_on_clock_inf :
  forall (c: clock) (lc: samplStr bool c), clock_inf (sp_on lc) c.
Proof.
  cofix sp_on_clock_inf; intros c lc; constructor 1; simpl; auto.
  case (sp_hd lc); simpl; auto. intros b; case b; simpl; auto.
Qed.

Variable A: Set.

Definition elt_merge (b: bool) (o: samplElt bool b) :
       samplElt A (elt_on o) ->
           samplElt A (elt_on (elt_extend (elt_const negb b) o)) -> samplElt A b :=
  match o as o0 in samplElt _ b0 return samplElt A (elt_on o0)
       -> samplElt A (elt_on (elt_extend (elt_const negb b0) o0)) -> samplElt A b0
  with
    | None _ => fun x y => None _
    | Any b0 => if b0 as b return samplElt A b -> samplElt A (negb b) -> samplElt A true
        then fun x y => x else fun x y => y
    | Fail _ => fun x y => Fail _
  end.

Lemma elt_merge_lfp :
  forall (b1 b2: bool) (o1: samplElt bool b1) (o2: samplElt bool b2)
      (x1: samplElt A (elt_on o1)) (x2: samplElt A (elt_on o2))
      (y1: samplElt A (elt_on (elt_extend (elt_const negb _) o1)))
      (y2: samplElt A (elt_on (elt_extend (elt_const negb _) o2))),
     flat_ord o1 o2 -> flat_ord x1 x2 -> flat_ord y1 y2 ->
            flat_ord (elt_merge _ x1 y1) (elt_merge _ x2 y2).
Proof.
  intros b1 b2 o1 o2; case o1; case o2; simpl; auto; clear o1 b1 o2 b2.
  intros b x1 x2 y1 y2 H; inversion H.
  intros x1 x2 y1 y2 H; inversion H.
  intros b x1 x2 y1 y2 H; inversion H.
  intros b1 b2 x1 x2 y1 y2 H1; generalize (eq_dep_eq _ _ _ _ _ H1); intros H2;
  injection H2; intro H3; generalize x1 y1 x2 y2; rewrite H3; case b1; simpl; auto.
  intros b x1 x2 y1 y2 H1; inversion H1.
Qed.

Lemma elt_merge_is_no_Fail :
  forall (b: bool) (o: samplElt bool b) (x: samplElt A (elt_on o))
      (y: samplElt A (elt_on (elt_extend (elt_const negb b) o))),
     is_no_Fail o -> is_no_Fail x -> is_no_Fail y -> is_no_Fail (elt_merge _ x y).
Proof.
   intros b o; case o; simpl; auto; clear o b.
   intros b x1; case x1; simpl; auto.
Qed.

Lemma elt_merge_true :
  forall (b: bool) (o: samplElt bool b) (x: samplElt A (elt_on o))
      (y: samplElt A (elt_on (elt_extend (elt_const negb b) o))),
    (o ==<< samplElt bool >> Any true) -> is_no_Fail x ->
          is_no_Fail (elt_merge _ x y).
Proof.
   intros b o x y H; generalize x y.
   apply eq_dep_ind_l with (x := Any true) (y := o)
        (P := fun (b: bool) (z: samplElt bool b) => forall (x0 : samplElt A (elt_on z))
  (y0 : samplElt A (elt_on (elt_extend (elt_const negb b) z))),
is_no_Fail x0 -> is_no_Fail (elt_merge z x0 y0))
        ; simpl; auto with eqD.
Qed.

Hint Resolve elt_merge_lfp elt_merge_is_no_Fail : sampled_str.

CoFixpoint sp_merge (c: clock) (lc: samplStr bool c) (x: samplStr A (sp_on lc))
    (y: samplStr A (sp_on (sp_not lc))) : samplStr A c :=
 sp_cons _ (elt_merge _ (sp_hd x) (sp_hd y))
                       (sp_merge _ (sp_tl x) (sp_tl y)).

Lemma sp_merge_lfp :
  forall (n: nat) (c1 c2: clock) (lc1: samplStr bool c1) (lc2: samplStr bool c2)
     (s1: samplStr A (sp_on lc1)) (s2: samplStr A (sp_on lc2))
     (t1: samplStr A (sp_on (sp_not lc1))) (t2: samplStr A (sp_on (sp_not lc2))),
    sp_inf n lc1 lc2 -> sp_inf n s1 s2 -> sp_inf n t1 t2 ->
         sp_inf n (sp_merge _ s1 t1) (sp_merge _ s2 t2).
Proof.
  intros n; elim n; simpl.
  intros; apply sp_inf_proof_O; simpl; apply elt_merge_lfp; auto with sampled_str.
    apply sp_inf_O_inv with (c1 := sp_on lc1) (c2 := sp_on lc2); auto.
    apply sp_inf_O_inv with (c1 := sp_on (sp_not lc1)) (c2 := sp_on (sp_not lc2)); auto.
  intros n0 HR c1 c2 lc1 lc2 x1 x2 s1 s2 H H0 H1; case (sp_inf_S_n_inv H);
  case (sp_inf_S_n_inv H0); case (sp_inf_S_n_inv H1); intros; apply sp_inf_proof_S_n; simpl;
  auto with sampled_str.
Qed.

Hint Resolve locle_O locle_S_false_false locle_S_false_true
 locle_S_true_true : sp_aux.
Hint Resolve loc_nfstwf_O loc_nfstwf_false_inv loc_nfstwf_S_n_n_tl : sp_aux.

Lemma sp_merge_loc_nfstwf :
  forall (n: nat) (c: clock) (lc: samplStr bool c) (s: samplStr A (sp_on lc))
      (t: samplStr A (sp_on (sp_not lc))),
     loc_nfstwf n lc ->
       (forall (m: nat), locle m n (sp_on lc) c -> loc_nfstwf m s)
       ->(forall (m: nat), locle m n (sp_on (sp_not lc)) c -> loc_nfstwf m t)
         -> loc_nfstwf n (sp_merge _ s t).
Proof.
  cofix sp_merge_loc_nfstwf.
  intros n; case n.
   intros; apply loc_nfstwf_O.
   intros n0 c lc s t H1 H2 H3; case (eq_false_dec (hd c)).
   intros H4; apply loc_nfstwf_false; simpl; auto.
    apply sp_merge_loc_nfstwf; auto with sp_aux.
      intros; apply loc_nfstwf_false_inv with (s := s); simpl; auto with sp_aux.
      apply H2; apply locle_S_false_false; simpl; auto with sp_aux.
      intros; apply loc_nfstwf_false_inv with (s := t); simpl; auto with sp_aux.
      apply H3; apply locle_S_false_false; simpl; auto with sp_aux.
  intros H4; apply loc_nfstwf_true; simpl; auto.
    apply elt_merge_is_no_Fail.
      apply loc_nfstwf_is_no_Fail with (n := n0); auto.
      case (eq_false_dec (elt_on (sp_hd lc))).
        generalize (sp_hd s); simpl; generalize (elt_on (sp_hd lc));
         intros b x H5; generalize x; rewrite H5;
         intros y; pattern y; apply samplElt_false_inv; simpl; auto.
        intros H5; apply loc_nfstwf_is_no_Fail with (n := O) (s := s); auto with sp_aux.
      case (eq_false_dec (elt_on (sp_hd (sp_not lc)))).
        generalize (sp_hd t); simpl;
        generalize (elt_on (elt_extend (elt_const negb (hd c)) (sp_hd lc)));
         intros b x H5; generalize x; rewrite H5;
         intros y; pattern y; apply samplElt_false_inv; simpl; auto.
        simpl; intros H5; apply loc_nfstwf_is_no_Fail with (n := O) (s := t); auto with sp_aux.
    apply sp_merge_loc_nfstwf; auto with sp_aux.
       intros m H5; case (eq_false_dec (elt_on (sp_hd lc))).
         intros; apply loc_nfstwf_false_inv with (s := s); auto with sp_aux.
         intros; apply loc_nfstwf_S_n_n_tl with (s := s); auto with sp_aux.
       intros m H5; case (eq_false_dec (elt_on (sp_hd (sp_not lc)))).
         intros H6; apply loc_nfstwf_false_inv with (s := t); auto with sp_aux.
         simpl; intros; apply loc_nfstwf_S_n_n_tl with (s := t); simpl; auto with sp_aux.
Qed.

Lemma sp_merge_glob_nfstwf :
  forall (n: nat) (c: clock) (lc: samplStr bool c) (s: samplStr A (sp_on lc))
       (t: samplStr A (sp_on (sp_not lc))),
     glob_nfstwf n lc -> glob_nfstwf n s -> glob_nfstwf n t->
         glob_nfstwf n (sp_merge _ s t).
Proof.
  intros n c lc s t H1 H2 H3;
   apply nfstwf_function_convert_inf with
     (f := fun t => sp_merge _ s t) (n := n); auto.
   intros m t' H4 H5; apply sp_merge_loc_nfstwf; auto.
   assert (glob2loc (loc2glob m c n) c = m).
   apply loc2glob_prop; auto.
   rewrite <- H.
     apply glob_nfstwf_loc_nfstwf.
     apply glob_nfstwf_n_le with (n := n); auto with sampled_str.
     intros m' H6.
     assert (glob2loc (loc2glob m' (sp_on lc) n) (sp_on lc) = m').
     apply loc2glob_prop; auto.
     apply locle_glob2loc_trans with (n2 := m) (c2 := c); auto.
     rewrite <- H.
     apply glob_nfstwf_loc_nfstwf;
     apply glob_nfstwf_n_le with (n := n); auto with sampled_str.
Qed.

Lemma sp_merge_loc_nfstwf_weak :
  forall (n: nat) (c: clock) (lc: samplStr bool c) (s: samplStr A (sp_on lc))
      (t: samplStr A (sp_on (sp_not lc))),
     loc_nfstwf n lc -> loc_nfstwf n s -> loc_nfstwf n t ->
         loc_nfstwf n (sp_merge _ s t).
Proof.
  cofix sp_merge_loc_nfstwf_weak.
  intros n; case n.
   intros; apply loc_nfstwf_O.
   intros n0 c lc s t H1 H2 H3; case (eq_false_dec (hd c)).
   intros H4; apply loc_nfstwf_false; simpl; auto.
    apply sp_merge_loc_nfstwf_weak.
      apply loc_nfstwf_false_inv ; simpl; auto.
      apply loc_nfstwf_false_inv with (s := s); simpl; auto.
       generalize (sp_hd lc); rewrite H4; intros s';
       pattern s'; apply samplElt_false_inv; simpl; auto.
      apply loc_nfstwf_false_inv with (s := t); simpl; auto.
       generalize (sp_hd lc); rewrite H4; intros s';
       pattern s'; apply samplElt_false_inv; simpl; auto.
  intros H4; apply loc_nfstwf_true; simpl; auto.
    apply elt_merge_is_no_Fail.
       apply loc_nfstwf_is_no_Fail with (n := n0); auto.
       apply loc_nfstwf_is_no_Fail with (n := n0) (s := s); auto.
       apply loc_nfstwf_is_no_Fail with (n := n0) (s := t); auto.
    apply sp_merge_loc_nfstwf_weak.
     apply loc_nfstwf_S_n_n_tl; auto.
     apply loc_nfstwf_S_n_n_tl with (s := s); auto.
     apply loc_nfstwf_S_n_n_tl with (s := t); auto.
Qed.

Lemma sp_merge_true_loc_nfstwf :
  forall (n: nat) (c: clock) (lc: samplStr bool c) (s: samplStr A (sp_on lc))
      (t: samplStr A (sp_on (sp_not lc))),
    is_fst_value true lc -> loc_nfstwf (S n) lc -> loc_nfstwf (S n) s ->
        loc_nfstwf n t -> loc_nfstwf (S n) (sp_merge _ s t).
Proof.
  cofix sp_merge_true_loc_nfstwf.
  intros n c lc s t H H1 H2 H3; case (eq_false_dec (hd c)).
  intros H4 ; apply loc_nfstwf_false; simpl; auto.
    apply sp_merge_true_loc_nfstwf.
      apply is_fst_value_false_inv ; auto.
      apply loc_nfstwf_false_inv ; simpl; auto.
      apply loc_nfstwf_false_inv with (s := s); simpl; auto.
       generalize (sp_hd lc); rewrite H4; intros s';
       pattern s'; apply samplElt_false_inv; simpl; auto.
      apply loc_nfstwf_false_inv with (s := t); simpl; auto.
       generalize (sp_hd lc); rewrite H4; intros s';
       pattern s'; apply samplElt_false_inv; simpl; auto.
  intros H4; apply loc_nfstwf_true; simpl; auto.
    apply elt_merge_true.
       apply is_fst_value_true_inv ; auto.
       apply loc_nfstwf_is_no_Fail with (n := n) (s := s); auto.
       apply sp_merge_loc_nfstwf_weak.
        apply loc_nfstwf_S_n_n_tl; auto.
        apply loc_nfstwf_S_n_n_tl with (s := s); auto.
        apply loc_nfstwf_false_inv with (s := t); simpl; auto.
        apply eq_dep_ind_l with (x := Any true) (y := sp_hd lc)
        (P := fun (b: bool) (z: samplElt bool b) => elt_on (elt_extend (elt_const negb b) z) = false)
        ; auto.
        apply eq_dep_sym; apply is_fst_value_true_inv; auto.
Qed.

Hint Resolve sp_merge_lfp sp_merge_loc_nfstwf_weak : sampled_str.

Lemma sp_merge_wf :
  forall (c: clock) (lc: samplStr bool c) (s: samplStr A (sp_on lc))
      (t: samplStr A (sp_on (sp_not lc))),
    sp_wf lc -> sp_wf s -> sp_wf t -> sp_wf (sp_merge _ s t).
Proof.
  auto with sampled_str.
Qed.

Definition elt_when (b: bool) (o: samplElt bool b) :
         samplElt A b -> samplElt A (elt_on o) :=
  match o as o0 in samplElt _ b0 return samplElt A b0 -> samplElt A (elt_on o0) with
    | None _ => fun x => None _
    | Any b0 => fun (x: samplElt A true) =>
             if b0 as b0' return samplElt A b0' then x else None _
    | Fail _ => fun x => Fail _
  end.

Lemma elt_when_lfp :
  forall (b1 b2: bool) (o1: samplElt bool b1) (o2: samplElt bool b2)
       (x1: samplElt A b1) (x2: samplElt A b2),
     flat_ord o1 o2 -> flat_ord x1 x2 ->
            flat_ord (elt_when o1 x1) (elt_when o2 x2).
Proof.
  intros b1 b2 o1 o2; case o1; case o2; simpl; auto; clear o1 b1 o2 b2.
  intros b x1 x2 H; inversion H.
  intros x1 x2 H; inversion H.
  intros b x1 x2 H; inversion H.
  intros b1 b2 x1 x2 H1; generalize (eq_dep_eq _ _ _ _ _ H1); intros H2;
  injection H2; intro H3; generalize x1 x2; rewrite H3; case b1; simpl; auto.
  intros b x1 x2 H; inversion H.
Qed.

Lemma elt_when_is_no_Fail :
  forall (b: bool) (o: samplElt bool b) (x: samplElt A b),
    is_no_Fail o -> is_no_Fail x -> is_no_Fail (elt_when o x).
Proof.
  intros b o; case o; simpl; auto; clear o b.
  intros b'; case b'; simpl; auto.
Qed.

Hint Resolve elt_when_lfp elt_when_is_no_Fail : sampled_str.

CoFixpoint sp_when (c: clock) (lc: samplStr bool c) (x: samplStr A c) :
           samplStr A (sp_on lc) :=
  sp_cons (sp_on lc) (elt_when (sp_hd lc) (sp_hd x))
                          (sp_when (sp_tl lc) (sp_tl x)).

Lemma sp_when_lfp :
  forall (n: nat) (c1 c2: clock) (lc1: samplStr bool c1) (lc2: samplStr bool c2)
        (s1: samplStr A c1) (s2: samplStr A c2),
   sp_inf n lc1 lc2 -> sp_inf n s1 s2 -> sp_inf n (sp_when lc1 s1) (sp_when lc2 s2).
Proof.
  intros n; elim n.
  intros; apply sp_inf_proof_O; simpl; auto with sampled_str.
  intros n0 HR c1 c2 lc1 lc2 s1 s2 H1 H2; case (sp_inf_S_n_inv H1); case (sp_inf_S_n_inv H2); intros;
  apply sp_inf_proof_S_n; simpl; auto with sampled_str.
Qed.

Lemma elt_when_true :
  forall (b: bool) (o: samplElt bool b) (x: samplElt A b),
      (o ==<< samplElt bool >> Any true) ->
      (elt_when o x ==<< samplElt A >> x).
Proof.
  intros b o x H; generalize x.
  apply eq_dep_ind_l with (x := Any true) (y := o)
  (P := fun (b: bool) (z: samplElt bool b) => forall x0 : samplElt A b, elt_when z x0 ==<< samplElt A >> x0)
  ; simpl; auto with eqD.
Qed.

Hint Resolve elt_when_true : sampled_str.

Require Arith.

Lemma sp_when_loc_nfstwf :
  forall (n m: nat) (c: clock) (lc: samplStr bool c) (s: samplStr A c),
    loc_nfstwf n lc -> loc_nfstwf n s -> locle m n (sp_on lc) c
           -> loc_nfstwf m (sp_when lc s).
Proof.
  cofix sp_when_loc_nfstwf.
  intros n m; case m.
  intros; apply loc_nfstwf_O.
  intros n0 c lc s H1 H2 H3; case (eq_false_dec (elt_on (sp_hd lc))).
   intros H4; apply loc_nfstwf_false; simpl; auto.
     apply sp_when_loc_nfstwf with (n := pseudo_pred n (hd c)).
     case (eq_false_dec (hd c)); intros H5; rewrite H5; simpl; auto with sp_aux;
     generalize H1; case n; simpl; auto with sp_aux.
     case (eq_false_dec (hd c)); intros H5; rewrite H5; simpl; auto with sp_aux;
     generalize H2; case n; simpl; auto with sp_aux.
     inversion_clear H3; simpl in H; simpl in H5; rewrite H4 in H; simpl in H.
        rewrite H0; rewrite <- pseudo_pred_S.
        eapply locle_le_1; eauto.
   intros H4; apply loc_nfstwf_true; simpl; auto.
     inversion_clear H3; rewrite (elt_on_eq_true_weak _ H4) in H0;
     simpl in H0; case (elt_on_eq_true _ H4).
     intros;
     apply eq_dep_ind_l with (x := sp_hd s)
     (y := elt_when (sp_hd lc) (sp_hd s))
     (P := fun (b: bool) (z: samplElt A b) => is_no_Fail z)
     ; simpl; auto with sampled_str eqD.
        intros; apply loc_nfstwf_is_no_Fail with (n := n2); auto; rewrite <- H0; auto.
       intros; absurd (is_no_Fail (sp_hd lc)).
       apply eq_dep_ind_l with (x := Fail bool) (y := sp_hd lc)
       (P := fun (b: bool) (z: samplElt bool b) => ~ is_no_Fail z)
       ; simpl; auto with eqD.
         intros; apply loc_nfstwf_is_no_Fail with (n := n2); auto; rewrite <- H0; auto.
     apply sp_when_loc_nfstwf with (n := pred n).
       generalize H1; case n; simpl; auto with sp_aux.
       generalize H2; case n; simpl; auto with sp_aux.
     inversion_clear H3; simpl in H; simpl in H5; rewrite H4 in H; simpl in H.
       rewrite H0; rewrite (elt_on_eq_true_weak _ H4); simpl.
       eapply locle_le_1; eauto with arith.
Qed.

Lemma sp_when_glob_nfstwf :
  forall (n: nat) (c: clock) (lc: samplStr bool c) (s: samplStr A c),
     glob_nfstwf n lc -> glob_nfstwf n s -> glob_nfstwf n (sp_when lc s).
Proof.
  intros n c lc s H1 H2; apply nfstwf_function_convert_sup
    with (f := fun s => sp_when lc s) (n := n); auto.
  apply sp_on_clock_inf.
  intros m k s' H3 H4 H5; apply sp_when_loc_nfstwf with (n := m); auto.
  assert (glob2loc (loc2glob m c n) c = m).
  apply loc2glob_prop; auto.
  rewrite <- H.
  apply glob_nfstwf_loc_nfstwf;
  apply glob_nfstwf_n_le with (n := n); auto with sampled_str.
Qed.

Lemma sp_when_wf :
  forall (c: clock) (lc: samplStr bool c) (s: samplStr A c),
     sp_wf lc -> sp_wf s -> sp_wf (sp_when lc s).
Proof.
  cofix sp_merge_wf.
  intros c ls s H1 H2; case (sp_wf_inv H1); case (sp_wf_inv H2);
   constructor 1;simpl; auto with sampled_str.
Qed.

End Sampling.

Hint Resolve sp_merge sp_when_wf : sampled_str sp_rec0.

Notation merge := sp_merge.

Notation swp_when := (fun lc s => sp_when s lc).
Infix "when" := swp_when (at level 100, right associativity).

Hint Resolve sp_fby_lfp sp_merge_lfp sp_when_lfp : sp_rec0.

Hint Resolve sp_fby_loc_nfstwf
 sp_extend_loc_nfstwf sp_merge_loc_nfstwf_weak : sampled_str.

Hint Resolve sp_when_glob_nfstwf sp_fby_glob_nfstwf
 sp_extend_glob_nfstwf sp_merge_glob_nfstwf : sp_rec0.

Hint Resolve sp_wf_glob_nfstwf glob_nfstwf_sp_wf : sp_rec0.

Section If.

Variable A: Set.

Definition If (b: bool) (x y: A) := if b then x else y.

Definition sp_if (c: clock) (lc: samplStr bool c) (x y: samplStr A c) :=
  sp_extend (sp_extend (sp_extend (sp_const If _) lc) x) y.

Lemma sp_if_lfp :
  forall (n: nat) (c: clock) (lc1 lc2: samplStr bool c) (s1 s2 t1 t2: samplStr A c),
   sp_inf n lc1 lc2 -> sp_inf n s1 s2 -> sp_inf n t1 t2 ->
         sp_inf n (sp_if lc1 s1 t1) (sp_if lc2 s2 t2).
Proof.
  unfold sp_if; auto with sampled_str.
Qed.

Lemma sp_if_loc_nfstwf :
  forall (n: nat) (c: clock) (lc: samplStr bool c) (s1 s2: samplStr A c),
    loc_nfstwf n lc -> loc_nfstwf n s1 -> loc_nfstwf n s2 ->
         loc_nfstwf n (sp_if lc s1 s2).
Proof.
  unfold sp_if; auto with sampled_str.
Qed.

Lemma sp_if_glob_nfstwf :
  forall (n: nat) (c: clock) (lc: samplStr bool c) (s1 s2: samplStr A c),
    glob_nfstwf n lc -> glob_nfstwf n s1 -> glob_nfstwf n s2 ->
         glob_nfstwf n (sp_if lc s1 s2).
Proof.
  unfold sp_if; auto with sp_rec0.
Qed.

Lemma if_equiv :
  forall (c: clock) (lc: samplStr bool c) (x y: samplStr A c),
    sp_wf x -> sp_wf y ->
    sp_eq (sp_if lc x y)
         (sp_merge _ (sp_when lc x)
                   (sp_when (sp_not lc) y)).
Proof.
 cofix if_equiv;
 intros c lc x y H1 H2; constructor 1.
 simpl; rewrite (unfold_samplStr x) in H1; rewrite (unfold_samplStr y) in H2;
 generalize lc x y H1 H2; case c; clear H2 H1 y x lc c; intros b s;
 case b; intros lc; pattern (sp_hd lc).
   apply samplElt_true_inv; simpl; auto with eqD.
   intros a x y; case a; simpl; pattern (sp_hd x); apply samplElt_true_inv; simpl; auto with eqD;
   pattern (sp_hd y); apply samplElt_true_inv; simpl; auto with eqD;
   intros a0 H1 H2.
     case (sp_wf_inv H2); simpl; intros H3; elim H3.
     case (sp_wf_inv H1); simpl; intros H3; elim H3.
 apply samplElt_false_inv; simpl; auto with eqD.
 case (sp_wf_inv H2); case (sp_wf_inv H1); intros;
 apply if_equiv with (lc := sp_tl lc) (x := sp_tl x) (y := sp_tl y);
 auto.
Qed.

Lemma if_false_equiv :
  forall (c: clock) (x y: samplStr A c),
     sp_wf x -> sp_eq y (sp_if (sp_const false _) x y).
Proof.
  cofix if_false_equiv.
  intros c x y; constructor 1.
   simpl; case (sp_wf_inv H); generalize (sp_hd x); case (sp_hd y); simpl; auto with eqD.
  intros a s; pattern s; apply samplElt_true_inv; simpl; auto.
  intros H'; elim H'.
  intros s; pattern s; apply samplElt_true_inv; simpl; auto.
  apply if_false_equiv with (x := sp_tl x) (y := sp_tl y); case (sp_wf_inv H); auto.
Qed.

Lemma const_decal_eq :
  forall (A: Set) (c: clock) (a: A),
     sp_eq (sp_const a c) (sp_delay (sp_const a c) (Any a)).
Proof.
  intros A'; cofix const_decal_eq.
  intros c a; constructor 1.
  case c; intros b c'; case b; simpl; auto with eqD.
  case c; intros b c'; case b; apply const_decal_eq with (c := c') (a := a).
Qed.

Hint Resolve const_decal_eq sp_if_lfp sp_if_loc_nfstwf : sampled_str.

Lemma arrow_equiv :
  forall (c: clock) (x y: samplStr A c),
     sp_wf x -> sp_wf y ->
       sp_eq (sp_arrow x y) (sp_if (`true` fby `false`) x y).
Proof.
 cofix arrow_equiv;
 intros c x y H1 H2; constructor 1.
 simpl; case (sp_wf_inv H2); generalize (sp_hd y); case (sp_hd x); simpl; auto with eqD.
  intros a s; pattern s; apply samplElt_true_inv; simpl; auto.
  intros H'; elim H'.
  case (sp_wf_inv H1); case (sp_wf_inv H2); generalize x y;
  case c; intros b c0; case b; clear b H1 H2 y x c.
  intros x y H1 H2 H3 H4;
  change (sp_eq (sp_tl y)
               (sp_if (sp_delay (sp_const false c0) (Any false)) (sp_tl x) (sp_tl y))).
  apply sp_eq_trans with (s2 := sp_if (sp_const false c0) (sp_tl x) (sp_tl y)).
  apply if_false_equiv; auto.
  apply sp_inf_wf_eq; auto with sampled_str.
  intros x y H1 H2 H3 H4; apply arrow_equiv with (x := sp_tl x) (y := sp_tl y); auto.
Qed.

End If.

Hint Resolve sp_if_lfp : sampled_str sp_rec0.
Hint Resolve sp_if_loc_nfstwf: sampled_str.
Hint Resolve sp_if_glob_nfstwf : sp_rec0.


Unset Implicit Arguments.