proposition: Theorem repr_fun_choice_imp_relational_choice : RepresentativeFunctionalChoice -> RelationalChoice.
proof: Proof. intros ReprFunChoice A B T Hexists. pose (D := (A*B)%type). pose (R (z z':D) := let x := fst z in let x' := fst z' in let y := snd z in let y' := snd z' in x = x' /\ (T x y -> y = y' \/ T x y') /\ (T x y' -> y = y' \/ T x y)). assert (Hequiv : Equivalence R). { split. - split. + easy. + firstorder. - intros (x,y) (x',y') (H1,(H2,H2')). split. + easy. + simpl fst in *. simpl snd in *. subst x'. split; intro H. * destruct (H2' H); firstorder. * destruct (H2 H); firstorder. - intros (x,y) (x',y') (x'',y'') (H1,(H2,H2')) (H3,(H4,H4')). simpl fst in *. simpl snd in *. subst x'' x'. split. { easy. } split; intro H. + simpl fst in *. simpl snd in *. destruct (H2 H) as [<-|H0]. * destruct (H4 H); firstorder. * destruct (H2' H0), (H4 H0); try subst y'; try subst y''; try firstorder. + simpl fst in *. simpl snd in *. destruct (H4' H) as [<-|H0]. * destruct (H2' H); firstorder. * destruct (H2' H0), (H4 H0); try subst y'; try subst y''; try firstorder. } destruct (ReprFunChoice D R Hequiv) as (g,Hg). set (T' x y := T x y /\ exists y', T x y' /\ g (x,y') = (x,y)). exists T'. split. - intros x y (H,_); easy. - intro x. destruct (Hexists x) as (y,Hy). exists (snd (g (x,y))). destruct (Hg (x,y)) as ((Heq1,(H',H'')),Hgxyuniq); clear Hg. destruct (H' Hy) as [Heq2|Hgy]; clear H'. + split;[split|]. * rewrite <- Heq2. assumption. * exists y. destruct (g (x,y)) as (x',y'). simpl in Heq1, Heq2. subst; easy. * intros y' (Hy',(y'',(Hy'',Heq))). rewrite (Hgxyuniq (x,y'')), Heq. { easy. } split. { easy. } split; right; easy. + split;[split|]. * assumption. * exists y. destruct (g (x,y)) as (x',y'). simpl in Heq1. subst x'; easy. * intros y' (Hy',(y'',(Hy'',Heq))). rewrite (Hgxyuniq (x,y'')), Heq. { easy. } split. { easy. } split; right; easy. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts