From 2c8cb9696729d1f03e4ed66350f7f5ab4628d7e4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 10 Apr 2024 23:16:29 +0900 Subject: [PATCH] replace original zorn lemma with georges' --- classical/classical_sets.v | 226 +++++++++---------------------------- classical/mathcomp_extra.v | 1 - classical/wochoice.v | 6 +- theories/forms.v | 2 +- theories/topology.v | 59 +++++----- 5 files changed, 89 insertions(+), 205 deletions(-) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index e40c77f370..3ce415d7d3 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg matrix finmap ssrnum. From mathcomp Require Import ssrint interval. -From mathcomp Require Import mathcomp_extra boolp. +From mathcomp Require Import mathcomp_extra boolp wochoice. (**md**************************************************************************) (* # Set Theory *) @@ -2599,127 +2599,55 @@ End partitions. #[deprecated(note="Use trivIset_setIl instead")] Notation trivIset_setI := trivIset_setIl (only parsing). +Section Zorn. + Definition total_on T (A : set T) (R : T -> T -> Prop) := forall s t, A s -> A t -> R s t \/ R t s. -Section ZL. - -Variable (T : Type) (t0 : T) (R : T -> T -> Prop). -Hypothesis (Rrefl : forall t, R t t). -Hypothesis (Rtrans : forall r s t, R r s -> R s t -> R r t). -Hypothesis (Rantisym : forall s t, R s t -> R t s -> s = t). -Hypothesis (tot_lub : forall A : set T, total_on A R -> exists t, - (forall s, A s -> R s t) /\ forall r, (forall s, A s -> R s r) -> R t r). -Hypothesis (Rsucc : forall s, exists t, R s t /\ s <> t /\ - forall r, R s r -> R r t -> r = s \/ r = t). - -Let Teq := @gen_eqMixin T. -Let Tch := @gen_choiceMixin T. -Let Tp : pointedType := (* FIXME: use HB.pack *) - Pointed.Pack (@Pointed.Class T (isPointed.Axioms_ t0) Tch Teq). -Let lub := fun A : {A : set T | total_on A R} => - [get t : Tp | (forall s, sval A s -> R s t) /\ - forall r, (forall s, sval A s -> R s r) -> R t r]. -Let succ := fun s => [get t : Tp | R s t /\ s <> t /\ - forall r, R s r -> R r t -> r = s \/ r = t]. - -Inductive tower : set T := - | Lub : forall A, sval A `<=` tower -> tower (lub A) - | Succ : forall t, tower t -> tower (succ t). - -Lemma ZL' : False. -Proof. -have lub_ub (A : {A : set T | total_on A R}) : - forall s, sval A s -> R s (lub A). - suff /getPex [] : exists t : Tp, (forall s, sval A s -> R s t) /\ - forall r, (forall s, sval A s -> R s r) -> R t r by []. - by apply: tot_lub; apply: (svalP A). -have lub_lub (A : {A : set T | total_on A R}) : - forall t, (forall s, sval A s -> R s t) -> R (lub A) t. - suff /getPex [] : exists t : Tp, (forall s, sval A s -> R s t) /\ - forall r, (forall s, sval A s -> R s r) -> R t r by []. - by apply: tot_lub; apply: (svalP A). -have RS s : R s (succ s) /\ s <> succ s. - by have /getPex [? []] : exists t : Tp, R s t /\ s <> t /\ - forall r, R s r -> R r t -> r = s \/ r = t by apply: Rsucc. -have succS s : forall t, R s t -> R t (succ s) -> t = s \/ t = succ s. - by have /getPex [? []] : exists t : Tp, R s t /\ s <> t /\ - forall r, R s r -> R r t -> r = s \/ r = t by apply: Rsucc. -suff Twtot : total_on tower R. - have [R_S] := RS (lub (exist _ tower Twtot)); apply. - by apply/Rantisym => //; apply/lub_ub/Succ/Lub. -move=> s t Tws; elim: Tws t => {s} [A sATw ihA|s Tws ihs] t Twt. - have [?|/asboolP] := pselect (forall s, sval A s -> R s t). - by left; apply: lub_lub. - rewrite asbool_neg => /existsp_asboolPn [s /asboolP]. - rewrite asbool_neg => /imply_asboolPn [As nRst]; right. - by have /lub_ub := As; apply: Rtrans; have [] := ihA _ As _ Twt. -suff /(_ _ Twt) [Rts|RSst] : forall r, tower r -> R r s \/ R (succ s) r. - by right; apply: Rtrans Rts _; have [] := RS s. - by left. -move=> r; elim=> {r} [A sATw ihA|r Twr ihr]. - have [?|/asboolP] := pselect (forall r, sval A r -> R r s). - by left; apply: lub_lub. - rewrite asbool_neg => /existsp_asboolPn [r /asboolP]. - rewrite asbool_neg => /imply_asboolPn [Ar nRrs]; right. - by have /lub_ub := Ar; apply: Rtrans; have /ihA [] := Ar. -have [Rrs|RSsr] := ihr; last by right; apply: Rtrans RSsr _; have [] := RS r. -have : tower (succ r) by apply: Succ. -move=> /ihs [RsSr|]; last by left. -by have [->|->] := succS _ _ Rrs RsSr; [right|left]; apply: Rrefl. -Qed. - -End ZL. - -Lemma Zorn T (R : T -> T -> Prop) : +Let total_on_wo_chain (T : Type) (R : rel T) (P : {pred T}) : + (forall A, total_on A R -> exists t, forall s, A s -> R s t) -> + wo_chain R P -> exists2 z, z \in predT & upper_bound R P z. +Proof. +move: R P; elim/Peq : T => T R P Atot RP. +suff : total_on P R by move=> /Atot[t ARt]; exists t. +move=> s t Ps Pt; have [| |] := RP [predU (pred1 s) & (pred1 t)]. +- by move=> x; rewrite !inE => /orP[/eqP ->{x}|/eqP ->{x}]. +- by exists s; rewrite !inE eqxx. +- move=> x [[]]; rewrite !inE => /orP[/eqP ->{x}|/eqP ->{x}]. + + by move=> /(_ t); rewrite !inE eqxx orbT => /(_ isT) Rst _; left. + + by move=> /(_ s); rewrite !inE eqxx => /(_ isT) Rts _; right. +Qed. + +Lemma Zorn (T : Type) (R : rel T) : (forall t, R t t) -> (forall r s t, R r s -> R s t -> R r t) -> (forall s t, R s t -> R t s -> s = t) -> (forall A : set T, total_on A R -> exists t, forall s, A s -> R s t) -> exists t, forall s, R t s -> s = t. Proof. -move=> Rrefl Rtrans Rantisym Rtot_max. -pose totR := {A : set T | total_on A R}. -set R' := fun A B : totR => sval A `<=` sval B. -have R'refl A : R' A A by []. -have R'trans A B C : R' A B -> R' B C -> R' A C by apply: subset_trans. -have R'antisym A B : R' A B -> R' B A -> A = B. - rewrite /R'; move: A B => [/= A totA] [/= B totB] sAB sBA. - by apply: eq_exist; rewrite predeqE=> ?; split=> [/sAB|/sBA]. -have R'tot_lub A : total_on A R' -> exists t, (forall s, A s -> R' s t) /\ - forall r, (forall s, A s -> R' s r) -> R' t r. - move=> Atot. - have AUtot : total_on (\bigcup_(B in A) (sval B)) R. - move=> s t [B AB Bs] [C AC Ct]. - have [/(_ _ Bs) Cs|/(_ _ Ct) Bt] := Atot _ _ AB AC. - by have /(_ _ _ Cs Ct) := svalP C. - by have /(_ _ _ Bs Bt) := svalP B. - exists (exist _ (\bigcup_(B in A) sval B) AUtot); split. - by move=> B ? ? ?; exists B. - by move=> B Bub ? /= [? /Bub]; apply. -apply: contrapT => nomax. -have {}nomax t : exists s, R t s /\ s <> t. - have /asboolP := nomax; rewrite asbool_neg => /forallp_asboolPn /(_ t). - move=> /asboolP; rewrite asbool_neg => /existsp_asboolPn [s]. - by move=> /asboolP; rewrite asbool_neg => /imply_asboolPn []; exists s. -have tot0 : total_on set0 R by []. -apply: (ZL' (exist _ set0 tot0)) R'tot_lub _ => // A. -have /Rtot_max [t tub] := svalP A; have [s [Rts snet]] := nomax t. -have Astot : total_on (sval A `|` [set s]) R. - move=> u v [Au|->]; last first. - by move=> [/tub Rvt|->]; right=> //; apply: Rtrans Rts. - move=> [Av|->]; [apply: (svalP A)|left] => //. - by apply: Rtrans Rts; apply: tub. -exists (exist _ (sval A `|` [set s]) Astot); split; first by move=> ? ?; left. -split=> [AeAs|[B Btot] sAB sBAs]. - have [/tub Rst|] := pselect (sval A s); first exact/snet/Rantisym. - by rewrite AeAs /=; apply; right. -have [Bs|nBs] := pselect (B s). - by right; apply: eq_exist; rewrite predeqE => r; split=> [/sBAs|[/sAB|->]]. -left; case: A tub Astot sBAs sAB => A Atot /= tub Astot sBAs sAB. -apply: eq_exist; rewrite predeqE => r; split=> [Br|/sAB] //. -by have /sBAs [|ser] // := Br; rewrite ser in Br. +move: R; elim/Peq : T => T R Rxx Rtrans Ranti Atot. +have [//| |P _ RP|] := @Zorn's_lemma _ R predT _. +- by move=> ? ? ? _ _ _; exact: Rtrans. +- exact: total_on_wo_chain. +by move=> x _ Rx; exists x => s Rxs; apply: (Ranti _ _ _ Rxs) => //; exact: Rx. +Qed. + +Definition premaximal T (R : T -> T -> Prop) (t : T) := + forall s, R t s -> R s t. + +Lemma ZL_preorder (T : Type) (t0 : T) (R : rel T) : + (forall t, R t t) -> (forall r s t, R r s -> R s t -> R r t) -> + (forall A, total_on A R -> exists t, forall s, A s -> R s t) -> + exists t, premaximal R t. +Proof. +move: t0 R; elim/Peq : T => T t0 R Rxx Rtrans Atot. +have [//| | |z _ Hz] := @Zorn's_lemma T R predT. +- by move=> ? ? ? _ _ _; exact: Rtrans. +- by move=> A _ RA; exact: total_on_wo_chain. +by exists z => s Rzs; exact: Hz. Qed. +End Zorn. + Section Zorn_subset. Variables (T : Type) (P : set (set T)). @@ -2728,20 +2656,24 @@ Lemma Zorn_bigcup : P (\bigcup_(X in F) X)) -> exists A, P A /\ forall B, A `<` B -> ~ P B. Proof. -move=> totP; pose R (sA sB : P) := sval sA `<=` sval sB. +move=> totP; pose R (sA sB : P) := `[< sval sA `<=` sval sB >]. have {}totR F (FR : total_on F R) : exists sB, forall sA, F sA -> R sA sB. have FP : [set val x | x in F] `<=` P. - by move=> _ [X FX <-]; apply: set_mem; apply: valP. + by move=> _ [X FX <-]; exact/set_mem/valP. have totF : total_on [set val x | x in F] subset. - by move=> _ _ [X FX <-] [Y FY <-]; apply: FR. - exists (SigSub (mem_set (totP _ FP totF))) => A FA; rewrite /R/=. - exact: (bigcup_sup (imageP val _)). + move=> _ _ [X FX <-] [Y FY <-]. + by have [/asboolP|/asboolP] := FR _ _ FX FY; [left|right]. + exists (SigSub (mem_set (totP _ FP totF))) => A FA. + exact/asboolP/(bigcup_sup (imageP val _)). have [| | |sA sAmax] := Zorn _ _ _ totR. -- by move=> ?; exact: subset_refl. -- by move=> ? ? ?; exact: subset_trans. -- by move=> [A PA] [B PB]; rewrite /R /= => AB BA; exact/eq_exist/seteqP. +- by move=> ?; apply/asboolP; exact: subset_refl. +- by move=> ? ? ? /asboolP ? /asboolP st; apply/asboolP; exact: subset_trans st. +- by move=> [A PA] [B PB] /asboolP AB /asboolP BA; exact/eq_exist/seteqP. - exists (val sA); case: sA => A PA /= in sAmax *; split; first exact: set_mem. - move=> B AB PB; have [BA] := sAmax (SigSub (mem_set PB)) (properW AB). + move=> B AB PB. + have : R (exist (fun x : T -> Prop => x \in P) A PA) (SigSub (mem_set PB)). + by apply/asboolP; exact: properW. + move=> /(sAmax (SigSub (mem_set PB)))[BA]. by move: AB; rewrite BA; exact: properxx. Qed. @@ -2775,58 +2707,6 @@ Qed. End maximal_disjoint_subcollection. -Definition premaximal T (R : T -> T -> Prop) (t : T) := - forall s, R t s -> R s t. - -Lemma ZL_preorder T (t0 : T) (R : T -> T -> Prop) : - (forall t, R t t) -> (forall r s t, R r s -> R s t -> R r t) -> - (forall A : set T, total_on A R -> exists t, forall s, A s -> R s t) -> - exists t, premaximal R t. -Proof. -set Teq := @gen_eqMixin T; set Tch := @gen_choiceMixin T. -pose Tpo := isPointed.Build T t0. -pose Tp : pointedType := HB.pack T Teq Tch Tpo. -move=> Rrefl Rtrans tot_max. -set eqR := fun s t => R s t /\ R t s; set ceqR := fun s => [set t | eqR s t]. -have eqR_trans r s t : eqR r s -> eqR s t -> eqR r t. - by move=> [Rrs Rsr] [Rst Rts]; split; [apply: Rtrans Rst|apply: Rtrans Rsr]. -have ceqR_uniq s t : eqR s t -> ceqR s = ceqR t. - by rewrite predeqE => - [Rst Rts] r; split=> [[Rr rR] | [Rr rR]]; split; - try exact: Rtrans Rr; exact: Rtrans rR _. -set ceqRs := ceqR @` setT; set quotR := sig ceqRs. -have ceqRP t : ceqRs (ceqR t) by exists t. -set lift := fun t => exist _ (ceqR t) (ceqRP t). -have lift_surj (A : quotR) : exists t : Tp, lift t = A. - case: A => A [t Tt ctA]; exists t; rewrite /lift; case : _ / ctA. - exact/congr1/Prop_irrelevance. -have lift_inj s t : eqR s t -> lift s = lift t. - by move=> eqRst; apply/eq_exist/ceqR_uniq. -have lift_eqR s t : lift s = lift t -> eqR s t. - move=> cst; have ceqst : ceqR s = ceqR t by have := congr1 sval cst. - by rewrite [_ s]ceqst; split; apply: Rrefl. -set repr := fun A : quotR => get [set t : Tp | lift t = A]. -have repr_liftE t : eqR t (repr (lift t)) - by apply: lift_eqR; have -> := getPex (lift_surj (lift t)). -set R' := fun A B : quotR => R (repr A) (repr B). -have R'refl A : R' A A by apply: Rrefl. -have R'trans A B C : R' A B -> R' B C -> R' A C by apply: Rtrans. -have R'antisym A B : R' A B -> R' B A -> A = B. - move=> RAB RBA; have [t tA] := lift_surj A; have [s sB] := lift_surj B. - rewrite -tA -sB; apply: lift_inj; apply (eqR_trans _ _ _ (repr_liftE t)). - have eAB : eqR (repr A) (repr B) by []. - rewrite tA; apply: eqR_trans eAB _; rewrite -sB. - by have [] := repr_liftE s. -have [A Atot|A Amax] := Zorn R'refl R'trans R'antisym. - have /tot_max [t tmax] : total_on [set repr B | B in A] R. - by move=> ?? [B AB <-] [C AC <-]; apply: Atot. - exists (lift t) => B AB; have [Rt _] := repr_liftE t. - by apply: Rtrans Rt; apply: tmax; exists B. -exists (repr A) => t RAt. -have /Amax <- : R' A (lift t). - by have [Rt _] := repr_liftE t; apply: Rtrans Rt. -by have [] := repr_liftE t. -Qed. - Section UpperLowerTheory. Import Order.TTheory. Variables (d : unit) (T : porderType d). diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 6d311b71c5..e2517f876e 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1,6 +1,5 @@ (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) Require Import BinPos. -From mathcomp Require choice. From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. From mathcomp Require Import finset interval. diff --git a/classical/wochoice.v b/classical/wochoice.v index c75343a393..35dce08987 100644 --- a/classical/wochoice.v +++ b/classical/wochoice.v @@ -171,7 +171,7 @@ have init_total Y Z: f_ind Y -> f_ind Z -> {init_seg Y Z} + {init_seg Z Y}. rewrite -(fY z Yz); congr f; apply/esym/funext=> x /=. apply/idP/idP=> [/andP[Yx] | Ix]; first by contra=> I'x; apply/minYz/andP. have Yx := sIY x Ix; rewrite Yx /=; contra: (I'z) => Rzx. - by rewrite (RYanti z x) // Rzx RIY. + by rewrite (RYanti z x) // Rzx RIY. case: iI1Y {iI1}(iI1 Z) => [<- _| iI1Y [||<-|iI1Z]//]; [by left | by right |]. by case/notCf/negP: Ich; apply/(maxI I1); [apply/asboolP|apply/predU1l]. pose U x := `[< exists2 X, x \in X & f_ind X >]. @@ -182,7 +182,7 @@ have Umax X: f_ind X -> init_seg X U. have RUanti: {in U &, antisymmetric R}. move=> x y /asboolP[X Xx indX] /asboolP[Y Yy indY]. without loss [sXY _]: x y X Y Xx Yy {indX} indY / init_seg X Y. - move=> IH. + move=> IH. by case: (init_total X Y) => // {}/IH-IH; [|rewrite andbC] => /IH->. have [/wo_chain_antisymmetric RYanti _] := indY. by apply: RYanti => //; apply: sXY. @@ -323,7 +323,7 @@ have /maxR/(_ _)/asboolP: ([predU1 z & D] : pred T, Rz : rel T) \in pwo. have /minXy/= := Xx; case: ifP => // _ /idPn[]. by rewrite negb_or andbT (memPn notDz). apply: Ux; split=> [|t /andP[/minXy]]; first exact/andP. - by rewrite /= Dy => /predU1P[-> /idPn[]|]. + by rewrite /= Dy => /predU1P[-> /idPn[]|]. case=> [|/= -> //]; last exact/predU1l. apply/asboolP; split=> [x|x y /= Dx]; first exact: predU1r. rewrite Dx => /predU1P[-> | /= Dy]; first by rewrite eqxx (negPf notDz). diff --git a/theories/forms.v b/theories/forms.v index fb8f7956fb..dccc0ae34e 100644 --- a/theories/forms.v +++ b/theories/forms.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg fingroup zmodp poly ssrnum. From mathcomp -Require Import matrix mxalgebra vector falgebra ssrnum algC algnum. +Require Import matrix mxalgebra vector falgebra ssrnum. From mathcomp Require Import fieldext. From mathcomp Require Import vector. diff --git a/theories/topology.v b/theories/topology.v index 691d1089b2..c349bc2c43 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. -From mathcomp Require Import boolp classical_sets functions. +From mathcomp Require Import boolp classical_sets functions wochoice. From mathcomp Require Import cardinality mathcomp_extra fsbigop. Require Import reals signed. @@ -3040,34 +3040,39 @@ Lemma ultraFilterLemma T (F : set_system T) : Proof. move=> FF. set filter_preordset := ({G : set_system T & ProperFilter G /\ F `<=` G}). -set preorder := fun G1 G2 : filter_preordset => projT1 G1 `<=` projT1 G2. -suff [G Gmax] : exists G : filter_preordset, premaximal preorder G. - have [GF sFG] := projT2 G; exists (projT1 G); split=> //; split=> // H HF sGH. +set preorder := + fun G1 G2 : {classic filter_preordset} => `[< projT1 G1 `<=` projT1 G2 >]. +suff [G Gmax] : exists G : {classic filter_preordset}, premaximal preorder G. + have [GF sFG] := projT2 G; exists (projT1 G); split; last exact: sFG. + split; [exact: GF|move=> H HF sGH]. have sFH : F `<=` H by apply: subset_trans sGH. - have sHG : preorder (existT _ H (conj HF sFH)) G by apply: Gmax. - by rewrite predeqE => ?; split=> [/sHG|/sGH]. + have sHG : preorder (existT _ H (conj HF sFH)) G. + by move/asboolP in sGH; exact: (Gmax (existT _ H (conj HF sFH)) sGH). + by rewrite predeqE => A; split; [move/asboolP : sHG; exact|exact: sGH]. have sFF : F `<=` F by []. -apply: (ZL_preorder ((existT _ F (conj FF sFF)) : filter_preordset)) => - [?|G H I sGH sHI ? /sGH /sHI|A Atot] //. -case: (pselect (A !=set0)) => [[G AG] | A0]; last first. - exists (existT _ F (conj FF sFF)) => G AG. - by have /asboolP := A0; rewrite asbool_neg => /forallp_asboolPn /(_ G). -have [GF sFG] := projT2 G. -suff UAF : ProperFilter (\bigcup_(H in A) projT1 H). - have sFUA : F `<=` \bigcup_(H in A) projT1 H. - by move=> B FB; exists G => //; apply: sFG. - exists (existT _ (\bigcup_(H in A) projT1 H) (conj UAF sFUA)) => H AH B HB /=. - by exists H. -apply: Build_ProperFilter. - by move=> B [H AH HB]; have [HF _] := projT2 H; apply: (@filter_ex _ _ HF). -split; first by exists G => //; apply: filterT. - move=> B C [HB AHB HBB] [HC AHC HCC]; have [sHBC|sHCB] := Atot _ _ AHB AHC. - exists HC => //; have [HCF _] := projT2 HC; apply: filterI HCC. - exact: sHBC. - exists HB => //; have [HBF _] := projT2 HB; apply: filterI HBB _. - exact: sHCB. -move=> B C SBC [H AH HB]; exists H => //; have [HF _] := projT2 H. -exact: filterS HB. +apply: (ZL_preorder (existT _ F (conj FF sFF))). +- by move=> t; exact/asboolP. +- move=> r s t; rewrite /preorder => /asboolP sr /asboolP st. + exact/asboolP/(subset_trans _ st). +- move=> A Atot; have [[G AG] | A0] := pselect (A !=set0); last first. + exists (existT _ F (conj FF sFF)) => G AG. + by have /asboolP := A0; rewrite asbool_neg => /forallp_asboolPn /(_ G). + have [GF sFG] := projT2 G. + suff UAF : ProperFilter (\bigcup_(H in A) projT1 H). + have sFUA : F `<=` \bigcup_(H in A) projT1 H. + by move=> B FB; exists G => //; exact: sFG. + exists (existT _ (\bigcup_(H in A) projT1 H) (conj UAF sFUA)) => H AH. + by apply/asboolP => B HB /=; exists H. + apply: Build_ProperFilter. + by move=> B [H AH HB]; have [HF _] := projT2 H; exact: (@filter_ex _ _ HF). + split; first by exists G => //; apply: filterT. + + move=> B C [HB AHB HBB] [HC AHC HCC]; have [sHBC|sHCB] := Atot _ _ AHB AHC. + * exists HC => //; have [HCF _] := projT2 HC; apply: filterI HCC. + by move/asboolP : sHBC; exact. + * exists HB => //; have [HBF _] := projT2 HB; apply: filterI HBB _. + by move/asboolP : sHCB; exact. + + move=> B C SBC [H AH HB]; exists H => //; have [HF _] := projT2 H. + exact: filterS HB. Qed. Lemma compact_ultra (T : topologicalType) :