From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.

From Coq Require Import Streams.
From Coq Require Import Sorting.Permutation.
From Coq Require Import Setoid.
From Coq Require Import Morphisms.

From Coq Require Import FSets.FMapPositive.
From Velus Require Import Common.
From Velus Require Import CommonProgram.
From Velus Require Import CommonList.
From Velus Require Import FunctionalEnvironment.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax.
From Velus Require Import Lustre.LOrdered.
From Velus Require Import CoindStreams.

Lustre semantics

Module Type LSEMANTICS
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import Senv : STATICENV Ids Op OpAux Cks)
       (Import Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Import Lord : LORDERED Ids Op OpAux Cks Senv Syn)
       (Import Str : COINDSTREAMS Ids Op OpAux Cks).

  CoInductive fby1 {A : Type} : A -> Stream (synchronous A) -> Stream (synchronous A) -> Stream (synchronous A) -> Prop :=
  | Fby1A:
      forall v xs ys rs,
        fby1 v xs ys rs ->
        fby1 v (absent ⋅ xs) (absent ⋅ ys) (absent ⋅ rs)
  | Fby1P:
      forall v w s xs ys rs,
        fby1 s xs ys rs ->
        fby1 v (present w ⋅ xs) (present s ⋅ ys) (present v ⋅ rs).

  CoInductive fby {A : Type} : Stream (synchronous A) -> Stream (synchronous A) -> Stream (synchronous A) -> Prop :=
  | FbyA:
      forall xs ys rs,
        fby xs ys rs ->
        fby (absent ⋅ xs) (absent ⋅ ys) (absent ⋅ rs)
  | FbyP:
      forall x y xs ys rs,
        fby1 y xs ys rs ->
        fby (present x ⋅ xs) (present y ⋅ ys) (present x ⋅ rs).

  CoInductive arrow1: Stream svalue -> Stream svalue -> Stream svalue -> Prop :=
  | Arrow1A: forall xs ys rs,
      arrow1 xs ys rs ->
      arrow1 (absent ⋅ xs) (absent ⋅ ys) (absent ⋅ rs)
  | Arrow1P: forall x y xs ys rs,
      arrow1 xs ys rs ->
      arrow1 (present x ⋅ xs) (present y ⋅ ys) (present y ⋅ rs).

  CoInductive arrow: Stream svalue -> Stream svalue -> Stream svalue -> Prop :=
  | ArrowA: forall xs ys rs,
      arrow xs ys rs ->
      arrow (absent ⋅ xs) (absent ⋅ ys) (absent ⋅ rs)
  | ArrowP: forall x y xs ys rs,
      arrow1 xs ys rs ->
      arrow (present x ⋅ xs) (present y ⋅ ys) (present x ⋅ rs).

  Inductive lustre_var := Var (x : ident) | Last (x : ident).

  Global Program Instance var_eq_dec : EqDec lustre_var eq.

  Global Program Instance var_fenv_key : FEnv.fenv_key lustre_var.

  Definition history : Type := @history lustre_var.
  Definition var_history (H : history) : @Str.history ident :=
    fun x => H (Var x).

  Section NodeSemantics.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.
    Variable G : @global PSyn prefs.

    Section Forall2Brs.
      Variable P : exp -> list (Stream svalue) -> Prop.

      Inductive Forall2Brs : list (enumtag * list exp) -> list (list (enumtag * Stream svalue)) -> Prop :=
      | F2Tnil : forall vs,
          Forall (fun vs => vs = []) vs ->
          Forall2Brs [] vs
      | F2Tcons : forall c es brs vs1 vs2 vs3,
          Forall2 P es vs1 ->
          Forall2Brs brs vs2 ->
          Forall3 (fun v1 vs2 vs3 => vs3 = (c, v1)::vs2) (concat vs1) vs2 vs3 ->
          Forall2Brs ((c, es)::brs) vs3.

    End Forall2Brs.

    Definition dom (H : history) Γ :=
      (forall x, FEnv.In (Var x) H <-> IsVar Γ x) /\ (forall x, FEnv.In (Last x) H <-> IsLast Γ x).

    Definition dom_ub (H : history) Γ :=
      (forall x, FEnv.In (Var x) H -> IsVar Γ x) /\ (forall x, FEnv.In (Last x) H -> IsLast Γ x).

    Definition dom_lb (H : history) Γ :=
      (forall x, IsVar Γ x -> FEnv.In (Var x) H) /\ (forall x, IsLast Γ x -> FEnv.In (Last x) H).

    Section sem_scope.
      Context {A : Type}.

      Variable sem_exp : history -> Stream bool -> exp -> list (Stream svalue) -> Prop.

      Inductive sem_last_decl (Hi Hi' : history) (bs : Stream bool) : (ident * (type * clock * ident * option (exp * ident))) -> Prop :=
      | sem_nolast : forall x ty ck cx,
          sem_last_decl Hi Hi' bs (x, (ty, ck, cx, None))
      | sem_last : forall x ty ck cx e0 clx vs0 vs1 vs,
          sem_exp (Hi + Hi') bs e0 [vs0] ->
          sem_var Hi' (Var x) vs1 ->
          fby vs0 vs1 vs ->
          sem_var Hi' (Last x) vs ->
          sem_last_decl Hi Hi' bs (x, (ty, ck, cx, Some (e0, clx))).

      Variable sem_block : history -> A -> Prop.

      Inductive sem_scope : history -> Stream bool -> (scope A) -> Prop :=
      | Sscope : forall Hi Hi' bs locs blks,
          dom Hi' (senv_of_decls locs) ->

          Forall (sem_last_decl Hi Hi' bs) locs ->

          sem_block (Hi + Hi') blks ->
          sem_scope Hi bs (Scope locs blks).
    End sem_scope.

    Section sem_branch.
      Context {A : Type}.

      Variable sem_block : A -> Prop.

      Variable must_def : ident -> Prop.
      Variable is_def : ident -> A -> Prop.

      Inductive sem_branch : history -> (branch A) -> Prop :=
      | Sbranch : forall Hi caus blks,
          sem_block blks ->
          (forall x, must_def x -> ~is_def x blks -> exists vs, sem_var Hi (Last x) vs /\ sem_var Hi (Var x) vs) ->
          sem_branch Hi (Branch caus blks).
    End sem_branch.

    Inductive sem_exp
      : history -> Stream bool -> exp -> list (Stream svalue) -> Prop :=
    | Sconst:
      forall H b c cs,
        cs ≡ const b c ->
        sem_exp H b (Econst c) [cs]

    | Senum:
      forall H b k ty es,
        es ≡ enum b k ->
        sem_exp H b (Eenum k ty) [es]

    | Svar:
      forall H b x s ann,
        sem_var H (Var x) s ->
        sem_exp H b (Evar x ann) [s]

    | Slast:
      forall H b x s ann,
        sem_var H (Last x) s ->
        sem_exp H b (Elast x ann) [s]

    | Sunop:
      forall H b e op ty s o ann,
        sem_exp H b e [s] ->
        typeof e = [ty] ->
        lift1 op ty s o ->
        sem_exp H b (Eunop op e ann) [o]

    | Sbinop:
      forall H b e1 e2 op ty1 ty2 s1 s2 o ann,
        sem_exp H b e1 [s1] ->
        sem_exp H b e2 [s2] ->
        typeof e1 = [ty1] ->
        typeof e2 = [ty2] ->
        lift2 op ty1 ty2 s1 s2 o ->
        sem_exp H b (Ebinop op e1 e2 ann) [o]

    | Sextcall:
      forall H b f es tyout ck tyins ss vs,
        Forall2 (fun ty cty => ty = Tprimitive cty) (typesof es) tyins ->
        Forall2 (sem_exp H b) es ss ->
        liftn (fun ss => sem_extern f tyins ss tyout) (concat ss) vs ->
        sem_exp H b (Eextcall f es (tyout, ck)) [vs]

    | Sfby:
      forall H b e0s es anns s0ss sss os,
        Forall2 (sem_exp H b) e0s s0ss ->
        Forall2 (sem_exp H b) es sss ->
        Forall3 fby (concat s0ss) (concat sss) os ->
        sem_exp H b (Efby e0s es anns) os

    | Sarrow:
      forall H b e0s es anns s0ss sss os,
        Forall2 (sem_exp H b) e0s s0ss ->
        Forall2 (sem_exp H b) es sss ->
        Forall3 arrow (concat s0ss) (concat sss) os ->
        sem_exp H b (Earrow e0s es anns) os

    | Swhen:
      forall H b x tx s k es lann ss os,
        Forall2 (sem_exp H b) es ss ->
        sem_var H (Var x) s ->
        Forall2 (fun s' => when k s' s) (concat ss) os ->
        sem_exp H b (Ewhen es (x, tx) k lann) os

    | Smerge:
      forall H b x tx s es lann vs os,
        sem_var H (Var x) s ->
        Forall2Brs (sem_exp H b) es vs ->
        Forall2 (merge s) vs os ->
        sem_exp H b (Emerge (x, tx) es lann) os

    | ScaseTotal:
      forall H b e s es tys ck vs os,
        sem_exp H b e [s] ->
        Forall2Brs (sem_exp H b) es vs ->
        Forall3 (case s) vs (List.map (fun _ => None) tys) os ->
        sem_exp H b (Ecase e es None (tys, ck)) os

    | ScaseDefault:
      forall H b e s es d lann vs vd os,
        sem_exp H b e [s] ->
        wt_streams [s] (typeof e) ->
        Forall2Brs (sem_exp H b) es vs ->
        Forall2 (sem_exp H b) d vd ->
        Forall3 (case s) vs (List.map Some (concat vd)) os ->
        sem_exp H b (Ecase e es (Some d) lann) os

    | Sapp:
      forall H b f es er lann ss os rs bs,
        Forall2 (sem_exp H b) es ss ->
        Forall2 (fun e r => sem_exp H b e [r]) er rs ->
        bools_ofs rs bs ->
        (forall k, sem_node f (List.map (maskv k bs) (concat ss)) (List.map (maskv k bs) os)) ->
        sem_exp H b (Eapp f es er lann) os

    with sem_equation: history -> Stream bool -> equation -> Prop :=
      Seq:
        forall H b xs es ss,
          Forall2 (sem_exp H b) es ss ->
          Forall2 (fun x => sem_var H (Var x)) xs (concat ss) ->
          sem_equation H b (xs, es)

    with sem_transitions: history -> Stream bool -> list (exp * (enumtag * bool)) -> (enumtag * bool) -> Stream (synchronous (enumtag * bool)) -> Prop :=
    | Stransdef : forall H bs default stres,
        stres ≡ const_stres bs default ->
        sem_transitions H bs [] default stres
    | Strans : forall H bs e C r trans default vs bs' stres1 stres,
        sem_exp H bs e [vs] ->
        bools_of vs bs' ->
          sem_transitions H bs trans default stres1 ->
          stres ≡ choose_first (const_stres bs' (C, r)) stres1 ->
          sem_transitions H bs ((e, (C, r))::trans) default stres

    with sem_block: history -> Stream bool -> block -> Prop :=
    | Sbeq:
      forall H b eq,
        sem_equation H b eq ->
        sem_block H b (Beq eq)

    | Sreset:
      forall H b blocks er sr r,
        sem_exp H b er [sr] ->
        bools_of sr r ->
        (forall k, Forall (sem_block (mask_hist k r H) (maskb k r b)) blocks) ->
        sem_block H b (Breset blocks er)

    | Sswitch:
      forall Hi b ec branches sc,
        sem_exp Hi b ec [sc] ->
        wt_streams [sc] (typeof ec) ->
        Forall (fun blks =>
                  exists Hi', when_hist (fst blks) Hi sc Hi'
                         /\ let bi := fwhenb (fst blks) b sc in
                           sem_branch (Forall (sem_block Hi' bi))
                             (fun x => Is_defined_in x (Bswitch ec branches))
                             (fun x => List.Exists (Is_defined_in x))
                             Hi' (snd blks)) branches ->
        sem_block Hi b (Bswitch ec branches)

    | SautoWeak:
      forall H bs ini oth states ck bs' stres0 stres1 stres,
        sem_clock (var_history H) bs ck bs' ->
        sem_transitions H bs' (List.map (fun '(e, t) => (e, (t, false))) ini) (oth, false) stres0 ->
        fby stres0 stres1 stres ->
        Forall (fun state =>
                  let tag := fst (fst state) in
                  forall k, exists Hik, select_hist tag k stres H Hik
                              /\ let bik := fselectb tag k stres bs in
                                sem_branch
                                  (fun blks =>
                                     sem_scope sem_exp
                                       (fun Hi' blks =>
                                          Forall (sem_block Hi' bik) (fst blks)
                                          /\ sem_transitions Hi' bik (snd blks) (tag, false) (fselect absent tag k stres stres1)
                                       ) Hik bik (snd blks))
                                  (fun x => Is_defined_in x (Bauto Weak ck (ini, oth) states))
                                  (fun x '(_, s) => Is_defined_in_scope (fun '(blks, _) => List.Exists (Is_defined_in x) blks) x s)
                                  Hik (snd state)
               ) states ->
        sem_block H bs (Bauto Weak ck (ini, oth) states)

    | SautoStrong:
      forall H bs ini states ck bs' stres stres1,
        sem_clock (var_history H) bs ck bs' ->
        fby (const_stres bs' (ini, false)) stres1 stres ->
        Forall (fun state =>
                  let tag := fst (fst state) in
                  forall k, exists Hik, select_hist tag k stres H Hik
                              /\ let bik := fselectb tag k stres bs in
                                sem_branch
                                  (fun blks =>
                                     sem_transitions Hik bik (fst blks) (tag, false) (fselect absent tag k stres stres1))
                                  (fun x => Is_defined_in x (Bauto Strong ck ([], ini) states))
                                  (fun x '(_, s) => Is_defined_in_scope (fun '(blks, _) => List.Exists (Is_defined_in x) blks) x s)
                                  Hik (snd state)
               ) states ->
        Forall (fun state =>
                  let tag := fst (fst state) in
                  forall k, exists Hik, select_hist tag k stres1 H Hik
                              /\ let bik := fselectb tag k stres1 bs in
                                sem_branch
                                  (fun blks =>
                                     sem_scope sem_exp
                                       (fun Hi' blks => Forall (sem_block Hi' bik) (fst blks))
                                       Hik bik (snd blks))
                                  (fun x => Is_defined_in x (Bauto Strong ck ([], ini) states))
                                  (fun x '(_, s) => Is_defined_in_scope (fun '(blks, _) => List.Exists (Is_defined_in x) blks) x s)
                                  Hik (snd state)
               ) states ->
        sem_block H bs (Bauto Strong ck ([], ini) states)

    | Slocal:
      forall Hi bs scope,
        sem_scope sem_exp (fun Hi' => Forall (sem_block Hi' bs)) Hi bs scope ->
        sem_block Hi bs (Blocal scope)

    with sem_node: ident -> list (Stream svalue) -> list (Stream svalue) -> Prop :=
    | Snode:
      forall f ss os n H,
          find_node f G = Some n ->
          Forall2 (fun x => sem_var H (Var x)) (List.map fst n.(n_in)) ss ->
          Forall2 (fun x => sem_var H (Var x)) (List.map fst n.(n_out)) os ->
          let bs := clocks_of ss in
          Forall (sem_last_decl sem_exp (FEnv.empty _) H bs) n.(n_out) ->
          sem_block H bs n.(n_block) ->
          sem_node f ss os.

  End NodeSemantics.

  Ltac inv_exp :=
    match goal with
    | H:sem_exp _ _ _ _ _ |- _ => inv H
    end.

  Ltac inv_scope :=
    match goal with
    | H:sem_scope _ _ _ _ _ |- _ => inv H
    end;
    destruct_conjs; subst.

  Ltac inv_branch :=
    match goal with
    | H:sem_branch _ _ _ _ _ |- _ => inv H
    end;
    destruct_conjs; subst.

  Ltac inv_block :=
    match goal with
    | H:sem_block _ _ _ _ |- _ => inv H
    end.

Some properties

  Lemma var_history_In : forall x H,
      FEnv.In x (var_history H) <-> FEnv.In (Var x) H.

  Lemma sem_var_history : forall H x vs,
      sem_var (var_history H) x vs <-> sem_var H (Var x) vs.

  Lemma var_history_mask : forall k rs H,
      FEnv.Equiv (@EqSt _) (var_history (mask_hist k rs H)) (mask_hist k rs (var_history H)).

  Lemma dom_dom_ub : forall H Γ,
      dom H Γ ->
      dom_ub H Γ.

  Lemma dom_dom_lb : forall H Γ,
      dom H Γ ->
      dom_lb H Γ.

  Lemma dom_map : forall f H Γ,
      dom (FEnv.map f H) Γ <-> dom H Γ.

  Lemma dom_ub_map : forall f H Γ,
      dom_ub (FEnv.map f H) Γ <-> dom_ub H Γ.

  Lemma dom_lb_map : forall f H Γ,
      dom_lb (FEnv.map f H) Γ <-> dom_lb H Γ.

  Lemma dom_ub_refines {R} : forall Hi1 Hi2 xs,
      FEnv.refines R Hi1 Hi2 ->
      dom_ub Hi2 xs ->
      dom_ub Hi1 xs.

  Lemma dom_ub_incl : forall H xs1 xs2,
      List.incl xs1 xs2 ->
      dom_ub H xs1 ->
      dom_ub H xs2.

  Lemma dom_ub_incl' : forall H xs1 xs2,
      (forall x, IsVar xs1 x -> IsVar xs2 x) ->
      (forall x, IsLast xs1 x -> IsLast xs2 x) ->
      dom_ub H xs1 ->
      dom_ub H xs2.

  Definition vars_of_senv (Γ : static_env) :=
    flat_map (fun '(x, ann) => (Var x)::if isSome ann.(causl_last) then [Last x] else []) Γ.

  Fact vars_of_senv_Var : forall Γ x,
      In (Var x) (vars_of_senv Γ) <-> IsVar Γ x.

  Fact vars_of_senv_Last : forall Γ x,
      In (Last x) (vars_of_senv Γ) <-> IsLast Γ x.

  Lemma vars_of_senv_NoLast : forall Γ,
      (forall x, ~IsLast Γ x) ->
      vars_of_senv Γ = List.map (fun '(x, _) => Var x) Γ.

  Lemma dom_fenv_dom : forall H Γ,
      dom H Γ <-> FEnv.dom H (vars_of_senv Γ).

Properties of Forall2Brs

  Lemma Forall2Brs_impl_In (P1 P2 : _ -> _ -> Prop) : forall es vs,
      (forall x y, List.Exists (fun es => In x (snd es)) es -> P1 x y -> P2 x y) ->
      Forall2Brs P1 es vs ->
      Forall2Brs P2 es vs.

  Lemma Forall2Brs_fst P : forall es vs,
      Forall2Brs P es vs ->
      Forall (fun vs => List.map fst vs = List.map fst es) vs.

  Lemma Forall2Brs_length1 (P : _ -> _ -> Prop) : forall es vs,
      Forall (fun es => Forall (fun e => forall v, P e v -> length v = numstreams e) (snd es)) es ->
      Forall2Brs P es vs ->
      Forall (fun es => length (annots (snd es)) = length vs) es.

  Lemma Forall2Brs_length2 (P : _ -> _ -> Prop) : forall es vs,
      Forall2Brs P es vs ->
      Forall (fun vs => length vs = length es) vs.

  Lemma Forall2Brs_map_1 (P : _ -> _ -> Prop) f : forall es vs,
      Forall2Brs (fun e => P (f e)) es vs <->
      Forall2Brs P (List.map (fun '(i, es) => (i, List.map f es)) es) vs.

  Lemma Forall2Brs_map_2 (P : _ -> _ -> Prop) f : forall es vs,
      Forall2Brs (fun e vs => P e (List.map f vs)) es vs ->
      Forall2Brs P es (List.map (List.map (fun '(i, v) => (i, f v))) vs).

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

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

  Add Parametric Morphism : arrow1
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _ ==> Basics.impl
        as arrow1_EqSt.

  Add Parametric Morphism : arrow
      with signature @EqSt _ ==> @EqSt _ ==> @EqSt _ ==> Basics.impl
        as arrow_EqSt.

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

  Add Parametric Morphism : const
      with signature @EqSt bool ==> eq ==> @EqSt svalue
        as const_EqSt.

  Add Parametric Morphism : enum
      with signature @EqSt bool ==> eq ==> @EqSt svalue
        as enum_EqSt.

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

  Definition history_equiv (Hi1 Hi2 : history) : Prop := FEnv.Equiv (@EqSt _) Hi1 Hi2.

  Global Instance history_equiv_refl : Reflexive history_equiv.

  Add Parametric Morphism {PSyn prefs} (G : @global PSyn prefs) : (sem_exp G)
      with signature history_equiv ==> @EqSt bool ==> eq ==> @EqSts svalue ==> Basics.impl
        as sem_exp_morph.

  Add Parametric Morphism {PSyn prefs} (G : @global PSyn prefs) : (sem_equation G)
      with signature history_equiv ==> @EqSt bool ==> eq ==> Basics.impl
        as sem_equation_morph.

  Add Parametric Morphism {PSyn prefs} (G: @global PSyn prefs) : (sem_transitions G)
      with signature history_equiv ==> @EqSt bool ==> eq ==> eq ==> @EqSt _ ==> Basics.impl
        as sem_transitions_morph.

  Add Parametric Morphism {PSyn prefs} (G: @global PSyn prefs) : (sem_last_decl (sem_exp G))
      with signature history_equiv ==> history_equiv ==> @EqSt bool ==> eq ==> Basics.impl
        as sem_last_decls_morph.

  Add Parametric Morphism : var_history
      with signature history_equiv ==> FEnv.Equiv (@EqSt _)
        as var_history_morph.

  Add Parametric Morphism {PSyn prefs} (G : @global PSyn prefs) : (sem_block G)
      with signature history_equiv ==> @EqSt bool ==> eq ==> Basics.impl
        as sem_block_morph.

  Add Parametric Morphism {PSyn prefs} (G : @global PSyn prefs) : (sem_node G)
      with signature eq ==> @EqSts svalue ==> @EqSts svalue ==> Basics.impl
        as sem_node_morph.

  Ltac inv_scope' := (Syn.inv_scope || inv_scope).
  Ltac inv_branch' := (Syn.inv_branch || inv_branch).
  Ltac inv_block' := (Syn.inv_block || inv_block).


  Section sem_exp_ind2.
    Context {prefs PSyn} (G: @global prefs PSyn).

    Variable P_exp : history -> Stream bool -> exp -> list (Stream svalue) -> Prop.
    Variable P_equation : history -> Stream bool -> equation -> Prop.
    Variable P_transitions : history -> Stream bool -> list (exp * (enumtag * bool)) -> (enumtag * bool) -> Stream (synchronous (enumtag * bool)) -> Prop.
    Variable P_block : history -> Stream bool -> block -> Prop.
    Variable P_node : ident -> list (Stream svalue) -> list (Stream svalue) -> Prop.

    Hypothesis ConstCase:
      forall H b c cs,
        cs ≡ const b c ->
        P_exp H b (Econst c) [cs].

    Hypothesis EnumCase:
      forall H b k ty es,
        es ≡ enum b k ->
        P_exp H b (Eenum k ty) [es].

    Hypothesis VarCase:
      forall H b x s ann,
        sem_var H (Var x) s ->
        P_exp H b (Evar x ann) [s].

    Hypothesis LastCase:
      forall H b x s ann,
        sem_var H (Last x) s ->
        P_exp H b (Elast x ann) [s].

    Hypothesis UnopCase:
      forall H b e op ty s o ann,
        sem_exp G H b e [s] ->
        P_exp H b e [s] ->
        typeof e = [ty] ->
        lift1 op ty s o ->
        P_exp H b (Eunop op e ann) [o].

    Hypothesis BinopCase:
      forall H b e1 e2 op ty1 ty2 s1 s2 o ann,
        sem_exp G H b e1 [s1] ->
        P_exp H b e1 [s1] ->
        sem_exp G H b e2 [s2] ->
        P_exp H b e2 [s2] ->
        typeof e1 = [ty1] ->
        typeof e2 = [ty2] ->
        lift2 op ty1 ty2 s1 s2 o ->
        P_exp H b (Ebinop op e1 e2 ann) [o].

    Hypothesis ExtcallCase:
      forall H b f es tyout ck tyins ss vs,
        Forall2 (fun cty ty => cty = Tprimitive ty) (typesof es) tyins ->
        Forall2 (sem_exp G H b) es ss ->
        Forall2 (P_exp H b) es ss ->
        liftn (fun ss => sem_extern f tyins ss tyout) (concat ss) vs ->
        P_exp H b (Eextcall f es (tyout, ck)) [vs].

    Hypothesis FbyCase:
      forall H b e0s es anns s0ss sss os,
        Forall2 (sem_exp G H b) e0s s0ss ->
        Forall2 (P_exp H b) e0s s0ss ->
        Forall2 (sem_exp G H b) es sss ->
        Forall2 (P_exp H b) es sss ->
        Forall3 fby (concat s0ss) (concat sss) os ->
        P_exp H b (Efby e0s es anns) os.

    Hypothesis ArrowCase:
      forall H b e0s es anns s0ss sss os,
        Forall2 (sem_exp G H b) e0s s0ss ->
        Forall2 (P_exp H b) e0s s0ss ->
        Forall2 (sem_exp G H b) es sss ->
        Forall2 (P_exp H b) es sss ->
        Forall3 arrow (concat s0ss) (concat sss) os ->
        P_exp H b (Earrow e0s es anns) os.

    Hypothesis WhenCase:
      forall H b x tx s k es lann ss os,
        Forall2 (sem_exp G H b) es ss ->
        Forall2 (P_exp H b) es ss ->
        sem_var H (Var x) s ->
        Forall2 (fun s' => when k s' s) (concat ss) os ->
        P_exp H b (Ewhen es (x, tx) k lann) os.

    Hypothesis MergeCase:
      forall H b x tx s es lann vs os,
        sem_var H (Var x) s ->
        Forall2Brs (sem_exp G H b) es vs ->
        Forall2Brs (P_exp H b) es vs ->
        Forall2 (merge s) vs os ->
        P_exp H b (Emerge (x, tx) es lann) os.

    Hypothesis CaseTotalCase:
      forall H b e s es tys ck vs os,
        sem_exp G H b e [s] ->
        P_exp H b e [s] ->
        Forall2Brs (sem_exp G H b) es vs ->
        Forall2Brs (P_exp H b) es vs ->
        Forall3 (case s) vs (List.map (fun _ => None) tys) os ->
        P_exp H b (Ecase e es None (tys, ck)) os.

    Hypothesis CaseDefaultCase:
      forall H b e s es d lann vs vd os,
        sem_exp G H b e [s] ->
        P_exp H b e [s] ->
        wt_streams [s] (typeof e) ->
        Forall2Brs (sem_exp G H b) es vs ->
        Forall2Brs (P_exp H b) es vs ->
        Forall2 (sem_exp G H b) d vd ->
        Forall2 (P_exp H b) d vd ->
        Forall3 (case s) vs (List.map Some (concat vd)) os ->
        P_exp H b (Ecase e es (Some d) lann) os.

    Hypothesis AppCase:
      forall H b f es er lann ss os sr bs,
        Forall2 (sem_exp G H b) es ss ->
        Forall2 (P_exp H b) es ss ->
        Forall2 (fun e r => sem_exp G H b e [r]) er sr ->
        Forall2 (fun e r => P_exp H b e [r]) er sr ->
        bools_ofs sr bs ->
        (forall k, sem_node G f (List.map (maskv k bs) (concat ss)) (List.map (maskv k bs) os)
              /\ P_node f (List.map (maskv k bs) (concat ss)) (List.map (maskv k bs) os)) ->
        P_exp H b (Eapp f es er lann) os.

    Hypothesis Equation:
      forall H b xs es ss,
        Forall2 (sem_exp G H b) es ss ->
        Forall2 (P_exp H b) es ss ->
        Forall2 (fun x => sem_var H (Var x)) xs (concat ss) ->
        P_equation H b (xs, es).

    Hypothesis BeqCase:
      forall H b eq,
        sem_equation G H b eq ->
        P_equation H b eq ->
        P_block H b (Beq eq).

    Hypothesis BresetCase:
      forall H b blocks er sr r,
        sem_exp G H b er [sr] ->
        P_exp H b er [sr] ->
        bools_of sr r ->
        (forall k, Forall (sem_block G (mask_hist k r H) (maskb k r b)) blocks /\
                Forall (P_block (mask_hist k r H) (maskb k r b)) blocks) ->
        P_block H b (Breset blocks er).

    Hypothesis BswitchCase:
      forall Hi b ec branches sc,
        sem_exp G Hi b ec [sc] ->
        P_exp Hi b ec [sc] ->
        wt_streams [sc] (typeof ec) ->
        Forall (fun blks => exists Hi', when_hist (fst blks) Hi sc Hi'
                                /\ let bi := fwhenb (fst blks) b sc in
                                  sem_branch
                                    (fun blks => Forall (sem_block G Hi' bi) blks
                                              /\ Forall (P_block Hi' bi) blks)
                                    (fun x : ident => Is_defined_in x (Bswitch ec branches))
                                    (fun x : ident => List.Exists (Is_defined_in x)) Hi' (snd blks)) branches ->
        P_block Hi b (Bswitch ec branches).

    Hypothesis TransDefCase:
      forall Hi bs default stres,
        stres ≡ const_stres bs default ->
        P_transitions Hi bs [] default stres.

    Hypothesis TransCase:
      forall Hi bs e C r trans default vs bs' stres1 stres,
        sem_exp G Hi bs e [vs] ->
        P_exp Hi bs e [vs] ->
        bools_of vs bs' ->
        sem_transitions G Hi bs trans default stres1 ->
        P_transitions Hi bs trans default stres1 ->
        stres ≡ choose_first (const_stres bs' (C, r)) stres1 ->
        P_transitions Hi bs ((e, (C, r))::trans) default stres.

    Hypothesis BautoWeakCase:
      forall Hi bs ini oth states ck bs' stres0 stres1 stres,
        sem_clock (var_history Hi) bs ck bs' ->
        sem_transitions G Hi bs' (List.map (fun '(e, t) => (e, (t, false))) ini) (oth, false) stres0 ->
        P_transitions Hi bs' (List.map (fun '(e, t) => (e, (t, false))) ini) (oth, false) stres0 ->
        fby stres0 stres1 stres ->
        Forall (fun '((tag, _), br) =>
                  forall k, exists Hik,
                    select_hist tag k stres Hi Hik
                    /\ let bik := fselectb tag k stres bs in
                      sem_branch
                        (fun '(_, scope) =>
                           sem_scope
                             (fun Hi' bik e vs => sem_exp G Hi' bik e vs /\ P_exp Hi' bik e vs)
                             (fun Hi' blks => Forall (sem_block G Hi' bik) (fst blks)
                                           /\ Forall (P_block Hi' bik) (fst blks)
                                           /\ sem_transitions G Hi' bik (snd blks) (tag, false) (fselect absent tag k stres stres1)
                                           /\ P_transitions Hi' bik (snd blks) (tag, false) (fselect absent tag k stres stres1)
                             ) Hik bik scope)
                        (fun x => Is_defined_in x (Bauto Weak ck (ini, oth) states))
                        (fun x '(_, s) => Is_defined_in_scope (fun '(blks, _) => List.Exists (Is_defined_in x) blks) x s)
                        Hik br) states ->
        P_block Hi bs (Bauto Weak ck (ini, oth) states).

    Hypothesis BautoStrongCase:
      forall Hi bs ini states ck bs' stres0 stres1,
        sem_clock (var_history Hi) bs ck bs' ->
        fby (const_stres bs' (ini, false)) stres1 stres0 ->
        Forall (fun '((tag, _), br) =>
                  forall k, exists Hik, select_hist tag k stres0 Hi Hik
                              /\ let bik := fselectb tag k stres0 bs in
                                sem_branch
                                  (fun '(unl, _) =>
                                     sem_transitions G Hik bik unl (tag, false) (fselect absent tag k stres0 stres1)
                                     /\ P_transitions Hik bik unl (tag, false) (fselect absent tag k stres0 stres1))
                                  (fun x => Is_defined_in x (Bauto Strong ck ([], ini) states))
                                  (fun x '(_, s) => Is_defined_in_scope (fun '(blks, _) => List.Exists (Is_defined_in x) blks) x s)
                                  Hik br) states ->
        Forall (fun '((tag, _), br) =>
                  forall k, exists Hik,
                    select_hist tag k stres1 Hi Hik
                    /\ let bik := fselectb tag k stres1 bs in
                      sem_branch
                        (fun '(_, scope) =>
                           sem_scope
                             (fun Hi' bik e vs => sem_exp G Hi' bik e vs /\ P_exp Hi' bik e vs)
                             (fun Hi' blks => Forall (sem_block G Hi' bik) (fst blks)
                                           /\ Forall (P_block Hi' bik) (fst blks)
                             ) Hik bik scope)
                        (fun x => Is_defined_in x (Bauto Strong ck ([], ini) states))
                        (fun x '(_, s) => Is_defined_in_scope (fun '(blks, _) => List.Exists (Is_defined_in x) blks) x s)
                        Hik br) states ->
        P_block Hi bs (Bauto Strong ck ([], ini) states).

    Hypothesis BlocalCase:
      forall Hi bs scope,
        sem_scope (fun Hi' bs e vs => sem_exp G Hi' bs e vs /\ P_exp Hi' bs e vs)
          (fun Hi' blks => Forall (sem_block G Hi' bs) blks /\ Forall (P_block Hi' bs) blks)
          Hi bs scope ->
        P_block Hi bs (Blocal scope).

    Hypothesis Node:
      forall f ss os n H,
        find_node f G = Some n ->
        Forall2 (fun x => sem_var H (Var x)) (List.map fst n.(n_in)) ss ->
        Forall2 (fun x => sem_var H (Var x)) (List.map fst n.(n_out)) os ->
        let bs := clocks_of ss in
        Forall (sem_last_decl (fun Hi' bs e vs => sem_exp G Hi' bs e vs /\ P_exp Hi' bs e vs) (FEnv.empty _) H bs) n.(n_out) ->
        sem_block G H bs n.(n_block) ->
        P_block H bs n.(n_block) ->
        P_node f ss os.

    Local Ltac SolveForall :=
      match goal with
      | H: Forall ?P1 ?l |- Forall ?P2 ?l =>
          induction H; eauto
      | H: Forall2 ?P1 ?l1 ?l2 |- Forall2 ?P2 ?l1 ?l2 =>
          induction H; eauto
      | _ => idtac
      end.

    Fixpoint sem_exp_ind2
      (H: history) (b: Stream bool) (e: exp) (ss: list (Stream svalue))
      (Sem: sem_exp G H b e ss)
      {struct Sem}
      : P_exp H b e ss
    with sem_equation_ind2
           (H: history) (b: Stream bool) (e: equation)
           (Sem: sem_equation G H b e)
           {struct Sem}
      : P_equation H b e
    with sem_transitions_ind2
           (H: history) (b: Stream bool) trans default stres
           (Sem: sem_transitions G H b trans default stres)
           {struct Sem}
      : P_transitions H b trans default stres
    with sem_block_ind2
           (H: history) (b: Stream bool) (d: block)
           (Sem: sem_block G H b d)
           {struct Sem}
      : P_block H b d
    with sem_node_ind2
           (f: ident) (ss os: list (Stream svalue))
           (Sem: sem_node G f ss os)
           {struct Sem}
      : P_node f ss os.

  End sem_exp_ind2.
  

properties of the global environment

  Ltac sem_cons :=
    intros; simpl_Forall; solve_Exists;
    unfold Is_node_in_eq in *;
    match goal with
    | H: Forall2Brs _ ?l1 ?l2 |- Forall2Brs _ ?l1 ?l2 =>
        eapply Forall2Brs_impl_In in H; eauto; intros; sem_cons
    | H: _ -> ?R |- ?R => eapply H; eauto
    | H: forall (_ : ident) (xs ys : list (Stream svalue)), _ -> _ -> sem_node _ _ _ _ |- sem_node _ _ _ _ =>
        eapply H; eauto using Is_node_in_exp; econstructor; sem_cons
    | Hname: n_name ?nd <> _, Hfind: find_node _ {| types := _; nodes := ?nd :: _ |} = _ |- _ =>
        rewrite find_node_other in Hfind; auto
    | Hname: n_name ?nd <> _ |- find_node _ {| types := _; nodes := ?nd :: _ |} = _ =>
        rewrite find_node_other; auto
    | Hname: n_name ?nd <> _ |- ~_ => idtac
    | H: ~Is_node_in_exp _ (Eapp _ _ _ _) |- _ <> _ => contradict H; subst; eapply INEapp2
    | H: ~_ |- ~_ => contradict H; try constructor; sem_cons
    | |- _ \/ _ => solve [left;sem_cons|right;sem_cons]
    | |- exists d, Some _ = Some d /\ List.Exists _ d =>
        do 2 esplit; [reflexivity|sem_cons]
    | k: nat,H: forall (_ : nat), _ |- _ => specialize (H k); sem_cons
    | H: Forall2 _ ?xs _ |- Forall2 _ ?xs _ =>
        eapply Forall2_impl_In in H; eauto; intros; sem_cons
    | |- exists _, when_hist _ _ _ _ /\ _ =>
        do 2 esplit; [auto|sem_cons]
    | |- exists _, select_hist _ _ _ _ _ /\ _ =>
        do 2 esplit; [auto|sem_cons]
    | H:sem_last_decl _ _ _ _ _ |- sem_last_decl _ _ _ _ _ =>
        inv H; destruct_conjs; econstructor; eauto
    | H:sem_branch _ _ _ _ _ |- _ =>
        inv H; destruct_conjs
    | |- sem_branch _ _ _ _ _ => econstructor; eauto
    | |- Is_node_in_branch _ _ => econstructor; sem_cons
    | H:sem_scope _ _ _ _ _ |- sem_scope _ _ _ _ _ =>
        inv H; destruct_conjs; econstructor; eauto
    | |- Is_node_in_scope _ _ _ => econstructor; sem_cons
    | |- _ /\ _ => split; sem_cons
    | |- exists _ _, _ /\ _ /\ _ =>
        do 2 esplit; split; [|split]; eauto; sem_cons
    | _ => auto
    end.

  Definition exp_cons1 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs e ss :=
    ~ Is_node_in_exp nd.(n_name) e -> sem_exp (Global typs exts nds) H bs e ss.
  Definition equation_cons1 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs equ :=
    ~ Is_node_in_eq nd.(n_name) equ -> sem_equation (Global typs exts nds) H bs equ.
  Definition transitions_cons1 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs trans default stres :=
    ~ List.Exists (fun '(e, _) => Is_node_in_exp nd.(n_name) e) trans -> sem_transitions (Global typs exts nds) H bs trans default stres.
  Definition block_cons1 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs blk :=
    ~ Is_node_in_block nd.(n_name) blk -> sem_block (Global typs exts nds) H bs blk.
  Definition node_cons1 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) f xs ys :=
    nd.(n_name) <> f -> sem_node (Global typs exts nds) f xs ys.
  Global Hint Unfold exp_cons1 equation_cons1 transitions_cons1 block_cons1 node_cons1 : lsem.

  Lemma sem_exp_cons1 {PSyn prefs} :
    forall typs exts (nd : @node PSyn prefs) nds Hi bs e ss,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      sem_exp (Global typs exts (nd::nds)) Hi bs e ss ->
      exp_cons1 typs exts nd nds Hi bs e ss.

  Lemma sem_block_cons1 {PSyn prefs} :
    forall typs exts (nd : @node PSyn prefs) nds Hi bs blk,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      sem_block (Global typs exts (nd::nds)) Hi bs blk ->
      block_cons1 typs exts nd nds Hi bs blk.

  Lemma sem_node_cons1 {PSyn prefs} :
    forall typs exts (nd : @node PSyn prefs) nds f xs ys,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      sem_node (Global typs exts (nd::nds)) f xs ys ->
      node_cons1 typs exts nd nds f xs ys.

  Corollary sem_node_cons1' {PSyn prefs} : forall typs exts (n nd: @node PSyn prefs) nds Hi bs,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      ~Is_node_in nd.(n_name) n ->
      sem_block (Global typs exts (nd::nds)) Hi bs (n_block n) ->
      Forall (sem_last_decl (sem_exp (Global typs exts (nd::nds))) (FEnv.empty (Stream svalue)) Hi bs) (n_out n) ->
      sem_block (Global typs exts nds) Hi bs (n_block n)
      /\ Forall (sem_last_decl (sem_exp (Global typs exts nds)) (FEnv.empty (Stream svalue)) Hi bs) (n_out n).

  Definition exp_cons2 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs e ss :=
    ~ Is_node_in_exp nd.(n_name) e -> sem_exp (Global typs exts (nd::nds)) H bs e ss.
  Definition equation_cons2 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs equ :=
    ~ Is_node_in_eq nd.(n_name) equ -> sem_equation (Global typs exts (nd::nds)) H bs equ.
  Definition transitions_cons2 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs trans default stres :=
    ~ List.Exists (fun '(e, _) => Is_node_in_exp nd.(n_name) e) trans -> sem_transitions (Global typs exts (nd::nds)) H bs trans default stres.
  Definition block_cons2 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) H bs blk :=
    ~ Is_node_in_block nd.(n_name) blk -> sem_block (Global typs exts (nd::nds)) H bs blk.
  Definition node_cons2 {PSyn prefs} typs exts (nd: @node PSyn prefs) (nds: list (@node PSyn prefs)) f xs ys :=
    nd.(n_name) <> f -> sem_node (Global typs exts (nd::nds)) f xs ys.
  Global Hint Unfold exp_cons2 equation_cons2 transitions_cons2 block_cons2 node_cons2 : lsem.

  Lemma sem_exp_cons2 {PSyn prefs} :
    forall typs exts (nd : @node PSyn prefs) nds Hi bs e ss,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      sem_exp (Global typs exts nds) Hi bs e ss ->
      exp_cons2 typs exts nd nds Hi bs e ss.

  Lemma sem_block_cons2 {PSyn prefs} :
    forall typs exts (nd : @node PSyn prefs) nds Hi bs blk,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      sem_block (Global typs exts nds) Hi bs blk ->
      block_cons2 typs exts nd nds Hi bs blk.

  Lemma sem_node_cons2 {PSyn prefs} :
    forall typs exts (nd : @node PSyn prefs) nds f xs ys,
      Ordered_nodes (Global typs exts (nd::nds)) ->
      sem_node (Global typs exts nds) f xs ys ->
      node_cons2 typs exts nd nds f xs ys.

  Lemma sem_node_cons_iff {PSyn prefs} :
    forall (n : @node PSyn prefs) nds types externs f xs ys,
      Ordered_nodes (Global types externs (n::nds)) ->
      n_name n <> f ->
      sem_node (Global types externs nds) f xs ys <->
      sem_node (Global types externs (n::nds)) f xs ys.

All the defined variables have a semantic

  Fact sem_var_In {K} : forall H x vs,
      @sem_var K H x vs ->
      FEnv.In x H.

  Corollary sem_vars_In : forall H xs vs,
      Forall2 (fun x => sem_var H (Var x)) xs vs ->
      Forall (fun x => FEnv.In (Var x) H) xs.

  Lemma sem_block_defined {PSyn prefs} (G: @global PSyn prefs) : forall blk H bs x,
      sem_block G H bs blk ->
      Is_defined_in x blk ->
      FEnv.In (Var x) H.

  Corollary Forall_sem_block_defined {PSyn prefs} (G: @global PSyn prefs) : forall blks x H bs,
      Forall (sem_block G H bs) blks ->
      List.Exists (Is_defined_in x) blks ->
      FEnv.In (Var x) H.

  Lemma sem_scope_defined {PSyn prefs} (G: @global PSyn prefs) : forall locs blks Hi bs x,
      sem_scope (sem_exp G) (fun Hi => Forall (sem_block G Hi bs)) Hi bs (Scope locs blks) ->
      Is_defined_in_scope (List.Exists (Is_defined_in x)) x (Scope locs blks) ->
      FEnv.In (Var x) Hi.

  Corollary sem_scope_defined1 {PSyn prefs} (G: @global PSyn prefs) :
    forall locs blks Hi bs Γ xs x,
      sem_scope (sem_exp G) (fun Hi => Forall (sem_block G Hi bs)) Hi bs (Scope locs blks) ->
      VarsDefinedCompScope (fun blks ys => exists xs, Forall2 VarsDefinedComp blks xs /\ Permutation (concat xs) ys) (Scope locs blks) xs ->
      NoDupScope (fun Γ => Forall (NoDupLocals Γ)) Γ (Scope locs blks) ->
      incl xs Γ ->
      In x xs ->
      FEnv.In (Var x) Hi.

  Corollary sem_scope_defined2 {A} {PSyn prefs} (G: @global PSyn prefs) :
    forall locs (blks: _ * A) Hi bs Γ xs x,
      sem_scope (sem_exp G) (fun Hi blks => Forall (sem_block G Hi bs) (fst blks)) Hi bs (Scope locs blks) ->
      VarsDefinedCompScope (fun blks ys => exists xs, Forall2 VarsDefinedComp (fst blks) xs /\ Permutation (concat xs) ys) (Scope locs blks) xs ->
      NoDupScope (fun Γ blks => Forall (NoDupLocals Γ) (fst blks)) Γ (Scope locs blks) ->
      incl xs Γ ->
      In x xs ->
      FEnv.In (Var x) Hi.

  Lemma sem_branch_defined {PSyn prefs} (G: @global PSyn prefs) must_def is_def : forall caus blks Hi bs x,
      sem_branch (Forall (sem_block G Hi bs)) must_def is_def Hi (Branch caus blks) ->
      Is_defined_in_branch (List.Exists (Is_defined_in x)) (Branch caus blks) ->
      FEnv.In (Var x) Hi.

  Corollary sem_branch_defined1 {PSyn prefs} (G: @global PSyn prefs) :
    forall caus ec branches blks Hi bs Γ xs x,
      sem_branch (Forall (sem_block G Hi bs))
        (fun x => Is_defined_in x (Bswitch ec branches))
        (fun x => List.Exists (Is_defined_in x))
        Hi (Branch caus blks) ->
      VarsDefinedCompBranch (fun blks ys => exists xs, Forall2 VarsDefinedComp blks xs /\ Permutation (concat xs) ys) (Branch caus blks) xs ->
      NoDupBranch (Forall (NoDupLocals Γ)) (Branch caus blks) ->
      incl xs Γ ->
      In x xs ->
      FEnv.In (Var x) Hi.

  Corollary sem_branch_defined2 {A} {PSyn prefs} (G: @global PSyn prefs) must_def is_def :
    forall caus (blks: (A * scope (_ * A))) Hi bs Γ xs x,
      sem_branch
        (fun blks =>
           sem_scope (sem_exp G)
             (fun Hi blks => Forall (sem_block G Hi bs) (fst blks)) Hi bs (snd blks))
        must_def is_def Hi (Branch caus blks) ->
      VarsDefinedCompBranch
        (fun blks => VarsDefinedCompScope (fun blks ys => exists xs, Forall2 VarsDefinedComp (fst blks) xs /\ Permutation (concat xs) ys) (snd blks))
        (Branch caus blks) xs ->
      NoDupBranch
        (fun blks => NoDupScope (fun Γ blks => Forall (NoDupLocals Γ) (fst blks)) Γ (snd blks))
        (Branch caus blks) ->
      incl xs Γ ->
      In x xs ->
      FEnv.In (Var x) Hi.

Preservation of the semantics while refining an environment

  Fact refines_eq_EqSt {K A} : forall (H H': @FEnv.t K _) ,
      FEnv.refines eq H H' ->
      FEnv.refines (@EqSt A) H H'.

  Fact sem_var_refines {K} : forall (H H' : @FEnv.t K _) id v,
      H ⊑ H' ->
      sem_var H id v ->
      sem_var H' id v.

  Lemma sem_var_refines_inv {K} : forall env (Hi1 Hi2: @FEnv.t K _) x vs,
      List.In x env ->
      FEnv.dom_lb Hi1 env ->
      (forall vs, sem_var Hi1 x vs -> sem_var Hi2 x vs) ->
      sem_var Hi2 x vs ->
      sem_var Hi1 x vs.

  Lemma sem_var_refines' {K} : forall (Hi1 Hi2: @FEnv.t K _) x vs,
      FEnv.In x Hi1 ->
      Hi1 ⊑ Hi2 ->
      sem_var Hi2 x vs ->
      sem_var Hi1 x vs.

  Corollary sem_var_refines'' {K} : forall env (Hi1 Hi2: @FEnv.t K _) x vs,
      List.In x env ->
      FEnv.dom_lb Hi1 env ->
      Hi1 ⊑ Hi2 ->
      sem_var Hi2 x vs ->
      sem_var Hi1 x vs.

  Lemma sem_clock_refines : forall H H' ck bs bs',
      H ⊑ H' ->
      sem_clock H bs ck bs' ->
      sem_clock H' bs ck bs'.

  Lemma sem_clock_refines' : forall vars H H' ck bs bs',
      wx_clock vars ck ->
      (forall x vs, IsVar vars x -> sem_var H x vs -> sem_var H' x vs) ->
      sem_clock H bs ck bs' ->
      sem_clock H' bs ck bs'.

  Fact sem_exp_refines {PSyn prefs} : forall (G : @global PSyn prefs) b e H H' v,
      H ⊑ H' ->
      sem_exp G H b e v ->
      sem_exp G H' b e v.

  Fact sem_equation_refines {PSyn prefs} : forall (G : @global PSyn prefs) H H' b equ,
      H ⊑ H' ->
      sem_equation G H b equ ->
      sem_equation G H' b equ.

  Fact sem_transitions_refines {PSyn prefs} : forall (G : @global PSyn prefs) H H' b trans default stres,
      H ⊑ H' ->
      sem_transitions G H b trans default stres ->
      sem_transitions G H' b trans default stres.

  Fact var_history_refines : forall Hi1 Hi2,
      Hi1 ⊑ Hi2 ->
      (var_history Hi1) ⊑ (var_history Hi2).

  Fact var_history_refines' : forall Hi1 Hi2,
      (forall x vs, sem_var Hi1 (Var x) vs -> sem_var Hi2 (Var x) vs) ->
      (var_history Hi1) ⊑ (var_history Hi2).

  Fact sem_block_refines {PSyn prefs} : forall (G: @global PSyn prefs) d H H' b,
      H ⊑ H' ->
      sem_block G H b d ->
      sem_block G H' b d.

  Section props.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.
    Variable (G : @global PSyn prefs).


    Fact sem_exp_numstreams : forall H b e v,
        wl_exp G e ->
        sem_exp G H b e v ->
        length v = numstreams e.

    Corollary sem_exps_numstreams : forall H b es vs,
        Forall (wl_exp G) es ->
        Forall2 (sem_exp G H b) es vs ->
        length (concat vs) = length (annots es).

    Lemma sem_exp_sem_var : forall H b e vs,
        wl_exp G e ->
        sem_exp G H b e vs ->
        Forall2 (fun '(_, o) s => LiftO True (fun x : ident => sem_var H (Var x) s) o) (nclockof e) vs.

    Corollary sem_exps_sem_var : forall H b es vs,
        Forall (wl_exp G) es ->
        Forall2 (sem_exp G H b) es vs ->
        Forall2 (fun '(_, o) s => LiftO True (fun x : ident => sem_var H (Var x) s) o) (nclocksof es) (concat vs).

    Lemma sem_vars_mask_inv {K} : forall k r (H: @FEnv.t K _) xs vs,
        Forall2 (sem_var (Str.mask_hist k r H)) xs vs ->
        exists vs', Forall2 (sem_var H) xs vs' /\ EqSts vs (List.map (maskv k r) vs').

    Fact sem_block_sem_var : forall blk x Hi bs,
        Is_defined_in x blk ->
        sem_block G Hi bs blk ->
        exists vs, sem_var Hi (Var x) vs.
  End props.

Restriction

  Definition restrict (H : history) Γ :=
    FEnv.restrict H (vars_of_senv Γ).

  Lemma restrict_dom_ub : forall H Γ,
      dom_ub (restrict H Γ) Γ.

  Fact sem_var_restrict {K} `{FEnv.fenv_key K} : forall vars (H: @FEnv.t K _) id v,
      List.In id vars ->
      sem_var H id v ->
      sem_var (FEnv.restrict H vars) id v.

  Fact sem_var_restrict_inv {K} `{FEnv.fenv_key K} : forall vars (H: @FEnv.t K _) id v,
      sem_var (FEnv.restrict H vars) id v ->
      List.In id vars /\ sem_var H id v.

  Fact sem_clock_restrict : forall Γ xs ck H bs bs',
      (forall x, IsVar Γ x -> In x xs) ->
      wx_clock Γ ck ->
      sem_clock H bs ck bs' ->
      sem_clock (FEnv.restrict H xs) bs ck bs'.

  Fact var_history_restrict : forall H Γ,
      FEnv.Equiv (@EqSt _) (var_history (restrict H Γ))
        (FEnv.restrict (var_history H) (List.map fst Γ)).

  Fact sem_clock_var_history_restrict : forall Γ ck H bs bs',
      wx_clock Γ ck ->
      sem_clock (var_history H) bs ck bs' ->
      sem_clock (var_history (restrict H Γ)) bs ck bs'.

  Fact sem_exp_restrict {PSyn prefs} : forall (G : @global PSyn prefs) Γ H b e vs,
      wx_exp Γ e ->
      sem_exp G H b e vs ->
      sem_exp G (restrict H Γ) b e vs.

  Lemma sem_equation_restrict {PSyn prefs} : forall (G : @global PSyn prefs) Γ H b eq,
      wx_equation Γ eq ->
      sem_equation G H b eq ->
      sem_equation G (restrict H Γ) b eq.

  Fact sem_transitions_restrict {PSyn prefs} : forall (G : @global PSyn prefs) Γ H b trans default stres,
      Forall (fun '(e, _) => wx_exp Γ e) trans ->
      sem_transitions G H b trans default stres ->
      sem_transitions G (restrict H Γ) b trans default stres.

  Definition vars_of_locs (locs : list (ident * (type * clock * ident * option (exp * ident)))) :=
    vars_of_senv (senv_of_decls locs).

  Fact vars_of_locs_Var : forall locs x,
      In (Var x) (vars_of_locs locs) <-> IsVar (senv_of_decls locs) x.

  Fact vars_of_locs_Last : forall locs x,
      In (Last x) (vars_of_locs locs) <-> IsLast (senv_of_decls locs) x.

  Lemma sem_scope_restrict {A} (wx_block : _ -> _ -> Prop) (sem_block : _ -> _ -> Prop) (P_vd : _ -> _ -> Prop) (P_nd : _ -> _ -> Prop) {PSyn prefs} (G: @global PSyn prefs) :
    forall Γ xs Hi bs locs (blks : A),
      (forall Γ xs Hi Hi',
          P_vd blks xs ->
          P_nd xs blks ->
          wx_block Γ blks ->
          sem_block Hi blks ->
          FEnv.Equiv (@EqSt _) Hi' (restrict Hi Γ) ->
          sem_block Hi' blks) ->
      VarsDefinedCompScope P_vd (Scope locs blks) xs ->
      NoDupScope P_nd xs (Scope locs blks) ->
      wx_scope wx_block Γ (Scope locs blks) ->
      sem_scope (sem_exp G) sem_block Hi bs (Scope locs blks) ->
      sem_scope (sem_exp G) sem_block (restrict Hi Γ) bs (Scope locs blks).

  Lemma sem_block_restrict {PSyn prefs} : forall (G: @global PSyn prefs) blk Γ xs H b,
      VarsDefinedComp blk xs ->
      NoDupLocals xs blk ->
      wx_block Γ blk ->
      sem_block G H b blk ->
      sem_block G (restrict H Γ) b blk.


  Lemma local_hist_dom : forall Γ locs (H H' : FEnv.t (Stream svalue)),
      dom H Γ ->
      dom H' (@senv_of_decls exp locs) ->
      dom (H + H') (Γ ++ senv_of_decls locs).

  Lemma local_hist_dom_ub : forall Γ locs (H H' : FEnv.t (Stream svalue)),
      dom_ub H Γ ->
      dom H' (@senv_of_decls exp locs) ->
      dom_ub (H + H') (Γ ++ senv_of_decls locs).

  Lemma local_hist_dom_lb : forall Γ locs (H H' : FEnv.t (Stream svalue)),
      dom_lb H Γ ->
      dom H' (@senv_of_decls exp locs) ->
      dom_lb (H + H') (Γ ++ senv_of_decls locs).

  Lemma local_hist_dom_ub_refines : forall Γ locs (H H': FEnv.t (Stream svalue)),
      (forall x, InMembers x locs -> ~IsVar Γ x) ->
      dom_ub H Γ ->
      dom H' (@senv_of_decls exp locs) ->
      H ⊑ H + H'.

  Corollary local_hist_dom_refines : forall Γ locs (H H': FEnv.t (Stream svalue)),
      (forall x, InMembers x locs -> ~IsVar Γ x) ->
      dom H Γ ->
      dom H' (@senv_of_decls exp locs) ->
      H ⊑ H + H'.