From 57a54d741b30adfa4671029f0aa8a32fe204953b Mon Sep 17 00:00:00 2001 From: qvermande Date: Fri, 8 Mar 2024 17:50:13 +0100 Subject: [PATCH 1/2] Zorn etc. Co-authored-by: Georges Gonthier --- _CoqProject | 1 + classical/Make | 1 + classical/wochoice.v | 333 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 335 insertions(+) create mode 100644 classical/wochoice.v diff --git a/_CoqProject b/_CoqProject index 65ec68c2e0..54e246e2da 100644 --- a/_CoqProject +++ b/_CoqProject @@ -11,6 +11,7 @@ classical/all_classical.v classical/boolp.v classical/contra.v +classical/wochoice.v classical/classical_sets.v classical/mathcomp_extra.v classical/functions.v diff --git a/classical/Make b/classical/Make index 4d4fe74c81..888b31ef14 100644 --- a/classical/Make +++ b/classical/Make @@ -9,6 +9,7 @@ boolp.v contra.v +wochoice.v classical_sets.v mathcomp_extra.v functions.v diff --git a/classical/wochoice.v b/classical/wochoice.v new file mode 100644 index 0000000000..c75343a393 --- /dev/null +++ b/classical/wochoice.v @@ -0,0 +1,333 @@ +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +Require Import boolp contra. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Section LocalProperties. + +Context {T1 T2 T3 : Type} {T : predArgType}. +Implicit Type A : {pred T}. + +Local Notation "{ 'allA' P }" := (forall A : {pred T}, P A : Prop) (at level 0). +Local Notation ph := (phantom _). + +Definition prop_within d P & ph {allA P} := forall A, sub_mem (mem A) d -> P A. + +Lemma withinW A P : {allA P} -> prop_within (mem A) (inPhantom {allA P}). +Proof. by move=> allP ? _; apply: allP. Qed. + +Lemma withinT P : prop_within (mem T) (inPhantom {allA P}) -> {allA P}. +Proof. by move=> allP A; apply: allP. Qed. + +Lemma sub_within d d' P : + sub_mem d d' -> forall phP, @prop_within d' P phP -> @prop_within d P phP. +Proof. by move=> sdd' phP Pd' A /(_ _ _)/sdd'-/Pd'. Qed. + +End LocalProperties. + +Notation "{ 'in' <= S , P }" := + (prop_within (mem S) (inPhantom P)) : type_scope. + +Section RelDefs. + +Variables (T : Type) (R : rel T). +Implicit Types (x y z : T) (A C : {pred T}). + +(* TOTHINK: This should be ported to mathcomp. *) +Definition maximal z := forall x, R z x -> R x z. + +Definition minimal z := forall x, R x z -> R z x. + +Definition upper_bound A z := {in A, forall x, R x z}. + +Definition lower_bound A z := {in A, forall x, R z x}. + +Definition preorder := reflexive R /\ transitive R. + +Definition partial_order := preorder /\ antisymmetric R. + +Definition total_order := partial_order /\ total R. + +Definition nonempty A := exists x, x \in A. + +Definition minimum_of A z := z \in A /\ lower_bound A z. + +Definition maximum_of A z := z \in A /\ upper_bound A z. + +Definition well_order := forall A, nonempty A -> exists! z, minimum_of A z. + +Definition chain C := {in C &, total R}. + +Definition wo_chain C := {in <= C, well_order}. + +Lemma antisymmetric_wo_chain C : + {in C &, antisymmetric R} -> + {in <= C, forall A, nonempty A -> exists z, minimum_of A z} -> + wo_chain C. +Proof. +move=> Ranti Rwo A sAC /Rwo[//|z [Az lbAz]]; exists z; split=> // x [Ax lbAx]. +by apply: Ranti; rewrite ?sAC ?lbAx ?lbAz. +Qed. + +Lemma antisymmetric_well_order : + antisymmetric R -> (forall A, nonempty A -> exists z, minimum_of A z) -> + well_order. +Proof. +by move=> Ranti /withinW/(antisymmetric_wo_chain (in2W Ranti))/withinT. +Qed. + +End RelDefs. + +Lemma wo_chainW (T : eqType) R C : @wo_chain T R C -> chain R C. +Proof. +have ne_cons x s: nonempty [mem x :: s : seq T] by exists x; apply: mem_head. +have all_mem s: all [mem s : seq T] s by apply/allP. +move=> Rwo x y Cx Cy; have /Rwo[] := ne_cons x [::y]; first exact/allP/and3P. +by move=> z [] [] /or3P[] // /eqP-> /allP/and3P[] => [_|] ->; rewrite ?orbT. +Qed. + +Lemma wo_chain_reflexive (T : eqType) R C : @wo_chain T R C -> {in C, reflexive R}. +Proof. by move/wo_chainW => Rtotal x xC; rewrite -[R x x]orbb Rtotal. Qed. + +Lemma wo_chain_antisymmetric (T : eqType) R C : @wo_chain T R C -> {in C &, antisymmetric R}. +Proof. +have ne_cons x s: nonempty [mem x :: s : seq T] by exists x; apply: mem_head. +have all_mem s: all [mem s : seq T] s by apply/allP. +move/[dup]/wo_chainW => Rtotal /[dup]/wo_chain_reflexive Rxx Rwo x y xC yC. +have /Rwo[] := ne_cons x [::y]; first exact/allP/and3P. +move=> z [_ Uz] /andP[Rxy Ryx]; have /and3P[xy_x xy_y _] := all_mem [:: x; y]. +by rewrite -(Uz x) ?(Uz y); split=> //; apply/allP; rewrite /= (Rxy, Ryx) Rxx. +Qed. + +(******************************************************************************) + +Section Zorn. + +Lemma Zorn's_lemma (T : eqType) (R : rel T) (S : {pred T}) : + {in S, reflexive R} -> {in S & &, transitive R} -> + {in <= S, forall C, wo_chain R C -> exists2 z, z \in S & upper_bound R C z} -> + {z : T | z \in S & {in S, maximal R z}}. +Proof. +suffices{T R S} Zorn (T : eqType) (R : rel T) (Well := wo_chain R) : + preorder R -> (forall C, Well C -> {z | upper_bound R C z}) -> + {z | maximal R z}. +- move=> Rxx Rtr UBch; pose T1 := {x | x \in S}. + have S_T1 (u : T1): val u \in S by case: u. + have [|C1 chC1|u maxT1u] := Zorn T1 (relpre val R); last 1 first. + - by exists (val u) => // x Sx Rux; apply: (maxT1u (Sub x Sx)). + - by split=> [x|y x z]; [apply: Rxx | apply: Rtr]. + pose C := [pred x | oapp (mem C1) false (insub x)]. + have sC1C u: u \in C1 -> val u \in C by rewrite inE valK. + have memC x: x \in C -> {u | u \in C1 & val u = x}. + by rewrite inE; case: insubP => //= u _ <-; exists u. + apply/cid; suffices /UBch[_ /memC[u _ <-]//|z Sz ubCz]: wo_chain R C. + by exists (Sub z Sz) => u C1u; apply/ubCz/sC1C. + move=> A sAC [x0 Ax0]. + have [||w [[C1w minC1w] Uw]] := chC1 [preim val of A]. + - by move=> v /sAC; rewrite inE valK. + - by have /sAC/memC[u0 C1u0 Du0] := Ax0; exists u0; rewrite inE Du0. + exists (val w); do ?[split] => // [y Ay | y [Ay minAy]]. + by case/sAC/memC: Ay (Ay) => v C1v <-; apply: minC1w. + have /sAC/memC[v C1v Dv] := Ay; rewrite (Uw v) //. + by split=> [|u Au]; rewrite ?inE /= Dv // minAy. +case=> Rxx Rtr UBch; absurd_not=> nomaxR. +pose R' := [rel x y | R x y && ~~ R y x]. +have{nomaxR} /all_sig[f fP] C: {z | Well C -> upper_bound R' C z}. + have /UBch[z0 _]: Well pred0 by move=> A sA0 [x /sA0]. + have [/UBch[y RCy]|] := asboolP (Well C); last by exists z0. + have [z Ryz notRzy] := nomaxR y; exists z => _ x /RCy-Rxy /=. + by rewrite (Rtr y) //=; contra: notRzy => /Rtr->. +have notCf C: Well C -> f C \notin C. + by move/fP=> R'Cf; apply/negP=> /R'Cf/=; rewrite Rxx ?andbF. +pose f_ind X := Well X /\ {in X, forall x, f [pred y in X | ~~ R x y] = x}. +pose init_seg (X Y : {pred T}) := + {subset X <= Y} /\ {in Y, forall y, y \notin X -> upper_bound R X y}. +have init_total Y Z: f_ind Y -> f_ind Z -> {init_seg Y Z} + {init_seg Z Y}. + move=> indY indZ; pose iniYZ X := `[< init_seg X Y /\ init_seg X Z >]. + pose I x := `[< exists2 X, X \in iniYZ & x \in X >]; pose I1 := [predU1 f I & I]. + have [iIY iIZ]: init_seg I Y /\ init_seg I Z. + split; split=> [x /asboolP[X /asboolP[[sXY _] [sXZ _]]]|]; try by move: (x). + move=> y Yy /asboolP-I'y x /asboolP[X iXYZ Xx]; have /asboolP[[_ RXY] _] := iXYZ. + by rewrite RXY //; contra: I'y; exists X. + move=> z Zz /asboolP-I'z x /asboolP[X iXYZ Xx]; have /asboolP[_ [_ RXZ]] := iXYZ. + by rewrite RXZ //; contra: I'z; exists X. + have maxI: {in iniYZ, forall X, {subset X <= I}}; last clearbody I. + by move=> X sXYZ x Xx; apply/asboolP; exists X. + have Ich: Well I by have [Ych _] := indY; apply: sub_within Ych; case: iIY. + generally have iI1, iI1Y: Y indY iIY {iniYZ maxI} / {I = Y} + {init_seg I1 Y}. + have [[Ych fY] [sIY RIY]] := (indY, iIY). + have /wo_chain_antisymmetric RYanti := Ych. + have [sYI | /notP-ltIY] := asboolP {subset Y <= I}; [left | right]. + by apply/funext=> y; apply/idP/idP=> [/sIY | /sYI]. + have{ltIY} /Ych[_ /andP[]//| z [[/andP/=[I'z Yz]]]]: nonempty [predD Y & I]. + by have [y] := ltIY; exists y; apply/andP. + move=> minYz _; suffices Dz: f I = z. + rewrite /I1 Dz; do 2?[split] => // [x /predU1P[->|/sIY] // | y Yy]. + by case/norP=> /= z'y I'y x /predU1P[->|/RIY->//]; apply/minYz/andP. + 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. + 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 >]. +have Umax X: f_ind X -> init_seg X U. + move=> indX; split=> [x Xx | y]; first by apply/asboolP; exists X. + case/asboolP=> Y Yy indY notXy x Xx. + by have [[sYX _]|[_ ->//]] := init_total Y X indY indX; rewrite sYX in notXy. +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. + by case: (init_total X Y) => // {}/IH-IH; [|rewrite andbC] => /IH->. + have [/wo_chain_antisymmetric RYanti _] := indY. + by apply: RYanti => //; apply: sXY. +have Uch: Well U. + apply: antisymmetric_wo_chain => // A sAU [x0 Ax0]. + have /sAU/asboolP[X Xx0 indX] := Ax0. + pose B := [predI A & X]; have sBX: {subset B <= X} by move=> y /andP[]. + have [[Xch _] /Umax[sXU iXU]] := (indX, indX). + have{x0 Ax0 Xx0} /Xch[//|z [[/andP[/= Az Xz] minBz] _]]: nonempty B. + by exists x0; apply/andP. + exists z; split=> // y Ay; have Uy := sAU y Ay. + by have [Xy | /iXU->//] := boolP (y \in X); apply/minBz/andP. +pose U1 := [predU1 f U & U]; have notUfU: f U \notin U by apply: notCf. +suffices indU1: f_ind U1. + by have [sU1U _] := Umax U1 indU1; rewrite sU1U ?inE ?eqxx in notUfU. +have RU1fU: upper_bound R U1 (f U) by move=> x /predU1P[-> // | /fP/andP[]] . +split=> [A sAU1 neA | x U1x]. + have [sAfU | {neA}/notP[x Ax fU'x]] := asboolP {subset A <= pred1 (f U)}. + have AfU: f U \in A by have [x Ax] := neA; have /sAfU/eqP<- := Ax. + by exists (f U); split=> [|y [/sAfU/eqP//]]; split=> // _ /sAfU/eqP->. + have Ux: x \in U by case/sAU1/orP: Ax => // /idPn. + pose B := [predI A & U]; have sBU: {subset B <= U} by move=> y /andP[]. + have /Uch[//|z [[/andP[/= Az Uz] minBz] _]]: nonempty B. + by exists x; apply/andP. + have{minBz} minAz: lower_bound R A z. + move=> y Ay; case/sAU1/predU1P: (Ay) => [->|/= Uy]; first exact/RU1fU/sAU1. + exact/minBz/andP. + exists z; do ?[split] => // y [Ay minAy]. + have /sAU1/predU1P[Dy|Uy] := Ay; last by apply: RUanti; rewrite ?minAz ?minAy. + by have /andP[_] := fP U Uch z Uz; rewrite -Dy minAy. +have /predU1P[-> | /asboolP[X Xx indX]] := U1x. + congr f; apply/funext=> y; apply/idP/idP=> [|Uy]; last first. + by rewrite !inE unfold_in -/(U y) Uy orbT; case/andP: (fP U Uch y Uy). + by case/andP=> /predU1P[->|//]; rewrite Rxx. +have{indX} [[_ f_indX] /Umax[sXU iXU]] := (indX, indX). +rewrite -[RHS]f_indX //; congr f; apply/funext=> y; apply/andb_id2r=> notRyx. +apply/idP/idP=> [U1y | Xy]; last exact/predU1r/sXU. +by contra: notRyx => notXy; have /predU1P[->|/iXU->] := U1y; first apply/RU1fU. +Qed. + +Theorem Hausdorff_maximal_principle T R (S C : {pred T}) : + {in S, reflexive R} -> {in S & &, transitive R} -> chain R C -> {subset C <= S} -> + {M : {pred T} | + [/\ {subset C <= M}, {subset M <= S} + & forall X, chain R X -> {subset M <= X} -> {subset X <= S} -> M = X]}. +Proof. +move=> Rxx Rtr Cch sCS. +pose CSch X := `[< [/\ chain R X, {subset C <= X} & {subset X <= S}] >]. +pose Rch (X Y : {pred T}) := `[< {subset X <= Y} >]. +have: {in CSch & &, transitive Rch}. + by apply: in3W => X Y Z /asboolP-sXY /asboolP-sYZ; apply/asboolP=> x /sXY/sYZ. +have /Zorn's_lemma/[apply]: {in CSch, reflexive Rch} by move=> X _; apply/asboolP. +case=> [XX CSchXX XXwo | M /asboolP[Mch sCM sMS] maxM]; last first. + exists M; split=> // X Xch sMX sXS. + suffices /asboolP-sXM: Rch X M by apply/funext=> x; apply/idP/idP=> [/sMX|/sXM]. + by apply: maxM; apply/asboolP=> //; split=> // x /sCM/sMX. +move/(@wo_chainW {pred T}): XXwo => XXch. +without loss XX_C: XX CSchXX XXch / C \in XX. + have CSchC: C \in CSch by apply/asboolP; split. + have RchC_CSch X: X \in CSch -> Rch C X by case/asboolP=> _ sCX _; apply/asboolP. + pose XX1 X := `[< X = C \/ X \in XX >]. + have CSchXX1: {subset XX1 <= CSch} by move=> X /asboolP[-> | /CSchXX]. + case/(_ XX1)=> // [||Z CSchZ ubZ]; first 2 [by apply/asboolP; left]. + move=> X Y /asboolP[-> /CSchXX1/RchC_CSch-> //| XX_X]. + by rewrite orbC => /asboolP[-> | /XXch->//]; rewrite RchC_CSch ?CSchXX. + by exists Z => // X XX_X; apply/ubZ/asboolP; right. +pose D x := `[< exists2 X, X \in XX & x \in X >]. +have sCD: {subset C <= D} by move=> x Cx; apply/asboolP; exists C. +have sDS: {subset D <= S} by move=> x /asboolP[X /CSchXX/asboolP[_ _ sXS] /sXS]. +have in2D: {in D &, forall x y, exists X, [/\ X \in XX, x \in X & y \in X]}. + move=> x y /asboolP[X XX_X Xx] /asboolP[Y XX_Y Yy]; have:= XXch X Y XX_X XX_Y. + by case/orP=> [/asboolP/(_ x Xx)|/asboolP/(_ y Yy)]; [exists Y | exists X]. +exists D => [|X XX_X]; last by apply/asboolP=> x Xx; apply/asboolP; exists X. +apply/asboolP; split=> //. +move=> x y xD /(in2D x)-/(_ xD) [X [/CSchXX/asboolP[Xch _ _] Xx Xy]]. +exact: Xch. +Qed. + +Theorem well_ordering_principle (T : eqType) : {R : rel T | well_order R}. +Proof. +have{T} [T ->]: {T1 : eqType | T = T1} by exists T. +pose srel := pred T * rel T : Type. +pose loc (R : srel) := [rel x y | [&& x \in R.1, y \in R.1 & R.2 x y]]. +pose pwo (R : srel) := `[< wo_chain R.2 R.1 >]. +pose init_seg (R S : srel) := + {in R.1 & S.1, forall x y, S.2 x y = (y \in R.1) ==> R.2 x y}. +pose initR R S := `[< {subset R.1 <= S.1} /\ init_seg R S >]. +have initRR: reflexive initR by move=> R; apply/asboolP; split=> // x y _ ->. +have initRtr: transitive initR. + move=> R2 R1 R3 /asboolP[D12 R12] /asboolP[D23 R23]; apply/asboolP. + split=> [x /D12/D23// | x y D1x D3y]; rewrite R23 ?(D12 x) //. + by case D2y: (y \in R2.1); [apply: R12 | rewrite (contraFF (D12 y))]. +have: {in pwo & &, transitive initR} by apply: in3W. +have/Zorn's_lemma/[apply]: {in pwo, reflexive initR} by []. +case=> [C pwoC Cch | [D R] /asboolP/=pwoR maxR]. + have /(@wo_chainW ({pred T} * rel T)%type) {}Cch := Cch. + pose D x := `[< exists2 S, S \in C & x \in S.1 >]; pose R x y := `[< exists2 S, S \in C & loc S x y >]. + exists (D, R). + apply/asboolP=> /= X sXD [x Xx]; have /sXD/asboolP[R0 CR0 /= D0x] := Xx. + have /pwoC/asboolP/=R0wo := CR0. + have{x Xx D0x}: nonempty [predI X & R0.1] by exists x; apply/andP. + case/R0wo=> [_ /andP[]// |z [[/andP/=[Xz D0z] min0z] _]]. + have{R0 CR0 R0wo D0z min0z} minXz: lower_bound R X z. + move=> y Xy; have /sXD/asboolP[R1 /= CR1 D1y] := Xy. + have /orP[/asboolP/=[D10 R10] | /asboolP/=[D01 R01]] := Cch _ _ CR1 CR0. + by apply/asboolP; exists R0; rewrite //= D0z min0z ?inE ?Xy D10. + apply/asboolP; exists R1; rewrite //= R01 ?D1y// D01//=. + by apply/implyP=> D0y; apply/min0z/andP. + exists z; split=> // y [{}/minXz/asboolP[R0 CR0 R0zy] minXy]. + case/minXy/asboolP: Xz => {minXy} R1 CR1 R1yz. + without loss /asboolP[D01 R01]: y z R0 R1 CR0 CR1 R0zy R1yz / initR R0 R1. + by move=> IH; have /orP[/(IH y z)-> | /(IH z y)-> ] := Cch _ _ CR0 CR1. + have{R1yz R0zy} [/and3P[D1y D1z R1zy] /and3P[D0z D0y R0yz]] := (R1yz, R0zy). + have /pwoC/asboolP/wo_chain_antisymmetric R1anti := CR1. + by apply: R1anti => //; rewrite R1zy R01 // D0y R0yz. + move=> R0 CR0; apply/asboolP; split=> [x D0x|]; first by apply/asboolP; exists R0. + move=> x y D0x Dy; apply/asboolP/idP=> [[R1 CR1 /and3P[D1x D1y R1xy]] | R0xy]. + have /orP[/asboolP[_ R10] | /asboolP[_ <- //]] := Cch _ _ CR1 CR0. + by apply/implyP=> D0y; rewrite R10 // D1y R1xy. + case/asboolP: Dy => R1 CR1 D1y. + have /orP[/asboolP[D10 _] | /asboolP[D01 R01]] := Cch _ _ CR1 CR0. + by exists R0; rewrite //= D0x (implyP R0xy) D10. + by exists R1; rewrite //= D1y D01 ?R01. +exists R; apply: withinT; apply: sub_within (pwoR) => z _; assume_not=> notDz. +pose Rz x := predU1 z (if x \in D then R x else pred0). +have /maxR/(_ _)/asboolP: ([predU1 z & D] : pred T, Rz : rel T) \in pwo. + apply/asboolP=> X sXxD neX; pose XD := [predI X & D]. + have [{neX}/pwoR[_ /andP[]//|x] | sXz] := asboolP (nonempty XD); last first. + have {}sXz x: x \in X -> x = z. + move=> Xx; case/sXxD/predU1P: (Xx) => // Dx. + by case: sXz; exists x; apply/andP. + have [x Xx] := neX; exists x; have /sXz-eq_xz := Xx. + by split=> [|_ [/sXz-> //]]; split=> // _ /sXz->; apply/predU1l. + case=> -[/andP/=[Xx Dx] minXDx] Ux; exists x; split=> [|y [Xy minXy]]. + split=> // y Xy; have /sXxD/predU1P[-> | Dy] := Xy; first exact/predU1l. + by rewrite /= Dx; apply/predU1r/minXDx/andP. + have Dy: y \in D. + 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[]|]. +case=> [|/= -> //]; last exact/predU1l. +apply/asboolP; split=> [x|x y /= Dx]; first exact: predU1r. +rewrite Dx => /predU1P[-> | /= Dy]; first by rewrite eqxx (negPf notDz). +by rewrite Dy -implyNb (memPn notDz). +Qed. + +End Zorn. From d17aefe03c8247e4a4df60166f3ae20a6e242322 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 10 Apr 2024 23:16:29 +0900 Subject: [PATCH 2/2] replace original zorn lemma with georges' - CI fix to please Coq 8.16 - change copyright after consulting georges - changelog and doc --- CHANGELOG_UNRELEASED.md | 15 +++ classical/classical_sets.v | 226 +++++++++---------------------------- classical/mathcomp_extra.v | 1 - classical/wochoice.v | 50 ++++++-- theories/topology.v | 61 +++++----- 5 files changed, 139 insertions(+), 214 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 894b37d94c..1e8e625de7 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -113,6 +113,15 @@ - in `classical_sets.v`: + lemmas `xsectionP`, `ysectionP` +- file `wochoice.v`: + + definition `prop_within` + + lemmas `withinW`, `withinT`, `sub_within` + + notation `{in <= _, _}` + + definitions `maximal`, `minimal`, `upper_bound`, `lower_bound`, `preorder`, `partial_order`, + `total_order`, `nonempty`, `minimum_of`, `maximum_of`, `well_order`, `chain`, `wo_chain` + + lemmas `antisymmetric_wo_chain`, `antisymmetric_well_order`, `wo_chainW`, `wo_chain_reflexive`, + `wo_chain_antisymmetric`, `Zorn's_lemma`, `Hausdorff_maximal_principle`, `well_ordering_principle` + ### Changed - in `topology.v`: @@ -147,6 +156,9 @@ - moved from `lebesgue_integral.v` to `cardinality.v`: + hint `solve [apply: fimfunP]` +- in `classical_sets.v`: + + lemmas `Zorn` and `ZL_preorder` now require a relation of type `rel T` instead of `T -> T -> Prop` + ### Renamed - in `constructive_ereal.v`: @@ -242,6 +254,9 @@ - in `topology.v`, `function_spaces.v`, `normedtype.v`: + local notation `to_set` +- in `classical_sets.v`: + + inductive `tower` + + lemma `ZL'` ### Infrastructure diff --git a/classical/classical_sets.v b/classical/classical_sets.v index a505f73999..d908707fd8 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 *) @@ -2757,127 +2757,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)). @@ -2886,20 +2814,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 <-]; apply: set_mem; exact/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. @@ -2933,58 +2865,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 : Order.disp_t) (T : porderType d). diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 77ec6d0316..2a60b17028 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..d291241465 100644 --- a/classical/wochoice.v +++ b/classical/wochoice.v @@ -1,14 +1,45 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. Require Import boolp contra. +(**md**************************************************************************) +(* # Well-ordered choice *) +(* *) +(* This file provides proofs of Zorn's lemma, Hausdorff maximal principle, *) +(* and the well-ordering principle. It does not rely on `classical_sets.v`. *) +(* *) +(* NB: Some definitions are likely to move to MathComp. Similar definitions *) +(* can be found in `classical_sets.v` but expressed with `Prop` instead of *) +(* `bool` (in particular); there is likely to be more sharing in the future. *) +(* *) +(* ``` *) +(* nonempty A := exists x, x \in A *) +(* {in <= S, P} == the predicate P holds for all subsets of S *) +(* P has type {pred T} -> Prop for T : predArgType. *) +(* maximal R z == z is a maximal element for the relation R *) +(* minimal R z == z is a minimal element for the relation R *) +(* upper_bound R A z == for all x in A, we have R x z *) +(* lower_bound R A z == for all x in A, we have R z x *) +(* preorder R == R is reflexive and transitive *) +(* partial_order R == R is an antisymmetric preorder *) +(* total_order R == R is a total partial order *) +(* minimum_of R A z := z \in A /\ lower_bound A z *) +(* maximum_of R A z := z \in A /\ upper_bound A z *) +(* well_order R == every non-empty subset has a unique minimum element *) +(* chain R C == the subset C is totally ordered *) +(* := {in C &, total R} *) +(* wo_chain R C := {in <= C, well_order R} *) +(* ``` *) +(* *) +(******************************************************************************) + Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Section LocalProperties. +Definition nonempty {T: Type} (A : {pred T}) := exists x, x \in A. +Section LocalProperties. Context {T1 T2 T3 : Type} {T : predArgType}. Implicit Type A : {pred T}. @@ -33,11 +64,10 @@ Notation "{ 'in' <= S , P }" := (prop_within (mem S) (inPhantom P)) : type_scope. Section RelDefs. - Variables (T : Type) (R : rel T). Implicit Types (x y z : T) (A C : {pred T}). -(* TOTHINK: This should be ported to mathcomp. *) +(* TODO: This should be ported to mathcomp. *) Definition maximal z := forall x, R z x -> R x z. Definition minimal z := forall x, R x z -> R z x. @@ -52,8 +82,6 @@ Definition partial_order := preorder /\ antisymmetric R. Definition total_order := partial_order /\ total R. -Definition nonempty A := exists x, x \in A. - Definition minimum_of A z := z \in A /\ lower_bound A z. Definition maximum_of A z := z \in A /\ upper_bound A z. @@ -103,8 +131,6 @@ move=> z [_ Uz] /andP[Rxy Ryx]; have /and3P[xy_x xy_y _] := all_mem [:: x; y]. by rewrite -(Uz x) ?(Uz y); split=> //; apply/allP; rewrite /= (Rxy, Ryx) Rxx. Qed. -(******************************************************************************) - Section Zorn. Lemma Zorn's_lemma (T : eqType) (R : rel T) (S : {pred T}) : @@ -171,7 +197,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 +208,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 +349,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/topology.v b/theories/topology.v index 25686fd456..b965b10c7c 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -2,8 +2,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. From mathcomp Require Import archimedean. -From mathcomp Require Import boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop. +From mathcomp Require Import boolp classical_sets functions wochoice. +From mathcomp Require Import cardinality mathcomp_extra fsbigop. Require Import reals signed. (**md**************************************************************************) @@ -3048,34 +3048,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) :