From adc95f1ca9dfd26da083d2398e9284244bc0d429 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 17 Mar 2017 09:52:21 +0100
Subject: [PATCH] Show equivalence of re-defined List.In and List.NoDup with
 Coq stdlib versions

---
 theories/base.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index f7f74c8f..270d2c21 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -933,10 +933,30 @@ Inductive elem_of_list {A} : ElemOf A (list A) :=
   | elem_of_list_further (x y : A) l : x ∈ l → x ∈ y :: l.
 Existing Instance elem_of_list.
 
+Lemma elem_of_list_In {A} (l : list A) x :
+  x ∈ l ↔ In x l.
+Proof.
+  induction l.
+  - split; inversion 1.
+  - split; inversion 1; subst; (left + (right; apply IHl)); now auto.
+Qed.
+
 Inductive NoDup {A} : list A → Prop :=
   | NoDup_nil_2 : NoDup []
   | NoDup_cons_2 x l : x ∉ l → NoDup l → NoDup (x :: l).
 
+Lemma NoDup_ListNoDup {A} (l : list A) :
+  NoDup l ↔ List.NoDup l.
+Proof.
+  induction l.
+  - split; intros _; now constructor.
+  - split; inversion 1; subst.
+    + constructor; [now rewrite <-elem_of_list_In|].
+      now apply IHl.
+    + constructor; [now rewrite elem_of_list_In|].
+      now apply IHl.
+Qed.
+
 (** Decidability of equality of the carrier set is admissible, but we add it
 anyway so as to avoid cycles in type class search. *)
 Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Union C,
-- 
GitLab