Show equivalence of re-defined List.In and List.NoDup with Coq stdlib versions

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,

[Robbert Krebbers]

What is the point of this, why would one ever use the ones from the stdlib? There are hardly no lemmas about it, and you won't get the ∈ notations.

[Ralf Jung]

I searched for lemmas relating Forall to something about list membership, found List.Forall_forall, and then spent 15min trying to do anything with the In I got out of that. Having this lemma would have meant I would have completed my proof at least 10min quicker.

Of course, I should have used the Forall_forall from std++, but there's no way I could have known. I'd rather have a not-perfectly-clean, but working proof after 5min than spend 20min to find the "right" proof.

[Robbert Krebbers]

But then, why would you use In and not elem_of?

[Ralf Jung]

Hu? I used List.Forall_forall, and it uses In. (Notice this is the one from the Coq standard library.)

[Robbert Krebbers]

I don't understand why it was difficult to find something relating Forall to list membership then:

Search elem_of Forall.
elem_of_mapM_fmap: ...
elem_of_mapM_Forall: ...
Forall_forall:
  ∀ (A : Type) (P : A → Prop) (l : list A),
  Forall P l ↔ (∀ x : A, x ∈ l → P x)

[Ralf Jung]

I did first SearchAbout Forall or so, stumbled upon Coq's Forall_forall, and then I spent 15min doing SearchAbout In <something> in dozens of variations (and other, related avenues) and found nothing. My mistake was using Coq's Forall_forall instead of the one from std++. I don't say the one from std++ cannot be found, but for me, it showed the one for Coq first, and I had no way to know that I was not supposed to use it.

[Robbert Krebbers]

We can blacklist stuff from the standard lib that we have redefined for search? Would that solve your problem?

[Ralf Jung]

Also, generally, people having some experience with Coq will know In and may even do SearchAbout Forall In, which will not even bring up anything from std++. It's not nice to lead them into a dead end like that. I honestly don't think it is a good idea to even redefine these notions from the standard library, that's just asking for exactly the kind of trouble I am having. But if we do redefine it, then at the very least we should provide some way to convert between the two worlds in that split ecosystem we are creating. There will always be the case of some lemma using In not having been proven with ∈.

[Ralf Jung]

We can blacklist stuff from the standard lib that we have redefined for search? Would that solve your problem?

It would help to make the first mistake less likely, but it may also be confusing. And I would still insist on having these equivalence lemmas somewhere.

[Robbert Krebbers]

Actually, never mind, that won't work. The blacklist functionality AFAIK only allows one to do some basic matching on lemma names.