Commit 71423d13 authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers
Browse files

prove NoDup_fmap_2_strong

parent 048ade3d
......@@ -3483,16 +3483,27 @@ Section fmap.
naive_solver eauto using elem_of_list_fmap_1, elem_of_list_fmap_2_inj.
(** A version of [NoDup_fmap_2] that does not require [f] to be injective for
*all* inputs. *)
Lemma NoDup_fmap_2_strong l :
(∀ x y, x ∈ l → y ∈ l → f x = f y → x = y) →
NoDup l →
NoDup (f <$> l).
intros Hinj. induction 1 as [|x l ?? IH]; simpl; constructor.
- intros [y [Hxy ?]]%elem_of_list_fmap.
apply Hinj in Hxy; [by subst|by constructor..].
- apply IH. clear- Hinj.
intros x' y Hx' Hy. apply Hinj; by constructor.
Lemma NoDup_fmap_1 l : NoDup (f <$> l) → NoDup l.
induction l; simpl; inversion_clear 1; constructor; auto.
rewrite elem_of_list_fmap in *. naive_solver.
Lemma NoDup_fmap_2 `{!Inj (=) (=) f} l : NoDup l → NoDup (f <$> l).
induction 1; simpl; constructor; trivial. rewrite elem_of_list_fmap.
intros [y [Hxy ?]]. apply (inj f) in Hxy. by subst.
Proof. apply NoDup_fmap_2_strong. intros ?? _ _. apply (inj f). Qed.
Lemma NoDup_fmap `{!Inj (=) (=) f} l : NoDup (f <$> l) ↔ NoDup l.
Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment