Dup_NoDup.v

Require Import List.
Variable A:Type.

Inductive NoDup : list A -> Prop :=
  NoDup_nil : NoDup nil
| NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x :: l).

Inductive Dup : list A -> Prop :=
  Dup_hd : forall x l, In x l -> Dup (x :: l)
| Dup_tl : forall x l, Dup l  -> Dup (x :: l).


Goal forall l, NoDup l -> ~ Dup l.
  induction l; inversion 1; inversion 1;
    subst; simpl in *; try congruence; tauto.
Qed.

Goal forall l, Dup l -> ~ NoDup l.
  induction l; inversion 1; inversion 1;
    subst; simpl in *; try congruence; tauto.
Qed.

Goal forall l, ~Dup l -> NoDup l.
  induction l; intros; constructor; [|apply IHl];
    intro C; apply H; now constructor.
Qed.

Definition not_neq_eq := forall (a b:A), ~ a <> b -> a = b.

Goal (forall l, (~ NoDup l -> Dup l)) ->  not_neq_eq.
  intros no_NoDup_Dup.
  intros a b Hnot_neq.
  enough (Hab: Dup (a :: b :: nil)).
  { inversion Hab.
    now inversion H0.
    now inversion H0; inversion H1.
  }
  apply no_NoDup_Dup.
  intro HnoDup.
  apply Hnot_neq.
  inversion 1.
  subst.
  inversion HnoDup.
  apply H2, in_eq.
Qed.