proposition: Lemma list_forall_option_is_sound : forall (A : Type) f l, match @list_forall_option A f l with | Some true => forall a, In a l -> f a = Some true | Some false => (exists a, In a l /\ f a = Some false) /\ (forall a, In a l -> f a = None -> False) | None => exists a, In a l /\ f a = None end.
proof: Proof. intros A f l; induction l as [ | a l]. simpl; intros; contradiction. simpl; assert (Fa : forall b, b = a -> f b = f a). intros; subst; trivial. destruct (f a) as [ [ | ] | ]; generalize (Fa _ (eq_refl _)); clear Fa; intro Fa. destruct (list_forall_option f l) as [ [ | ] | ]. intros b [b_eq_a | b_in_l]; [subst; rewrite Fa | rewrite IHl]; trivial. destruct IHl as [[b [b_in_l fb_eq_false]] IHl]. split. exists b; split; trivial; right; trivial. intros c [c_eq_a | c_in_l]; [ subst; rewrite Fa; discriminate | apply IHl; trivial]. destruct IHl as [b [b_in_l fb_eq_none]]; exists b; split; trivial; right; trivial. destruct (list_forall_option f l) as [ [ | ] | ]. split. exists a; split; trivial; left; trivial. intros b [b_eq_a | b_in_l]; [ subst; rewrite Fa | rewrite IHl; trivial]; discriminate. destruct IHl as [[b [b_in_l fb_eq_false]] IHl]. split. exists a; split; trivial; left; trivial. intros c [c_eq_a | c_in_l]; [ subst; rewrite Fa; discriminate | apply IHl; trivial]. destruct IHl as [b [b_in_l fb_eq_none]]; exists b; split; trivial; right; trivial. exists a; split; trivial; left; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)