From Coq Require Import List.
From Coq Require Export Lists.Streams.
From Coq Require Import Setoid.
From Coq Require Import Morphisms.
From Coq Require Import Arith.EqNat.
From Coq Require Import Omega.

From Velus Require Import Common.
From Velus Require Import Operators.
From Velus Require Import Environment.
From Velus Require Import Clocks.

Module Type COINDSTREAMS
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Op).

  Open Scope stream_scope.

  Lemma const_nth:
    forall {A} n (c: A),
      (Streams.const c) # n = c.

  Ltac unfold_Stv xs :=
    rewrite (unfold_Stream xs);
    destruct xs as [[|]];
    simpl.

  Ltac unfold_St xs :=
    rewrite (unfold_Stream xs);
    destruct xs;
    simpl.

  Lemma eq_EqSt:
    forall {A}, inclusion (Stream A) eq (@EqSt A).

  Add Parametric Morphism A : (@Cons A)
      with signature eq ==> @EqSt A ==> @EqSt A
        as Cons_EqSt.

  Add Parametric Morphism A : (@hd A)
      with signature @EqSt A ==> eq
        as hd_EqSt.

  Add Parametric Morphism A : (@tl A)
      with signature @EqSt A ==> @EqSt A
        as tl_EqSt.

  Add Parametric Morphism A (n: nat) : (@Str_nth A n)
      with signature @EqSt A ==> eq
        as Str_nth_EqSt.

  Section EqSts.
    Context {A: Type}.

    Definition EqSts (xss yss: list (Stream A)) :=
      Forall2 (@EqSt A) xss yss.

    Theorem EqSts_reflex: forall xss, EqSts xss xss.

    Theorem EqSts_sym: forall xss yss, EqSts xss yss -> EqSts yss xss.

    Theorem EqSts_trans: forall xss yss zss, EqSts xss yss -> EqSts yss zss -> EqSts xss zss.

  End EqSts.

  Add Parametric Relation A : (list (Stream A)) (@EqSts A)
      reflexivity proved by (@EqSts_reflex A)
      symmetry proved by (@EqSts_sym A)
      transitivity proved by (@EqSts_trans A)
        as EqStsrel.

  Add Parametric Morphism A : (@List.cons (Stream A))
      with signature @EqSt A ==> @EqSts A ==> @EqSts A
        as cons_EqSt.

  Add Parametric Morphism A : (@List.app (Stream A))
      with signature @EqSts A ==> @EqSts A ==> @EqSts A
        as app_EqSts.

  Add Parametric Morphism
      A B (P: A -> Stream B -> Prop) xs
      (P_compat: Proper (eq ==> @EqSt B ==> Basics.impl) P)
    : (@Forall2 A (Stream B) P xs)
      with signature @EqSts B ==> Basics.impl
        as Forall2_EqSt.

  Add Parametric Morphism
      A B (P: A -> Stream B -> Prop) xs
      (P_compat: Proper (eq ==> @EqSt B ==> iff) P)
    : (@Forall2 A (Stream B) P xs)
      with signature @EqSts B ==> iff
        as Forall2_EqSt_iff.

  Add Parametric Morphism
      A B (P: Stream A -> B -> Prop)
      (P_compat: Proper (@EqSt A ==> eq ==> Basics.impl) P)
    : (@Forall2 (Stream A) B P)
      with signature @EqSts A ==> eq ==> Basics.impl
        as Forall2_EqSt'.

  Add Parametric Morphism
      A B (P: A -> Stream B -> Prop) xs
      (P_compat: Proper (eq ==> @EqSt B ==> Basics.flip Basics.impl) P)
    : (@Forall2 A (Stream B) P xs)
      with signature @EqSts B ==> Basics.flip Basics.impl
        as Forall2_EqSt_flip.

  Add Parametric Morphism
      A B C (P: A -> B -> Stream C -> Prop) xs ys
      (P_compat: Proper (eq ==> eq ==> @EqSt C ==> Basics.impl) P)
    : (@Forall3 A B (Stream C) P xs ys)
      with signature @EqSts C ==> Basics.impl
        as Forall3_EqSt.

  Add Parametric Morphism
      A B
    : (@List.map (Stream A) (Stream B))
      with signature (fun (f f': Stream A -> Stream B) => forall xs xs', xs ≡ xs' -> f xs ≡ f' xs') ==> @EqSts A ==> @EqSts B
        as map_st_EqSt.

  Add Parametric Morphism
      A B
    : (@List.map (Stream A) B)
      with signature (fun (f f': Stream A -> B) => forall xs xs', xs ≡ xs' -> f xs = f' xs') ==> @EqSts A ==> eq
        as map_EqSt.

  Add Parametric Morphism
      A P
      (P_compat: Proper (@EqSt A ==> Basics.impl) P)
    : (@Forall (Stream A) P)
      with signature @EqSts A ==> Basics.impl
        as Forall_EqSt.


  CoFixpoint const (b: Stream bool) (c: const): Stream value :=
    (if hd b then present (sem_const c) else absent) ⋅ const (tl b) c.

  CoInductive lift1 (op: unop) (ty: type)
    : Stream value -> Stream value -> Prop :=
  | Lift1A:
      forall xs rs,
        lift1 op ty xs rs ->
        lift1 op ty (absent ⋅ xs) (absent ⋅ rs)
  | Lift1P:
      forall x r xs rs,
        sem_unop op x ty = Some r ->
        lift1 op ty xs rs ->
        lift1 op ty (present x ⋅ xs) (present r ⋅ rs).

  CoInductive lift2 (op: binop) (ty1 ty2: type)
    : Stream value -> Stream value -> Stream value -> Prop :=
  | Lift2A:
      forall xs ys rs,
        lift2 op ty1 ty2 xs ys rs ->
        lift2 op ty1 ty2 (absent ⋅ xs) (absent ⋅ ys) (absent ⋅ rs)
  | Lift2P:
      forall x y r xs ys rs,
        sem_binop op x ty1 y ty2 = Some r ->
        lift2 op ty1 ty2 xs ys rs ->
        lift2 op ty1 ty2 (present x ⋅ xs) (present y ⋅ ys) (present r ⋅ rs).

  CoInductive when (b: bool)
    : Stream value -> Stream value -> Stream value -> Prop :=
  | WhenA:
      forall xs cs rs,
        when b xs cs rs ->
        when b (absent ⋅ xs) (absent ⋅ cs) (absent ⋅ rs)
  | WhenPA:
      forall x c xs cs rs,
        when b xs cs rs ->
        val_to_bool c = Some (negb b) ->
        when b (present x ⋅ xs) (present c ⋅ cs) (absent ⋅ rs)
  | WhenPP:
      forall x c xs cs rs,
        when b xs cs rs ->
        val_to_bool c = Some b ->
        when b (present x ⋅ xs) (present c ⋅ cs) (present x ⋅ rs).

  CoInductive merge
    : Stream value -> Stream value -> Stream value -> Stream value -> Prop :=
  | MergeA:
      forall xs ts fs rs,
        merge xs ts fs rs ->
        merge (absent ⋅ xs) (absent ⋅ ts) (absent ⋅ fs) (absent ⋅ rs)
  | MergeT:
      forall t xs ts fs rs,
        merge xs ts fs rs ->
        merge (present true_val ⋅ xs)
              (present t ⋅ ts) (absent ⋅ fs) (present t ⋅ rs)
  | MergeF:
      forall f xs ts fs rs,
        merge xs ts fs rs ->
        merge (present false_val ⋅ xs)
              (absent ⋅ ts) (present f ⋅ fs) (present f ⋅ rs).

  CoInductive ite
    : Stream value -> Stream value -> Stream value -> Stream value -> Prop :=
  | IteA:
      forall s ts fs rs,
        ite s ts fs rs ->
        ite (absent ⋅ s) (absent ⋅ ts) (absent ⋅ fs) (absent ⋅ rs)
  | IteT:
      forall t f s ts fs rs,
        ite s ts fs rs ->
        ite (present true_val ⋅ s)
            (present t ⋅ ts) (present f ⋅ fs) (present t ⋅ rs)
  | IteF:
      forall t f s ts fs rs,
        ite s ts fs rs ->
        ite (present false_val ⋅ s)
            (present t ⋅ ts) (present f ⋅ fs) (present f ⋅ rs).

  CoInductive bools_of: Stream value -> Stream bool -> Prop :=
    bools_of_intro:
      forall v vs b bs,
        bools_of vs bs ->
        value_to_bool v = Some b ->
        bools_of (v ⋅ vs) (b ⋅ bs).

  CoFixpoint mask (k: nat) (rs: Stream bool) (xs: Stream value) : Stream value :=
    let mask' k' := mask k' (tl rs) (tl xs) in
    match k, hd rs with
    | 0, true => Streams.const absent
    | 0, false => hd xs ⋅ mask' 0
    | 1, true => hd xs ⋅ mask' 0
    | S k', true => absent ⋅ mask' k'
    | S _, false => absent ⋅ mask' k
    end.

  CoFixpoint count_acc (s: nat) (rs: Stream bool): Stream nat :=
    let s := if hd rs then S s else s in
    s ⋅ count_acc s (tl rs).

  Definition count := count_acc 0.

  Lemma count_acc_grow_trans:
    forall s s' rs,
      s' <= s ->
      ForAll (fun x => s' <= hd x) (count_acc s rs).

  Corollary count_acc_grow:
    forall s rs,
      ForAll (fun x => s <= hd x) (count_acc s rs).

  Lemma count_S_nth:
    forall n s rs,
      hd (Str_nth_tl n (count_acc (S s) rs)) =
      S (hd (Str_nth_tl n (count_acc s rs))).

  Lemma mask_nth:
    forall n k rs xs,
      (mask k rs xs) # n = if (count rs) # n =? k then xs # n else absent.

  Lemma mask_EqSt' : forall b x y,
    (forall (k : nat), mask k b x ≡ mask k b y) ->
    x ≡ y.

Boolean mask

  CoFixpoint maskb (k: nat) (rs: Stream bool) (xs: Stream bool) : Stream bool :=
    let mask' k' := maskb k' (tl rs) (tl xs) in
    match k, hd rs with
    | 0, true => Streams.const false
    | 0, false => hd xs ⋅ mask' 0
    | 1, true => hd xs ⋅ mask' 0
    | S k', true => false ⋅ mask' k'
    | S _, false => false ⋅ mask' k
    end.

  Lemma maskb_nth:
    forall n k rs xs,
      (maskb k rs xs) # n = if (count rs) # n =? k then xs # n else false.

  Corollary maskb_Cons:
    forall k r rs x xs,
      (maskb k (r ⋅ rs) (x ⋅ xs))
        ≡ (match k with
           | 0 => if r then (Streams.const false) else (x ⋅ (maskb 0 rs xs))
           | 1 => if r then (x ⋅ (maskb 0 rs xs)) else (false ⋅ maskb 1 rs xs)
           | S (S _ as k') => if r then (false ⋅ maskb k' rs xs) else (false ⋅ maskb k rs xs)
           end).

  Lemma maskb_EqSt' : forall b x y,
    (forall (k : nat), maskb k b x ≡ maskb k b y) ->
    x ≡ y.

  Lemma maskb_idem : forall k b x,
      maskb k b (maskb k b x) ≡ maskb k b x.

fby stream

  CoFixpoint sfby (v : Op.val) (str : Stream OpAux.value) :=
    match str with
    | (present v') ⋅ str' => (present v) ⋅ (sfby v' str')
    | absent ⋅ str' => absent ⋅ (sfby v str')
    end.

  Fact sfby_Cons : forall v y ys,
      sfby v (y ⋅ ys) =
      match y with
      | present v' => (present v) ⋅ (sfby v' ys)
      | absent => absent ⋅ (sfby v ys)
      end.

  Add Parametric Morphism : sfby
      with signature eq ==> @EqSt value ==> @EqSt value
    as sfby_EqSt.

exp level synchronous operators specifications To ease the use of coinductive hypotheses to prove non-coinductive goals, we give for each coinductive predicate an indexed specification, reflecting the shapes of the involved streams pointwise speaking. In general this specification is a disjunction with a factor for each case of the predicate. The corresponding lemmas simply go by induction on n and by inversion of the coinductive hypothesis for the direct direction, and by coinduction on the converse.

  Lemma const_spec:
    forall xs c b,
      xs ≡ const b c <->
      forall n, xs # n = if b # n then present (sem_const c) else absent.

  Corollary const_true: forall bs c n,
      bs # n = true ->
      (const bs c) # n = present (sem_const c).

  Corollary const_false : forall bs c n,
      bs # n = false ->
      (const bs c) # n = absent.

  Lemma const_inv1 :
    forall c b s,
      const b c ≡ absent ⋅ s ->
      exists b', s ≡ const b' c /\ b ≡ false ⋅ b'.

  Lemma const_inv2 :
    forall c c' b s,
      const b c ≡ present c' ⋅ s ->
      exists b', s ≡ const b' c
            /\ b ≡ true ⋅ b'
            /\ c' = sem_const c.

  Lemma const_tl :
    forall c b v tl,
      const b c ≡ v ⋅ tl ->
      const (Streams.tl b) c ≡ tl.

  Lemma const_Cons : forall c b bs,
      const (b ⋅ bs) c ≡
      (if b then present (sem_const c) else absent) ⋅ (const bs c).

  Ltac cofix_step CoFix H :=
    let n := fresh "n" in
    apply CoFix; intro n; specialize (H (S n));
    repeat rewrite Str_nth_S in H; auto.

  Lemma when_spec:
    forall k xs cs rs,
      when k xs cs rs <->
      (forall n,
          (xs # n = absent
           /\ cs # n = absent
           /\ rs # n = absent)
          \/
          (exists x c,
              xs # n = present x
              /\ cs # n = present c
              /\ val_to_bool c = Some (negb k)
              /\ rs # n = absent)
          \/
          (exists x c,
              xs # n = present x
              /\ cs # n = present c
              /\ val_to_bool c = Some k
              /\ rs # n = present x)).

  Lemma lift1_spec:
    forall op t xs ys,
      lift1 op t xs ys <->
      (forall n,
          (xs # n = absent /\ ys # n = absent)
          \/
          (exists x y,
              xs # n = present x
              /\ sem_unop op x t = Some y
              /\ ys # n = present y)).

  Lemma lift2_spec:
    forall op t1 t2 xs ys zs,
      lift2 op t1 t2 xs ys zs <->
      (forall n,
          (xs # n = absent
           /\ ys # n = absent
           /\ zs # n = absent)
          \/
          (exists x y z,
              xs # n = present x
              /\ ys # n = present y
              /\ sem_binop op x t1 y t2 = Some z
              /\ zs # n = present z)).

cexp level synchronous operators specifications

  Lemma merge_spec:
    forall xs ts fs rs,
      merge xs ts fs rs <->
      (forall n,
          (xs # n = absent
           /\ ts # n = absent
           /\ fs # n = absent
           /\ rs # n = absent)
          \/
          (exists t,
              xs # n = present true_val
              /\ ts # n = present t
              /\ fs # n = absent
              /\ rs # n = present t)
          \/
          (exists f,
              xs # n = present false_val
              /\ ts # n = absent
              /\ fs # n = present f
              /\ rs # n = present f)).

  Lemma ite_spec:
    forall xs ts fs rs,
      ite xs ts fs rs <->
      (forall n,
          (xs # n = absent
           /\ ts # n = absent
           /\ fs # n = absent
           /\ rs # n = absent)
          \/
          (exists t f,
              xs # n = present true_val
              /\ ts # n = present t
              /\ fs # n = present f
              /\ rs # n = present t)
          \/
          (exists t f,
              xs # n = present false_val
              /\ ts # n = present t
              /\ fs # n = present f
              /\ rs # n = present f)).

  Add Parametric Morphism k : (mask k)
      with signature @EqSt bool ==> @EqSt value ==> @EqSt value
        as mask_EqSt.

  Add Parametric Morphism k : (maskb k)
      with signature @EqSt bool ==> @EqSt bool ==> @EqSt bool
        as maskb_EqSt.


  Add Parametric Morphism : ite
      with signature @EqSt value ==> @EqSt value ==> @EqSt value ==> @EqSt value ==> Basics.impl
        as ite_EqSt.

history and it's properties

  Definition history := Env.t (Stream value).
  Definition history_tl (H: history) : history := Env.map (@tl value) H.

  Fact history_tl_find_Some : forall (H: history) id vs,
      Env.find id H = Some vs ->
      Env.find id (history_tl H) = Some (tl vs).

  Fact history_tl_find_Some' : forall (H: history) id vs,
      Env.find id (history_tl H) = Some vs ->
      exists v, Env.find id H = Some (v ⋅ vs).

  Fact history_tl_find_None : forall (H: history) id,
      Env.find id H = None ->
      Env.find id (history_tl H) = None.

  Fact history_tl_find_None' : forall (H: history) id,
      Env.find id (history_tl H) = None ->
      Env.find id H = None.

  Definition env := Env.t value.

  Definition history_nth (n : nat) (H: history) : env :=
    Env.map (Str_nth n) H.

  Definition history_hd (H: history) : env := history_nth 0 H.

  Lemma history_nth_tl : forall H n,
      history_nth (S n) H = history_nth n (history_tl H).

  Fact history_nth_find_None : forall n (H: history) id,
      Env.find id H = None ->
      Env.find id (history_nth n H) = None.

  Fact history_nth_find_None' : forall n (H: history) id,
      Env.find id (history_nth n H) = None ->
      Env.find id H = None.

  Fact history_nth_find_Some : forall n (H: history) id vs,
      Env.find id H = Some vs ->
      Env.find id (history_nth n H) = Some (Str_nth n vs).

  Fact history_nth_find_Some' : forall n (H: history) id v,
      Env.find id (history_nth n H) = Some v ->
      exists vs, Env.find id H = Some vs /\ vs # n = v.

  Fact history_nth_find_Some'' : forall (H: history) vs id,
      (forall n, Env.find id (history_nth n H) = Some (vs # n)) ->
      exists vs', Env.find id H = Some vs' /\ vs' ≡ vs.

  Fact history_hd_refines : forall H H',
      Env.refines eq H H' ->
      Env.refines eq (history_hd H) (history_hd H').

  Fact history_tl_refines : forall H H',
      Env.refines eq H H' ->
      Env.refines eq (history_tl H) (history_tl H').

  Lemma history_nth_refines : forall H H',
      Env.refines eq H H' ->
      forall n, Env.refines eq (history_nth n H) (history_nth n H').

  Lemma env_find_tl : forall x x' H H',
      orel (@EqSt value) (Env.find x H) (Env.find x' H') ->
      orel (@EqSt value)
           (Env.find x (history_tl H))
           (Env.find x' (history_tl H')).

sem_var This is common to Lustre and NLustre Semantics

  Inductive sem_var: history -> ident -> Stream value -> Prop :=
    sem_var_intro:
      forall H x xs xs',
        Env.MapsTo x xs' H ->
        xs ≡ xs' ->
        sem_var H x xs.

  Instance sem_var_Proper:
    Proper (@eq history ==> @eq ident ==> @EqSt value ==> iff)
           sem_var.

  Lemma sem_var_det : forall H x s1 s2,
      sem_var H x s1 ->
      sem_var H x s2 ->
      s1 ≡ s2.

  Lemma env_maps_tl :
    forall i v s H,
      Env.MapsTo i (v ⋅ s) H -> Env.MapsTo i s (history_tl H).

  Lemma sem_var_step :
    forall H x v s,
      sem_var H x (v ⋅ s) -> sem_var (history_tl H) x s.

  Lemma sem_var_step_nl :
    forall H x v s,
      sem_var H x (v ⋅ s) -> sem_var (history_tl H) x s.

  Lemma sem_var_switch_env:
    forall H H' x v,
      orel (@EqSt value) (Env.find x H) (Env.find x H') ->
      sem_var H x v <-> sem_var H' x v.

  Lemma sem_var_env_eq :
    forall H H' xs ss,
      Forall2 (sem_var H) xs ss ->
      Forall2 (sem_var H') xs ss ->
      Forall (fun x => orel (EqSt (A:=value)) (Env.find x H) (Env.find x H')) xs.

sem_clock This is also common to Lustre and NLustre *

clocks_of and its properties

  CoFixpoint clocks_of (ss: list (Stream value)) : Stream bool :=
    existsb (fun s => hd s <>b absent) ss ⋅ clocks_of (List.map (@tl value) ss).

  Add Parametric Morphism : clocks_of
      with signature @EqSts value ==> @EqSt bool
        as clocks_of_EqSt.

  Lemma clocks_of_nth : forall n xs,
      (clocks_of xs) # n = existsb (fun s => s <>b absent) (List.map (Str_nth n) xs).

  Lemma clocks_of_mask : forall xs k rs,
      clocks_of (List.map (mask k rs) xs) ≡ (maskb k rs (clocks_of xs)).

sem_clock and its properties

  CoInductive sem_clock: history -> Stream bool -> clock -> Stream bool -> Prop :=
  | Sbase:
      forall H b b',
        b ≡ b' ->
        sem_clock H b Cbase b'
  | Son:
      forall H b bk bs ck x k xs c,
        sem_clock H b ck (true ⋅ bk) ->
        sem_var H x (present c ⋅ xs) ->
        val_to_bool c = Some k ->
        sem_clock (history_tl H) (tl b) (Con ck x k) bs ->
        sem_clock H b (Con ck x k) (true ⋅ bs)
  | Son_abs1:
      forall H b bk bs ck x k xs,
        sem_clock H b ck (false ⋅ bk) ->
        sem_var H x (absent ⋅ xs) ->
        sem_clock (history_tl H) (tl b) (Con ck x k) bs ->
        sem_clock H b (Con ck x k) (false ⋅ bs)
  | Son_abs2:
      forall H b bk bs ck x k c xs,
        sem_clock H b ck (true ⋅ bk) ->
        sem_var H x (present c ⋅ xs) ->
        val_to_bool c = Some k ->
        sem_clock (history_tl H) (tl b) (Con ck x (negb k)) bs ->
        sem_clock H b (Con ck x (negb k)) (false ⋅ bs).

  Fact history_tl_Equiv : forall H H',
      Env.Equiv (@EqSt value) H H' ->
      Env.Equiv (@EqSt value) (history_tl H) (history_tl H').

  Add Parametric Morphism : sem_clock
      with signature Env.Equiv (@EqSt value) ==> @EqSt bool ==> eq ==> @EqSt bool ==> Basics.impl
        as sem_clock_morph.

  Lemma sc_step :
    forall H b ck s ss,
      sem_clock H b ck (s ⋅ ss) ->
      sem_clock (history_tl H) (Streams.tl b) ck ss.

  Ltac discriminate_stream :=
    let H := fresh in
    match goal with
    | H1: ?b ≡ true ⋅ _, H2 : ?b ≡ false ⋅ _ |- _ =>
      rewrite H1 in H2; inversion H2 as [? H]; simpl in H; discriminate
    end.

  Ltac discriminate_var :=
    repeat match goal with
           | H: sem_var _ _ _ |- _ => auto
           end;
    match goal with
    | H1: sem_var ?H ?x (present _ ⋅ _),
          H2 : sem_var ?H ?x (absent ⋅ _)
      |- _ => eapply sem_var_det with (2 := H2) in H1;
            inv H1; simpl in *; discriminate
    end.

  Lemma sem_clock_det :
    forall (ck : clock) (H : history)
      (b xs xs' : Stream bool),
      sem_clock H b ck xs ->
      sem_clock H b ck xs' ->
      xs ≡ xs'.

  Fact sem_clock_true_inv : forall H ck b bs bs',
      sem_clock H (b ⋅ bs) ck (true ⋅ bs') ->
      b = true.

  Ltac discriminate_clock :=
    let HH := fresh in
    match goal with
    | H1: sem_clock ?H ?b ?ck (true ⋅ _),
          H2 : sem_clock ?H ?b ?ck (false ⋅ _) |- _ =>
      eapply sem_clock_det with (2 := H2) in H1; eauto;
      inversion H1 as [HH ?]; simpl in HH; discriminate
    end.

  CoInductive sub_clock : relation (Stream bool) :=
  | SubP1 : forall s s',
      sub_clock s s' -> sub_clock (true ⋅ s) (true ⋅ s')
  | SubP2 : forall s s',
      sub_clock s s' -> sub_clock (true ⋅ s) (false ⋅ s')
  | SubA : forall s s',
      sub_clock s s' -> sub_clock (false ⋅ s) (false ⋅ s').

  Global Instance sub_clock_trans : Transitive sub_clock.

  Global Instance sub_clock_refl : Reflexive sub_clock.

  Add Parametric Morphism : (sub_clock)
      with signature @EqSt bool ==> @EqSt bool ==> Basics.impl
        as sub_clock_EqSt.

  Lemma sub_clock_step :
    forall b b', sub_clock b b' -> sub_clock (Streams.tl b) (Streams.tl b').

  Lemma sub_clock_Con :
    forall H b ck x b0 s s',
      sem_clock H b ck s ->
      sem_clock H b (Con ck x b0) s' ->
      sub_clock s s'.

  Lemma sub_clock_parent :
    forall H b ck ck' s s',
      sem_clock H b ck s ->
      sem_clock H b ck' s' ->
      clock_parent ck ck' ->
      sub_clock s s'.

Aligned and its properties

  CoInductive aligned: Stream value -> Stream bool -> Prop :=
  | synchro_present:
      forall v vs bs,
        aligned vs bs ->
        aligned (present v ⋅ vs) (true ⋅ bs)
  | synchro_absent:
      forall vs bs,
        aligned vs bs ->
        aligned (absent ⋅ vs) (false ⋅ bs).

  Instance aligned_Proper:
    Proper (@EqSt value ==> @EqSt bool ==> iff)
           aligned.

  Lemma aligned_spec : forall vs bs,
      aligned vs bs <->
      (forall n, (exists v, bs # n = true /\ vs # n = present v)
            \/ (bs # n = false /\ vs # n = absent)).

  Lemma aligned_EqSt : forall vs bs1 bs2,
      aligned vs bs1 ->
      aligned vs bs2 ->
      bs1 ≡ bs2.

  Lemma const_aligned : forall bs c,
      aligned (const bs c) bs.

  CoFixpoint abstract_clock (xs: Stream value) : Stream bool:=
    match xs with
    | absent ⋅ xs => false ⋅ abstract_clock xs
    | present _ ⋅ xs => true ⋅ abstract_clock xs
    end.

  Add Parametric Morphism : (abstract_clock)
      with signature @EqSt value ==> @EqSt bool
        as ac_EqSt.

  Lemma ac_tl :
    forall s, abstract_clock (Streams.tl s) ≡ Streams.tl (abstract_clock s).

  Lemma ac_when :
    forall k cs xs rs,
      when k cs xs rs -> abstract_clock cs ≡ abstract_clock xs.

  Lemma ac_const:
    forall c b cs,
      const b c ≡ cs -> b ≡ abstract_clock cs.

  Lemma ac_ite :
    forall s ts fs rs,
      ite s ts fs rs -> abstract_clock ts ≡ abstract_clock rs.

  Lemma ac_lift1 :
    forall op ty s o,
      lift1 op ty s o -> abstract_clock s ≡ abstract_clock o.

  Lemma ac_lift2 :
    forall op ty1 ty2 s1 s2 o,
      lift2 op ty1 ty2 s1 s2 o -> abstract_clock s1 ≡ abstract_clock o.

  Lemma ac_aligned :
    forall s, aligned s (abstract_clock s).

  Lemma sub_clock_sclocksof :
    forall s ss,
      In s ss ->
      Forall (fun s' => sub_clock (abstract_clock s) (abstract_clock s')) ss ->
      clocks_of ss ≡ abstract_clock s.

  Fact ac_Streams_const :
    abstract_clock (Streams.const absent) ≡ Streams.const false.

  Lemma ac_mask : forall k rs xs,
      abstract_clock (mask k rs xs) ≡ maskb k rs (abstract_clock xs).

End COINDSTREAMS.

Module CoindStreamsFun
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Op) <: COINDSTREAMS Op OpAux.
  Include COINDSTREAMS Op OpAux.
End CoindStreamsFun.