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

From Velus Require Import Common.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import NLustre.NLSyntax.
From Velus Require Import CoreExpr.CESyntax.
From Velus Require Import NLustre.IsVariable.
From Velus Require Import NLustre.IsDefined.
From Velus Require Import NLustre.Memories.

No duplication of variables

Module Type NODUP
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import CESyn : CESYNTAX Ids Op OpAux Cks)
       (Import Syn : NLSYNTAX Ids Op OpAux Cks CESyn)
       (Import Mem : MEMORIES Ids Op OpAux Cks CESyn Syn)
       (Import IsD : ISDEFINED Ids Op OpAux Cks CESyn Syn Mem)
       (Import IsV : ISVARIABLE Ids Op OpAux Cks CESyn Syn Mem IsD).

  Inductive NoDup_defs : list equation -> Prop :=
  | NDDNil: NoDup_defs nil
  | NDDCons: forall eq eqs,
      NoDup_defs eqs ->
      (forall x, Is_defined_in_eq x eq -> ~Is_defined_in x eqs) ->
      NoDup_defs (eq :: eqs).

Properties

  Lemma NoDup_defs_cons:
    forall eq eqs,
      NoDup_defs (eq :: eqs) -> NoDup_defs eqs.

Proof.

    intros eq eqs Hndd.
    destruct eq; inversion_clear Hndd; assumption.
  Qed.

  Lemma NoDup_defs_NoDup_vars_defined:
    forall eqs,
      NoDup (vars_defined eqs) ->
      NoDup (lasts_defined eqs) ->
      NoDup_defs eqs.

Proof.

    unfold vars_defined, lasts_defined.
    induction eqs as [|eq eqs]; simpl; intros * VD LD.
    - auto using NoDup_defs.
    - simpl.
      constructor; eauto using NoDup_app_r.
      intros ? Hdef1 Hdef2. destruct x.
      + eapply NoDup_app_In in VD. eapply VD.
        * apply Is_defined_in_vars_defined; eauto.
        * apply Is_defined_in_var_defined; eauto.
      + eapply NoDup_app_In in LD. eapply LD.
        * apply Is_defined_in_lasts_defined; eauto.
        * apply Is_defined_in_last_defined; eauto.
  Qed.

  Lemma NoDup_defs_node:
    forall n,
      NoDup_defs n.(n_eqs).

Proof.

End NODUP.

Module NoDupFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (CESyn : CESYNTAX Ids Op OpAux Cks)
       (Syn : NLSYNTAX Ids Op OpAux Cks CESyn)
       (Mem : MEMORIES Ids Op OpAux Cks CESyn Syn)
       (IsD : ISDEFINED Ids Op OpAux Cks CESyn Syn Mem)
       (IsV : ISVARIABLE Ids Op OpAux Cks CESyn Syn Mem IsD)
       <: NODUP Ids Op OpAux Cks CESyn Syn Mem IsD IsV.
  Include NODUP Ids Op OpAux Cks CESyn Syn Mem IsD IsV.
End NoDupFun.