proposition: Lemma reduce_assoc_list : forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}), forall (l : list (A * B)), exists l', (forall a, nb_occ eqA a l' <= 1) /\ (forall a, find eqA a l = find eqA a l').
proof: Proof. intros A B eqA l; induction l as [ | [a1 b1] l]. exists (nil : list (A * B)); split; trivial; auto. elim IHl; intros l' [H1 H2]. assert (In_a1 : forall a, a = a1 -> find eqA a l' = find eqA a1 l'). intros; subst; trivial. destruct (find eqA a1 l') as [ b | ]; generalize (In_a1 _ (refl_equal _)); clear In_a1; intro In_a1. assert (In_a1' : exists l1, exists l2, l' = l1 ++ (a1,b) :: l2). clear H1 H2; induction l' as [ | [a' b'] l']. discriminate. simpl in In_a1; destruct (eqA a1 a') as [a1_eq_a' | _]. subst; inversion In_a1; exists (nil : list (A * B)); exists l'; simpl; trivial. elim (IHl' In_a1); intros l1 [l2 H]; exists ((a',b') :: l1); exists l2; subst; trivial. elim In_a1'; intros l1 [l2 H]; exists ((a1,b1) :: l1 ++ l2); split. intro a; generalize (H1 a); subst l'; rewrite nb_occ_app; simpl; destruct (eqA a a1) as [a_eq_a1 | _]; subst; rewrite nb_occ_app; [ rewrite plus_comm; simpl; rewrite plus_comm | idtac ]; trivial. intro a; simpl; destruct (eqA a a1) as [a_eq_a1 | a_diff_a1]; trivial. rewrite H2; subst l'; clear H1 H2 In_a1 In_a1'; induction l1 as [ | [a1' b1'] l1]; simpl. destruct (eqA a a1); trivial; absurd (a = a1); trivial. rewrite IHl1; trivial. exists ((a1,b1) :: l'); split; trivial; intro a; simpl. destruct (eqA a a1) as [a_eq_a1 | a_diff_a1]; trivial. rewrite none_nb_occ_O; subst; trivial. rewrite (H2 a); trivial. Qed.
imports: List Arith