proposition: Lemma reduce_assoc_list : equivalence _ eqA -> forall (B : Type) (l : list (A * B)), {l' : list (A * B) | (forall a, nb_occ a l' <= 1) /\ (forall a, find a l = find a l')}.
proof: Proof. intro eq_proof. fix reduce_assoc_list 2. intros B l; case l; clear l; simpl. exists (nil : list (A * B)); simpl; split. intros _; apply Nat.le_0_l. intros _; reflexivity. intros p l; case p; clear p; simpl. case (reduce_assoc_list _ l). intros k' H; case H; clear H; intros H1 H2. intros a b; case_eq (find a l). intros b' F; rewrite H2 in F. case (find_mem _ _ F). intros a' H; case H; clear H. intros k1 H; case H; clear H. intros k2 H; case H; clear H. intros a_eq_a' H; subst k'. exists (k1 ++ (a',b) :: k2); split. intro a''; generalize (H1 a''); do 2 rewrite nb_occ_app; simpl; intro H; exact H. intro a''; rewrite H2; generalize (H1 a''); rewrite nb_occ_app; simpl. case_eq (eq_bool a'' a'). intro a''_eq_a'; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; intro L. assert (L' := le_S_n _ _ L). inversion L' as [L'' | ]; clear L L'. assert (L1 : nb_occ a'' k1 = 0). revert L''; case (nb_occ a'' k1). intros _; reflexivity. simpl; intros n Abs; discriminate. case_eq (eq_bool a'' a). intro a''_eq_a. revert L1; generalize k1; fix IHk 1. intro k; case k; clear k; simpl. intros _; rewrite a''_eq_a'; reflexivity. intros p k; case p; clear p. intros a1 b1; case (eq_bool a'' a1). intro; discriminate. apply IHk. intro a''_diff_a. absurd (eqA a'' a). generalize (eq_bool_ok a'' a); rewrite a''_diff_a; intro H; exact H. case eq_proof; intros Req Teq Seq. apply (Teq a'' a' a). generalize (eq_bool_ok a'' a'); rewrite a''_eq_a'; intro H; exact H. apply Seq; assumption. intro a''_diff_a'; case_eq (eq_bool a'' a). intro a''_eq_a; absurd (eqA a'' a'). generalize (eq_bool_ok a'' a'); rewrite a''_diff_a'; intro H; exact H. case eq_proof; intros Req Teq Seq. apply (Teq a'' a a'). generalize (eq_bool_ok a'' a); rewrite a''_eq_a; intro H; exact H. assumption. intros _ _; generalize k1; fix IHk 1. intro k; case k; clear k; simpl. rewrite a''_diff_a'; reflexivity. intros p k; case p; clear p; simpl; intros a1 b1; rewrite IHk; reflexivity. intro F; rewrite H2 in F; exists ((a,b) :: k'); repeat split. simpl; intro a'; case_eq (eq_bool a' a). intro a'_eq_a; rewrite <- (eq_find_eq eq_proof k' a'_eq_a) in F. rewrite (none_nb_occ_O _ _ F); apply le_n. intros _; apply H1. simpl; intro a''; rewrite H2; reflexivity. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)