From 5da813c6798fe7b1124076c479115524c993dc81 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Thu, 20 Jul 2023 18:13:40 +0900
Subject: [PATCH] Zorn lemma for inclusion (#978)

* Zorn lemma for inclusion

Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>
Co-authored-by: Cyril Cohen <cohen@crans.org>
---
 CHANGELOG_UNRELEASED.md    |  3 +++
 classical/classical_sets.v | 37 ++++++++++++++++++++++++++++++++-----
 2 files changed, 35 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 0252e99cf..8a0ca059d 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -61,6 +61,9 @@
 - in `classical_sets.v`:
   + lemmas `properW`, `properxx`
 
+- in `classical_sets.v`:
+  + lemma `Zorn_bigcup`
+
 ### Changed
 
 - moved from `lebesgue_measure.v` to `real_interval.v`:
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index 1655043cc..4b6a0c008 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -2677,12 +2677,12 @@ Lemma Zorn T (R : T -> T -> Prop) :
   exists t, forall s, R t s -> s = t.
 Proof.
 move=> Rrefl Rtrans Rantisym Rtot_max.
-set totR := ({A : set T | total_on A R}).
+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'; case: A; case: B => /= B totB A totA sAB sBA.
+  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.
@@ -2693,7 +2693,7 @@ have R'tot_lub A : total_on A R' -> exists t, (forall s, A s -> R' s t) /\
       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 ? ? ?; exists B.
   by move=> B Bub ? /= [? /Bub]; apply.
 apply: contrapT => nomax.
 have {}nomax t : exists s, R t s /\ s <> t.
@@ -2708,9 +2708,9 @@ have Astot : total_on (sval A `|` [set s]) R.
     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.
+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.
+  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|->]].
@@ -2719,6 +2719,33 @@ apply: eq_exist; rewrite predeqE => r; split=> [Br|/sAB] //.
 by have /sBAs [|ser] // := Br; rewrite ser in Br.
 Qed.
 
+Section Zorn_subset.
+Variables (T : Type) (P : set (set T)).
+
+Lemma Zorn_bigcup :
+    (forall F : set (set T), F `<=` P -> total_on F subset ->
+      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.
+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.
+   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 _)).
+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.
+- 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).
+  by move: AB; rewrite BA; exact: properxx.
+Qed.
+
+End Zorn_subset.
+
 Definition premaximal T (R : T -> T -> Prop) (t : T) :=
   forall s, R t s -> R s t.