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

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

From Coq Require Import Morphisms.
From Coq Require Import Permutation.

From Coq Require Import Program.Basics Program.Wf.
Open Scope program_scope.

Lustre clocking

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

  Definition ident_map := ident -> option ident.

  Definition WellInstantiated (bck : clock) (sub : ident_map)
                              (xc : ident * clock) (nc : nclock) : Prop :=
    sub (fst xc) = snd nc
    /\ instck bck sub (snd xc) = Some (fst nc).

  Section WellClocked.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.

    Variable G : @global PSyn prefs.
    Variable Γ : static_env.

    Inductive wc_exp : exp -> Prop :=
    | wc_Econst: forall c,
        wc_exp (Econst c)

    | wc_Eenum: forall x ty,
        wc_exp (Eenum x ty)

    | wc_Evar: forall x ty ck,
        HasClock Γ x ck ->
        wc_exp (Evar x (ty, ck))

    | wc_Elast: forall x ty ck,
        HasClock Γ x ck ->
        IsLast Γ x ->
        wc_exp (Elast x (ty, ck))

    | wc_Eunop: forall op e ty ck,
        wc_exp e ->
        clockof e = [ck] ->
        wc_exp (Eunop op e (ty, ck))

    | wc_Ebinop: forall op e1 e2 ty ck,
        wc_exp e1 ->
        wc_exp e2 ->
        clockof e1 = [ck] ->
        clockof e2 = [ck] ->
        wc_exp (Ebinop op e1 e2 (ty, ck))

    | wc_Eextcall: forall f es tyout ck,
        Forall wc_exp es ->
        Forall (eq ck) (clocksof es) ->
        clocksof es <> [] ->
        wc_exp (Eextcall f es (tyout, ck))

    | wc_Efby: forall e0s es anns,
        Forall wc_exp e0s ->
        Forall wc_exp es ->
        Forall2 eq (map snd anns) (clocksof e0s) ->
        Forall2 eq (map snd anns) (clocksof es) ->
        wc_exp (Efby e0s es anns)

    | wc_Earrow: forall e0s es anns,
        Forall wc_exp e0s ->
        Forall wc_exp es ->
        Forall2 eq (map snd anns) (clocksof e0s) ->
        Forall2 eq (map snd anns) (clocksof es) ->
        wc_exp (Earrow e0s es anns)

    | wc_Ewhen: forall es x tx ty b tys ck,
        HasClock Γ x ck ->
        Forall wc_exp es ->
        Forall (eq ck) (clocksof es) ->
        length tys = length (clocksof es) ->
        wc_exp (Ewhen es (x, tx) b (tys, (Con ck x (ty, b))))

    | wc_Emerge: forall x tx es tys ck,
        HasClock Γ x ck ->
        es <> nil ->
        Forall (fun es => Forall wc_exp (snd es)) es ->
        Forall (fun '(i, es) => Forall (eq (Con ck x (tx, i))) (clocksof es)) es ->
        Forall (fun es => length tys = length (clocksof (snd es))) es ->
        wc_exp (Emerge (x, tx) es (tys, ck))

    | wc_Ecase: forall e es d tys ck,
        wc_exp e ->
        clockof e = [ck] ->
        es <> nil ->
        Forall (fun es => Forall wc_exp (snd es)) es ->
        Forall (fun es => Forall (eq ck) (clocksof (snd es))) es ->
        Forall (fun es => length tys = length (clocksof (snd es))) es ->
        (forall d0, d = Some d0 -> Forall wc_exp d0) ->
        (forall d0, d = Some d0 -> Forall (eq ck) (clocksof d0)) ->
        (forall d0, d = Some d0 -> length tys = length (clocksof d0)) ->
        wc_exp (Ecase e es d (tys, ck))

    | wc_Eapp: forall f es er anns n bck sub,
        Forall wc_exp es ->
        Forall wc_exp er ->
        find_node f G = Some n ->
        Forall2 (WellInstantiated bck sub) (map (fun '(x, (_, ck, _)) => (x, ck)) n.(n_in)) (nclocksof es) ->
        Forall2 (WellInstantiated bck sub) (map (fun '(x, (_, ck, _, _)) => (x, ck)) n.(n_out)) (map (fun '(_, ck) => (ck, None)) anns) ->
        Forall (fun e => exists ck, clockof e = [ck]) er ->
        wc_exp (Eapp f es er anns).

    Inductive wc_equation : equation -> Prop :=
    | wc_EqApp : forall xs f es er anns n bck sub,
        Forall wc_exp es ->
        Forall wc_exp er ->
        find_node f G = Some n ->
        Forall2 (WellInstantiated bck sub) (map (fun '(x, (_, ck, _)) => (x, ck)) n.(n_in)) (nclocksof es) ->
        Forall3 (fun xck ck2 x2 => WellInstantiated bck sub xck (ck2, Some x2)) (map (fun '(x, (_, ck, _, _)) => (x, ck)) n.(n_out)) (map snd anns) xs ->
        Forall (fun e => exists ck, clockof e = [ck]) er ->
        Forall2 (HasClock Γ) xs (map snd anns) ->
        wc_equation (xs, [Eapp f es er anns])
    | wc_Eq : forall xs es,
        Forall wc_exp es ->
        Forall2 (HasClock Γ) xs (clocksof es) ->
        wc_equation (xs, es).
  End WellClocked.

  Inductive wc_scope {A} (P_wc : static_env -> A -> Prop) {PSyn prefs} (G: @global PSyn prefs) : static_env -> scope A -> Prop :=
  | wc_Scope : forall Γ locs blks,
      let Γ' := Γ ++ senv_of_decls locs in
      Forall (wc_clock (idck Γ')) (map (fun '(_, (_, ck, _, _)) => ck) locs) ->
      Forall (fun '(_, (_, ck, _, o)) => LiftO True (fun '(e, _) => wc_exp G Γ' e /\ clockof e = [ck]) o) locs ->
      P_wc Γ' blks ->
      wc_scope P_wc G Γ (Scope locs blks).

  Inductive wc_branch {A} (P_wc : A -> Prop) : branch A -> Prop :=
  | wc_Branch : forall caus blks,
      P_wc blks ->
      wc_branch P_wc (Branch caus blks).

  Inductive wc_block {PSyn prefs} (G: @global PSyn prefs) : static_env -> block -> Prop :=
  | wc_Beq : forall Γ eq,
      wc_equation G Γ eq ->
      wc_block G Γ (Beq eq)

  | wc_Breset : forall Γ blocks er ck,
      Forall (wc_block G Γ) blocks ->
      wc_exp G Γ er ->
      clockof er = [ck] ->
      wc_block G Γ (Breset blocks er)

  | wc_Bswitch : forall Γ Γ' ec branches ck,
      wc_exp G Γ ec ->
      clockof ec = [ck] ->
      branches <> [] ->
      (forall x ck', HasClock Γ' x ck' -> HasClock Γ x ck /\ ck' = Cbase) ->
      (forall x, IsLast Γ' x -> IsLast Γ x) ->
      Forall (fun blks => wc_branch (Forall (wc_block G Γ')) (snd blks)) branches ->
      wc_block G Γ (Bswitch ec branches)

  | wc_Bauto : forall Γ Γ' type ini oth states ck,
      wc_clock (idck Γ) ck ->
      states <> [] ->
      (forall x ck', HasClock Γ' x ck' -> HasClock Γ x ck /\ ck' = Cbase) ->
      (forall x, IsLast Γ' x -> IsLast Γ x) ->
      Forall (fun '(e, _) => wc_exp G Γ' e /\ clockof e = [Cbase]) ini ->
      Forall (fun blks =>
                wc_branch
                  (fun blks =>
                     Forall (fun '(e, (t, _)) => wc_exp G Γ' e /\ clockof e = [Cbase]) (fst blks)
                     /\ wc_scope (fun Γ' blks =>
                                   Forall (wc_block G Γ') (fst blks)
                                   /\ Forall (fun '(e, (t, _)) => wc_exp G Γ' e /\ clockof e = [Cbase]) (snd blks))
                         G Γ' (snd blks))
                  (snd blks)) states ->
      wc_block G Γ (Bauto type ck (ini, oth) states)

  | wc_Blocal : forall Γ s,
      wc_scope (fun Γ' => Forall (wc_block G Γ')) G Γ s ->
      wc_block G Γ (Blocal s).

  Inductive wc_node {PSyn prefs} (G: @global PSyn prefs) : @node PSyn prefs -> Prop :=
  | wc_Node : forall n,
      let Γ := senv_of_ins n.(n_in) ++ senv_of_decls n.(n_out) in
      wc_env (map (fun '(x, (_, ck, _)) => (x, ck)) n.(n_in)) ->
      wc_env (map (fun '(x, (_, ck, _)) => (x, ck)) n.(n_in) ++ map (fun '(x, (_, ck, _, _)) => (x, ck)) n.(n_out)) ->
      Forall (fun '(_, (_, ck, _, o)) => LiftO True (fun '(e, _) => wc_exp G Γ e /\ clockof e = [ck]) o) n.(n_out) ->
      wc_block G Γ n.(n_block) ->
      wc_node G n.

  Definition wc_global {PSyn prefs} : @global PSyn prefs -> Prop :=
    wt_program wc_node.

Basic properties of clocking

  Global Hint Constructors wc_exp wc_equation wc_block wc_node : lclocking.
  Global Hint Unfold wc_global wc_env : lclocking.

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

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

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

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

  Lemma wc_global_NoDup {PSyn prefs}:
    forall (g: @global PSyn prefs),
      wc_global g ->
      NoDup (map n_name (nodes g)).

  Lemma wc_find_node {PSyn prefs}:
    forall (G: @global PSyn prefs) f n,
      wc_global G ->
      find_node f G = Some n ->
      exists G', wc_node G' n.

  Global Instance wc_exp_Proper {PSyn prefs}:
    Proper (@eq (@global PSyn prefs) ==> @Permutation _
                ==> @eq exp ==> iff)
           wc_exp.

  Global Instance wc_equation_Proper {PSyn prefs}:
    Proper (@eq (@global PSyn prefs) ==> @Permutation _
                ==> @eq equation ==> iff)
           wc_equation.

  Global Instance wc_block_Proper {PSyn prefs}:
    Proper (@eq (@global PSyn prefs) ==> @Permutation _
                ==> @eq block ==> iff)
           wc_block.

  Global Instance wc_block_pointwise_Proper {PSyn prefs}:
    Proper (@eq (@global PSyn prefs) ==> @Permutation _
                ==> pointwise_relation _ iff)
           wc_block.

  Lemma wc_env_Is_free_in_clock_In : forall vars x id ck,
      wc_env vars ->
      In (x, ck) vars ->
      Is_free_in_clock id ck ->
      InMembers id vars.

  Lemma wc_env_has_Cbase':
    forall vars x xck,
      wc_env vars ->
      In (x, xck) vars ->
      exists y, In (y, Cbase) vars.

  Lemma wc_env_has_Cbase:
    forall vars,
      wc_env vars ->
      0 < length vars ->
      exists y, In (y, Cbase) vars.

  Lemma WellInstantiated_parent :
    forall bck sub cks lck,
      Forall2 (WellInstantiated bck sub) cks lck ->
      Forall (fun ck => fst ck = bck \/ clock_parent bck (fst ck)) lck.

  Lemma WellInstantiated_bck :
    forall vars bck sub lck,
      wc_env vars ->
      0 < length vars ->
      Forall2 (WellInstantiated bck sub) vars lck ->
      In bck (map stripname lck).


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

    Lemma wc_exp_incl : forall Γ Γ' e,
        (forall x ck, HasClock Γ x ck -> HasClock Γ' x ck) ->
        (forall x, IsLast Γ x -> IsLast Γ' x) ->
        wc_exp G Γ e ->
        wc_exp G Γ' e .

    Lemma wc_equation_incl : forall Γ Γ' eq,
        (forall x ck, HasClock Γ x ck -> HasClock Γ' x ck) ->
        (forall x, IsLast Γ x -> IsLast Γ' x) ->
        wc_equation G Γ eq ->
        wc_equation G Γ' eq.

    Lemma wc_scope_incl {A} P_wc : forall Γ Γ' locs (blks: A),
        (forall x ck, HasClock Γ x ck -> HasClock Γ' x ck) ->
        (forall x, IsLast Γ x -> IsLast Γ' x) ->
        wc_scope P_wc G Γ (Scope locs blks) ->
        (forall Γ Γ',
            (forall x ck, HasClock Γ x ck -> HasClock Γ' x ck) ->
            (forall x, IsLast Γ x -> IsLast Γ' x) ->
            P_wc Γ blks -> P_wc Γ' blks) ->
        wc_scope P_wc G Γ' (Scope locs blks).

    Lemma wc_block_incl : forall d Γ Γ',
        (forall x ck, HasClock Γ x ck -> HasClock Γ' x ck) ->
        (forall x, IsLast Γ x -> IsLast Γ' x) ->
        wc_block G Γ d ->
        wc_block G Γ' d .

  End incl.

Validation

  Section ValidateExpression.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.

    Variable G : @global PSyn prefs.
    Variable venv venvl : Env.t clock.
    Variable env : static_env.

    Hypothesis Henv : forall x ck, Env.find x venv = Some ck -> HasClock env x ck.
    Hypothesis Henvl : forall x ck, Env.find x venvl = Some ck -> HasClock env x ck /\ IsLast env x.

    Open Scope option_monad_scope.

    Definition check_var (x : ident) (ck : clock) : bool :=
      match Env.find x venv with
      | None => false
      | Some xc => ck ==b xc
      end.

    Definition check_last (x : ident) (ck : clock) : bool :=
      match Env.find x venvl with
      | None => false
      | Some xc => ck ==b xc
      end.

    Definition check_paired_clocks (nc1 nc2 : clock) (tc : ann) : bool :=
      match tc with
      | (t, c) => (nc1 ==b c) && (nc2 ==b c)
      end.

    Definition check_merge_clocks {A} (x : ident) (tx : type) (ck : clock) (ncs : list (enumtag * list clock)) (n : nat) (tys : list A) : bool :=
      forallb (fun '(i, ncs) => forallb (fun ck' => ck' ==b (Con ck x (tx, i))) ncs
                             && (length ncs ==b length tys)) ncs.

    Definition check_case_clocks {A} (ck : clock) (ncs : list (list clock)) (tys : list A) : bool :=
      forallb (fun ncs => forallb (fun ck' => ck' ==b ck) ncs
                       && (length ncs ==b length tys)) ncs.

    Definition add_isub
               (sub : Env.t ident)
               (nin : (ident * (type * clock * ident)))
               (nc : nclock) : Env.t ident :=
      match snd nc, nin with
      | Some y, (x, (xt, xc, xcaus)) => Env.add x y sub
      | None, _ => sub
      end.

    Definition add_osub
               (sub : Env.t ident)
               (nout : decl)
               (tnc : type * nclock) : Env.t ident :=
      let '(x, (ty, ck, cx, _)) := nout in
      add_isub sub (x, (ty, ck, cx)) (snd tnc).

    Section CheckInst.
      Variables (bck : clock) (sub : Env.t ident).

      Fixpoint check_inst (ick ck : clock) : bool :=
        match ick with
        | Cbase => (ck ==b bck)
        | Con ick' x xb =>
          match ck, Env.find x sub with
          | Con ck' y yb, Some sx =>
            (yb ==b xb) && (y ==b sx) && (check_inst ick' ck')
          | _, _ => false
          end
        end.
    End CheckInst.

    Fixpoint find_base_clock (ick ck : clock) : option clock :=
      match ick with
      | Cbase => Some ck
      | Con ick' _ _ =>
        match ck with
        | Cbase => None
        | Con ck' _ _ => find_base_clock ick' ck'
        end
      end.

    Definition check_reset (ckr : list (list clock)) : bool :=
      forallb (fun cks => match cks with [ck] => true | _ => false end) ckr.

    Lemma nclockof_clockof:
      forall e xs ys,
        nclockof e = xs ->
        ys = map fst xs ->
        clockof e = ys.

    Fixpoint check_exp (e : exp) : option (list clock) :=
      match e with
      | Econst c => Some [Cbase]

      | Eenum _ _ => Some [Cbase]

      | Evar x (xt, xc) =>
        if (check_var x xc) then Some [xc] else None

      | Elast x (xt, xc) =>
        if (check_last x xc) then Some [xc] else None

      | Eunop op e (xt, xc) =>
        do nce <- assert_singleton (check_exp e);
        if xc ==b nce then Some [xc] else None

      | Ebinop op e1 e2 (xt, xc) =>
        do nc1 <- assert_singleton (check_exp e1);
        do nc2 <- assert_singleton (check_exp e2);
        if (xc ==b nc1) && (xc ==b nc2) then Some [xc] else None

      | Eextcall f es (_, ck) =>
        do ncs <- oconcat (map check_exp es);
        if forallb (fun ck' => ck' ==b ck) ncs && negb (is_nil ncs) then Some [ck] else None


      | Efby e0s es anns =>
        do nc0s <- oconcat (map check_exp e0s);
        do ncs <- oconcat (map check_exp es);
        if forall3b check_paired_clocks nc0s ncs anns
        then Some (map snd anns) else None

      | Earrow e0s es anns =>
        do nc0s <- oconcat (map check_exp e0s);
        do ncs <- oconcat (map check_exp es);
        if forall3b check_paired_clocks nc0s ncs anns
        then Some (map snd anns) else None

      | Ewhen es (x, _) b (tys, nc) =>
        match nc with
        | Con xc y (_, yb) =>
          do nces <- oconcat (map check_exp es);
          if (x ==b y) && (b ==b yb) && (check_var x xc)
             && (forall2b (fun c _ => xc ==b c) nces tys)
          then Some (map (fun _ => nc) tys) else None
        | _ => None
        end

      | Emerge (x, tx) es (tys, ck) =>
        do ncs <- omap (fun es => oconcat (map check_exp (snd es))) es;
        if check_var x ck && check_merge_clocks x tx ck (combine (map fst es) ncs) (length es) tys
           && (negb (is_nil es))
        then Some (map (fun _ => ck) tys) else None

      | Ecase e brs d (tys, ck) =>
        do nds <- or_default_with (Some []) (fun d => do nds <- oconcat (map check_exp d); Some [nds]) d;
        do ncs <- omap (fun es => oconcat (map check_exp (snd es))) brs;
        do ce <- assert_singleton (check_exp e);
        if (ce ==b ck) && check_case_clocks ck (nds++ncs) tys
           && (negb (is_nil brs))
        then Some (map (fun _ => ck) tys) else None

      | Eapp f es er anns =>
        do n <- find_node f G;
        do _x <- oconcat (map check_exp es);
        do nr <- omap check_exp er;
        do nin0 <- option_map (fun '(_, (_, ck, _)) => ck) (hd_error n.(n_in));
        let nces := nclocksof es in
        do nces0 <- option_map fst (hd_error nces);
        do bck <- find_base_clock nin0 nces0;
        let nanns := map (fun '(ty, ck) => (ty, (ck, None))) anns in
        let isub := fold_left2 add_isub n.(n_in) nces (Env.empty ident) in
        let sub := fold_left2 add_osub n.(n_out) nanns isub in
        if (forall2b (fun '(_, (_, ck, _)) '(ck', _) => check_inst bck sub ck ck')
                     n.(n_in) nces)
           && (forall2b (fun '(_, (_, ck, _, _)) '(_, (ck', _)) => check_inst bck sub ck ck')
                        n.(n_out) nanns)
           && (check_reset nr)
        then Some (map snd anns) else None

      end.

    Definition check_equation (eq : equation) : bool :=
      let '(xs, es) := eq in
      match es with
      | [Eapp f es er anns] =>
        match
          (do n <- find_node f G;
           do _x <- oconcat (map check_exp es);
           do nr <- omap check_exp er;
           do nin0 <- option_map (fun '(_, (_, ck, _)) => ck) (hd_error n.(n_in));
           let nces := nclocksof es in
           do nces0 <- option_map fst (hd_error nces);
           do bck <- find_base_clock nin0 nces0;
           let nanns := map (fun '((ty, ck), x) => (ty, (ck, Some x))) (combine anns xs) in
           let isub := fold_left2 add_isub n.(n_in) nces (Env.empty ident) in
           let sub := fold_left2 add_osub n.(n_out) nanns isub in
           if (forall2b (fun '(_, (_, ck, _)) '(ck', _) => check_inst bck sub ck ck')
                        n.(n_in) nces)
              && (length xs ==b length anns)
              && (forall2b (fun '(_, (_, ck, _, _)) '(_, ck') => check_inst bck sub ck ck')
                           n.(n_out) anns)
              && (check_reset nr)
           then Some (map snd anns) else None)
        with
        | None => false
        | Some ncks => forall2b check_var xs ncks
        end
      | _ => match oconcat (map check_exp es) with
            | None => false
            | Some ncks => forall2b check_var xs ncks
            end
      end.

    Lemma check_var_correct:
      forall x ck,
        check_var x ck = true ->
        HasClock env x ck.

    Corollary check_vars_correct: forall xs cks,
        forall2b check_var xs cks = true ->
        Forall2 (HasClock env) xs cks.

    Lemma check_last_correct:
      forall x ck,
        check_last x ck = true ->
        HasClock env x ck /\ IsLast env x.

    Lemma check_paired_clocks_correct:
      forall cks1 cks2 anns,
        forall3b check_paired_clocks cks1 cks2 anns = true ->
        cks1 = map snd anns
        /\ cks2 = map snd anns.

    Lemma check_merge_clocks_correct:
      forall {A} x tx ck ncs n (tys : list A),
        check_merge_clocks x tx ck ncs n tys = true ->
        Forall (fun '(i, ncs) => Forall (fun ck' => (Con ck x (tx, i)) = ck') ncs) ncs /\
        Forall (fun '(_, ncs) => length ncs = length tys) ncs.

    Lemma check_case_clocks_correct:
      forall {A} ck ncs (tys : list A),
        check_case_clocks ck ncs tys = true ->
        Forall (Forall (fun ck' => ck = ck')) ncs /\
        Forall (fun ncs => length ncs = length tys) ncs.

    Lemma oconcat_map_check_exp':
      forall {f} es cks,
        (forall e cks,
            In e es ->
            f e = Some cks ->
            wc_exp G env e /\ clockof e = cks) ->
        oconcat (map f es) = Some cks ->
        Forall (wc_exp G env) es
        /\ clocksof es = cks.

    Lemma omap_concat_map_check_exp':
      forall {f} (ess : list (enumtag * _)) ncks,
        (forall es e ncks,
            In es ess ->
            In e (snd es) ->
            f e = Some ncks ->
            wc_exp G env e /\ clockof e = ncks) ->
        omap (fun es => oconcat (map f (snd es))) ess = Some ncks ->
        Forall (fun es => Forall (wc_exp G env) (snd es)) ess
        /\ Forall2 (fun es ncks => clocksof (snd es) = ncks) ess ncks.

    Lemma omap_check_exp':
      forall {f} es cks,
        (forall e cks,
            In e es ->
            f e = Some cks ->
            wc_exp G env e /\ clockof e = cks) ->
        omap f es = Some cks ->
        Forall (wc_exp G env) es
        /\ Forall2 (fun e ck => clockof e = ck) es cks.

    Lemma find_add_isub:
      forall sub x tc ck nm,
        ~Env.In x sub ->
        Env.find x (add_isub sub (x, tc) (ck, nm)) = nm.

    Lemma fold_left2_add_osub_skip:
      forall x xs anns sub,
        ~In x (map fst xs) ->
        Env.find x (fold_left2 add_osub xs anns sub) = Env.find x sub.

    Lemma fold_left2_add_isub_skip:
      forall x xs ncs sub,
        ~In x (map fst xs) ->
        Env.find x (fold_left2 add_isub xs ncs sub) = Env.find x sub.

    Lemma fold_left2_add_isub:
      forall x xt xc ck nm xs ncs sub,
        In ((x, (xt, xc)), (ck, nm)) (combine xs ncs) ->
        NoDupMembers xs ->
        ~Env.In x sub ->
        Env.find x (fold_left2 add_isub xs ncs sub) = nm.

    Lemma fold_left2_add_osub:
      forall x xt xc ty ck nm xs ans sub,
        In ((x, (xt, xc)), (ty, (ck, nm))) (combine xs ans) ->
        NoDupMembers xs ->
        ~Env.In x sub ->
        Env.find x (fold_left2 add_osub xs ans sub) = nm.

    Lemma check_inst_correct:
      forall bck xc ck sub,
        check_inst bck sub xc ck = true ->
        instck bck (fun x => Env.find x sub) xc = Some ck.

    Lemma check_reset_correct: forall cks,
        check_reset cks = true ->
        Forall (fun cks => exists ck, cks = [ck]) cks.

    Local Hint Constructors wc_exp : lclocking.
    Lemma check_exp_correct:
      forall e ncks,
        check_exp e = Some ncks ->
        wc_exp G env e
        /\ clockof e = ncks.

    Corollary omap_check_exp:
      forall es ncks,
        omap check_exp es = Some ncks ->
        Forall (wc_exp G env) es
        /\ Forall2 (fun e ck => clockof e = ck) es ncks.

    Corollary oconcat_map_check_exp:
      forall es ncks,
        oconcat (map check_exp es) = Some ncks ->
        Forall (wc_exp G env) es
        /\ clocksof es = ncks.

    Lemma check_equation_correct:
      forall eq,
        check_equation eq = true ->
        wc_equation G env eq.

    Fixpoint check_clock (ck : clock) : bool :=
      match ck with
      | Cbase => true
      | Con ck' x b =>
          check_var x ck' && check_clock ck'
      end.

    Lemma check_clock_correct : forall ck,
        check_clock ck = true ->
        wc_clock (idck env) ck.

  End ValidateExpression.

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

    Definition check_base_exp venv venvl e :=
      match check_exp G venv venvl e with
      | Some [Cbase] => true
      | _ => false
      end.

    Lemma check_base_exp_correct venv venvl env : forall e,
        (forall x ty, Env.find x venv = Some ty -> HasClock env x ty) ->
        (forall x ty, Env.find x venvl = Some ty -> HasClock env x ty /\ IsLast env x) ->
        check_base_exp venv venvl e = true ->
        wc_exp G env e /\ clockof e = [Cbase].

    Definition check_last_decl venv venvl (d : decl) :=
      let '(_, (_, ck, _, o)) := d in
      match o with
      | None => true
      | Some (e, _) => match check_exp G venv venvl e with
                      | Some [ck'] => ck' ==b ck
                      | _ => false
                      end
      end.

    Definition check_scope {A} (f_check : Env.t clock -> Env.t clock -> A -> bool)
               (venv venvl : Env.t clock) (s : scope A) : bool :=
      let 'Scope locs blks := s in
      let venv' := Env.adds' (map (fun '(x, (_, ck, _, _)) => (x, ck)) locs) venv in
      let venvl' := Env.adds' (map_filter (fun '(x, (_, ck, _, o)) => option_map (fun _ => (x, ck)) o) locs) venvl in
      forallb (check_clock venv') (map (fun '(_, (_, ck, _, _)) => ck) locs)
      && forallb (check_last_decl venv' venvl') locs
      && f_check venv' venvl' blks.

    Fixpoint check_block (venv venvl : Env.t clock) (blk : block) : bool :=
      match blk with
      | Beq eq => check_equation G venv venvl eq
      | Breset blocks er =>
        forallb (check_block venv venvl) blocks &&
        match check_exp G venv venvl er with
        | Some [ck] => true
        | _ => false
        end
      | Bswitch ec branches =>
        negb (is_nil branches) &&
        match check_exp G venv venvl ec with
        | Some [ck] =>
          let venv' := Env.map (fun _ => Cbase) (Env.Props.P.filter (fun x ck' => (ck' ==b ck)) venv) in
          let venvl' := Env.map (fun _ => Cbase) (Env.Props.P.filter (fun x ck' => (ck' ==b ck)) venvl) in
          forallb (fun '(_, Branch _ blks) => forallb (check_block venv' venvl') blks) branches
        | _ => false
        end
      | Bauto type ck (ini, oth) states =>
          let venv' := Env.map (fun _ => Cbase) (Env.Props.P.filter (fun x ck' => (ck' ==b ck)) venv) in
          let venvl' := Env.map (fun _ => Cbase) (Env.Props.P.filter (fun x ck' => (ck' ==b ck)) venvl) in
          check_clock venv ck
          && forallb (fun '(e, _) => check_base_exp venv' venvl' e) ini
          && negb (is_nil states)
          && forallb (fun '(_, Branch _ (unl, blks)) =>
                        forallb (fun '(e, _) => check_base_exp venv' venvl' e) unl
                        && check_scope (fun venv' venvl' '(blks, trans) =>
                                          forallb (check_block venv' venvl') blks
                                          && forallb (fun '(e, _) => check_base_exp venv' venvl' e) trans)
                                       venv' venvl' blks) states
      | Blocal s =>
          check_scope (fun venv' venvl' => forallb (check_block venv' venvl')) venv venvl s
      end.

    Lemma check_scope_correct {A} f_check (P_nd : _ -> _ -> Prop) (P_wc : _ -> _ -> Prop) :
      forall venv venvl env locs (blks: A),
        (forall x ty, Env.find x venv = Some ty -> HasClock env x ty) ->
        (forall x ty, Env.find x venvl = Some ty -> HasClock env x ty /\ IsLast env x) ->
        (forall venv venvl env,
            NoDupMembers env ->
            P_nd (map fst env) blks ->
            (forall x ty, Env.find x venv = Some ty -> HasClock env x ty) ->
            (forall x ty, Env.find x venvl = Some ty -> HasClock env x ty /\ IsLast env x) ->
            f_check venv venvl blks = true ->
            P_wc env blks) ->
        NoDupMembers env ->
        NoDupScope P_nd (map fst env) (Scope locs blks) ->
        check_scope f_check venv venvl (Scope locs blks) = true ->
        wc_scope P_wc G env (Scope locs blks).

    Lemma check_block_correct: forall blk venv venvl env,
        (forall x ty, Env.find x venv = Some ty -> HasClock env x ty) ->
        (forall x ty, Env.find x venvl = Some ty -> HasClock env x ty /\ IsLast env x) ->
        NoDupMembers env ->
        NoDupLocals (map fst env) blk ->
        check_block venv venvl blk = true ->
        wc_block G env blk.

  End ValidateBlock.

  Section ValidateGlobal.

    Definition check_env (env : list (ident * clock)) : bool :=
      forallb (check_clock (Env.from_list env)) (List.map snd env).

    Definition check_node {PSyn prefs} (G : @global PSyn prefs) (n : @node PSyn prefs) :=
      let ins := map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n) in
      let outs := map (fun '(x, (_, ck, _, _)) => (x, ck)) (n_out n) in
      let insouts := ins++outs in
      let venv := Env.from_list insouts in
      let venvl := Env.from_list (map_filter (fun '(x, (_, ck, _, o)) => option_map (fun _ => (x, ck)) o) (n_out n)) in
      check_env ins
      && check_env insouts
      && forallb (check_last_decl G venv venvl) (n_out n)
      && check_block G venv venvl (n_block n).

    Definition check_global {PSyn prefs} (G : @global PSyn prefs) :=
      check_nodup (List.map n_name G.(nodes)) &&
      (fix aux nds := match nds with
                      | [] => true
                      | hd::tl => check_node (update G tl) hd && aux tl
                      end) G.(nodes).

    Lemma check_env_correct : forall env,
        check_env env = true ->
        wc_env env.

    Lemma check_node_correct {PSyn prefs} : forall (G : @global PSyn prefs) n,
        check_node G n = true ->
        wc_node G n.

    Lemma check_global_correct {PSyn prefs} : forall (G : @global PSyn prefs),
        check_global G = true ->
        wc_global G.

  End ValidateGlobal.

Some additional properties related to remove_member

  Definition remove_member {B} := @remove_member _ B Common.EqDec_instance_0.

  Lemma wc_clock_nfreein_remove : forall vars id ck,
      ~Is_free_in_clock id ck ->
      wc_clock vars ck ->
      wc_clock (remove_member id vars) ck.

  Lemma wc_env_nfreein_remove : forall id vars,
      NoDupMembers vars ->
      wc_env vars ->
      Forall (fun '(_, ck) => ~Is_free_in_clock id ck) vars ->
      wc_env (remove_member id vars).

  Lemma wc_clock_nfreein_remove' : forall vars id ck ck',
      ~Is_free_in_clock id ck' ->
      wc_clock ((id, ck)::vars) ck' ->
      wc_clock vars ck'.

  Fact clock_parent_In : forall vars ck ck' id b,
      wc_clock vars ck ->
      clock_parent (Con ck' id b) ck ->
      In (id, ck') vars.

  Lemma wc_nfree_in_clock : forall vars ck id,
      NoDupMembers vars ->
      In (id, ck) vars ->
      wc_clock vars ck ->
      ~Is_free_in_clock id ck.

A clock dependency order

  Inductive dep_ordered_clocks : list (ident * clock) -> Prop :=
  | dep_ord_clock_nil : dep_ordered_clocks nil
  | dep_ord_clock_cons : forall ck id ncks,
      dep_ordered_clocks ncks ->
      ~Exists (Is_free_in_clock id) (map snd ncks) ->
      dep_ordered_clocks ((id, ck)::ncks).

  Program Fixpoint wc_env_dep_ordered (vars : list (ident * clock)) {measure (length vars)} :
      NoDupMembers vars ->
      wc_env vars ->
      exists vars', Permutation vars vars' /\ dep_ordered_clocks vars' := _.

  Fact wc_clock_dep_ordered_remove : forall id ck x xs,
      NoDupMembers (x::xs) ->
      In (id, ck) xs ->
      dep_ordered_clocks (x::xs) ->
      wc_clock (x::xs) ck ->
      wc_clock xs ck.

  Corollary wc_env_dep_ordered_remove : forall x xs,
      NoDupMembers (x::xs) ->
      dep_ordered_clocks (x::xs) ->
      wc_env (x::xs) ->
      wc_env xs.

Another equivalent clock dependency order

  Definition only_depends_on (vars : list ident) (ck : clock) :=
    forall id, Is_free_in_clock id ck -> In id vars.

  Lemma only_depends_on_Con : forall vars ck id b,
      only_depends_on vars (Con ck id b) ->
      only_depends_on vars ck.

  Lemma only_depends_on_incl : forall vars vars' ck,
      incl vars vars' ->
      only_depends_on vars ck ->
      only_depends_on vars' ck.

  Lemma wc_clock_only_depends_on : forall vars ck,
      wc_clock vars ck ->
      only_depends_on (map fst vars) ck.

  Inductive dep_ordered_on : list (ident * clock) -> Prop :=
  | dep_ordered_nil : dep_ordered_on []
  | dep_ordered_cons : forall nck ncks,
      dep_ordered_on ncks ->
      only_depends_on (map fst ncks) (snd nck) ->
      dep_ordered_on (nck::ncks).

  Lemma dep_ordered_on_InMembers : forall ncks,
      dep_ordered_on ncks ->
      Forall (fun ck => forall id, Is_free_in_clock id ck -> InMembers id ncks) (map snd ncks).

  Lemma dep_ordered_dep_ordered_on : forall ncks,
      NoDupMembers ncks ->
      wc_env ncks ->
      dep_ordered_clocks ncks ->
      dep_ordered_on ncks.

  Lemma dep_ordered_on_dep_ordered : forall ncks,
      NoDupMembers ncks ->
      wc_env ncks ->
      dep_ordered_on ncks ->
      dep_ordered_clocks ncks.

  Corollary dep_ordered_iff : forall vars,
      NoDupMembers vars ->
      wc_env vars ->
      (dep_ordered_clocks vars <-> dep_ordered_on vars).

  Corollary wc_env_dep_ordered_on_remove : forall x xs,
      NoDupMembers (x::xs) ->
      dep_ordered_on (x::xs) ->
      wc_env (x::xs) ->
      wc_env xs.

  Corollary wc_env_dep_ordered_on : forall vars,
      NoDupMembers vars ->
      wc_env vars ->
      exists vars', Permutation vars vars' /\ dep_ordered_on vars'.

  Global Instance only_depends_on_Proper:
    Proper (@Permutation.Permutation ident ==> @eq clock ==> iff)
           only_depends_on.

Additional properties about WellInstantiated

  Definition anon_streams (l : list nclock) : list (ident * clock) :=
    map_filter (fun '(ck, id) => match id with
                              | None => None
                              | Some id => Some (id, ck)
                              end) l.

  Fact WellInstantiated_sub_fsts : forall bck sub ins outs,
      Forall2 (WellInstantiated bck sub) ins outs ->
      map_filter sub (map fst ins) = (map fst (anon_streams outs)).

  Lemma instck_only_depends_on : forall vars bck bckvars sub ck ck',
      only_depends_on bckvars bck ->
      only_depends_on vars ck ->
      instck bck sub ck = Some ck' ->
      only_depends_on (bckvars++map_filter sub vars) ck'.

wc_exp implies wc_clock

  Definition preserving_sub bck (sub : ident -> option ident) (vars vars' : list (ident * clock)) dom :=
    Forall (fun i => forall i' ck ck',
                sub i = Some i' ->
                instck bck sub ck = Some ck' ->
                In (i, ck) vars ->
                In (i', ck') vars'
           ) dom.

  Fact preserving_sub_incl1 : forall bck sub vars1 vars1' vars2 dom,
      incl vars1' vars1 ->
      preserving_sub bck sub vars1 vars2 dom ->
      preserving_sub bck sub vars1' vars2 dom.

  Fact preserving_sub_incl2 : forall bck sub vars1 vars2 vars2' dom,
      incl vars2 vars2' ->
      preserving_sub bck sub vars1 vars2 dom ->
      preserving_sub bck sub vars1 vars2' dom.

  Fact preserving_sub_incl3 : forall bck sub vars vars' dom dom',
      incl dom dom' ->
      preserving_sub bck sub vars vars' dom' ->
      preserving_sub bck sub vars vars' dom.

  Global Instance preserving_sub_Proper:
    Proper (@eq clock ==> @eq (ident -> option ident)
                ==> @Permutation (ident * clock) ==> @Permutation (ident * clock) ==> @Permutation ident
                ==> iff)
           preserving_sub.

  Fixpoint frees_in_clock (ck : clock) :=
    match ck with
    | Cbase => []
    | Con ck' id _ => id::(frees_in_clock ck')
    end.

  Lemma Is_free_in_frees_in_clock : forall ck,
      Forall (fun id => Is_free_in_clock id ck) (frees_in_clock ck).

  Lemma only_depends_on_frees_in_clock : forall vars ck,
      only_depends_on vars ck ->
      incl (frees_in_clock ck) vars.

  Fact instck_wc_clock : forall vars vars' bck sub ck ck',
      wc_clock vars ck ->
      wc_clock vars' bck ->
      preserving_sub bck sub vars vars' (frees_in_clock ck) ->
      instck bck sub ck = Some ck' ->
      wc_clock vars' ck'.

  Fact WellInstantiated_wc_clock : forall vars vars' sub bck id ck ck' name,
      wc_clock vars ck ->
      wc_clock vars' bck ->
      preserving_sub bck sub vars vars' (frees_in_clock ck) ->
      WellInstantiated bck sub (id, ck) (ck', name) ->
      wc_clock vars' ck'.

  Lemma WellInstantiated_wc_clocks' : forall vars' bck sub xs ys,
      NoDupMembers xs ->
      dep_ordered_on xs ->
      wc_clock vars' bck ->
      wc_env xs ->
      Forall2 (WellInstantiated bck sub) xs ys ->
      (preserving_sub bck sub xs (anon_streams ys) (map fst xs) /\
       Forall (wc_clock (vars'++anon_streams ys)) (map fst ys)).

  Corollary WellInstantiated_wc_clocks : forall vars' bck sub xs ys,
      NoDupMembers xs ->
      wc_clock vars' bck ->
      wc_env xs ->
      Forall2 (WellInstantiated bck sub) xs ys ->
      Forall (wc_clock (vars'++anon_streams ys)) (map fst ys).

  Lemma wc_exp_nclockof_In {PSyn prefs} : forall (G: @global PSyn prefs) Γ e,
      wc_exp G Γ e ->
      Forall (fun '(ck, o) => LiftO True (fun x => HasClock Γ x ck) o) (nclockof e).

  Corollary wc_exps_nclocksof_In {PSyn prefs} : forall (G: @global PSyn prefs) Γ es,
      Forall (wc_exp G Γ) es ->
      Forall (fun '(ck, o) => LiftO True (fun x => HasClock Γ x ck) o) (nclocksof es).

  Lemma wc_exp_clockof {PSyn prefs} : forall (G: @global PSyn prefs) Γ e,
      wc_global G ->
      wc_env (idck Γ) ->
      wc_exp G Γ e ->
      Forall (wc_clock (idck Γ)) (clockof e).

  Corollary wc_exp_clocksof {PSyn prefs} : forall (G: @global PSyn prefs) Γ es,
      wc_global G ->
      wc_env (idck Γ) ->
      Forall (wc_exp G Γ) es ->
      Forall (wc_clock (idck Γ)) (clocksof es).

  Lemma wc_clock_is_free_in : forall vars ck,
      wc_clock vars ck ->
      forall x, Is_free_in_clock x ck -> InMembers x vars.

  Section interface_incl.
    Context {PSyn1 PSyn2 : list decl -> block -> Prop}.
    Context {prefs1 prefs2 : PS.t}.
    Variable G1 : @global PSyn1 prefs1.
    Variable G2 : @global PSyn2 prefs2.

    Hypothesis Heq : global_iface_incl G1 G2.

    Hint Constructors wc_exp : lclocking.
    Fact iface_incl_wc_exp : forall Γ e,
        wc_exp G1 Γ e ->
        wc_exp G2 Γ e.

    Fact iface_incl_wc_equation : forall Γ equ,
        wc_equation G1 Γ equ ->
        wc_equation G2 Γ equ.

    Fact iface_incl_wc_scope {A} (P_wc1 P_wc2: _ -> _ -> Prop) : forall Γ locs (blks : A),
        (forall Γ, P_wc1 Γ blks -> P_wc2 Γ blks) ->
        wc_scope P_wc1 G1 Γ (Scope locs blks) ->
        wc_scope P_wc2 G2 Γ (Scope locs blks).

    Fact iface_incl_wc_block : forall d Γ,
        wc_block G1 Γ d ->
        wc_block G2 Γ d.

  End interface_incl.

  Lemma iface_incl_wc_node {PSyn prefs} (G1 G2 : @global PSyn prefs) : forall n,
      global_iface_incl G1 G2 ->
      wc_node G1 n ->
      wc_node G2 n.

  Global Hint Resolve iface_incl_wc_exp iface_incl_wc_equation iface_incl_wc_block : lclocking.

wc implies wl

  Local Hint Constructors wl_exp wl_block : lclocking.

  Fact wc_exp_wl_exp {PSyn prefs} : forall (G: @global PSyn prefs) Γ e,
      wc_exp G Γ e ->
      wl_exp G e.
  Global Hint Resolve wc_exp_wl_exp : lclocking.

  Corollary Forall_wc_exp_wl_exp {PSyn prefs} : forall (G: @global PSyn prefs) Γ es,
      Forall (wc_exp G Γ) es ->
      Forall (wl_exp G) es.
  Global Hint Resolve Forall_wc_exp_wl_exp : lclocking.

  Fact wc_equation_wl_equation {PSyn prefs} : forall (G: @global PSyn prefs) Γ equ,
      wc_equation G Γ equ ->
      wl_equation G equ.
  Global Hint Resolve wc_equation_wl_equation : lclocking.

  Fact wc_scope_wl_scope {A} (P_wc: _ -> _ -> Prop) (P_wl: _ -> Prop) {PSyn prefs} (G: @global PSyn prefs) :
    forall locs (blks: A) Γ,
      (forall Γ, P_wc Γ blks -> P_wl blks) ->
      wc_scope P_wc G Γ (Scope locs blks) ->
      wl_scope P_wl G (Scope locs blks).

  Fact wc_block_wl_block {PSyn prefs} : forall (G: @global PSyn prefs) d Γ,
      wc_block G Γ d ->
      wl_block G d.
  Global Hint Resolve wc_block_wl_block : lclocking.

  Fact wc_node_wl_node {PSyn prefs} : forall (G: @global PSyn prefs) n,
      wc_node G n ->
      wl_node G n.
  Global Hint Resolve wc_node_wl_node : lclocking.

  Fact wc_global_wl_global {PSyn prefs} : forall (G: @global PSyn prefs),
      wc_global G ->
      wl_global G.
  Global Hint Resolve wc_global_wl_global : lclocking.

wc implies wx

  Global Hint Constructors wx_exp wl_block : lclocking.

  Lemma wc_clock_wx_clock : forall vars ck,
      wc_clock (idck vars) ck ->
      wx_clock vars ck.

  Fact wc_exp_wx_exp {PSyn prefs} (G: @global PSyn prefs) : forall Γ e,
      wc_exp G Γ e ->
      wx_exp Γ e.
  Global Hint Resolve wc_clock_wx_clock wc_exp_wx_exp : lclocking.

  Corollary Forall_wc_exp_wx_exp {PSyn prefs} (G: @global PSyn prefs) : forall Γ es,
      Forall (wc_exp G Γ) es ->
      Forall (wx_exp Γ) es.
  Global Hint Resolve Forall_wc_exp_wx_exp : lclocking.

  Fact wc_equation_wx_equation {PSyn prefs} (G: @global PSyn prefs) : forall Γ equ,
      wc_equation G Γ equ ->
      wx_equation Γ equ.
  Global Hint Resolve wc_equation_wx_equation : lclocking.

  Fact wc_scope_wx_scope {A} (P_wc: _ -> _ -> Prop) (P_wx: _ -> _ -> Prop) {PSyn prefs} (G: @global PSyn prefs) :
    forall locs (blks: A) Γ,
      (forall Γ, P_wc Γ blks -> P_wx Γ blks) ->
      wc_scope P_wc G Γ (Scope locs blks) ->
      wx_scope P_wx Γ (Scope locs blks).

  Fact wc_block_wx_block {PSyn prefs} (G: @global PSyn prefs) : forall blk Γ,
      wc_block G Γ blk ->
      wx_block Γ blk.
  Global Hint Resolve wc_block_wx_block : lclocking.

  Fact wc_node_wx_node {PSyn prefs} : forall (G: @global PSyn prefs) n,
      wc_node G n ->
      wx_node n.
  Global Hint Resolve wc_node_wx_node : lclocking.

  Fact wc_global_wx_global {PSyn prefs} : forall (G: @global PSyn prefs),
      wc_global G ->
      wx_global G.
  Global Hint Resolve wc_global_wx_global : lclocking.


  Lemma wc_block_Is_defined_in {PSyn prefs} (G: @global PSyn prefs) : forall blk Γ x,
      wc_block G Γ blk ->
      Is_defined_in x blk ->
      InMembers x Γ.

  Lemma wc_scope_Is_defined_in {A} P_wc P_def {PSyn prefs} (G: @global PSyn prefs) : forall Γ locs (blks: A) x,
      wc_scope P_wc G Γ (Scope locs blks) ->
      Is_defined_in_scope P_def x (Scope locs blks) ->
      (forall Γ, P_wc Γ blks -> P_def blks -> InMembers x Γ) ->
      InMembers x Γ.

Change unifying substitution

  Lemma instck_refines : forall bck sub1 sub2 ck ck',
      (forall x y, sub1 x = Some y -> sub2 x = Some y) ->
      instck bck sub1 ck = Some ck' ->
      instck bck sub2 ck = Some ck'.

  Lemma WellInstantiated_refines1 : forall bck sub1 sub2 x ck1 ck2 o,
      (forall x y, sub1 x = Some y -> sub2 x = Some y) ->
      sub2 x = o ->
      WellInstantiated bck sub1 (x, ck1) (ck2, None) ->
      WellInstantiated bck sub2 (x, ck1) (ck2, o).

  Lemma WellInstantiated_refines2 : forall bck sub1 sub2 x ck1 ck2 y,
      (forall x y, sub1 x = Some y -> sub2 x = Some y) ->
      WellInstantiated bck sub1 (x, ck1) (ck2, Some y) ->
      WellInstantiated bck sub2 (x, ck1) (ck2, Some y).


  Lemma map_filter_clo_HasClock1 : forall Γ Γ' ck,
    (forall x ck', HasClock Γ' x ck' -> HasClock Γ x ck /\ ck' = Cbase) ->
    forall x ck',
      HasClock Γ' x ck' ->
      HasClock
        (map_filter (fun '(x2, ann0) => if clo ann0 ==b ck then Some (x2, ann_with_clock ann0 Cbase) else None) Γ)
        x ck'.

  Lemma map_filter_clo_IsLast1 : forall Γ Γ' ck,
      NoDupMembers Γ ->
      (forall x ck', HasClock Γ' x ck' -> HasClock Γ x ck /\ ck' = Cbase) ->
      (forall x, IsLast Γ' x -> IsLast Γ x) ->
      forall x, IsLast Γ' x ->
           IsLast (map_filter (fun '(x2, ann0) => if clo ann0 ==b ck then Some (x2, ann_with_clock ann0 Cbase) else None) Γ) x.

End LCLOCKING.

Module LClockingFun
       (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)
       <: LCLOCKING Ids Op OpAux Cks Senv Syn.
  Include LCLOCKING Ids Op OpAux Cks Senv Syn.
End LClockingFun.