Commit 5bdd73dd authored by Robbert's avatar Robbert

Merge branch 'ralf/no-dup-fmap' into 'master'

prove NoDup_fmap_2_strong

See merge request !173
parents 048ade3d 71423d13
Pipeline #31526 passed with stage
in 10 minutes and 57 seconds
......@@ -3483,16 +3483,27 @@ Section fmap.
naive_solver eauto using elem_of_list_fmap_1, elem_of_list_fmap_2_inj.
Qed.
(** 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).
Proof.
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.
Qed.
Lemma NoDup_fmap_1 l : NoDup (f <$> l) NoDup l.
Proof.
induction l; simpl; inversion_clear 1; constructor; auto.
rewrite elem_of_list_fmap in *. naive_solver.
Qed.
Lemma NoDup_fmap_2 `{!Inj (=) (=) f} l : NoDup l NoDup (f <$> l).
Proof.
induction 1; simpl; constructor; trivial. rewrite elem_of_list_fmap.
intros [y [Hxy ?]]. apply (inj f) in Hxy. by subst.
Qed.
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