proposition: Lemma prop_map12_without_repetition : forall A B (eq_bool : A -> A -> bool) (eq_bool_ok :forall a1 a2 : A, match eq_bool a1 a2 with true => a1 = a2 | false => a1 <> a2 end) (P : B -> Prop) f l, (forall a, In a l -> match f a with | (None, None) => True | (Some b, None) => P b | (None, Some c) => P c | (Some b, Some c) => P b /\ P c end) -> (forall d, In d (map12_without_repetition eq_bool f l) -> P d).
proof: Proof. intros A B eq_bool eq_bool_ok P f; fix prop_map12_without_repetition 1; intro l; case l; clear l. intros _ b b_in_nil; contradiction. intros a l IH; generalize (prop_map12_without_repetition l (tail_prop _ IH)); revert IH. case l; clear l; simpl. intros IH H b; generalize (IH a (or_introl _ (eq_refl _))); destruct (f a) as [[b' | ] [b'' | ]]. intros [Pb' Pb''] [b_eq_b' | [b_eq_b'' | b_in_nil]]. subst b'; assumption. subst b''; assumption. contradiction. intros Pb' [b_eq_b' | b_in_nil]. subst b'; assumption. contradiction. intros Pb'' [b_eq_b'' | b_in_nil]. subst b''; assumption. contradiction. contradiction. intros a2 l IH; simpl; generalize (eq_bool_ok a a2); case (eq_bool a a2); [intro a_eq_a2 | intro a_diff_a2]. intros Hl b b_in_map; apply Hl; assumption. generalize (IH a (or_introl _ (eq_refl _))); destruct (f a) as [[b' | ] [b'' | ]]. intros [Pb' Pb''] Hl b [b_eq_b' | [b_eq_b'' | b_in_map]]. subst b; assumption. subst b; assumption. apply Hl; assumption. intros Pb' Hl b [b_eq_b' | b_in_map]. subst b; assumption. apply Hl; assumption. intros Pb'' Hl b [b_eq_b'' | b_in_map]. subst b; assumption. apply Hl; assumption. intros _ Hl b b_in_map; apply Hl; assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)