proposition: Lemma findA_NoDupA : forall l a b, NoDupA (fun p p' => eqA (fst p) (fst p')) l -> (InA (fun p p' => eqA (fst p) (fst p') /\ snd p = snd p') (a,b) l <-> findA (fun a' => if eqA_dec a a' then true else false) l = Some b).
proof: Proof. set (eqk := fun p p' : A*B => eqA (fst p) (fst p')). set (eqke := fun p p' : A*B => eqA (fst p) (fst p') /\ snd p = snd p'). intros l; induction l as [|a l IHl]; intros a0 b H; simpl. - split; intros H0; try discriminate. invlist InA. - destruct a as (a',b'); rename a0 into a. invlist NoDupA. split; intros. + invlist InA. * match goal with H2 : eqke (a, b) (a', b') |- _ => compute in H2; destruct H2 end. subst b'. destruct (eqA_dec a a'); intuition. * destruct (eqA_dec a a') as [HeqA|]; simpl. -- match goal with H0 : ~ InA eqk (a', b') l |- _ => contradict H0 end. match goal with H2 : InA eqke (a, b) l |- _ => revert HeqA H2; clear - eqA_equiv end. induction l. ++ intros; invlist InA. ++ intros; invlist InA; auto. match goal with |- InA eqk _ (?p :: _) => destruct p as [a0 b0] end. match goal with H : eqke (a, b) (a0, b0) |- _ => compute in H; destruct H end. subst b. left; auto. compute. transitivity a; auto. symmetry; auto. -- rewrite <- IHl; auto. + destruct (eqA_dec a a'); simpl in *. * left; split; simpl; congruence. * right. rewrite IHl; auto. Qed.
imports: List Sorted Setoid Basics Morphisms