NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library nodup

Require Import ssreflect ssrbool eqtype.
Require Import Lists_ext.

Lemma beq_eq : forall (A : eqType) (n m : A), n == m -> n = m.


nodup is a predicate for lists without redundancy, similar to the Coq standard library NoDup (no duplicate), but expressed as a bool fixpoint instead of a Prop inductive; similar to uniq in ssreflect but expressed with standard lists instead of seq's

Section nodup.

Variable A : eqType.

Fixpoint nodup (l : list A) : bool :=
  match l with
    | nil => true
    | hd :: tl => ~~ (inb (fun x y => x == y) hd tl) && nodup tl
  end.

Lemma nodup_NoDup : forall (l : list A), nodup l -> NoDup l.

Lemma NoDup_nodup : forall (l : list A), NoDup l -> nodup l.

Lemma nodup_head : forall (hd : A) tl tl', ~ In hd tl' ->
  (nodup tl -> nodup tl') -> nodup (hd :: tl) -> nodup (hd :: tl').

Lemma nodup_head' : forall (hd : A) tl lst',
  (nodup tl -> nodup lst') -> nodup (hd :: tl) -> nodup lst'.

Lemma nodup_rotate : forall t (h : A), nodup (h :: t) -> nodup (t ++ h :: nil).

Lemma nodup_rotate' : forall (hd : A) tl lst',
  (nodup (tl ++ hd :: nil) -> nodup lst') -> nodup (hd :: tl) -> nodup lst'.

Lemma nodup_head1 : forall (hd : A) tl, nodup (hd :: tl) -> nodup tl.

Lemma list_is_not_set_hd_hd : forall (hd : A) tl, nodup (hd :: hd :: tl) -> False.

Lemma nodup_remove_idx : forall (l : list A), nodup l -> forall p i, nodup (remove_idx l p i).

Require Import Permutation.

Lemma nodup_Permutation : forall (l1 l2 : list A),
  Permutation l1 l2 -> nodup l1 -> nodup l2.


Lemma nodup_app_disj : forall (l k : list A),
  nodup l -> nodup k -> disj l k -> nodup (l ++ k).

Lemma nodup_rotate'' : forall hd (tl : A), nodup (hd ++ tl :: nil) -> nodup (tl :: hd).

Lemma nodup_app_inv : forall (l k : list A), nodup (l ++ k) -> nodup l /\ nodup k.


Lemma nodup_disj : forall (l k : list A), nodup (l ++ k) -> disj l k.

Lemma substitution_nodup : forall n s, length s = n ->
  Permutation s (List.seq O n) ->
  forall (def : A) l k, length l = n -> length k = n ->
    (forall i, (i < n)%nat -> nth i k def = nth (nth i s O) l def) ->
    nodup l -> nodup k.

Lemma nodup_ith_inj : forall (B : Type) (l : list (A * B)) n x m,
  nodup (uzip1 l) -> ith n l = Some x -> ith m (uzip1 l) = Some (fst x) ->
  n = m.

Lemma Nth_assoc_get : forall (B : Type) (l : list (A * B)) x v,
  nodup (uzip1 l) -> ith x l = Some v -> assoc_get (fst v) l = Some (snd v).

Lemma In_assoc_get : forall (B : Type) (l : list (A * B)) (a : A) (b : B),
  In (a, b) l -> nodup (uzip1 l) -> assoc_get a l = Some b.

Definition nodup_function : forall (B : Type) (g : list (A * B)), nodup (uzip1 g) ->
  forall a b1 b2, assoc_get a g = Some b1 ->
    assoc_get a g = Some b2 -> b1 = b2.

End nodup.

Implicit Arguments nodup [A].
Implicit Arguments nodup_rotate'' [A].
Implicit Arguments nodup_app_inv [A].
Implicit Arguments nodup_ith_inj [A B].
Implicit Arguments In_assoc_get [A B].
Implicit Arguments nodup_function [A B].

Notation "'nodup(' a , .. , b ')'" := (nodup (cons a .. (cons b nil) ..)) (at level 10, no associativity, format "'[v' 'nodup(' a , .. , b ')' ']'") : nodup_scope.

Require seq_ext.

Lemma uniq_nodup : forall {A : eqType} (l : seq.seq A), seq.uniq l = nodup (seq_ext.s2l l).

Lemma nodup_seq : forall n a, nodup (seq a n : list ssrnat.nat_eqType).

compute an injection of from_list into to_list



Ltac compute_list_injection to_list from_list :=
  match from_list with
    | @List.cons ?A ?hd ?tl =>
      let hd' := Find_var A hd to_list O in
      let tl' := compute_list_injection to_list tl in
      constr : (List.cons hd' tl')
    | _ => constr : (@List.nil nat)
  end.

Ltac remove_useless :=
  match goal with
    | |- is_true (nodup ?l) -> is_true (nodup ?k)=>
      let inj := compute_list_injection l k in
      let perm := eval compute in
          (remove_idx l (fun x => negb (inb beq_nat x inj)) O) in
      let Htmp := fresh in
      move=> Htmp ;
      move: (nodup_remove_idx _ _ Htmp (fun x => negb (inb beq_nat x inj)) O);
      rewrite [remove_idx _ _ _]/= {Htmp}
  end.

Ltac loop n :=
  match n with
    | O => idtac
    | S ?m => (case => //) ; loop m
  end.

Ltac loop' n :=
  match n with
    | O => idtac
    | S ?m => (move/Lt.lt_S_n) ; loop' m
  end.

Ltac nodup_permut default_value :=
  match goal with
    | |- is_true (nodup ?l) -> is_true (nodup ?k)=>
      let bij := compute_list_injection l k in
      let len := eval compute in (length l) in
      let Hn := fresh in
      let Hnot_lt_O := fresh in
        apply substitution_nodup with
          (n:=len) (s:=bij) (def:=default_value);
          [done | apply (function_permut_Permutation Peano_dec.eq_nat_dec len) => // | done | done |
            (
              loop len ; move=> Hn ; loop' len ;
              move: (Lt.lt_n_O Hn) => Hnot_lt_O; move/Hnot_lt_O => //
            )
          ]
  end.

Ltac Nodup_nodup default_value :=
   match goal with
   | H:is_true (nodup ?l1) |- is_true (nodup ?l2) =>
     move: H; remove_useless ; nodup_permut default_value
   end.

Ltac look_for_double_in_list lst :=
  match lst with
    | nil => None
    | ?hd :: ?tl =>
      match Lists_ext.In_list hd tl with
        | true => constr:(Some hd)
        | false => look_for_double_in_list tl
      end
  end.

Ltac nodup_remove_elements candidate :=
  match goal with
    | H:is_true (nodup (candidate :: candidate :: _)) |- _ =>
      move: {H}(list_is_not_set_hd_hd _ _ _ H) => //
    | H:is_true (nodup (candidate :: ?tl)) |- _ =>
      move: {H}(nodup_rotate _ _ _ H); simpl app; move=> H ;
        nodup_remove_elements candidate
    | H:is_true (nodup (?hd :: ?tl)) |- _ =>
      move: {H}(nodup_head1 _ _ _ H) => H ;
        nodup_remove_elements candidate
    | _ => fail "no interesting nodup predicate in the context"
  end.



Ltac nodup_false :=
    match goal with
      | H:is_true (nodup ?lst) |- False =>
        let candidate := look_for_double_in_list lst in
        
  match candidate with
    | Some ?candidate' => nodup_remove_elements candidate'
    | _ => clear H; nodup_false

  end

      | _ => fail "no double in any nodup predicate"
    end.

Ltac Nodup_not_In_singleton := match goal with
| [ H : is_true (nodup ?lst) |- ~ In ?a (?k :: nil) ] =>
  let K := fresh in
    move=> /= [K | // ];
      match k with
        | _ => rewrite <- K in H
      end ;
      nodup_false
end.

Ltac Nodup_not_In :=
  match goal with
    | [ H : is_true (nodup ?lst) |- ~ In ?a (?b :: nil) ] =>
      by Nodup_not_In_singleton
    | [ H : is_true (nodup ?lst) |- ~ In ?a (?b :: ?k) ] =>
      apply not_In_cons; [by Nodup_not_In_singleton | Nodup_not_In]
    | |- ?X => idtac X
  end.

Ltac Nodup_neq :=
  match goal with
    | [ H : is_true (nodup ?lst) |- ?a <> ?b ] =>
      let K := fresh in
        intro K;
rewrite <- K in H
;
          nodup_false
  end.