proposition: Theorem fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice : FunctionalChoice -> ExtensionalFunctionRepresentative -> ExcludedMiddle -> RepresentativeFunctionalChoice.
proof: Proof. intros FunChoice SetoidFunRepr EM A R (Hrefl,Hsym,Htrans). assert (H:forall P:Prop, exists b, b = true <-> P). { intros P. destruct (EM P). - exists true; firstorder. - exists false; easy. } destruct (FunChoice _ _ _ H) as (c,Hc). pose (class_of a y := c (R a y)). pose (isclass f := exists x:A, f x = true). pose (class := {f:A -> bool | isclass f}). pose (contains (c:class) (a:A) := proj1_sig c a = true). destruct (FunChoice class A contains) as (f,Hf). - intros f. destruct (proj2_sig f) as (x,Hx). exists x. easy. - destruct (SetoidFunRepr A bool) as (h,Hh). assert (Hisclass:forall a, isclass (h (class_of a))). { intro a. exists a. destruct (Hh (class_of a)) as (Ha,Huniqa). rewrite <- Ha. apply Hc. apply Hrefl. } pose (f':= fun a => exist _ (h (class_of a)) (Hisclass a) : class). exists (fun a => f (f' a)). intros x. destruct (Hh (class_of x)) as (Hx,Huniqx). split. + specialize Hf with (f' x). unfold contains in Hf. simpl in Hf. rewrite <- Hx in Hf. apply Hc. assumption. + intros y Hxy. f_equal. assert (Heq1: h (class_of x) = h (class_of y)). { apply Huniqx. intro z. unfold class_of. destruct (c (R x z)) eqn:Hxz. - symmetry. apply Hc. apply -> Hc in Hxz. firstorder. - destruct (c (R y z)) eqn:Hyz. + apply -> Hc in Hyz. rewrite <- Hxz. apply Hc. firstorder. + easy. } assert (Heq2:rew Heq1 in Hisclass x = Hisclass y). { apply proof_irrelevance_cci, EM. } unfold f'. rewrite <- Heq2. rewrite <- Heq1. reflexivity. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts