[stdlib] several NoDup lemmas

[haansn08]

This PR adds following lemmas about NoDup:

NoDup_app: NoDup l1 -> NoDup l2 -> (forall a, In a l1 -> ~ In a l2) -> NoDup (l1 ++ l2).
InjectiveOn_map_NoDup: InjectiveOn P f -> Forall P l -> NoDup l -> NoDup (map f l).
ForallOrdPairs_NoDup: ForallOrdPairs (fun a b => a <> b) l <-> NoDup l.
NoDup_concat: Forall NoDup A L -> ForallOrdPairs (fun l1 l2 => forall a, In a l1 -> ~ In a l2) L -> NoDup (concat L).

The last lemma was useful to me for arguing about NoDup (flat_map ...) using flat_map_concat_map.

[mrhaandi]

Fyi, there already is a Injective_map_NoDup.
Also, while new lemmas on existing definitions are mostly welcome, new definitions, such as InjectiveOn, need to be introduced carefully. In particular, one would need to consider properties of this new definition wrt. all existing definitions.

[haansn08]

@mrhaandi Injective_map_NoDup was not strong enough for my use case. Consider this way to enumerate all permutations of a list.

Definition insert_at i x l :=
  firstn i l ++ x :: skipn i l.

Definition additions x l :=
  map (fun i => insert_at i x l) (seq 0 (S (length l))).

Definition permutations :=
  fix F l :=
    match l with
    | nil => [ nil ]
    | x::l' => flat_map (additions x) (F l')
    end.

The function fun i => insert_at i x l ist injective if x is not found in l, but only if i does not exceed the length of the list. Any i larger than length(l) will result in the list l++[x] making fun i => insert_at i x l not injective, which means I cannot apply Injective_map_NoDup. However NoDup (additions x l) still holds since map is called only on indices where insert_at is injective. My lemma InjectiveOn_map_NoDup can help here, where as Injective_map_NoDup cannot.

[mrhaandi]

For your use-case, what about:

Lemma ForallPairs_inj_map_NoDup [A B] (f: A->B) (l: list A) :
  ForallPairs (fun x y => f x = f y -> x = y) l -> NoDup l -> NoDup (map f l).
Proof.
  intros Hinj Hl.
  induction Hl as [|x ?? _ IH]; cbn; constructor.
  - intros [y [??]]%in_map_iff.
    destruct (Hinj y x); cbn; auto.
  - apply IH.
    intros x' y' Hx' Hy'.
    now apply Hinj; right.
Qed.

[haansn08]

@mrhaandi Nice, I like it! Should I replace InjectiveOn_map_NoDup with this lemma?

[mrhaandi]

Should I replace InjectiveOn_map_NoDup with this lemma?

Yes, that would be my suggestion (and remove InjectiveOn).

[mrhaandi]

Fyi, here are different proofs of the above statements. Feel free to ignore or copy (this is entirely stylistic choice).

Lemma NoDup_app (l1 l2 : list A):
  NoDup l1 -> NoDup l2 -> (forall a, In a l1 -> ~ In a l2) ->
  NoDup (l1 ++ l2).
Proof.
  intros H ?. induction H; [easy|].
  cbn. intros H'. constructor; [|now auto].
  intros [?|?%H']%in_app_or; now auto.
Qed.

Lemma NoDup_concat [A] (L: list (list A)):
  Forall (@NoDup A) L ->
  ForallOrdPairs (fun l1 l2 => forall a, In a l1 -> ~ In a l2) L ->
  NoDup (concat L).
Proof.
  intros H' H. revert H'.
  induction H as [|l L HL _ IH]; [constructor|].
  cbn. intros [??%IH]%Forall_cons_iff.
  apply NoDup_app; [easy..|].
  intros ??[?[??]]%in_concat.
  rewrite Forall_forall in HL.
  eapply HL; eassumption.
Qed.

[andres-erbsen]

These are welcome additions. It's a pity that this PR has fallen through the cracks.

[haansn08]

@andres-erbsen I changed the names accordingly and added a changelog.

[andres-erbsen]

@coqbot run full ci

[andres-erbsen]

@coqbot merge now

[coqbot-app]

@andres-erbsen: You cannot merge this PR because:

• No milestone has been set.

[andres-erbsen]

@coqbot merge now