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

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

From Coq Require Import Logic.IndefiniteDescription.

Infix "⊑" := (@FEnv.refines _ _ (@EqSt _)) (at level 70, no associativity) : fenv_scope.

Module Type COINDSTREAMS
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Ids Op)
       (Import Clocks : CLOCKS Ids Op OpAux).

  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.

  Add Parametric Morphism
      A
      : (@length (Stream A))
      with signature @EqSts A ==> eq
        as length_EqSt.

  Lemma map_nth_error_orel:
    forall {A B} (l : list (Stream A)) (f: Stream A -> Stream B) n x,
      (forall x y, x ≡ y -> f x ≡ f y) ->
      orel (@EqSt _) (nth_error l n) (Some x) ->
      orel (@EqSt _) (nth_error (List.map f l) n) (Some (f x)).

  Lemma map_nth_error_orel':
    forall {A B} (l: list (Stream A)) (f: Stream A -> Stream B) n x,
      orel (@EqSt _) (nth_error (List.map f l) n) (Some x) ->
      exists y,
        orel (@EqSt _) (nth_error l n) (Some y)
        /\ x ≡ f y.

  Add Parametric Morphism
      A
      : (@List.nth_error (Stream A))
      with signature @EqSts A ==> eq ==> orel (@EqSt A)
        as nth_error_EqSt.

  Lemma EqSts_nil:
    forall {A} (l: list (Stream A)),
      EqSts l [] <-> l = [].

  Section EqStN.
    Context {A : Type}.

    Inductive EqStN : nat -> Stream A -> Stream A -> Prop :=
    | EqSt0 : forall xs1 xs2, EqStN 0 xs1 xs2
    | EqStS : forall n x1 xs1 x2 xs2,
        x1 = x2 ->
        EqStN n xs1 xs2 ->
        EqStN (S n) (x1 ⋅ xs1) (x2 ⋅ xs2).

    Lemma EqStN_spec : forall n xs1 xs2,
        (EqStN n xs1 xs2) <->
        (forall k, k < n -> xs1 # k = xs2 # k).

    Lemma EqStN_EqSt : forall xs1 xs2,
        (forall n, EqStN n xs1 xs2) <-> xs1 ≡ xs2.

    Corollary EqStN_EqSts : forall xs1 xs2,
        (forall n, Forall2 (EqStN n) xs1 xs2) <-> EqSts xs1 xs2.

    Lemma EqStN_weaken : forall k n xs1 xs2,
        k < n ->
        EqStN n xs1 xs2 ->
        EqStN k xs1 xs2.

    Corollary EqStN_weaken_S : forall n xs1 xs2,
        EqStN (S n) xs1 xs2 ->
        EqStN n xs1 xs2.
  End EqStN.

  Global Hint Constructors EqStN : coindstreams.

  Global Instance EqStN_refl {A} n : Reflexive (@EqStN A n).

  Global Instance EqStN_sym {A} n : Symmetric (@EqStN A n).

  Global Instance EqStN_trans {A} n : Transitive (@EqStN A n).

  Add Parametric Morphism A n : (@EqStN A n)
      with signature @EqSt _ ==> @EqSt _ ==> Basics.impl
        as EqStN_morph.

  Add Parametric Morphism {A B} (f : A -> B) n : (map f)
      with signature @EqStN _ n ==> @EqStN _ n
        as map_EqStN.

  CoFixpoint init_from {A} (n: nat) (f: nat -> A) : Stream A :=
    f n ⋅ init_from (S n) f.

  Lemma init_from_n:
    forall {A} (f: nat -> A) n,
      init_from n f = f n ⋅ init_from (S n) f.

  Lemma init_from_nth:
    forall {A} m n (f: nat -> A),
      (init_from n f) # m = f (m + n).

  Lemma init_from_tl:
    forall {A} n (f: nat -> A),
      tl (init_from n f) = init_from (S n) f.

  Lemma init_from_nth_tl:
    forall {A} n m (f: nat -> A),
      Str_nth_tl n (init_from m f) = init_from (n + m) f.

Typing of streams

  Definition wt_stream (sv : Stream svalue) (ty : type) : Prop :=
    SForall (fun v => wt_svalue v ty) sv.

  Definition wt_streams: list (Stream svalue) -> list type -> Prop :=
    Forall2 wt_stream.

  Fact wt_stream_enum : forall xs tx tn,
      wt_stream xs (Tenum tx tn) ->
      SForall (fun v => match v with
                     | present (Vscalar _) => False
                     | _ => True
                     end) xs.

Synchronous operators

  CoFixpoint const (b: Stream bool) (c: cconst): Stream svalue :=
    (if hd b then present (Vscalar (sem_cconst c)) else absent) ⋅ const (tl b) c.

  CoFixpoint enum (b: Stream bool) (c: enumtag): Stream svalue :=
    (if hd b then present (Venum c) else absent) ⋅ enum (tl b) c.

  CoInductive lift1 (op: unop) (ty: type)
    : Stream svalue -> Stream svalue -> 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 svalue -> Stream svalue -> Stream svalue -> Prop :=
  | Lift2A:
      forall xs ys rs,
        lift2 op ty1 ty2 xs ys rs ->
        lift2 op ty1 ty2 (absent ⋅ xs) (absent ⋅ ys) (absent ⋅ rs)
  | Lift2ScalarP:
      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 liftn (sem_extern : list cvalue -> cvalue -> Prop)
    : list (Stream svalue) -> Stream svalue -> Prop :=
  | LiftNA:
      forall xss ys,
        Forall (fun xs => hd xs = absent) xss ->
        liftn sem_extern (List.map (@tl _) xss) ys ->
        liftn sem_extern xss (absent ⋅ ys)
  | LiftNScalarP:
      forall xs xss y ys,
        Forall2 (fun xs x => hd xs = present (Vscalar x)) xss xs ->
        sem_extern xs y ->
        liftn sem_extern (List.map (@tl _) xss) ys ->
        liftn sem_extern xss (present (Vscalar y) ⋅ ys).

  CoInductive when (c: enumtag)
    : Stream svalue -> Stream svalue -> Stream svalue -> Prop :=
  | WhenA:
      forall xs cs rs,
        when c xs cs rs ->
        when c (absent ⋅ xs) (absent ⋅ cs) (absent ⋅ rs)
  | WhenPA:
      forall x c' xs cs rs,
        when c xs cs rs ->
        c <> c' ->
        when c (present x ⋅ xs) (present (Venum c') ⋅ cs) (absent ⋅ rs)
  | WhenPP:
      forall x xs cs rs,
        when c xs cs rs ->
        when c (present x ⋅ xs) (present (Venum c) ⋅ cs) (present x ⋅ rs).

  CoInductive merge
    : Stream svalue -> list (enumtag * Stream svalue) -> Stream svalue -> Prop :=
  | MergeA:
      forall xs ess rs,
        merge xs (List.map (fun '(i, es) => (i, tl es)) ess) rs ->
        Forall (fun es => hd (snd es) = absent) ess ->
        merge (absent ⋅ xs) ess (absent ⋅ rs)
  | MergeP:
      forall c xs ess rs v,
        merge xs (List.map (fun '(i, es) => (i, tl es)) ess) rs ->
        List.Exists (fun '(i, es) => i = c /\ hd es = present v) ess ->
        Forall (fun '(i, es) => i <> c -> hd es = absent) ess ->
        merge (present (Venum c) ⋅ xs) ess (present v ⋅ rs).

  CoInductive case
    : Stream svalue -> list (enumtag * Stream svalue) -> option (Stream svalue) -> Stream svalue -> Prop :=
  | CaseA:
      forall xs ess d rs,
        case xs (List.map (fun '(i, es) => (i, tl es)) ess) (option_map (@tl _) d) rs ->
        Forall (fun es => hd (snd es) = absent) ess ->
        LiftO True (fun d => hd d = absent) d ->
        case (absent ⋅ xs) ess d (absent ⋅ rs)
  | CaseP:
      forall c xs ess d rs v,
        case xs (List.map (fun '(i, es) => (i, tl es)) ess) (option_map (@tl _) d) rs ->
        Forall (fun es => hd (snd es) <> absent) ess ->
        LiftO True (fun d => hd d <> absent) d ->
        List.Exists (fun '(i, es) => i = c /\ hd es = present v) ess ->
        case (present (Venum c) ⋅ xs) ess d (present v ⋅ rs)
  | CasePDef:
      forall c xs ess d rs vd,
        case xs (List.map (fun '(i, es) => (i, tl es)) ess) (Some d) rs ->
        Forall (fun es => hd (snd es) <> absent) ess ->
        Forall (fun es => (fst es) <> c) ess ->
        case (present (Venum c) ⋅ xs) ess (Some (present vd ⋅ d)) (present vd ⋅ rs).

  Add Parametric Morphism op t : (lift1 op t)
      with signature @EqSt svalue ==> @EqSt svalue ==> Basics.impl
        as lift1_EqSt.

  Add Parametric Morphism op t1 t2 : (lift2 op t1 t2)
      with signature @EqSt svalue ==> @EqSt svalue ==> @EqSt svalue ==> Basics.impl
        as lift2_EqSt.

  Add Parametric Morphism : merge
      with signature @EqSt svalue ==> eq ==> @EqSt svalue ==> Basics.impl
        as merge_EqSt.

  Add Parametric Morphism : case
      with signature @EqSt svalue ==> eq ==> eq ==> @EqSt svalue ==> Basics.impl
        as case_EqSt.

  Add Parametric Morphism : case
      with signature eq ==> Forall2 (fun xs1 xs2 => eq (fst xs1) (fst xs2) /\ EqSt (snd xs1) (snd xs2)) ==> eq ==> eq ==> Basics.impl
        as case_EqStS.

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 (Vscalar (sem_cconst c)) else absent.

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

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

  Corollary const_nth' : forall bs c n,
      (const bs c) # n = if (bs # n) then present (Vscalar (sem_cconst c)) else 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' = Vscalar (sem_cconst 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 (Vscalar (sem_cconst c)) else absent) ⋅ (const bs c).

  Lemma enum_spec:
    forall xs c b,
      xs ≡ enum b c <->
      forall n, xs # n = if b # n then present (Venum c) else absent.

  Corollary enum_true: forall bs c n,
      bs # n = true ->
      (enum bs c) # n = present (Venum c).

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

  Corollary enum_nth' : forall bs c n,
      (enum bs c) # n = if (bs # n) then present (Venum c) else absent.

  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 c xs cs rs,
      when c xs cs rs <->
      (forall n,
          (xs # n = absent
           /\ cs # n = absent
           /\ rs # n = absent)
          \/
          (exists x c',
              xs # n = present x
              /\ cs # n = present (Venum c')
              /\ c <> c'
              /\ rs # n = absent)
          \/
          (exists x,
              xs # n = present x
              /\ cs # n = present (Venum c)
              /\ rs # n = present x)).

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

  Lemma lift2_spec:
    forall op ty1 ty2 xs ys zs,
      lift2 op ty1 ty2 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 ty1 y ty2 = Some z
              /\ zs # n = present z)).

  Lemma liftn_spec:
    forall sem_extern xss ys,
      liftn sem_extern xss ys <->
      (forall n,
          (Forall (fun xs => xs # n = absent) xss
           /\ ys # n = absent)
          \/
          (exists xs y,
             Forall2 (fun xs x => xs # n = present (Vscalar x)) xss xs
             /\ sem_extern xs y
             /\ ys # n = present (Vscalar y))).

  Add Parametric Morphism sem_extern : (liftn sem_extern)
      with signature @EqSts svalue ==> @EqSt svalue ==> Basics.impl
        as liftn_EqSt.

cexp level synchronous operators specifications

  Lemma merge_spec:
    forall xs ess rs,
      merge xs ess rs <->
      (forall n,
          (xs # n = absent
           /\ Forall (fun es => (snd es) # n = absent) ess
           /\ rs # n = absent)
          \/
          (exists c v,
              xs # n = present (Venum c)
              /\ List.Exists (fun '(i, es) => i = c /\ es # n = present v) ess
              /\ Forall (fun '(i, es) => i <> c -> es # n = absent) ess
              /\ rs # n = present v)).

  Lemma case_spec:
    forall xs ess d rs,
      case xs ess d rs <->
      (forall n,
          (xs # n = absent
           /\ Forall (fun es => (snd es) # n = absent) ess
           /\ LiftO True (fun d => d # n = absent) d
           /\ rs # n = absent)
          \/
          (exists c v,
              xs # n = present (Venum c)
              /\ Forall (fun es => (snd es) # n <> absent) ess
              /\ List.Exists (fun '(i, es) => i = c /\ es # n = present v) ess
              /\ LiftO True (fun d => d # n <> absent) d
              /\ rs # n = present v
          )
          \/
          (exists c v,
              xs # n = present (Venum c)
              /\ Forall (fun es => (snd es) # n <> absent) ess
              /\ Forall (fun es => (fst es) <> c) ess
              /\ LiftO False (fun d => d # n = present v) d
              /\ rs # n = present v)).

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

bools_of : extract boolean from an svalue stream

  CoInductive bools_of : Stream svalue -> Stream bool -> Prop :=
  | bools_of_T:
      forall vs bs,
        bools_of vs bs ->
        bools_of (present (Venum true_tag) ⋅ vs) (true ⋅ bs)
  | bools_of_F:
      forall vs bs,
        bools_of vs bs ->
        bools_of (present (Venum false_tag) ⋅ vs) (false ⋅ bs)
  | bools_of_A:
      forall vs bs,
        bools_of vs bs ->
        bools_of (absent ⋅ vs) (false ⋅ bs).

  Global Instance bools_of_Proper:
    Proper (@EqSt svalue ==> @EqSt bool ==> Basics.impl)
           bools_of.

  Corollary bools_of_det : forall xs ys ys',
      bools_of xs ys ->
      bools_of xs ys' ->
      ys ≡ ys'.

  Lemma bools_of_absent :
    bools_of (Streams.const absent) (Streams.const false).

  Lemma bools_of_nth : forall xs bs,
      bools_of xs bs <->
      (forall n, (xs # n = present (Venum true_tag) /\ bs # n = true) \/
            (xs # n = present (Venum false_tag) /\ bs # n = false) \/
            (xs # n = absent /\ bs # n = false)).

  CoFixpoint disj_str (rss : list (Stream bool)) : Stream bool :=
    (existsb (fun rs => hd rs) rss) ⋅ (disj_str (List.map (@tl _) rss)).

  Lemma disj_str_spec:
    forall n rss,
      (disj_str rss) # n = existsb (fun rs => rs # n) rss.

  Corollary disj_str_cons: forall r rs,
      disj_str (r::rs) ≡ disj_str [r;disj_str rs].

  Corollary disj_str_app : forall rs1 rs2,
      disj_str (rs1++rs2) ≡ disj_str [disj_str rs1;disj_str rs2].

  Definition bools_ofs (vs : list (Stream svalue)) (rs : Stream bool) :=
    exists rss, Forall2 bools_of vs rss /\
           rs ≡ disj_str rss.

  Lemma bools_ofs_empty :
    bools_ofs nil (Streams.const false).

  Lemma bools_ofs_absent {A} : forall (xs : list A),
      bools_ofs (List.map (fun _ => Streams.const absent) xs) (Streams.const false).

  Global Instance bools_ofs_Proper:
    Proper (@EqSts svalue ==> @EqSt bool ==> Basics.impl)
           bools_ofs.

  Lemma bools_ofs_det : forall xs r r',
      bools_ofs xs r ->
      bools_ofs xs r' ->
      r ≡ r'.

  Global Instance disj_str_SameElements_Proper:
    Proper (SameElements (@EqSt bool) ==> @EqSt bool) disj_str.

  Global Instance bools_ofs_SameElements_Proper:
    Proper (SameElements (@EqSt svalue) ==> eq ==> Basics.impl)
           bools_ofs.

fby stream

  CoFixpoint sfby (v : value) (str : Stream svalue) :=
    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 svalue ==> @EqSt svalue
    as sfby_EqSt.

Properties of history

  Section history.
    Context {K : Type}.

    Definition history := @FEnv.t K (Stream svalue).
    Definition history_tl (H: history) : history := FEnv.map (@tl svalue) H.

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

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

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

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

    Definition env := @FEnv.t K svalue.

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

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

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

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

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

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

    Open Scope fenv_scope.

    Fact history_tl_refines : forall H H',
        H ⊑ H' ->
        (history_tl H) ⊑ (history_tl H').

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

  End history.

  Global Hint Unfold history_tl : fenv.

sem_var This is common to Lustre and NLustre Semantics

  Section sem_var.
    Context {K : Type}.

    Inductive sem_var: history -> K -> Stream svalue -> Prop :=
      sem_var_intro:
        forall H x xs xs',
          H x = Some xs' ->
          xs ≡ xs' ->
          sem_var H x xs.

    Global Add Parametric Morphism : sem_var
        with signature FEnv.Equiv (@EqSt _) ==> @eq _ ==> @EqSt svalue ==> Basics.impl
          as sem_var_morph.

    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,
        H i = Some (v ⋅ s) -> (@history_tl K H) i = Some s.

    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_inv :
      forall H x s,
        sem_var (history_tl H) x s ->
        exists v, sem_var H x (v ⋅ 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 svalue) (H x) (H' x) ->
        sem_var H x v <-> sem_var H' x v.

    Open Scope fenv_scope.

    Lemma sem_var_union : forall Hi1 Hi2 x vs,
        sem_var (Hi1 + Hi2) x vs ->
        sem_var Hi1 x vs \/ sem_var Hi2 x vs.

    Lemma sem_var_union' : forall Hi1 Hi2 x vs,
        sem_var (Hi1 + Hi2) x vs ->
        (~FEnv.In x Hi2 /\ sem_var Hi1 x vs) \/ sem_var Hi2 x vs.

    Lemma sem_var_disj_union : forall Hi1 Hi2 x vs,
        (forall x, FEnv.In x Hi1 -> ~FEnv.In x Hi2) ->
        sem_var (Hi1 + Hi2) x vs <-> sem_var Hi1 x vs \/ sem_var Hi2 x vs.

    Context `{FEnv.fenv_key K}.

    Lemma sem_var_of_list : forall xs x vs,
        NoDupMembers xs ->
        In (x, vs) xs ->
        sem_var (FEnv.of_list xs) x vs.

    Lemma sem_var_of_list' : forall xs x vs,
        sem_var (FEnv.of_list xs) x vs ->
        exists vs', vs ≡ vs' /\ In (x, vs') xs.

    Lemma sem_var_union2 : forall Hi1 Hi2 x vs,
        sem_var Hi1 x vs ->
        ~FEnv.In x Hi2 ->
        sem_var (Hi1 + Hi2) x vs.

    Lemma sem_var_union3' : forall Hi1 Hi2 x vs,
        sem_var Hi2 x vs ->
        sem_var (Hi1 + Hi2) x vs.

  End sem_var.

clocks_of and its properties

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

  Lemma clocks_of_EqStN : forall n xs1 xs2,
      Forall2 (EqStN n) xs1 xs2 ->
      EqStN n (clocks_of xs1) (clocks_of xs2).

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

abstract_clock and some properties

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

  Add Parametric Morphism {A} : (@abstract_clock A)
      with signature @EqSt _ ==> @EqSt bool
        as ac_EqSt.

  Lemma ac_Cons {A} : forall x xs,
      @abstract_clock A (x ⋅ xs) ≡
      (match x with absent => false | _ => true end) ⋅ (abstract_clock xs).

  Lemma ac_tl {A} :
    forall s, @abstract_clock A (Streams.tl s) ≡ Streams.tl (abstract_clock s).

  Lemma ac_nth {A} : forall xs n,
      (@abstract_clock A xs) # n = (match xs # n with absent => false | _ => true end).

sem_clock and its properties

  CoInductive enums_of (e : enumtag) : Stream svalue -> Stream bool -> Prop :=
  | enums_of_abs : forall xs ys,
      enums_of e xs ys ->
      enums_of e (absent ⋅ xs) (false ⋅ ys)
  | enums_of_eq : forall xs ys,
      enums_of e xs ys ->
      enums_of e (present (Venum e) ⋅ xs) (true ⋅ ys)
  | enums_of_neq : forall e' xs ys,
      enums_of e xs ys ->
      e' <> e ->
      enums_of e (present (Venum e') ⋅ xs) (false ⋅ ys).

  Lemma enums_of_nth e : forall xs bs,
      enums_of e xs bs
      <-> (forall n, (xs # n = absent /\ bs # n = false)
              \/ (xs # n = present (Venum e) /\ bs # n = true)
              \/ (exists e', xs # n = present (Venum e') /\ e' <> e /\ bs # n = false)).

  Inductive 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 bs ck x t k xs bs',
        sem_clock H b ck bs ->
        sem_var H x xs ->
        abstract_clock xs ≡ bs ->
        enums_of k xs bs' ->
        sem_clock H b (Con ck x (t, k)) bs'.

  Add Parametric Morphism e : (enums_of e)
      with signature @EqSt _ ==> @EqSt _ ==> Basics.impl
        as enums_of_EqSt.

  Lemma enums_of_detn e n : forall xs1 xs2 bs1 bs2,
      EqStN n xs1 xs2 ->
      enums_of e xs1 bs1 ->
      enums_of e xs2 bs2 ->
      EqStN n bs1 bs2.

  Add Parametric Morphism : sem_clock
      with signature FEnv.Equiv (@EqSt _) ==> @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.

  Lemma enums_of_det e : forall xs bs1 bs2,
      enums_of e xs bs1 ->
      enums_of e xs bs2 ->
      bs1 ≡ bs2.

  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.

sub_clock

  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 {A} : Stream (synchronous A) -> 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).

  Global Instance aligned_Proper {A} :
    Proper (@EqSt (synchronous A) ==> @EqSt bool ==> iff)
           aligned.

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

  Lemma aligned_EqSt {A} : forall (vs: Stream (synchronous A)) bs1 bs2,
      aligned vs bs1 ->
      aligned vs bs2 ->
      bs1 ≡ bs2.

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

  Lemma enum_aligned : forall bs c,
      aligned (enum bs c) bs.

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

  Lemma ac_merge :
    forall cs xs rs,
      merge cs xs rs -> abstract_clock cs ≡ abstract_clock rs.

  Lemma ac_const:
    forall c b,
      abstract_clock (const b c) ≡ b.

  Lemma ac_enum:
    forall b k,
      abstract_clock (enum b k) ≡ b.

  Lemma ac_case:
    forall cs vs d ss,
      case cs vs d ss ->
      abstract_clock cs ≡ abstract_clock ss.

  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_liftn :
    forall f ss vs,
      liftn f ss vs ->
      Forall (fun ss => abstract_clock ss ≡ abstract_clock vs) ss.

  Lemma ac_aligned {A} :
    forall (s: Stream (synchronous A)), 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 {A} :
    @abstract_clock A (Streams.const absent) ≡ Streams.const false.

count and mask

  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))).

  Corollary count_S_nth':
    forall n s rs,
      (count_acc (S s) rs) # n =
      S ((count_acc s rs) # n).

  Lemma count_0: forall n r,
      (forall m, m <= n -> r # m = false) <->
      (count r) # n = 0.

  Lemma count_not_0: forall n r,
      (exists m, m <= n /\ r # m = true) ->
      (count r) # n > 0.

  Add Parametric Morphism n : count
      with signature @EqStN _ n ==> @EqStN _ n
        as count_EqStN.

  Add Parametric Morphism : count
      with signature @EqSt _ ==> @EqSt _
        as count_EqSt.

  Lemma count_increasing : forall n1 n2 r,
      n1 <= n2 ->
      (count r) # n1 <= (count r) # n2.

  Corollary count_0_inv : forall n r,
      (count r) # n = 0 ->
      r # 0 = false.

  Fact count_disj_le2 : forall n r1 r2,
      (count r2) # n <= (count (disj_str [r1;r2])) # n.

  Lemma count_shift : forall n1 n2 r,
      n1 < n2 ->
      (count r) # n2 = ((count r) # n1 + (count (Str_nth_tl (S n1) r)) # (n2 - S n1))%nat.

  Lemma count_eq_false : forall n1 n2 r,
      n1 < n2 ->
      (count r) # n1 = (count r) # n2 <->
      (forall k, n1 < k -> k <= n2 -> r # k = false).

  Lemma count_between : forall r n1 n2,
      n1 <= n2 ->
      (count r) # n1 = (count r) # n2 ->
      (forall k, n1 <= k -> k <= n2 -> (count r) # k = (count r) # n1).

mask and friends

  CoFixpoint mask' {A : Type} (absent: A) (k k': nat) (rs: Stream bool) (xs: Stream A) : Stream A :=
    let mask' k' := mask' absent k k' (tl rs) (tl xs) in
    match hd rs with
    | false => (if k' =? k then hd xs else absent) ⋅ mask' k'
    | true => (if S k' =? k then hd xs else absent) ⋅ mask' (S k')
    end.
  Definition mask {A : Type} (absent: A) k rs xs :=
    mask' absent k 0 rs xs.

  Definition maskv k rs := @mask svalue absent k rs.

  Definition mask_hist {K} k rs := @FEnv.map K _ _ (maskv k rs).
  Global Hint Unfold mask_hist : fenv.

  Definition maskb := mask false.

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

  Corollary maskv_nth:
    forall n k rs xs,
      (maskv k rs xs) # n = if (count rs) # n =? k then xs # n else absent.

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

  Lemma mask'_Cons {A} (absent: A) :
    forall k r rs x xs k',
      (mask' absent k k' (r ⋅ rs) (x ⋅ xs))
      = (match r with
         | false => (if k' =? k then x else absent) ⋅ mask' absent k k' rs xs
         | true => (if S k' =? k then x else absent) ⋅ mask' absent k (S k') rs xs
         end).

  Lemma mask'_S {A} (absent: A) : forall k k' rs xs,
      mask' absent (S k) (S k') rs xs ≡ mask' absent k k' rs xs.

  Lemma EqSt_unmask {A} (absent: A) : forall b x y,
    (forall (k : nat), mask absent k b x ≡ mask absent k b y) ->
    x ≡ y.

  Lemma mask_false_0 {A} (absent: A) : forall xs,
      mask absent 0 (Streams.const false) xs ≡ xs.

  Corollary masks_false_0 {A} (absent: A) : forall xs,
      EqSts (List.map (mask absent 0 (Streams.const false)) xs) xs.

  Corollary maskb_false_0 : forall bs,
      maskb 0 (Streams.const false) bs ≡ bs.

  Lemma mask_false_S {A} (absent: A) : forall n xs,
      mask absent (S n) (Streams.const false) xs ≡ Streams.const absent.

  Corollary masks_false_S {A} (absent: A) : forall n xs,
      EqSts (List.map (mask absent (S n) (Streams.const false)) xs) (List.map (fun _ => Streams.const absent) xs).

  Corollary maskb_false_S : forall n bs,
      maskb (S n) (Streams.const false) bs ≡ Streams.const false.

  Lemma mask_hist_false_0 {K} : forall H,
      @FEnv.Equiv K _ (@EqSt _) (mask_hist 0 (Streams.const false) H) H.

  Lemma mask_hist_false_S {K} : forall n H,
      @FEnv.Equiv K _ (@EqSt _) (mask_hist (S n) (Streams.const false) H) (FEnv.map (fun _ => Streams.const absent) H).

  Lemma consolidate_mask {A} (absent: A) : forall P r,
      (Proper (eq ==> (@EqSt _) ==> Basics.impl) P) ->
      (forall k, exists v, P k (mask absent k r v)) ->
      exists v, forall k, P k (mask absent k r v).

  Lemma consolidate_mask_hist {K} : forall P r d,
      (Proper (eq ==> (FEnv.Equiv (@EqSt _)) ==> Basics.impl) P) ->
      (forall k H, P k H -> @FEnv.dom K _ H d) ->
      (forall k, exists H, P k (mask_hist k r H)) ->
      exists H, forall k, P k (mask_hist k r H).

  Add Parametric Morphism {A} (absent: A) k : (mask absent k)
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _
        as mask_morph.

  Add Parametric Morphism k : (maskv k)
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _
        as maskv_morph.

  Add Parametric Morphism {K} k : (@mask_hist K k)
      with signature @EqSt _ ==> FEnv.Equiv (@EqSt _) ==> FEnv.Equiv (@EqSt _)
        as mask_hist_morph.

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

  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.

  Lemma mask_absent {A} (absent: A) : forall k rs,
      mask absent k rs (Streams.const absent) ≡ Streams.const absent.

  Corollary mask_hist_absent {K} : forall k rs (H: @FEnv.t K (Stream svalue)),
      FEnv.Equiv (@EqSt _) (mask_hist k rs (FEnv.map (fun _ => Streams.const absent) H))
                 (FEnv.map (fun _ => Streams.const absent) H).

  Corollary mask_hist_absent' {K} : forall k rs (H: @FEnv.t K (Stream svalue)),
      FEnv.Equiv (@EqSt _) (FEnv.map (fun _ => Streams.const (@absent value)) (mask_hist k rs H))
                 (FEnv.map (fun _ => Streams.const absent) H).

  Corollary maskb_absent: forall k rs,
      maskb k rs (Streams.const false) ≡ Streams.const false.

  Open Scope fenv_scope.

  Lemma refines_mask {K} : forall r (H H' : @history K) k,
      H ⊑ H' ->
      (mask_hist k r H) ⊑ (mask_hist k r H').

  Lemma refines_unmask {K} : forall r (H H' : @history K),
      (forall k, (mask_hist k r H) ⊑ (mask_hist k r H')) ->
      H ⊑ H'.


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

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

  Lemma bools_of_mask : forall rs xs bs,
      (forall k, bools_of (maskv k rs xs) (maskb k rs bs)) <->
      bools_of xs bs.

  Lemma bools_of_mask_inv : forall rs k xs bs,
      bools_of (maskv k rs xs) bs ->
      exists bs', bs ≡ maskb k rs bs'.

  Lemma bools_of_mask_det : forall xs rs k bs1 bs2,
      bools_of xs bs1 ->
      bools_of (maskv k rs xs) bs2 ->
      bs2 ≡ maskb k rs bs1.

  Lemma sem_var_mask {K}: forall k r (H : @history K) x v,
      sem_var H x v ->
      sem_var (mask_hist k r H) x (maskv k r v).

  Lemma sem_var_mask_inv {K} : forall k r (H : @history K) x v,
      sem_var (mask_hist k r H) x v ->
      exists v', sem_var H x v' /\ v ≡ (maskv k r v').

Caracterizing a stream that is slower than a clock stream

  CoInductive slower {A} : Stream (synchronous A) -> Stream bool -> Prop :=
  | slowerF : forall vs bs,
      slower vs bs ->
      slower (absent ⋅ vs) (false ⋅ bs)
  | slowerT : forall v vs bs,
      slower vs bs ->
      slower (v ⋅ vs) (true ⋅ bs).

  Definition slower_hist {K} (H : @history K) bs :=
    forall x vs, H x = Some vs -> slower vs bs.


  Lemma slower_nth {A} : forall bs vs,
      @slower A vs bs <->
      (forall n, bs # n = false -> vs # n = absent).

  Add Parametric Morphism {A} : (@slower A)
      with signature @EqSt _ ==> @EqSt _ ==> Basics.impl
        as slower_morph.


  Lemma aligned_slower {A} : forall bs (vs: Stream (synchronous A)),
      aligned vs bs ->
      slower vs bs.

  Lemma sc_slower : forall H bs ck bs' (vs: Stream (synchronous value)),
      sem_clock H bs ck bs' ->
      aligned vs bs' ->
      slower vs bs.

  Lemma slower_mask : forall vs bs k r,
      slower vs (maskb k r bs) ->
      vs ≡ maskv k r vs.

  Corollary slower_mask_hist {K} : forall (H : @history K) bs k r,
      slower_hist H (maskb k r bs) ->
      FEnv.Equiv (@EqSt _) H (mask_hist k r H).

  Lemma ac_slower {A} : forall vs,
      @slower A vs (abstract_clock vs).

  Global Hint Resolve ac_slower : coindstreams.

  Lemma slower_ac_morph {A B} : forall (vs1 : Stream (synchronous A)) (vs2 : Stream (synchronous B)) bs,
      abstract_clock vs1 ≡ abstract_clock vs2 ->
      slower vs1 bs ->
      slower vs2 bs.

when relation

  Definition when_hist {K} (sel : enumtag) (Hi : @history K) (es : Stream svalue) (Hi' : history) :=
    FEnv.refines (fun vs' vs => when sel vs es vs') Hi' Hi.

  Add Parametric Morphism sel : (when sel)
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _ ==> Basics.impl
        as when_EqSt.

  Add Parametric Morphism {K} sel : (@when_hist K sel)
      with signature FEnv.Equiv (@EqSt _) ==> @EqSt _ ==> FEnv.Equiv (@EqSt _) ==> Basics.impl
        as when_hist_EqSt.


  CoFixpoint fwhen {A} (abs : A) (sel : enumtag) (vs : Stream A) (es : Stream svalue) : Stream A :=
    (if hd es ==b present (Venum sel) then hd vs else abs) ⋅ (fwhen abs sel (tl vs) (tl es)).

  Definition fwhenv sel vs es := fwhen (@absent value) sel vs es.
  Definition fwhen_hist {K} sel H es := @FEnv.map K _ _ (fun vs => fwhenv sel vs es) H.
  Definition fwhenb := fwhen false.

  Global Hint Unfold fwhen_hist : fenv.

  Lemma fwhen_nth {A} (abs : A) :
    forall n sel es xs,
      (fwhen abs sel xs es) # n = if es # n ==b present (Venum sel) then xs # n else abs.

  Corollary fwhenv_nth:
    forall n e es xs,
      (fwhenv e xs es) # n = if es # n ==b present (Venum e) then xs # n else absent.

  Corollary fwhenb_nth:
    forall n e es xs,
      (fwhenb e xs es) # n = if es # n ==b present (Venum e) then xs # n else false.

  Lemma fwhen_Cons {A} (abs : A) :
    forall sel e es x xs,
      (fwhen abs sel (x ⋅ xs) (e ⋅ es))
        = (if e ==b present (Venum sel) then x else abs) ⋅ (fwhen abs sel xs es).

  Lemma when_fwhen sel : forall es vs vs',
      when sel vs es vs' ->
      vs' ≡ fwhenv sel vs es.

  Lemma fwhenv_whenv sel : forall es vs,
      SForall (fun v => match v with present (Venum _) | absent => True | _ => False end) es ->
      abstract_clock vs ≡ abstract_clock es ->
      when sel vs es (fwhenv sel vs es).

  Lemma when_hist_fwhen_hist {K} sel es : forall (Hi Hi' : @history K),
      when_hist sel Hi es Hi' ->
      Hi' ⊑ (fwhen_hist sel Hi es).

  Lemma when_hist_restrict_ac {K} `{FEnv.fenv_key K} sel es : forall (Hi : @history K) xs,
      SForall (fun v => match v with present (Venum _) | absent => True | _ => False end) es ->
      (forall x vs, List.In x xs -> sem_var Hi x vs -> abstract_clock vs ≡ abstract_clock es) ->
      when_hist sel Hi es (FEnv.restrict (fwhen_hist sel Hi es) xs).

  Add Parametric Morphism {A} (absent: A) k : (fwhen absent k)
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _
        as fwhen_EqSt.

  Add Parametric Morphism k : (fwhenv k)
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _
        as fwhenv_morph.

  Add Parametric Morphism {K} k : (@fwhen_hist K k)
      with signature FEnv.Equiv (@EqSt _) ==> @EqSt _ ==> FEnv.Equiv (@EqSt _)
        as fwhen_hist_EqSt.

  Add Parametric Morphism k : (fwhenb k)
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _
        as fwhenb_EqSt.

  Lemma ac_fwhen : forall k sc xs,
      abstract_clock (fwhenv k xs sc) ≡ fwhenb k (abstract_clock xs) sc.

  Lemma sem_var_fwhen {K} : forall k r (H: @history K) x v,
      sem_var H x v ->
      sem_var (fwhen_hist k H r) x (fwhenv k v r).

  Lemma sem_var_when {K} x : forall sel sc (Hi Hi': @history K) vs,
      when_hist sel Hi sc Hi' ->
      sem_var Hi x vs ->
      FEnv.In x Hi' ->
      when sel vs sc (fwhenv sel vs sc).

  Lemma sem_var_when_inv {K} : forall k r (Hi Hi' : @history K) x v,
      when_hist k Hi r Hi' ->
      sem_var Hi' x v ->
      exists v', sem_var Hi x v' /\ when k v' r v.

  Lemma sem_var_fwhen_inv {K} : forall k sc (H: @history K) x v,
      sem_var (fwhen_hist k H sc) x v ->
      exists v', sem_var H x v' /\ v ≡ (fwhenv k v' sc).

  Lemma refines_fwhen {K} : forall e sc (H H': @history K),
      H ⊑ H' ->
      (fwhen_hist e H sc) ⊑ (fwhen_hist e H' sc).

  Lemma when_absent e :
    when e (Streams.const absent) (Streams.const absent) (Streams.const absent).

  Corollary when_hist_absent {K} e sc : forall (Hi Hi': @history K),
    when_hist e Hi sc Hi' ->
    when_hist e (FEnv.map (fun _ => Streams.const absent) Hi) (Streams.const absent) (FEnv.map (fun _ => Streams.const absent) Hi').

  Lemma fwhen_absent {A} (absent: A) : forall k sc,
      fwhen absent k (Streams.const absent) sc ≡ Streams.const absent.

  Corollary fwhen_hist_absent {K}: forall k sc (H: @history K),
      FEnv.Equiv (@EqSt _) (fwhen_hist k (FEnv.map (fun _ => Streams.const absent) H) sc)
                 (FEnv.map (fun _ => Streams.const absent) H).

  Corollary fwhen_hist_absent' {K} : forall k sc (H: @history K),
      FEnv.Equiv (@EqSt _) (FEnv.map (fun _ => Streams.const (@absent value)) (fwhen_hist k H sc))
                 (FEnv.map (fun _ => Streams.const absent) H).

  Corollary fwhenb_absent: forall k sc,
      fwhenb k (Streams.const false) sc ≡ Streams.const false.

  Lemma fwhenb_both_slower : forall k sc bs bs',
      slower sc bs ->
      slower sc bs' ->
      fwhenb k bs sc ≡ fwhenb k bs' sc.

select and fselect, combining when and mask

  Definition stres_st (stres : Stream (synchronous (enumtag * bool))) :=
    Streams.map (fun v => match v with present (e, _) => present (Venum e) | absent => absent end) stres.
  Definition stres_res (stres : Stream (synchronous (enumtag * bool))) :=
    Streams.map (fun v => match v with present (_, b) => b | absent => false end) stres.

  CoInductive select' (sel : enumtag) (k : nat) : nat -> Stream (synchronous (enumtag * bool)) -> Stream svalue -> Stream svalue -> Prop :=
  | select_abs : forall k' stres xs ys,
      select' sel k k' stres xs ys ->
      select' sel k k' (absent ⋅ stres) (absent ⋅ xs) (absent ⋅ ys)
  | select_nsel : forall k' v r stres x xs ys,
      select' sel k k' stres xs ys ->
      v <> sel ->
      select' sel k k' (present (v, r) ⋅ stres) (present x ⋅ xs) (absent ⋅ ys)
  | select_nreset : forall k' stres x xs ys,
      select' sel k k' stres xs ys ->
      select' sel k k' (present (sel, false) ⋅ stres) (present x ⋅ xs) ((if k' =? k then present x else absent) ⋅ ys)
  | select_reset : forall k' stres x xs ys,
      select' sel k (S k') stres xs ys ->
      select' sel k k' (present (sel, true) ⋅ stres) (present x ⋅ xs) ((if S k' =? k then present x else absent) ⋅ ys).
  Definition select sel k := select' sel k 0.

  Definition select_hist {K} sel k stres (Hi Hi': @history K) :=
    FEnv.refines (fun vs' vs => select sel k stres vs vs') Hi' Hi.

  Definition fselect {A} (absent : A) (e : enumtag) (k : nat) (stres : Stream (synchronous (enumtag * bool))) (xs : Stream A) :=
    mask absent k
         (fwhenb e (stres_res stres) (stres_st stres))
         (fwhen absent e xs (stres_st stres)).

  Definition fselectb := fselect false.
  Definition fselectv e k stres xs := fselect (@absent value) e k stres xs.
  Definition fselect_hist {K} e k stres H := @FEnv.map K _ _ (fselectv e k stres) H.
  Global Hint Unfold fselect_hist : fenv.

  Add Parametric Morphism : stres_st
      with signature @EqSt _ ==> @EqSt _
        as stres_st_EqSt.

  Add Parametric Morphism : stres_res
      with signature @EqSt _ ==> @EqSt _
        as stres_res_EqSt.

  Lemma select_mask_when sel k : forall stres xs zs,
      select sel k stres xs zs
      <-> exists ys, when sel xs (stres_st stres) ys
              /\ zs ≡ maskv k (fwhenb sel (stres_res stres) (stres_st stres)) ys.

  Add Parametric Morphism e k : (select e k)
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _ ==> Basics.impl
        as select_EqSt.

  Add Parametric Morphism {K} sel k : (@select_hist K sel k)
      with signature @EqSt _ ==> FEnv.Equiv (@EqSt _) ==> FEnv.Equiv (@EqSt _) ==> Basics.impl
        as select_hist_EqSt.

  Add Parametric Morphism {A} (abs : A) e k : (fselect abs e k)
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _
        as fselect_EqSt.

  Add Parametric Morphism e k : (fselectb e k)
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _
        as fselectb_EqSt.

  Add Parametric Morphism e k : (fselectv e k)
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _
        as fselectv_morph.

  Add Parametric Morphism {K} e k : (@fselect_hist K e k)
      with signature @EqSt _ ==> FEnv.Equiv (@EqSt _) ==> FEnv.Equiv (@EqSt _)
        as fselect_hist_EqSt.

  Lemma ac_fselect : forall e k sc xs,
      abstract_clock (fselectv e k sc xs) ≡ fselectb e k sc (abstract_clock xs).

  Lemma select_fselect sel k : forall es vs vs',
      select sel k es vs vs' ->
      vs' ≡ fselectv sel k es vs.

  Lemma sem_var_fselect {K} : forall e k r (H: @history K) x v,
      sem_var H x v ->
      sem_var (fselect_hist e k r H) x (fselectv e k r v).

  Lemma sem_var_select {K} x : forall sel k sc (Hi Hi': @history K) vs,
      select_hist sel k sc Hi Hi' ->
      sem_var Hi x vs ->
      FEnv.In x Hi' ->
      select sel k sc vs (fselectv sel k sc vs).

  Lemma sem_var_select_inv {K} : forall sel k r (Hi Hi': @history K) x v,
      select_hist sel k r Hi Hi' ->
      sem_var Hi' x v ->
      exists v', sem_var Hi x v' /\ select sel k r v' v.

  Lemma sem_var_fselect_inv {K}: forall sel k r (H: @history K) x v,
      sem_var (fselect_hist sel k r H) x v ->
      exists v', sem_var H x v' /\ v ≡ (fselectv sel k r v').

  Lemma fselectv_selectv sel k : forall es vs,
      abstract_clock vs ≡ abstract_clock es ->
      select sel k es vs (fselectv sel k es vs).

  Lemma select_hist_fselect_hist {K} sel k es : forall (Hi Hi': @history K),
      select_hist sel k es Hi Hi' ->
      Hi' ⊑ (fselect_hist sel k es Hi).

  Lemma select_hist_restrict_ac sel k es : forall Hi xs,
      (forall x vs, List.In x xs -> sem_var Hi x vs -> abstract_clock vs ≡ abstract_clock es) ->
      select_hist sel k es Hi (FEnv.restrict (fselect_hist sel k es Hi) xs).

  Fact stres_st_ac : forall stres,
      abstract_clock (stres_st stres) ≡ abstract_clock stres.

  Lemma ac_select :
    forall e k cs xs rs,
      select e k cs xs rs -> abstract_clock cs ≡ abstract_clock xs.

  Fact stres_st_absent : stres_st (Streams.const absent) ≡ Streams.const absent.

  Fact stres_res_absent : stres_res (Streams.const absent) ≡ Streams.const false.

  Lemma select_absent e k :
    select e k (Streams.const absent) (Streams.const absent) (Streams.const absent).

  Corollary select_hist_absent {K} e k sc : forall (Hi Hi': @history K),
    select_hist e k sc Hi Hi' ->
    select_hist e k (Streams.const absent)
                (FEnv.map (fun _ => Streams.const absent) Hi) (FEnv.map (fun _ => Streams.const absent) Hi').

  Lemma fselect_absent {A} (absent: A) : forall e k sc,
      fselect absent e k sc (Streams.const absent) ≡ Streams.const absent.

  Corollary fselect_hist_absent {K} : forall e k sc (H: @history K),
      FEnv.Equiv (@EqSt _) (fselect_hist e k sc (FEnv.map (fun _ => Streams.const absent) H))
                (FEnv.map (fun _ => Streams.const absent) H).

  Corollary fselect_hist_absent' {K} : forall e k sc (H: @history K),
      FEnv.Equiv (@EqSt _) (FEnv.map (fun _ => Streams.const (@absent value)) (fselect_hist e k sc H))
                (FEnv.map (fun _ => Streams.const absent) H).
    intros * x. simpl_fenv.
    destruct (H x); constructor.
    reflexivity.
  Qed.