From Coq Require Import String.
From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.
From Coq Require Import Permutation.
From Coq Require Import Setoid Morphisms.

From compcert Require Import common.Errors.

From Velus Require Import Common Environment.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import AcyGraph.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax.

Lustre causality

Module Type LCAUSALITY
       (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).

Causality definition

  Inductive Is_free_left (Γ : static_env) (cx : ident) : nat -> exp -> Prop :=
  | IFLvar : forall x a,
      HasCaus Γ x cx ->
      Is_free_left Γ cx 0 (Evar x a)
  | IFLlast : forall x a,
      HasLastCaus Γ x cx ->
      Is_free_left Γ cx 0 (Elast x a)
  | IFLunop : forall op e a,
      Is_free_left Γ cx 0 e ->
      Is_free_left Γ cx 0 (Eunop op e a)
  | IFLbinop : forall op e1 e2 a,
      Is_free_left Γ cx 0 e1
      \/ Is_free_left Γ cx 0 e2 ->
      Is_free_left Γ cx 0 (Ebinop op e1 e2 a)
  | IFLextcall : forall f es a,
      (exists k, Exists (Is_free_left Γ cx k) es) ->
      Is_free_left Γ cx 0 (Eextcall f es a)
  | IFLfby : forall e0s es a k,
      Is_free_left_list Γ cx k e0s ->
      Is_free_left Γ cx k (Efby e0s es a)
  | IFLarrow : forall e0s es a k,
      Is_free_left_list Γ cx k e0s
      \/ Is_free_left_list Γ cx k es ->
      Is_free_left Γ cx k (Earrow e0s es a)
  | IFLwhen : forall es x tx b a k,
      (k < length (fst a) /\ HasCaus Γ x cx)
      \/ Is_free_left_list Γ cx k es ->
      Is_free_left Γ cx k (Ewhen es (x, tx) b a)
  | IFLmerge : forall x es ty a k,
      (k < length (fst a) /\ HasCaus Γ x cx)
      \/ Exists (fun es => Is_free_left_list Γ cx k (snd es)) es ->
      Is_free_left Γ cx k (Emerge (x, ty) es a)
  | IFLcase : forall e es d a k,
      (k < length (fst a) /\ Is_free_left Γ cx 0 e)
      \/ Exists (fun es => Is_free_left_list Γ cx k (snd es)) es
      \/ (exists d0, d = Some d0 /\ Is_free_left_list Γ cx k d0) ->
      Is_free_left Γ cx k (Ecase e es d a)
  | IFLapp : forall f es er a k,
      k < length a ->
      (exists k', Exists (Is_free_left Γ cx k') es)
      \/ (Exists (Is_free_left Γ cx 0) er) ->
      Is_free_left Γ cx k (Eapp f es er a)

  with Is_free_left_list (Γ : static_env) (cx : ident) : nat -> list exp -> Prop :=
  | IFLLnow : forall k e es,
      k < numstreams e ->
      Is_free_left Γ cx k e ->
      Is_free_left_list Γ cx k (e::es)
  | IFLLlater : forall k e es,
      k >= numstreams e ->
      Is_free_left_list Γ cx (k - numstreams e) es ->
      Is_free_left_list Γ cx k (e::es).

  Local Hint Constructors Is_free_left Is_free_left_list : lcaus.

  Definition idcaus {A B} (l : list (ident * (A * B * ident))) : list (ident * ident) :=
    map (fun '(x, (_, _, cx)) => (x, cx)) l.

  Fact idcaus_app {A B} : forall (l1 l2 : list (ident * (A * B * ident))),
      idcaus (l1 ++ l2) = idcaus l1 ++ idcaus l2.

  Fact map_fst_idcaus {A B} : forall (l1 : list (ident * (A * B * ident))),
      map fst (idcaus l1) = map fst l1.

  Global Hint Unfold idcaus : list.

  Lemma NoDupMembers_idcaus {A B} : forall (xs : list (ident * (A * B * ident))),
      NoDupMembers (idcaus xs) <-> NoDupMembers xs.

  Fact idcaus_of_senv_ins : forall xs,
      idcaus_of_senv (senv_of_ins xs) = idcaus xs.

  Definition replace_idcaus (caus : list (ident * ident)) (Γ: static_env) :=
    List.map (fun '(x, ann) => (x, or_default_with ann (ann_with_caus ann) (assoc_ident x caus))) Γ.
  Global Hint Unfold replace_idcaus : list.

  Lemma replace_idcaus_HasCaus1 : forall caus Γ x cx1 cx2,
      NoDupMembers caus ->
      In (x, cx2) caus ->
      HasCaus Γ x cx1 ->
      HasCaus (replace_idcaus caus Γ) x cx2.

  Lemma replace_idcaus_HasCaus2 : forall caus Γ x cx,
      ~InMembers x caus ->
      HasCaus Γ x cx ->
      HasCaus (replace_idcaus caus Γ) x cx.

  Lemma replace_idcaus_HasCaus3 : forall caus Γ x cx,
      HasCaus (replace_idcaus caus Γ) x cx ->
      HasCaus Γ x cx \/ In (x, cx) caus.

  Fact ann_with_caus_causl_last : forall a o,
      causl_last (or_default_with a (ann_with_caus a) o) = causl_last a.

  Lemma replace_idcaus_IsVar: forall caus Γ x,
      IsVar (replace_idcaus caus Γ) x <-> IsVar Γ x.

  Lemma replace_idcaus_HasType: forall caus Γ x ty,
      HasType (replace_idcaus caus Γ) x ty <-> HasType Γ x ty.

  Lemma replace_idcaus_HasClock: forall caus Γ x ck,
      HasClock (replace_idcaus caus Γ) x ck <-> HasClock Γ x ck.

  Lemma replace_idcaus_IsLast: forall caus Γ x,
      IsLast (replace_idcaus caus Γ) x <-> IsLast Γ x.

  Lemma replace_idcaus_HasLastCaus : forall caus Γ x ck,
      HasLastCaus (replace_idcaus caus Γ) x ck <-> HasLastCaus Γ x ck.

  Lemma map_fst_replace_idcaus : forall caus Γ,
      map fst (replace_idcaus caus Γ) = map fst Γ.

  Global Hint Rewrite -> replace_idcaus_IsVar replace_idcaus_HasType replace_idcaus_HasClock replace_idcaus_IsLast replace_idcaus_HasLastCaus : list.
  Global Hint Rewrite -> map_fst_replace_idcaus.

  Lemma replace_idcaus_HasCaus_incl caus : forall Γ Γ',
      (forall x cx, HasCaus Γ x cx -> HasCaus Γ' x cx) ->
      (forall x cx, HasCaus (replace_idcaus caus Γ) x cx -> HasCaus (replace_idcaus caus Γ') x cx).

  Lemma replace_idcaus_HasLastCaus_incl caus : forall Γ Γ',
      (forall x cx, HasLastCaus Γ x cx -> HasLastCaus Γ' x cx) ->
      (forall x cx, HasLastCaus (replace_idcaus caus Γ) x cx -> HasLastCaus (replace_idcaus caus Γ') x cx).

  Fact replace_idcaus_In_snd : forall Γ caus cx,
      In cx (map snd (idcaus_of_senv (replace_idcaus caus Γ))) ->
      In cx (map snd (idcaus_of_senv Γ)) \/ In cx (map snd caus).

  Lemma replace_idcaus_NoDup : forall Γ caus xs,
      NoDupMembers Γ ->
      NoDup (map snd (idcaus_of_senv Γ ++ caus ++ xs)) ->
      NoDup (map snd (idcaus_of_senv (replace_idcaus caus Γ) ++ xs)).

  Inductive Is_defined_in_scope {A} (Pdef : static_env -> A -> Prop) Γ (cx: ident) : scope A -> Prop :=
  | DefScope1 : forall locs blks,
      Pdef (Γ++senv_of_decls locs) blks ->
      Is_defined_in_scope Pdef Γ cx (Scope locs blks).

  Inductive Is_defined_in_branch {A} (Pdef : static_env -> A -> Prop) Γ (cx: ident) : branch A -> Prop :=
  | DefBranch1 : forall caus blks,
      Pdef (replace_idcaus caus Γ) blks ->
      Is_defined_in_branch Pdef Γ cx (Branch caus blks)
  | DefBranch2 : forall caus blks x,
      InMembers x caus ->
      HasCaus Γ x cx ->
      Is_defined_in_branch Pdef Γ cx (Branch caus blks).

  Inductive Is_defined_in Γ (cx : ident) : block -> Prop :=
  | DefEq : forall x xs es,
      In x xs ->
      HasCaus Γ x cx ->
      Is_defined_in Γ cx (Beq (xs, es))
  | DefReset : forall blocks er,
      Exists (Is_defined_in Γ cx) blocks ->
      Is_defined_in Γ cx (Breset blocks er)
  | DefSwitch : forall ec branches,
      Exists (fun blks => Is_defined_in_branch (fun Γ => Exists (Is_defined_in Γ cx)) Γ cx (snd blks)) branches ->
      Is_defined_in Γ cx (Bswitch ec branches)
  | DefAuto : forall type ini states ck,
      Exists (fun blks => Is_defined_in_branch
                         (fun Γ blks => Is_defined_in_scope
                                       (fun Γ blks => Exists (Is_defined_in Γ cx) (fst blks))
                                       Γ cx (snd blks))
                         Γ cx (snd blks)) states ->
      Is_defined_in Γ cx (Bauto type ck ini states)
  | DefLocal : forall scope,
      Is_defined_in_scope (fun Γ => Exists (Is_defined_in Γ cx)) Γ cx scope ->
      Is_defined_in Γ cx (Blocal scope).

  Inductive Is_last_in_scope {A} (Plast : A -> Prop) (cx : ident) : scope A -> Prop :=
  | LastScope1 : forall locs blks,
      Plast blks ->
      Is_last_in_scope Plast cx (Scope locs blks)
  | LastScope2 : forall locs blks x ty ck cx' e,
      In (x, (ty, ck, cx', Some (e, cx))) locs ->
      Is_last_in_scope Plast cx (Scope locs blks).

  Inductive Is_last_in_branch {A} (Plast : A -> Prop) : branch A -> Prop :=
  | LastBranch1 : forall caus blks,
      Plast blks ->
      Is_last_in_branch Plast (Branch caus blks).

  Inductive Is_last_in (cx : ident) : block -> Prop :=
  | LastReset : forall blocks er,
      Exists (Is_last_in cx) blocks ->
      Is_last_in cx (Breset blocks er)
  | LastSwitch : forall ec branches,
      Exists (fun blks => Is_last_in_branch (Exists (Is_last_in cx)) (snd blks)) branches ->
      Is_last_in cx (Bswitch ec branches)
  | LastAuto : forall type ini states ck,
      Exists (fun blks => Is_last_in_branch
                         (fun blks => Is_last_in_scope
                                     (fun blks => Exists (Is_last_in cx) (fst blks))
                                     cx (snd blks))
                         (snd blks)) states ->
      Is_last_in cx (Bauto type ck ini states)
  | LastLocal : forall scope,
      Is_last_in_scope (Exists (Is_last_in cx)) cx scope ->
      Is_last_in cx (Blocal scope).

  Inductive depends_on_last_decl Γ (cx cy : ident) : decl -> Prop :=
  | DepOnLast : forall x ty ck cl e,
      Is_free_left Γ cy 0 e ->
      depends_on_last_decl Γ cx cy (x, (ty, ck, cl, Some (e, cx))).

  Inductive depends_on_scope {A} (P_dep : _ -> _ -> _ -> _ -> Prop) Γ (cx cy : ident) : scope A -> Prop :=
  | DepOnScope1 : forall locs blks Γ',
      Γ' = Γ ++ senv_of_decls locs ->
      P_dep Γ' cx cy blks ->
      depends_on_scope P_dep Γ cx cy (Scope locs blks)
  | DepOnScope2 : forall locs blks Γ',
      Γ' = Γ ++ senv_of_decls locs ->
      Exists (depends_on_last_decl Γ' cx cy) locs ->
      depends_on_scope P_dep Γ cx cy (Scope locs blks).

  Inductive depends_on_branch {A} (P_dep : _ -> _ -> _ -> _ -> Prop) Γ (cx cy : ident) : branch A -> Prop :=
  | DepOnBranch1 : forall caus blks,
      P_dep (replace_idcaus caus Γ) cx cy blks ->
      depends_on_branch P_dep Γ cx cy (Branch caus blks)
  | DepOnBranch2 : forall caus blks x,
      HasCaus Γ x cx ->
      In (x, cy) caus ->
      depends_on_branch P_dep Γ cx cy (Branch caus blks).

  Inductive depends_on Γ (cx cy : ident) : block -> Prop :=
  | DepOnEq : forall xs es k x,
      nth_error xs k = Some x ->
      HasCaus Γ x cx ->
      Is_free_left_list Γ cy k es ->
      depends_on Γ cx cy (Beq (xs, es))

  | DepOnReset1 : forall blocks er,
      Exists (depends_on Γ cx cy) blocks ->
      depends_on Γ cx cy (Breset blocks er)
  | DepOnReset2 : forall blocks er,
      Is_defined_in Γ cx (Breset blocks er) \/ Is_last_in cx (Breset blocks er) ->
      Is_free_left Γ cy 0 er ->
      depends_on Γ cx cy (Breset blocks er)

  | DepOnSwitch1 : forall ec branches,
      Exists (fun blks => depends_on_branch (fun Γ cx cy => Exists (depends_on Γ cx cy)) Γ cx cy (snd blks)) branches ->
      depends_on Γ cx cy (Bswitch ec branches)
  | DepOnSwitch2 : forall ec branches,
      Is_defined_in Γ cx (Bswitch ec branches) \/ Is_last_in cx (Bswitch ec branches) ->
      Is_free_left Γ cy 0 ec ->
      depends_on Γ cx cy (Bswitch ec branches)

  | DepOnAuto1 : forall type ini states ck,
      Exists (fun blks => depends_on_branch
                         (fun Γ ck cy blks => depends_on_scope
                                             (fun Γ cx cy blks => Exists (depends_on Γ cx cy) (fst blks))
                                             Γ cx cy (snd blks))
                         Γ cx cy (snd blks)) states ->
      depends_on Γ cx cy (Bauto type ck ini states)
  | DepOnAuto2 : forall type ini oth states ck y,
      Is_defined_in Γ cx (Bauto type ck (ini, oth) states) \/ Is_last_in cx (Bauto type ck (ini, oth) states) ->
      Is_free_in_clock y ck ->
      HasCaus Γ y cy ->
      depends_on Γ cx cy (Bauto type ck (ini, oth) states)
  | DepOnAuto3 : forall type ini oth states ck,
      Is_defined_in Γ cx (Bauto type ck (ini, oth) states) \/ Is_last_in cx (Bauto type ck (ini, oth) states) ->
      Exists (fun '(e, _) => Is_free_left Γ cy 0 e) ini ->
      depends_on Γ cx cy (Bauto type ck (ini, oth) states)
  | DepOnAuto4 : forall type ini oth states ck,
      Is_defined_in Γ cx (Bauto type ck (ini, oth) states) \/ Is_last_in cx (Bauto type ck (ini, oth) states) ->
      Exists (fun '(_, Branch _ (unl, _)) => Exists (fun '(e, _) => Is_free_left Γ cy 0 e) unl) states ->
      depends_on Γ cx cy (Bauto type ck (ini, oth) states)

  | DepOnLocal : forall scope,
      depends_on_scope (fun Γ cx cy => Exists (depends_on Γ cx cy)) Γ cx cy scope ->
      depends_on Γ cx cy (Blocal scope).

  Inductive depends_on_node {PSyn prefs} (cx cy : ident) : @node PSyn prefs -> Prop :=
  | DepOnNode1 : forall n,
      depends_on (senv_of_ins (n_in n) ++ senv_of_decls (n_out n)) cx cy (n_block n) ->
      depends_on_node cx cy n
  | DepOnNode2 : forall n,
      Exists (depends_on_last_decl (senv_of_ins (n_in n) ++ senv_of_decls (n_out n)) cx cy) (n_out n) ->
      depends_on_node cx cy n.

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

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

  Ltac inv_block :=
    match goal with
    | H:Is_defined_in _ _ _ |- _ => inv H
    | H:Is_last_in _ _ |- _ => inv H
    | H:depends_on _ _ _ _ |- _ => inv H
    end.

  Section incl.
    Fact Is_free_left_list_incl' : forall Γ Γ' es,
      Forall (fun e => forall cx k, Is_free_left Γ cx k e -> Is_free_left Γ' cx k e) es ->
      forall cx k, Is_free_left_list Γ cx k es ->
              Is_free_left_list Γ' cx k es.

    Lemma Is_free_left_incl : forall Γ Γ' e,
        (forall x cx, HasCaus Γ x cx -> HasCaus Γ' x cx) ->
        (forall x cx, HasLastCaus Γ x cx -> HasLastCaus Γ' x cx) ->
        forall cx k, Is_free_left Γ cx k e ->
                Is_free_left Γ' cx k e.

    Fact Is_defined_in_scope_incl {A} P_def : forall locs (blk: A) Γ Γ' cx,
        (forall x cx, HasCaus Γ x cx -> HasCaus Γ' x cx) ->
        Is_defined_in_scope P_def Γ cx (Scope locs blk) ->
        (forall Γ Γ',
            (forall x cx, HasCaus Γ x cx -> HasCaus Γ' x cx) ->
            P_def Γ blk ->
            P_def Γ' blk) ->
        Is_defined_in_scope P_def Γ' cx (Scope locs blk).

    Fact Is_defined_in_branch_incl {A} P_def : forall caus (blk: A) Γ Γ' cx,
        (forall x cx, HasCaus Γ x cx -> HasCaus Γ' x cx) ->
        Is_defined_in_branch P_def Γ cx (Branch caus blk) ->
        (forall Γ Γ',
            (forall x cx, HasCaus Γ x cx -> HasCaus Γ' x cx) ->
            P_def Γ blk ->
            P_def Γ' blk) ->
        Is_defined_in_branch P_def Γ' cx (Branch caus blk).

    Lemma Is_defined_in_incl : forall blk Γ Γ',
        (forall x cx, HasCaus Γ x cx -> HasCaus Γ' x cx) ->
        forall cx, Is_defined_in Γ cx blk -> Is_defined_in Γ' cx blk.

    Fact depends_on_scope_incl {A} (P_dep : _ -> _ -> _ -> A -> Prop) : forall locs blks Γ Γ',
        (forall x cx, HasCaus Γ x cx -> HasCaus Γ' x cx) ->
        (forall x cx, HasLastCaus Γ x cx -> HasLastCaus Γ' x cx) ->
        (forall Γ Γ' cx cy,
            (forall x cx, HasCaus Γ x cx -> HasCaus Γ' x cx) ->
            (forall x cx, HasLastCaus Γ x cx -> HasLastCaus Γ' x cx) ->
            P_dep Γ cx cy blks -> P_dep Γ' cx cy blks) ->
        forall cx cy, depends_on_scope P_dep Γ cx cy (Scope locs blks) ->
                 depends_on_scope P_dep Γ' cx cy (Scope locs blks).

    Fact depends_on_branch_incl {A} (P_dep : _ -> _ -> _ -> A -> Prop) : forall caus blks Γ Γ',
        (forall x cx, HasCaus Γ x cx -> HasCaus Γ' x cx) ->
        (forall x cx, HasLastCaus Γ x cx -> HasLastCaus Γ' x cx) ->
        (forall Γ Γ' cx cy,
            (forall x cx, HasCaus Γ x cx -> HasCaus Γ' x cx) ->
            (forall x cx, HasLastCaus Γ x cx -> HasLastCaus Γ' x cx) ->
            P_dep Γ cx cy blks -> P_dep Γ' cx cy blks) ->
        forall cx cy, depends_on_branch P_dep Γ cx cy (Branch caus blks) ->
                 depends_on_branch P_dep Γ' cx cy (Branch caus blks).

    Lemma depends_on_incl : forall blk Γ Γ',
        (forall x cx, HasCaus Γ x cx -> HasCaus Γ' x cx) ->
        (forall x cx, HasLastCaus Γ x cx -> HasLastCaus Γ' x cx) ->
        forall cx cy, depends_on Γ cx cy blk -> depends_on Γ' cx cy blk.
  End incl.

  Definition idcaus_of_decls {A} locs :=
    idcaus_of_senv (@senv_of_decls A locs).

  Global Hint Unfold idcaus_of_decls : list.

  Definition idcaus_of_scope {A} f_idcaus (s : scope A) :=
    let 'Scope locs blks := s in
    idcaus_of_decls locs ++ f_idcaus blks.

  Definition idcaus_of_branch {A} f_idcaus (b : branch A) :=
    let 'Branch caus blks := b in
    caus ++ f_idcaus blks.

  Fixpoint idcaus_of_locals blk :=
    match blk with
    | Beq _ => []
    | Breset blocks _ => flat_map idcaus_of_locals blocks
    | Bswitch _ branches => flat_map (fun '(_, b) => idcaus_of_branch (flat_map idcaus_of_locals) b) branches
    | Bauto _ _ _ states => flat_map (fun '(_, b) => idcaus_of_branch (fun '(_, s) => idcaus_of_scope (fun '(blks, _) => flat_map idcaus_of_locals blks) s) b) states
    | Blocal s => idcaus_of_scope (flat_map idcaus_of_locals) s
    end.

  Global Hint Unfold idcaus_of_locals : list.

  Definition graph_of_node {PSyn prefs v a} (n : @node PSyn prefs) (g : AcyGraph v a) : Prop :=
    PS.Equal (vertices g)
             (PSP.of_list (map snd (idcaus (n_in n) ++ idcaus_of_decls (n_out n) ++ idcaus_of_locals (n_block n))))
    /\ (forall cx cy, depends_on_node cx cy n -> is_arc g cy cx).

  Definition node_causal {PSyn prefs} (n : @node PSyn prefs) :=
    NoDup (map snd (idcaus (n_in n) ++ idcaus_of_decls (n_out n) ++ idcaus_of_locals (n_block n))) /\
    exists v a (g : AcyGraph v a), graph_of_node n g.


  Lemma node_causal_NoDup {PSyn prefs} : forall (nd : @node PSyn prefs),
      node_causal nd ->
      NoDup (map snd (idcaus (n_in nd) ++ idcaus_of_decls (n_out nd))).

  Fact Is_free_left_list_length' Γ : forall es x k,
      Forall (fun e => forall x k, Is_free_left Γ x k e -> k < Datatypes.length (annot e)) es ->
      Is_free_left_list Γ x k es ->
      k < length (annots es).

  Lemma Is_free_left_length {PSyn prefs} (G: @global PSyn prefs) Γ : forall e x k,
      wl_exp G e ->
      Is_free_left Γ x k e ->
      k < length (annot e).

  Corollary Is_free_left_list_length {PSyn prefs} (G: @global PSyn prefs) Γ : forall es x k,
      Forall (wl_exp G) es ->
      Is_free_left_list Γ x k es ->
      k < length (annots es).

  Lemma Is_free_left_list_Exists Γ : forall es x k,
      Is_free_left_list Γ x k es ->
      exists k', Exists (Is_free_left Γ x k') es.

  Lemma Is_free_left_In_snd Γ : forall e x k,
      Is_free_left Γ x k e ->
      exists y, HasCaus Γ y x \/ HasLastCaus Γ y x.

  Corollary Is_free_left_list_In_snd Γ : forall es x k,
      Is_free_left_list Γ x k es ->
      exists y, HasCaus Γ y x \/ HasLastCaus Γ y x.

  Local Hint Constructors Is_defined_in : lcaus.

  Lemma Is_defined_scope_Is_defined_scope {A} P_def1 (P_def2: _ -> _ -> Prop) :
    forall locs (blk: A) x cx Γ,
      HasCaus Γ x cx ->
      Syn.Is_defined_in_scope P_def1 x (Scope locs blk) ->
      (forall Γ,
          HasCaus Γ x cx ->
          P_def1 blk ->
          P_def2 Γ blk) ->
      Is_defined_in_scope P_def2 Γ cx (Scope locs blk).

  Lemma Is_defined_branch_Is_defined_branch {A} P_def1 (P_def2: _ -> _ -> Prop) :
    forall caus (blk: A) x cx Γ,
      HasCaus Γ x cx ->
      Syn.Is_defined_in_branch P_def1 (Branch caus blk) ->
      (forall Γ,
          HasCaus Γ x cx ->
          P_def1 blk ->
          P_def2 Γ blk) ->
      Is_defined_in_branch P_def2 Γ cx (Branch caus blk).

  Lemma Is_defined_in_Is_defined_in : forall blk x cx Γ,
      HasCaus Γ x cx ->
      Syn.Is_defined_in x blk ->
      Is_defined_in Γ cx blk.

Causality check

  Section collect_free.

    Variable cenv cenvl : Env.t ident.

    Definition assemble_brs_free_left_list {A} pss (tys : list A) :=
      List.fold_left (fun ps1 ps2 => List.map (fun '(ps1, ps2) => PS.union ps1 ps2) (List.combine ps1 ps2))
                     pss (List.map (fun _ => PS.empty) tys).

    Definition collect_free_var cenv (x : ident) : ident :=
      or_default xH (Env.find x cenv).

    Fixpoint collect_free_clock (ck : clock) : PS.t :=
      match ck with
      | Cbase => PS.empty
      | Con ck x _ => PS.add (collect_free_var cenv x) (collect_free_clock ck)
      end.

    Fixpoint collect_free_left (e : exp) {struct e} : list PS.t :=
      let collect_free_left_list (es : list exp) := flat_map collect_free_left es in
      match e with
      | Econst _ | Eenum _ _ => [PS.empty]
      | Evar x _ => [PS.singleton (collect_free_var cenv x)]
      | Elast x _ => [PS.singleton (collect_free_var cenvl x)]
      | Eunop _ e _ => (collect_free_left e)
      | Ebinop _ e1 e2 _ =>
        let ps1 := collect_free_left e1 in
        let ps2 := collect_free_left e2 in
        List.map (fun '(ps1, ps2) => PS.union ps1 ps2) (List.combine ps1 ps2)
      | Eextcall _ es _ =>
          [PSUnion (collect_free_left_list es)]
      | Efby e0s _ _ =>
        collect_free_left_list e0s
      | Earrow e0s es _ =>
        let ps1 := collect_free_left_list e0s in
        let ps2 := collect_free_left_list es in
        List.map (fun '(ps1, ps2) => PS.union ps1 ps2) (List.combine ps1 ps2)
      | Ewhen es (x, _) _ _ =>
        let cx := collect_free_var cenv x in
        List.map (fun ps => PS.add cx ps) (collect_free_left_list es)
      | Emerge (x, _) es (tys, _) =>
        let ps := assemble_brs_free_left_list (List.map (fun es => collect_free_left_list (snd es)) es) tys in
        List.map (PS.add (collect_free_var cenv x)) ps
      | Ecase e es d (tys, _) =>
        let ps0 := collect_free_left e in
        let psd := or_default_with (List.map (fun _ => PS.empty) tys) collect_free_left_list d in
        let ps1 := assemble_brs_free_left_list (psd::List.map (fun es => collect_free_left_list (snd es)) es) tys in
        List.map (PS.union (nth 0 ps0 PS.empty)) ps1
      | Eapp _ es er a =>
        let ps := PSUnion (collect_free_left_list er ++ collect_free_left_list es) in
        List.map (fun _ => ps) a
      end.

    Definition collect_free_left_list (es : list exp) :=
      flat_map collect_free_left es.

  End collect_free.

  Definition unions_fuse envs := List.fold_left (Env.union_fuse PS.union) envs (@Env.empty _).

  Definition collect_depends_last_decls cenv cenvl (decls : list decl) :=
    Env.from_list
      (map_filter (fun '(_, (_, ck, _, o)) =>
                     option_map (fun '(e, cx) => (cx, nth 0 (collect_free_left cenv cenvl e) PS.empty)) o) decls).

  Definition collect_depends_scope {A} (f_coll : _ -> _ -> A -> Env.t PS.t) (cenv cenvl : Env.t ident) (s : scope A) :=
    let 'Scope locs blks := s in
    let cenv' := Env.adds' (map (fun '(x, (_, _, cx, _)) => (x, cx)) locs) cenv in
    let cenvl' := Env.adds' (map_filter (fun '(x, (_, _, _, o)) => option_map (fun '(_, cx) => (x, cx)) o) locs) cenvl in
    let deps1 := f_coll cenv' cenvl' blks in
    let deps2 := collect_depends_last_decls cenv' cenvl' locs in
    Env.union_fuse PS.union deps1 deps2.

  Definition collect_depends_branch {A} (f_coll : _ -> _ -> A -> Env.t PS.t) (cenv cenvl : Env.t ident) (s : branch A) :=
    let 'Branch caus blks := s in
    let cenv' := Env.mapi (fun x cx => or_default cx (assoc_ident x caus)) cenv in
    let deps1 := f_coll cenv' cenvl blks in
    let deps2 := Env.from_list (map (fun '(x, cx) => (or_default x (Env.find x cenv), PS.singleton cx)) caus) in
    Env.union_fuse PS.union deps1 deps2.

  Fixpoint collect_depends_on (cenv cenvl : Env.t ident) (d : block) : Env.t PS.t :=
    match d with
    | Beq (xs, es) =>
      Env.from_list
        (List.combine
           (List.map (collect_free_var cenv) xs)
           (collect_free_left_list cenv cenvl es))
    | Breset blocks er =>
      let pr := collect_free_left cenv cenvl er in
      Env.map (fun ps => PS.union (nth 0 pr PS.empty) ps)
              (unions_fuse (map (collect_depends_on cenv cenvl) blocks))
    | Bswitch ec branches =>
      let pc := collect_free_left cenv cenvl ec in
      Env.map (fun ps => PS.union (nth 0 pc PS.empty) ps)
              (unions_fuse (map (fun blks =>
                                   collect_depends_branch
                                     (fun cenv cenvl blks => unions_fuse (map (collect_depends_on cenv cenvl) blks)) cenv cenvl (snd blks)) branches))
    | Bauto _ ck (ini, oth) states =>
        let pc1 := collect_free_clock cenv ck in
        let pc2 := PSUnion (map (fun '(e, _) => nth 0 (collect_free_left cenv cenvl e) PS.empty) ini) in
        let pc3 := PSUnion (map (fun '(_, Branch _ (unl, _)) => PSUnion (map (fun '(e, _) => nth 0 (collect_free_left cenv cenvl e) PS.empty) unl)) states) in
        let pc := PS.union pc1 (PS.union pc2 pc3) in
        Env.map (fun ps => PS.union pc ps)
                (unions_fuse (map (fun '(_, br) =>
                                     collect_depends_branch
                                       (fun cenv cenvl '(_, blks) =>
                                          collect_depends_scope
                                            (fun cenv cenvl blks => unions_fuse (map (collect_depends_on cenv cenvl) (fst blks)))
                                            cenv cenvl blks) cenv cenvl br) states))
    | Blocal scope =>
        collect_depends_scope (fun cenv' cenvl' blks => unions_fuse (map (collect_depends_on cenv' cenvl') blks))
                              cenv cenvl scope
    end.

  Definition build_graph {PSyn prefs} (n : @node PSyn prefs) : Env.t PS.t :=
    let cenv := Env.from_list (idcaus (n_in n) ++ map (fun '(x, (_, _, cx, _)) => (x, cx)) (n_out n)) in
    let cenvl := Env.from_list (map_filter (fun '(x, (_, _, _, o)) => option_map (fun '(_, cx) => (x, cx)) o) (n_out n)) in
    let indeps := Env.from_list (map (fun '(_, (_, _, cx)) => (cx, PS.empty)) (n_in n)) in
    let blkdeps := collect_depends_on cenv cenvl (n_block n) in
    let lastdeps := collect_depends_last_decls cenv cenvl (n_out n) in
    unions_fuse [indeps; blkdeps; lastdeps].

  Section msgs_of_labels.

    Definition msgs_of_decl (x : ident * (type * clock * ident * option (exp * ident))) :=
      let '(x, (_, _, cx, o)) := x in
      (cx, [CTX x])::
        (match o with
         | None => []
         | Some (_, clx) => [(clx, [MSG "last "; CTX x])]
         end).

    Definition msg_of_caus (tag : ident) (x : ident * ident) :=
      let '(x, cx) := x in
      (cx, CTX x::MSG "(" :: CTX tag :: msg ")").

    Definition enum_nth_constructor (ty : type) k :=
      match ty with
      | Tenum _ tys => List.nth k tys xH
      | _ => xH
      end.

    Fixpoint msgs_of_local_labels (blk : block) : Env.t errmsg :=
      match blk with
      | Beq _ => Env.empty _
      | Breset blks _ => Env.unions (map msgs_of_local_labels blks)
      | Bswitch e brs =>
          let ty := List.hd bool_velus_type (typeof e) in
          Env.unions (map (fun '(k, Branch caus blks) =>
                             let tag := enum_nth_constructor ty k in
                             Env.adds' (map (msg_of_caus tag) caus)
                               (Env.unions (map msgs_of_local_labels blks))) brs)
      | Bauto _ _ _ states =>
          Env.unions (map (fun '((_, tag), Branch caus (_, Scope locs (blks, _))) =>
                             Env.adds'
                                  (map (msg_of_caus tag) caus++flat_map msgs_of_decl locs)
                                  (Env.unions (map msgs_of_local_labels blks))
                        ) states)
      | Blocal (Scope locs blks) =>
          Env.adds' (flat_map msgs_of_decl locs)
            (Env.unions (map msgs_of_local_labels blks))
      end.

    Definition msgs_of_ins (x : ident * (type * clock * ident)) :=
      let '(x, (_, _, cx)) := x in
      (cx, [CTX x]).

    Definition msgs_of_labels {PSyn prefs} (n : @node PSyn prefs) : Env.t errmsg :=
      Env.adds' (map msgs_of_ins (n_in n) ++ flat_map msgs_of_decl (n_out n))
        (msgs_of_local_labels (n_block n)).

  End msgs_of_labels.

  Definition check_node_causality {PSyn prefs} (n : @node PSyn prefs) : res unit :=
    let idcaus := (map snd (idcaus (n_in n) ++ idcaus_of_decls (n_out n) ++ idcaus_of_locals (n_block n))) in
    let graph := build_graph n in
    if check_nodup idcaus
       && PS.equal (PSP.of_list idcaus) (PSP.of_list (map fst (Env.elements graph))) then
      match build_acyclic_graph (Env.map PSP.to_list graph) (fun _ => msgs_of_labels n) with
      | OK _ => OK tt
      | Error msg => Error (MSG "Node " :: (CTX (n_name n)) :: MSG " : " :: msg)
      end
    else Error (MSG "Node " :: (CTX (n_name n)) :: MSG " has duplicated causality annotations" :: nil).

  Definition check_causality {PSyn prefs} (G : @global PSyn prefs) :=
    mmap check_node_causality (nodes G).

  Fact collect_free_left_list_length' cenv cenv' : forall es,
      Forall (fun e => length (collect_free_left cenv cenv' e) = length (annot e)) es ->
      length (collect_free_left_list cenv cenv' es) = length (annots es).

  Fact assemble_brs_free_left_list_length {A} : forall pss (tys : list A),
      Forall (fun ps => length ps = length tys) pss ->
      length (assemble_brs_free_left_list pss tys) = length tys.

  Lemma collect_free_left_length {PSyn prefs} : forall (G: @global PSyn prefs) cenv cenv' e,
      wl_exp G e ->
      length (collect_free_left cenv cenv' e) = length (annot e).

  Corollary collect_free_left_list_length {PSyn prefs} : forall (G: @global PSyn prefs) cenv cenv' es,
      Forall (wl_exp G) es ->
      length (collect_free_left_list cenv cenv' es) = length (annots es).

  Section collect_free_spec.

    Variable Γ : static_env.
    Variable cenv' cenvl' : Env.t ident.

    Hypothesis Heq : forall x cx, Env.find x cenv' = Some cx <-> HasCaus Γ x cx.
    Hypothesis Heql : forall x cx, Env.find x cenvl' = Some cx <-> HasLastCaus Γ x cx.

    Lemma collect_free_var_correct : forall x cx,
        InMembers x Γ ->
        collect_free_var cenv' x = cx ->
        HasCaus Γ x cx.

    Hypothesis Hnd1 : NoDupMembers Γ.

    Lemma collect_free_var_complete : forall x cx,
        HasCaus Γ x cx ->
        collect_free_var cenv' x = cx.

    Lemma collect_free_last_complete : forall x cx,
        HasLastCaus Γ x cx ->
        collect_free_var cenvl' x = cx.

    Lemma collect_free_left_list_spec' {PSyn prefs} : forall (G: @global PSyn prefs) es x k,
        Forall (wl_exp G) es ->
        Forall (wx_exp Γ) es ->
        Forall (fun e => forall k, wl_exp G e -> wx_exp Γ e ->
                           Is_free_left Γ x k e ->
                           PS.In x (nth k (collect_free_left cenv' cenvl' e) PS.empty)) es ->
        Is_free_left_list Γ x k es ->
        PS.In x (List.nth k (collect_free_left_list cenv' cenvl' es) PS.empty).

    Lemma psunion_collect_free_list_spec' {PSyn prefs} : forall (G: @global PSyn prefs) es x,
        Forall (wl_exp G) es ->
        Forall (wx_exp Γ) es ->
        Forall (fun e => forall k, wl_exp G e ->
                           wx_exp Γ e->
                           Is_free_left Γ x k e ->
                           PS.In x (nth k (collect_free_left cenv' cenvl' e) PS.empty)) es ->
        (exists k', Exists (Is_free_left Γ x k') es) ->
        PS.In x (PSUnion (collect_free_left_list cenv' cenvl' es)).

    Fact ps_In_k_lt : forall x l k,
        PS.In x (nth k l PS.empty) ->
        k < length l.

    Lemma Exists_Exists_Is_free {PSyn prefs} : forall (G: @global PSyn prefs) es x k,
      Forall (wl_exp G) es ->
      Forall (fun e => numstreams e = 1) es ->
      Exists (Is_free_left Γ x k) es ->
      Exists (Is_free_left Γ x 0) es.
    Local Hint Resolve Exists_Exists_Is_free : lcaus.

    Fact assemble_brs_free_left_list_spec: forall x k pss (tys : list type),
        Forall (fun ps => length ps = length tys) pss ->
        Exists (fun ps => PS.In x (List.nth k ps PS.empty)) pss ->
        PS.In x (List.nth k (assemble_brs_free_left_list pss tys) PS.empty).

    Fact collect_free_left_spec {PSyn prefs}: forall (G: @global PSyn prefs) x e k,
        wl_exp G e ->
        wx_exp Γ e ->
        Is_free_left Γ x k e ->
        PS.In x (List.nth k (collect_free_left cenv' cenvl' e) PS.empty).

    Corollary collect_free_left_list_spec {PSyn prefs} : forall (G: @global PSyn prefs) es x k,
        Forall (wl_exp G) es ->
        Forall (wx_exp Γ) es ->
        Is_free_left_list Γ x k es ->
        PS.In x (List.nth k (collect_free_left_list cenv' cenvl' es) PS.empty).

  End collect_free_spec.

  Lemma unions_fuse_PS_In : forall x envs,
      Env.In x (unions_fuse envs) <-> Exists (Env.In x) envs.

  Fact equiv_env_scope {A} : forall Γ locs cenv',
      NoDupMembers locs ->
      (forall x, InMembers x locs -> ~In x (map fst Γ)) ->
      (forall x cx, Env.find x cenv' = Some cx <-> HasCaus Γ x cx) ->
      (forall x cx, Env.find x (Env.adds' (map (fun '(x1, (_, _, cx1, _)) => (x1, cx1)) locs) cenv') = Some cx
               <-> HasCaus (Γ ++ @senv_of_decls A locs) x cx).

  Lemma collect_depends_scope_dom {A} P_vd P_nd (P_wl: A -> _) P_wx f_coll P_def P_last
        {PSyn prefs} (G: @global PSyn prefs) :
    forall locs blks xs Γ cenv' cenvl' cx,
      NoDupMembers Γ ->
      (forall x cx, Env.find x cenv' = Some cx <-> HasCaus Γ x cx) ->
      incl xs (map fst Γ) ->
      VarsDefinedCompScope P_vd (Scope locs blks) xs ->
      NoDupScope P_nd (map fst Γ) (Scope locs blks) ->
      wl_scope P_wl G (Scope locs blks) ->
      wx_scope P_wx Γ (Scope locs blks) ->
      Is_defined_in_scope P_def Γ cx (Scope locs blks) \/ Is_last_in_scope P_last cx (Scope locs blks) ->
      (forall Γ xs cenv' cenvl',
          NoDupMembers Γ ->
          (forall x cx, Env.find x cenv' = Some cx <-> HasCaus Γ x cx) ->
          incl xs (map fst Γ) ->
          P_vd blks xs ->
          P_nd (map fst Γ) blks ->
          P_wl blks ->
          P_wx Γ blks ->
          P_def Γ blks \/ P_last blks ->
          Env.In cx (f_coll cenv' cenvl' blks)) ->
      (forall Γ Γ',
          (forall x, IsVar Γ x -> IsVar Γ' x) ->
          (forall x, IsLast Γ x -> IsLast Γ' x) ->
          P_wx Γ blks -> P_wx Γ' blks) ->
      Env.In cx (collect_depends_scope f_coll cenv' cenvl' (Scope locs blks)).

  Fact equiv_env_branch : forall Γ caus cenv',
      (forall x cx, Env.find x cenv' = Some cx <-> HasCaus Γ x cx) ->
      (forall x cx, Env.find x (Env.mapi (fun x cx => or_default cx (assoc_ident x caus)) cenv') = Some cx
               <-> HasCaus (replace_idcaus caus Γ) x cx).

  Lemma collect_depends_branch_dom {A} P_vd P_nd (P_wl: A -> _) P_wx f_coll P_def P_last
        {PSyn prefs} (G: @global PSyn prefs) :
    forall caus blks xs Γ cenv' cenvl' cx,
      NoDupMembers Γ ->
      (forall x cx, Env.find x cenv' = Some cx <-> HasCaus Γ x cx) ->
      incl xs (map fst Γ) ->
      VarsDefinedCompBranch P_vd (Branch caus blks) xs ->
      NoDupBranch P_nd (Branch caus blks) ->
      wl_branch P_wl (Branch caus blks) ->
      wx_branch P_wx (Branch caus blks) ->
      Is_defined_in_branch P_def Γ cx (Branch caus blks) \/ Is_last_in_branch P_last (Branch caus blks) ->
      (forall Γ' xs cenv' cenvl',
          NoDupMembers Γ' ->
          (forall x cx, Env.find x cenv' = Some cx <-> HasCaus Γ' x cx) ->
          incl xs (map fst Γ') ->
          (forall x, IsVar Γ x <-> IsVar Γ' x) ->
          (forall x, IsLast Γ x -> IsLast Γ' x) ->
          P_vd blks xs ->
          P_nd blks ->
          P_wl blks ->
          P_wx blks ->
          P_def Γ' blks \/ P_last blks ->
          Env.In cx (f_coll cenv' cenvl' blks)) ->
      Env.In cx (collect_depends_branch f_coll cenv' cenvl' (Branch caus blks)).

  Lemma collect_depends_on_dom {PSyn prefs} (G: @global PSyn prefs) : forall blk xs Γ cenv' cenvl' cx,
      NoDupMembers Γ ->
      (forall x cx, Env.find x cenv' = Some cx <-> HasCaus Γ x cx) ->
      VarsDefinedComp blk xs ->
      incl xs (map fst Γ) ->
      NoDupLocals (map fst Γ) blk ->
      wl_block G blk ->
      wx_block Γ blk ->
      Is_defined_in Γ cx blk \/ Is_last_in cx blk ->
      Env.In cx (collect_depends_on cenv' cenvl' blk).

  Lemma unions_fuse_Subset : forall x envs e ps,
      In e envs ->
      Env.find x e = Some ps ->
      exists ps', Env.find x (unions_fuse envs) = Some ps' /\ PS.Subset ps ps'.

  Lemma collect_free_var_nodup: forall xs cenv',
      Forall (fun x => Env.In x cenv') xs ->
      NoDup xs ->
      NoDup (map snd (Env.elements cenv')) ->
      NoDup (map (collect_free_var cenv') xs).

  Fact NoDup_locals_inv : forall blks blk xs,
      In blk blks ->
      NoDup (map snd (xs ++ flat_map idcaus_of_locals blks)) ->
      NoDup (map snd (xs ++ idcaus_of_locals blk)).

  Fact NoDup_locals_inv2 {A B} (f_idcaus : B -> list (ident * ident)) : forall (brs : list (A * B)) k blks xs,
      In (k, blks) brs ->
      NoDup (map snd (xs ++ flat_map (fun '(_, blks) => f_idcaus blks) brs)) ->
      NoDup (map snd (xs ++ f_idcaus blks)).

  Fact NoDup_locals_inv3 {A B T} (f_idcaus : B -> list (ident * ident)) : forall (brs : list (A * (T * B))) k trans blks xs,
      In (k, (trans, blks)) brs ->
      NoDup (map snd (xs ++ flat_map (fun '(_, (_, blks)) => f_idcaus blks) brs)) ->
      NoDup (map snd (xs ++ f_idcaus blks)).

  Fact map_fst_map_filter : forall (locs : list (ident * (type * clock * ident * option _))),
      map fst (map_filter (fun '(x0, (_, _, _, o)) => option_map (fun '(_, cx) => (x0, cx)) o) locs) =
      map_filter (fun '(x0, (_, _, o)) => option_map (fun _ : exp * ident => x0) o) locs.

  Fact equiv_env_last_scope {A} : forall Γ locs cenv',
      NoDupMembers locs ->
      (forall x, InMembers x locs -> ~In x (map fst Γ)) ->
      (forall x cx, Env.find x cenv' = Some cx <-> HasLastCaus Γ x cx) ->
      (forall x cx, Env.find x (Env.adds' (map_filter (fun '(x2, (_, _, _, o)) => option_map (fun '(_, cx0) => (x2, cx0)) o) locs) cenv') = Some cx
               <-> HasLastCaus (Γ ++ @senv_of_decls A locs) x cx).

  Fact equiv_env_last_branch : forall Γ caus cenv',
      (forall x cx, Env.find x cenv' = Some cx <-> HasLastCaus Γ x cx) ->
      (forall x cx, Env.find x cenv' = Some cx
               <-> HasLastCaus (replace_idcaus caus Γ) x cx).

  Fact collect_free_clock_spec : forall Γ cenv x cx ck,
      (forall x cx, Env.find x cenv = Some cx <-> HasCaus Γ x cx) ->
      Is_free_in_clock x ck ->
      HasCaus Γ x cx ->
      PS.In cx (collect_free_clock cenv ck).

  Fact find_caus_NoDupMembers cenv : forall caus,
    NoDup (map snd (Env.elements cenv)) ->
    NoDupMembers caus ->
    Forall (fun '(x, _) => Env.In x cenv) caus ->
    NoDupMembers (map (fun '(x, cx) => (or_default x (Env.find x cenv), PS.singleton cx)) caus).

  Fact find_caus_NoDup cenv : forall (caus: list (ident * ident)),
      NoDup (map snd cenv) ->
      NoDupMembers cenv ->
      Forall (fun '(_, x) => ~In x (map snd caus)) cenv ->
      NoDup (map snd caus) ->
      NoDup (map snd (map (fun '(x0, y0) => (x0, or_default y0 (assoc_ident x0 caus))) cenv)).

  Lemma collect_depends_last_spec {PSyn prefs} (G: @global PSyn prefs) : forall Γ cenv cenvl cx cy decls,
      (forall x cx, Env.find x cenv = Some cx <-> HasCaus Γ x cx) ->
      (forall x cx, Env.find x cenvl = Some cx <-> HasLastCaus Γ x cx) ->
      NoDup (map snd (idcaus_of_decls decls)) ->
      NoDupMembers decls ->
      Forall (fun '(_, (_, _, _, o)) => LiftO True (fun '(e, _) => wl_exp G e /\ numstreams e = 1) o) decls ->
      Forall (fun '(_, (_, _, _, o)) => LiftO True (fun '(e, _) => wx_exp Γ e) o) decls ->
      Exists (depends_on_last_decl Γ cx cy) decls ->
      exists s, Env.MapsTo cx s (collect_depends_last_decls cenv cenvl decls) /\ PS.In cy s.


  Lemma collect_depends_scope_spec {A} f_idcaus P_vd P_nd P_wl P_wx P_dep f_dep {PSyn prefs} (G: @global PSyn prefs) :
    forall x y locs (blks: A) xs Γ cenv' cenvl',
      NoDupMembers Γ ->
      (forall x cx, Env.find x cenv' = Some cx <-> HasCaus Γ x cx) ->
      (forall x cx, Env.find x cenvl' = Some cx <-> HasLastCaus Γ x cx) ->
      NoDup (map snd (Env.elements cenv' ++ Env.elements cenvl' ++ idcaus_of_scope f_idcaus (Scope locs blks))) ->
      VarsDefinedCompScope P_vd (Scope locs blks) xs ->
      NoDup xs ->
      Forall (fun x => Env.In x cenv') xs ->
      NoDupScope P_nd (map fst Γ) (Scope locs blks) ->
      wl_scope P_wl G (Scope locs blks) ->
      wx_scope P_wx Γ (Scope locs blks) ->
      depends_on_scope P_dep Γ x y (Scope locs blks) ->
      (forall xs Γ cenv' cenvl',
          NoDupMembers Γ ->
          (forall x cx, Env.find x cenv' = Some cx <-> HasCaus Γ x cx) ->
          (forall x cx, Env.find x cenvl' = Some cx <-> HasLastCaus Γ x cx) ->
          NoDup (map snd (Env.elements cenv' ++ Env.elements cenvl' ++ f_idcaus blks)) ->
          P_vd blks xs ->
          NoDup xs ->
          Forall (fun x => Env.In x cenv') xs ->
          P_nd (map fst Γ) blks ->
          P_wl blks ->
          P_wx Γ blks ->
          P_dep Γ x y blks ->
          exists s, Env.MapsTo x s (f_dep cenv' cenvl' blks) /\ PS.In y s) ->
      exists s, Env.MapsTo x s (collect_depends_scope f_dep cenv' cenvl' (Scope locs blks)) /\ PS.In y s.

  Lemma collect_depends_branch_spec {A} f_idcaus P_vd P_nd P_wl P_wx P_dep f_dep {PSyn prefs} (G: @global PSyn prefs) :
    forall x y caus (blks: A) xs Γ cenv' cenvl',
      NoDupMembers Γ ->
      (forall x cx, Env.find x cenv' = Some cx <-> HasCaus Γ x cx) ->
      (forall x cx, Env.find x cenvl' = Some cx <-> HasLastCaus Γ x cx) ->
      NoDup (map snd (Env.elements cenv' ++ Env.elements cenvl' ++ idcaus_of_branch f_idcaus (Branch caus blks))) ->
      VarsDefinedCompBranch P_vd (Branch caus blks) xs ->
      NoDup xs ->
      Forall (fun x => Env.In x cenv') xs ->
      NoDupBranch P_nd (Branch caus blks) ->
      wl_branch P_wl (Branch caus blks) ->
      wx_branch P_wx (Branch caus blks) ->
      depends_on_branch P_dep Γ x y (Branch caus blks) ->
      (forall xs Γ' cenv' cenvl',
          NoDupMembers Γ' ->
          (forall x cx, Env.find x cenv' = Some cx <-> HasCaus Γ' x cx) ->
          (forall x cx, Env.find x cenvl' = Some cx <-> HasLastCaus Γ' x cx) ->
          (forall x, IsVar Γ x <-> IsVar Γ' x) ->
          (forall x, IsLast Γ x -> IsLast Γ' x) ->
          NoDup (map snd (Env.elements cenv' ++ Env.elements cenvl' ++ f_idcaus blks)) ->
          P_vd blks xs ->
          NoDup xs ->
          Forall (fun x => Env.In x cenv') xs ->
          P_nd blks ->
          P_wl blks ->
          P_wx blks ->
          P_dep Γ' x y blks ->
          exists s, Env.MapsTo x s (f_dep cenv' cenvl' blks) /\ PS.In y s) ->
      exists s, Env.MapsTo x s (collect_depends_branch f_dep cenv' cenvl' (Branch caus blks)) /\ PS.In y s.

  Lemma collect_depends_on_spec {PSyn prefs} : forall (G: @global PSyn prefs) x y blk xs Γ cenv' cenvl',
      NoDupMembers Γ ->
      (forall x cx, Env.find x cenv' = Some cx <-> HasCaus Γ x cx) ->
      (forall x cx, Env.find x cenvl' = Some cx <-> HasLastCaus Γ x cx) ->
      NoDup (map snd (Env.elements cenv' ++ Env.elements cenvl' ++ idcaus_of_locals blk)) ->
      VarsDefinedComp blk xs ->
      NoDup xs ->
      Forall (fun x => Env.In x cenv') xs ->
      NoDupLocals (map fst Γ) blk ->
      wl_block G blk ->
      wx_block Γ blk ->
      depends_on Γ x y blk ->
      exists s, Env.MapsTo x s (collect_depends_on cenv' cenvl' blk) /\ PS.In y s.

  Local Hint Constructors Is_defined_in : lcaus.

  Fact Is_free_in_clock_In Γ : forall x ck,
      wx_clock Γ ck ->
      Is_free_in_clock x ck ->
      IsVar Γ x.

  Lemma Is_free_left_In Γ Γ' : forall e k x cx,
      NoDup (map snd (idcaus_of_senv Γ)) ->
      HasCaus Γ x cx \/ HasLastCaus Γ x cx ->
      wx_exp Γ' e ->
      Is_free_left Γ cx k e ->
      IsVar Γ' x.

  Lemma depends_scope_In {A} f_idcaus P_vd P_nd P_wx P_dep : forall locs (blks: A) Γ Γ' xs cy x cx,
      NoDupMembers Γ ->
      NoDup (map snd (idcaus_of_senv Γ ++ idcaus_of_scope f_idcaus (Scope locs blks))) ->
      incl xs (map fst Γ') ->
      HasCaus Γ x cx \/ HasLastCaus Γ x cx ->
      VarsDefinedCompScope P_vd (Scope locs blks) xs ->
      NoDupScope P_nd (map fst Γ) (Scope locs blks) ->
      wx_scope P_wx Γ' (Scope locs blks) ->
      depends_on_scope P_dep Γ cy cx (Scope locs blks) ->
      (forall Γ Γ' xs,
          NoDupMembers Γ ->
          NoDup (map snd (idcaus_of_senv Γ ++ f_idcaus blks)) ->
          incl xs (map fst Γ') ->
          HasCaus Γ x cx \/ HasLastCaus Γ x cx ->
          P_vd blks xs ->
          P_nd (map fst Γ) blks ->
          P_wx Γ' blks ->
          P_dep Γ cy cx blks ->
          IsVar Γ' x) ->
      IsVar Γ' x.

  Lemma depends_branch_In {A} f_idcaus P_vd P_nd P_wx P_dep : forall caus (blks: A) Γ1 Γ2 xs cy x cx,
      NoDupMembers Γ1 ->
      NoDup (map snd (idcaus_of_senv Γ1 ++ idcaus_of_branch f_idcaus (Branch caus blks))) ->
      incl xs (map fst Γ2) ->
      HasCaus Γ1 x cx \/ HasLastCaus Γ1 x cx ->
      VarsDefinedCompBranch P_vd (Branch caus blks) xs ->
      NoDupBranch P_nd (Branch caus blks) ->
      wx_branch P_wx (Branch caus blks) ->
      depends_on_branch P_dep Γ1 cy cx (Branch caus blks) ->
      (forall Γ1' xs,
          NoDupMembers Γ1' ->
          NoDup (map snd (idcaus_of_senv Γ1' ++ f_idcaus blks)) ->
          incl xs (map fst Γ2) ->
          HasCaus Γ1' x cx \/ HasLastCaus Γ1' x cx ->
          (forall x, IsVar Γ1 x <-> IsVar Γ1' x) ->
          (forall x, IsLast Γ1 x -> IsLast Γ1' x) ->
          P_vd blks xs ->
          P_nd blks ->
          P_wx blks ->
          P_dep Γ1' cy cx blks ->
          IsVar Γ2 x) ->
      IsVar Γ2 x.

  Lemma depends_on_In : forall blk Γ Γ' xs cy x cx,
      NoDupMembers Γ ->
      NoDup (map snd (idcaus_of_senv Γ ++ idcaus_of_locals blk)) ->
      incl xs (map fst Γ') ->
      HasCaus Γ x cx \/ HasLastCaus Γ x cx ->
      VarsDefinedComp blk xs ->
      NoDupLocals (map fst Γ) blk ->
      wx_block Γ' blk ->
      depends_on Γ cy cx blk ->
      IsVar Γ' x.

  Global Hint Constructors Is_defined_in Is_defined_in_scope Is_defined_in_branch Is_last_in Is_last_in_scope Is_last_in_branch : lcaus.
  Global Hint Constructors depends_on depends_on_scope depends_on_branch : lcaus.

  Lemma depends_scope_def_last {A} P_dep P_def P_last cy cx : forall locs (blk: A) Γ,
      depends_on_scope P_dep Γ cy cx (Scope locs blk) ->
      (forall Γ, P_dep Γ cy cx blk -> P_def Γ blk \/ P_last blk) ->
      Is_defined_in_scope P_def Γ cy (Scope locs blk)
      \/ Is_last_in_scope P_last cy (Scope locs blk).

  Lemma depends_branch_def_last {A} P_dep P_def P_last cy cx : forall caus (blk: A) Γ,
      depends_on_branch P_dep Γ cy cx (Branch caus blk) ->
      (forall Γ, P_dep Γ cy cx blk -> P_def Γ blk \/ P_last blk) ->
      Is_defined_in_branch P_def Γ cy (Branch caus blk)
      \/ Is_last_in_branch P_last (Branch caus blk).

  Lemma depends_on_def_last cy cx : forall blk Γ,
      depends_on Γ cy cx blk ->
      Is_defined_in Γ cy blk \/ Is_last_in cy blk.

  Lemma build_graph_find {prefs} : forall (G: @global complete prefs) n x y,
      wl_node G n ->
      wx_node n ->
      NoDup (map snd (idcaus (n_in n) ++ idcaus_of_decls (n_out n) ++ idcaus_of_locals (n_block n))) ->
      depends_on_node x y n ->
      exists ys, (Env.find x (build_graph n)) = Some ys /\ PS.In y ys.

  Lemma check_node_causality_correct {prefs} : forall (G: @global complete prefs) n,
      wl_node G n ->
      wx_node n ->
      check_node_causality n = OK tt ->
      node_causal n.

  Corollary check_causality_correct {prefs} : forall (G: @global complete prefs) tts,
      wl_global G ->
      wx_global G ->
      check_causality G = OK tts ->
      Forall node_causal (nodes G).

Induction lemmas over a causal node

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

    Variable Γ : static_env.

    Variable P_var : ident -> Prop.
    Variable P_exp : exp -> nat -> Prop.

    Inductive P_exps : list exp -> nat -> Prop :=
    | P_exps_now e es k :
        k < numstreams e ->
        P_exp e k ->
        P_exps (e::es) k
    | P_exps_later e es k :
        k >= numstreams e ->
        P_exps es (k-numstreams e) ->
        P_exps (e::es) k.

    Lemma Pexp_Pexps : forall es k,
        Forall (fun e => forall k, k < numstreams e
                           -> (forall x, Is_free_left Γ x k e -> P_var x)
                           -> P_exp e k) es ->
        (forall x, Is_free_left_list Γ x k es -> P_var x) ->
        k < length (annots es) ->
        P_exps es k.

    Hypothesis EconstCase : forall c,
        P_exp (Econst c) 0.

    Hypothesis EenumCase : forall k ty,
        P_exp (Eenum k ty) 0.

    Hypothesis EvarCase : forall x cx ann,
        HasCaus Γ x cx ->
        P_var cx ->
        P_exp (Evar x ann) 0.

    Hypothesis ElastCase : forall x cx ann,
        HasLastCaus Γ x cx ->
        P_var cx ->
        P_exp (Elast x ann) 0.

    Hypothesis EunopCase : forall op e1 ann,
        P_exp e1 0 ->
        P_exp (Eunop op e1 ann) 0.

    Hypothesis EbinopCase : forall op e1 e2 ann,
        P_exp e1 0 ->
        P_exp e2 0 ->
        P_exp (Ebinop op e1 e2 ann) 0.

    Hypothesis EextcallCase : forall f es ann,
        (forall k, k < length (annots es) -> P_exps es k) ->
        P_exp (Eextcall f es ann) 0.

    Hypothesis EfbyCase : forall e0s es ann k,
        k < length ann ->
        P_exps e0s k ->
        P_exp (Efby e0s es ann) k.

    Hypothesis EarrowCase : forall e0s es ann k,
        k < length ann ->
        P_exps e0s k ->
        P_exps es k ->
        P_exp (Earrow e0s es ann) k.

    Hypothesis EwhenCase : forall es x tx cx b ann k,
        k < length (fst ann) ->
        P_exps es k ->
        HasCaus Γ x cx ->
        P_var cx ->
        P_exp (Ewhen es (x, tx) b ann) k.

    Hypothesis EmergeCase : forall x cx tx es ann k,
        k < length (fst ann) ->
        HasCaus Γ x cx ->
        P_var cx ->
        Forall (fun es => P_exps (snd es) k) es ->
        P_exp (Emerge (x, tx) es ann) k.

    Hypothesis EcaseCase : forall e es d ann k,
        k < length (fst ann) ->
        P_exp e 0 ->
        Forall (fun es => P_exps (snd es) k) es ->
        LiftO True (fun d => P_exps d k) d ->
        P_exp (Ecase e es d ann) k.

    Hypothesis EappCase : forall f es er ann k,
        k < length ann ->
        (forall k, k < length (annots es) -> P_exps es k) ->
        (forall k, k < length (annots er) -> P_exps er k) ->
        P_exp (Eapp f es er ann) k.

    Fixpoint exp_causal_ind e {struct e} : forall k,
        wl_exp G e ->
        wx_exp Γ e ->
        (forall x, Is_free_left Γ x k e -> P_var x) ->
        k < numstreams e ->
        P_exp e k.

  End exp_causal_ind.

  Section node_causal_ind.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.
    Variable n : @node PSyn prefs.

    Variable P_vars : list ident -> Prop.

    Lemma causal_ind {v a} : forall (g : AcyGraph v a),
        graph_of_node n g ->
        (forall xs ys, Permutation xs ys -> P_vars xs -> P_vars ys) ->
        P_vars [] ->
        (forall x xs,
            In x (map snd (idcaus (n_in n) ++ idcaus_of_decls (n_out n))) \/ In x (map snd (idcaus_of_locals (n_block n))) ->
            P_vars xs ->
            (forall y, depends_on_node x y n -> In y xs) ->
            P_vars (x::xs)) ->
        P_vars (PS.elements (vertices g)).

    Corollary node_causal_ind :
        node_causal n ->
        (forall xs ys, Permutation xs ys -> P_vars xs -> P_vars ys) ->
        P_vars [] ->
        (forall x xs,
            In x (map snd (idcaus (n_in n) ++ idcaus_of_decls (n_out n))) \/ In x (map snd (idcaus_of_locals (n_block n))) ->
            P_vars xs ->
            (forall y, depends_on_node x y n -> In y xs) ->
            P_vars (x::xs)) ->
        P_vars (map snd (idcaus (n_in n) ++ idcaus_of_decls (n_out n) ++ idcaus_of_locals (n_block n))).
  End node_causal_ind.

End LCAUSALITY.

Module LCausalityFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (Senv : STATICENV Ids Op OpAux Cks)
       (Syn : LSYNTAX Ids Op OpAux Cks Senv)
       <: LCAUSALITY Ids Op OpAux Cks Senv Syn.
  Include LCAUSALITY Ids Op OpAux Cks Senv Syn.
End LCausalityFun.