changelog and doc

CHANGELOG_UNRELEASED.md

@@ -111,6 +111,15 @@
     `parameterized_integral_continuous`
   + corollary `continuous_FTC2`
 
+- 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`:
@@ -145,6 +154,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`:
@@ -238,6 +250,10 @@
   + lemmas `floor0`, `floor1`
   + lemma `le_floor` (use `Num.Theory.floor_le` instead)
 
+- in `classical_sets.v`:
+  + inductive `tower`
+  + lemma `ZL'`
+
 ### Infrastructure
 
 ### Misc

classical/wochoice.v

@@ -2,12 +2,44 @@
 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}.
 
@@ -32,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.
@@ -51,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.