From 1164de27bfacfe1f971d2806c67d9cf3eccf6b03 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 19 Dec 2023 10:22:37 +0100 Subject: [PATCH] added wochoice.v in classical --- _CoqProject | 1 + classical/Make | 1 + classical/wochoice.v | 1411 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 1413 insertions(+) create mode 100644 classical/wochoice.v diff --git a/_CoqProject b/_CoqProject index 92897c40b0..748914597d 100644 --- a/_CoqProject +++ b/_CoqProject @@ -10,6 +10,7 @@ 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 b498a965a7..488a00c694 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..b5af56dfc1 --- /dev/null +++ b/classical/wochoice.v @@ -0,0 +1,1411 @@ +(* (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. + +(******************************************************************************) +(* This file contains the definitions of: *) +(* choiceType == interface for types with a choice operator. *) +(* countType == interface for countable types (implies choiceType). *) +(* subCountType == interface for types that are both subType and countType. *) +(* xchoose exP == a standard x such that P x, given exP : exists x : T, P x *) +(* when T is a choiceType. The choice depends only on the *) +(* extent of P (in particular, it is independent of exP). *) +(* choose P x0 == if P x0, a standard x such that P x. *) +(* pickle x == a nat encoding the value x : T, where T is a countType. *) +(* unpickle n == a partial inverse to pickle: unpickle (pickle x) = Some x *) +(* pickle_inv n == a sharp partial inverse to pickle pickle_inv n = Some x *) +(* if and only if pickle x = n. *) +(* choiceMixin T == type of choice mixins; the exact contents is *) +(* documented below in the Choice submodule. *) +(* ChoiceType T m == the packed choiceType class for T and mixin m. *) +(* [choiceType of T for cT] == clone for T of the choiceType cT. *) +(* [choiceType of T] == clone for T of the choiceType inferred for T. *) +(* CountType T m == the packed countType class for T and mixin m. *) +(* [countType of T for cT] == clone for T of the countType cT. *) +(* [count Type of T] == clone for T of the countType inferred for T. *) +(* [choiceMixin of T by <:] == Choice mixin for T when T has a subType p *) +(* structure with p : pred cT and cT has a Choice *) +(* structure; the corresponding structure is Canonical.*) +(* [countMixin of T by <:] == Count mixin for a subType T of a countType. *) +(* PcanChoiceMixin fK == Choice mixin for T, given f : T -> cT where cT has *) +(* a Choice structure, a left inverse partial function *) +(* g and fK : pcancel f g. *) +(* CanChoiceMixin fK == Choice mixin for T, given f : T -> cT, g and *) +(* fK : cancel f g. *) +(* PcanCountMixin fK == Count mixin for T, given f : T -> cT where cT has *) +(* a Countable structure, a left inverse partial *) +(* function g and fK : pcancel f g. *) +(* CanCountMixin fK == Count mixin for T, given f : T -> cT, g and *) +(* fK : cancel f g. *) +(* GenTree.tree T == generic n-ary tree type with nat-labeled nodes and *) +(* T-labeled leaves, for example GenTree.Leaf (x : T), *) +(* GenTree.Node 5 [:: t; t']. GenTree.tree is equipped *) +(* with canonical eqType, choiceType, and countType *) +(* instances, and so simple datatypes can be similarly *) +(* equipped by encoding into GenTree.tree and using *) +(* the mixins above. *) +(* CodeSeq.code == bijection from seq nat to nat. *) +(* CodeSeq.decode == bijection inverse to CodeSeq.code. *) +(* In addition to the lemmas relevant to these definitions, this file also *) +(* contains definitions of a Canonical choiceType and countType instances for *) +(* all basic datatypes (e.g., nat, bool, subTypes, pairs, sums, etc.). *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(******************************************************************************) +(**** ssrfun contents ****) +(******************************************************************************) + +(** header **) +(* nfun n A R == A -> ... A -> R (with n A arguments). *) +(* ndfun n A R == forall (i1 : D) (x1 : A i1) ... (xn : A i_n), R *) +(* S <--> T == S and T are equipotent types (i.e., S -> T and T -> S). *) +(* move_view S T == an S -> T wrapper that does _NOT_ coerce to S -> T, but *) +(* is usable as an S -> T move/ view. Useful for views with *) +(* indeterminate T, to force matching the top assumption *) +(* with S and prevent overapplication of the view. *) +(* Forall P == forall x, P x for P : A -> S with A a Type and S a sort. *) +(* A forallSort structure implicit argument handles the *) +(* nonuniform forall typing rules for Type/Set/Prop (SProp, *) +(* which follows a different pattern, is not handled). The *) +(* Forall combinator can be used as a rewrite or projection *) +(* head constant, and for congruence (i.e., congr Forall). *) +(* \Forall x ... z, E == Forall (fun x => ... Forall (fun z => E) ... ). *) +(* ForallI == change the first forall in the goal into a Forall (this *) +(* might be a non-dependent forall, i.e., P -> Q). *) +(* ForallI pat == change the term described by pat into a Forall. *) +(* wrappedType == specialization of wrapped to Type, which coerces to Type *) +(* and whose default instance has 4 wrapping layers. *) +(* wrappedProp == specialization of wrapped to Prop, which coerces to Type *) +(* and whose default instance has 4 wrapping layers. *) + +(* option complements *) + +Lemma isSome_map S T (f : S -> T) u : isSome (omap f u) = u. +Proof. by case: u. Qed. + +Lemma isSome_bind S T (f : S -> option T) u : isSome (obind f u) -> u. +Proof. by case: u. Qed. + +Lemma ocancel_id T f x : @ocancel T T f id -> f x -> f x = Some x. +Proof. by move=> /(_ x); case: f => //= _ ->. Qed. + +(* n-ary function type constructors. *) + +Definition nfun n A := iter n (fun R => A -> R). +Definition ndfun n {D} A := iter n (fun R => forall (i : D) (x : A i), R). + +(* More eq groupoid lemmas (in addition to the existing esymK). *) +(* Most of these are in Logic, under a different naming convention. *) + +Section EqGroupoid. + +Variables (S R : Type) (T U : S -> Type) (V : R -> Type). +Variables (f : S -> R) (g : forall x, T x) (h : forall x, T x -> U x). +Variable (k : forall x, T x -> V (f x)). +Variables x1 x2 x3 x4 : S. +Hypotheses (eq12 : x1 = x2) (eq23 : x2 = x3) (eq34 : x3 = x4). + +Definition etransr (eq31 : x3 = x1) : x3 = x2 := etrans eq31 eq12. +Definition etransl (eq13 : x1 = x3) : x2 = x3 := etrans (esym eq12) eq13. + +Lemma etrans_refl : etrans (erefl x1) eq12 = eq12. +Proof. by case: x2 / eq12. Defined. + +Lemma etrans_reflr : etrans eq12 (erefl x2) = eq12. Proof. by []. Defined. + +Lemma etrans_syml : etrans (esym eq12) eq12 = erefl x2. +Proof. by case: x2 / eq12. Defined. + +Lemma etrans_symr : etrans eq12 (esym eq12) = erefl x1. +Proof. by case: x2 / eq12. Defined. + +Lemma esym_trans : esym (etrans eq12 eq23) = etrans (esym eq23) (esym eq12). +Proof. by case: x3 / eq23; case: x2 / eq12. Defined. + +Lemma etransA : etrans eq12 (etrans eq23 eq34) = etrans (etrans eq12 eq23) eq34. +Proof. by case: x4 / eq34. Defined. + +Lemma etransKl : etrans (esym eq12) (etrans eq12 eq23) = eq23. +Proof. by case: x3 / eq23; apply: etrans_syml. Defined. + +Lemma etransKVl (eq13 : x1 = x3) : etrans eq12 (etrans (esym eq12) eq13) = eq13. +Proof. by case: x3 / eq13; apply: etrans_symr. Defined. + +Lemma etransKr : etrans (etrans eq12 eq23) (esym eq23) = eq12. +Proof. by case: x3 / eq23. Defined. + +Lemma etransKVr (eq32 : x3 = x2) : etrans (etrans eq12 (esym eq32)) eq32 = eq12. +Proof. by case: x2 / eq32 eq12. Defined. + +(* Transport action. *) + +Notation ecastT E y := (ecast x (T x) E y). + +Lemma ecast_refl y : ecastT (erefl x1) y = y. Proof. by []. Defined. + +Lemma ecast_trans y : ecastT (etrans eq12 eq23) y = ecastT eq23 (ecastT eq12 y). +Proof. by case: x3 / eq23. Defined. + +Lemma ecastK y : ecastT (esym eq12) (ecastT eq12 y) = y. +Proof. by case: x2 / eq12. Defined. + +Lemma ecastKv y : ecastT eq12 (ecastT (esym eq12) y) = y. +Proof. by case: x2 / eq12 y. Defined. + +(* Congruence morphism. *) + +Notation "e ^f" := (congr1 f e) (at level 8, format "e ^f") : type_scope. + +Lemma congr1refl : (erefl x1)^f = erefl (f x1). Proof. by []. Defined. + +Lemma congr1trans : (etrans eq12 eq23)^f = etrans eq12^f eq23^f. +Proof. by case: x3 / eq23. Defined. + +Lemma congr1sym : (esym eq12)^f = esym eq12^f. +Proof. by case: x2 / eq12. Defined. + +Lemma ecast_congr1 z : + ecast y (V y) (congr1 f eq12) z = ecast x (V (f x)) eq12 z. +Proof. by case: x2 / eq12. Defined. + +Lemma ecast_congrT y : ecast U U (congr1 T eq12) y = ecast x (T x) eq12 y. +Proof. by case: x2 / eq12. Defined. + +(* Cast substitution *) + +Lemma ecast_const y : ecast x R eq12 y = y. Proof. by case: x2 / eq12. Defined. + +Lemma ecast_subst : ecast x (T x) eq12 (g x1) = g x2. +Proof. by case: x2 / eq12. Defined. + +Lemma ecast_subst_fun y : ecast x (U x) eq12 (h y) = h (ecast x (T x) eq12 y). +Proof. by case: x2 / eq12. Defined. + +Lemma ecast_subst_congr z : + ecast y (V y) (congr1 f eq12) (k z) = k (ecast x (T x) eq12 z). +Proof. by case: x2 / eq12. Defined. + +End EqGroupoid. + +Lemma congr1idl T h (id_h : id =1 h) x : congr1 h (id_h x) = id_h (h x : T). +Proof. +set Exhx := id_h x; set Exy := Exhx; set y := h x in Exy *. +transitivity (etrans (etrans (esym Exy) Exhx) (congr1 h Exy)). + by rewrite etrans_syml etrans_refl. +by case: y / Exy; rewrite etrans_refl. +Defined. + +Lemma congr1idr T h (h_id : h =1 id) x : congr1 h (h_id x) = h_id (h x : T). +Proof. +pose id_h x := esym (h_id x). +by rewrite -[h_id x]esymK congr1sym (congr1idl id_h) esymK. +Defined. + +(* Making nat equalities normalize to erefl on ground instances. *) + +Definition nat_cast : forall m n, m = n -> m = n := + let fix addr i j := if i is i1.+1 then addr i1 j.+1 else j in + let eqn i j k := addr i j = addr i k in + let fix loop i j1 k1 : eqn i j1 k1 -> eqn i j1 k1 := match j1, k1 with + j.+1, k.+1 => loop i.+1 j k | 0, 0 => fun=> erefl | _, _ => id + end in loop 0. +Arguments nat_cast {m n} eq_mn : simpl never. + +Lemma nat_castK n Enn : @nat_cast n n Enn = erefl n. +Proof. +rewrite /nat_cast; set loop := (loop in loop 0). +set addr := fix addr i j := if i is k.+1 then addr k j.+1 else j in loop *. +rewrite -[n]/(addr 0 n) -[loop 0 _ _]/(loop 0 n n) in Enn *. +elim: n => [|n IHn] //= in (m := 0) Enn *; apply: (IHn m.+1 Enn). +Defined. + +Lemma nat_castE m n Emn : @nat_cast m n Emn = Emn. +Proof. by case: n / Emn; apply: nat_castK. Qed. + +Lemma nat_cast_irr m n Emn1 Emn2 : @nat_cast m n Emn1 = nat_cast Emn2. +Proof. by case: n / {Emn2}(nat_cast Emn2) in Emn1 *; apply: nat_castK. Defined. + +Polymorphic Lemma nat_cast_r@{i} n (T : forall m, m = n -> Type@{i}) : + T n (erefl n) -> forall m (Emn : m = n), T m (nat_cast Emn). +Proof. +move=> Tnn m Emn; case: m / {Emn}(nat_cast (esym Emn)) (Emn) => Emn. +by rewrite nat_castK. +Defined. + +Polymorphic Lemma nat_castS@{i} m n (Emn : m = n) (Emn1 : m.+1 = n.+1) + (T : nat -> Type@{i}) (x : T m.+1) : + ecast n (T n) (nat_cast Emn1) x = ecast n (T n.+1) (nat_cast Emn) x. +Proof. +by case: n / {Emn}(nat_cast Emn) in x Emn1 *; rewrite nat_castK. +Defined. + + +(******************************************************************************) +(* Type-level equivalence *) +(******************************************************************************) + +Variant equivT S T := EquivT of S -> T & T -> S. +Notation "S <--> T" := (equivT S T) (at level 95, no associativity). + +Definition equivT_refl S : S <--> S := EquivT id id. +Definition equivT_transl {S T U} : S <--> T -> S <--> U -> T <--> U := + fun '(EquivT S_T T_S) '(EquivT S_U U_S) => EquivT (S_U \o T_S) (S_T \o U_S). +Definition equivT_sym {S T} : S <--> T -> T <--> S := + equivT_transl^~ (equivT_refl S). +Definition equivT_trans {S T U} : S <--> T -> T <--> U -> S <--> U := + equivT_transl \o equivT_sym. +Definition equivT_transr {S T U} eqST : U <--> S -> U <--> T := + equivT_trans^~ eqST. +Definition equivT_Prop (P Q : Prop) : (P <--> Q) <-> (P <-> Q). +Proof. split; destruct 1; split; assumption. Defined. +Definition equivT_LR {S T} '(EquivT S_T _) : S -> T := S_T. +Definition equivT_RL {S T} '(EquivT _ T_S) : T -> S := T_S. + +Hint View for move/ equivT_LR|2 equivT_RL|2. +Hint View for apply/ equivT_RL|2 equivT_LR|2. + +(******************************************************************************) +(* Universe polymorphic dependent pairs (i.e., sigT in Init.Datatypes), *) +(* with more supporting Notation, in particular for constructors and non *) +(* dependent pairs. *) +(******************************************************************************) + +Polymorphic Variant dpair@{i} {A : Type@{i}} (T : A -> Type@{i}) : Type@{i} := + Dpair x of T x. + +Notation "{ 'dpair' x .. z , T }" := + (dpair (fun x => .. (dpair (fun z => T)) .. )) + (at level 0, x binder, z binder, + format "{ '[hv' 'dpair' '[' x '/' .. '/' z , ']' '/ ' T } ']'") + : type_scope. +Notation "{ 'pair' S , T }" := {dpair _ : S, T} + (at level 0, format "{ 'pair' S , T }") : type_scope. + +Arguments Dpair {A T} x y. +Polymorphic Definition Pair@{i} {S T : Type@{i}} : S -> T -> {pair S, T} := + @Dpair S (fun=> T). +Notation "[ 'dpair' x := y , v : T ]" := (@Dpair _ (fun x => T) y v) + (at level 0, x ident, v at level 99, + format "[ 'dpair' '[hv' x := y , '/' v : T ] ']'") : form_scope. +Notation "[ 'dpair' x : A := y , v : T ]" := (@Dpair A (fun x => T) y v) + (at level 0, x ident, v at level 99, only parsing) : form_scope. +Notation "[ 'dpair' x , v : T ]" := (@Dpair _ (fun x => T) x v) + (at level 0, x ident, v at level 99, + format "[ 'dpair' x , '/' v : T ]") : form_scope. +Notation "[ 'dpair' x : A , v : T ]" := (@Dpair A (fun x => T) x v) + (at level 0, x ident, v at level 99, only parsing) : form_scope. +Notation "[ 'dpair' := y , v ]" := (Dpair y v) + (at level 0, only parsing) : form_scope. +Notation "[ 'pair' x , y ]" := (Pair x y) + (at level 0, format "[ 'pair' '[hv' x , '/' y ] ']'") : form_scope. + +Polymorphic Definition dfst@{i} {A T} : @dpair@{i} A T -> A := + fun '(Dpair x _) => x. +Notation "u .1d" := (dfst u) (at level 2, format "u .1d") : pair_scope. +Polymorphic Definition dsnd@{i} {A T} : forall u : @dpair@{i} A T, T u.1d := + fun '(Dpair _ y) => y. +Notation "u .2d" := (dsnd u) (at level 2, format "u .2d") : pair_scope. +Polymorphic Definition ndsnd@{i} {S T : Type@{i}} : {pair S, T} -> T := dsnd. +Notation "u .2nd" := (ndsnd u) (at level 2, format "u .2nd") : pair_scope. + +Polymorphic Lemma dpair_eta@{i} S T u : u = @Dpair@{i} S T u.1d u.2d. +Proof. by case: u. Defined. + +(******************************************************************************) +(* The Context module provides support for a shallow embedding of Gallina *) +(* contexts, allowing abstraction over (fully) dependent sequences of binders *) +(* as well as instantiation of such abstrations. It defines: *) +(* context == type of sequences of dependent types *) +(* [ctx (X1 : A1) (X2 : A2) .... (Xn : An)] *) +(* where X1 may appear in T2, ... and X1, ..., Xn-1 in Tn. *) +(* Null is the null context, and Abs A ctxA is the context *) +(* starting with (x : A), and continuing with ctxA x : context. *) +(* --> The %ctx scope is bound to type context, and open by default. *) +(* [ctx (X1 : A1) ... (Xn : An), C] := Notation for a context that begins *) +(* with (X1 : A1) .. (Xn : An) and continues with C (in which *) +(* X1 .. Xn may appear. The notation supports the usual binder *) +(* conventions: type can be omitted or grouped, and parentheses *) +(* may be omitted when there is only a single constraint. Also, *) +(* the ', C' part may be omitted when C is Null, so that *) +(* [ctx (X1 : A1) .. (Xn : An)] denotes a contex of length n. *) +(* Furthermore if n = 1 X1 may be omitted if it does not occur *) +(* in C, e.g., when C is Null, so [ctx: A] denotes a context of *) +(* length 1. *) +(* --> Below we assume ctx : context is [ctx (X1 : A1) .. (Xn : An)], and *) +(* ctx2 : context is [ctx (Y1 : B1) .. (Ym : Bm)]. *) +(* telescope == a context >-> Sortclass coercion, interpreting a context as *) +(* the coresponding type of dependent value sequences, i.e., *) +(* v : ctx means v : {dpair (X1 : A1) ... (Xn : An), unit}. *) +(* --> The %tele scope is bound to telescope, but not open by defaut. *) +(* [tele x : A := y, v : ctx] == the telescope in [ctx x : A, ctx] that *) +(* consists of y followed by v (i.e., [dpair y, v]). The ': A' *) +(* type constraint may be omitted, ':= y' can be omitted if *) +(* y = x; alternatively x and both type constraints can be *) +(* can be omitted, and further v can also be omitted if ctx is *) +(* Null (and v is tt). *) +(* ctx /.v T == the type of dependent functions with arguments in ctx and *) +(* whose result type T may depend on a telescope v : ctx. *) +(* := forall (X1 : A1) .. (Xn : An), *) +(* let v := [tele X1 : A1, .. [tele:= Xn] ..] in T. *) +(* --> ctx /.v T is notation for under (fun v : ctx => T). *) +(* ctx / T := ctx /.v T where T does not depend on v. n *) +(* := forall (X1 : A1) .. (Xn : An), T. *) +(* A ->.x B := forall x, B (alternative notation). *) +(* cf.[v] == apply cf : ctx /.v T to the contents of telescope v : ctx. *) +(* := let: Dpair y1 (Dpair y2 ...) := v return T in cf y1 ... yn *) +(* --> cf.[v] is notation for subst cf v. *) +(* wType_subst cT v == WrapType cT.[v] with the computation interlocked so *) +(* the WrapType constructor is only exposed AFTER w2 has been *) +(* decomposed and passed to cT. *) +(* abs f == the function of type ctx /.v T derived from f : ctx ->.v T, *) +(* which maps X1 .. Xn to f [tele X1, .. [tele:= Xn] ..]. *) +(* cf =* cg <-> functions cf, cg : ctx /.v T are extensionally equal. *) +(* := forall X1 .. Xn, cf X1 .. Xn = cg X1 .. Xn. *) +(* ctx :+ cT == extend ctx on the right with cT : ctx / Type. *) +(* := [ctx (X1 : A1) .... (Xn : An) (Xn+1: cT X1 ... Xn)]. *) +(* (v :+ z)%tele == the ctx :+ cT telescope (for cT : ctx / Type) obtained by *) +(* extending telescope v : ctx with z : cT.[v]. *) +(* split_extend vz == the decomposition of vz : ctx :+ cT into a dependent *) +(* telescope-value pair of type {dpair v : ctx, cT.[v]}. *) +(* ctx ++ ctx2 == sum (non-dependent concatenation) of ctx, ctx2 : context. *) +(* := [ctx (X1 : A1) ... (Xn : An) (Y1 : B1) .. (Ym : Bm)]. *) +(* --> ctx ++ ctx2 is notation for sum ctx ctx2. *) +(* (v ++ w)%tele == the ctx ++ ctx2 telescope obtained by concatenating *) +(* v : ctx and w : ctx'. *) +(* split_sum vw == the decomposition of vw : ctx ++ ctx2 into a pair of *) +(* telescopes of type {pair ctx, ctx2}. *) +(* split_sum_under cvw == decomposition of cvw : ctx / (ctx1 ++ ctx2) into *) +(* a pair of functions of type {pair ctx / ctx1, ctx / ctx2}. *) +(* map g cf == the ctx / T function obtained by composing g : S -> T with *) +(* cf : ctx / S, and which maps X1 .. Xn to g (cf X1 ... Xn). *) +(* map2 h cf cg == the ctx / R function obtained by composing f : S -> T -> R *) +(* with both cf : ctx / S and cg : ctx / T, which thus maps *) +(* X1..Xn to h (cf X1..Xn) (cg X1..Xn). *) +(* dmap g cf == the (ctx :+ map S w) / R function obtained by composing *) +(* the dependent function g : S ->.x T x -> R with cf : ctx / S *) +(* and which maps X1 .. Xn (Xn+1 : T (cf X1..Xn)) to *) +(* f (cf X1..Xn) Xn+1. *) +(* map_sum h cf cg == a (ctx + ctx') / R function obtained by composing *) +(* h : S -> T -> R with cf : ctx / S and cg : ctx' / T, and *) +(* which maps X1..Xn Y1..Ym to h (cf X1..Xn) (cg Y1..Yn). *) +(* Because some uses of Context involve self-application, all the contents of *) +(* this module is universe polymorphic. *) +(******************************************************************************) + +Module Context. + +Set Universe Polymorphism. +Set Printing Universes. + +Inductive context@{i} : Type@{i+1} := Null | Abs (A : Type@{i}) of A -> context. +Arguments Abs A ctxA : clear implicits. + +Fixpoint telescope@{i} (ctx : context@{i}) : Type@{i} := + if ctx is Abs A ctxA then dpair@{i} (fun x => telescope (ctxA x)) else unit. +Coercion telescope : context >-> Sortclass. + +Declare Scope context_scope. +Declare Scope telescope_scope. + +Bind Scope context_scope with context. +Bind Scope telescope_scope with telescope. + +Delimit Scope context_scope with ctx. +Delimit Scope telescope_scope with tele. + +Local Open Scope context_scope. + +Notation "[ 'ctx' x .. z , C ]" := + (Abs _ (fun x => .. (Abs _ (fun z => C)) .. )) + (at level 0, x binder, z binder, + format "[ 'ctx' x .. z , C ]") : form_scope. +Notation "[ 'ctx' x .. z ]" := + (Abs _ (fun x => .. (Abs _ (fun z => Null)) .. )) + (at level 0, x binder, z binder, + format "[ 'ctx' x .. z ]") : form_scope. +Notation "[ 'ctx' : A , C ]" := (Abs A (fun=> C)) + (at level 0, format "[ 'ctx' : A , C ]") : form_scope. +Notation "[ 'ctx' : A ]" := [ctx: A , Null] + (at level 0, format "[ 'ctx' : A ]") : form_scope. + +Definition TelePair@{i} A ctxA y v : Abs@{i} A ctxA := @Dpair A ctxA y v. +Notation "[ 'tele' x := y , v : ctx ]" := (@TelePair _ (fun x => ctx) y v) + (at level 0, x ident, v at level 99, + format "[ 'tele' '[hv' x := y , '/' v : ctx ] ']'") : form_scope. +Notation "[ 'tele' x , v : ctx ]" := (@TelePair _ (fun x => ctx) x v) + (at level 0, x ident, v at level 99, + format "[ 'tele' x , v : ctx ]") : form_scope. +Notation "[ 'tele' := y , v ]" := (@TelePair _ _ y v) + (at level 0, only parsing) : form_scope. +Notation "[ 'tele' := y ]" := (@TelePair _ (fun=> Null) y tt) + (at level 0, format "[ 'tele' := y ]") : form_scope. + +Reserved Notation "ctx /. v T" + (at level 40, v ident, T at next level, format "ctx /. v T"). +Reserved Notation "ctx ++. v T" + (at level 60, v ident, T at next level, format "ctx ++. v T"). +(*Notation "A ->. x T" := (forall x : A, T) + (at level 99, x ident, T at level 200, right associativity, only parsing). *) +Reserved Notation "cf =* cg" (at level 70). +Reserved Notation "s :+ x" (at level 60). + +Implicit Type ctx : context. + +(* Operator definitions. *) + +Fixpoint under@{i j} {ctx : context@{j}} : (ctx -> Type@{i}) -> Type@{i} := + if ctx isn't Abs A ctxA then @^~ tt else + fun T => forall x, ctxA x /.v T [tele:= x, v] +where "ctx /. v T" := (@under ctx (fun v => T)) : context_scope. +Notation "ctx / T" := (@under ctx (fun=> T)) : context_scope. + +Fixpoint eq_under@{i j} {ctx} : forall {T} (cT1 cT2 : @under@{i j} ctx T), Prop := + if ctx isn't Abs A ctxA then fun=> eq else + fun T cT1 cT2 => forall x : A, cT1 x =* cT2 x +where "c1 =* c2" := (eq_under c1 c2) : type_scope. + +Fixpoint subst@{i j} {ctx} : forall {T}, @under@{i j} ctx T -> forall v, T v := + if ctx isn't Abs A ctxA then fun T y 'tt => y else + fun T cf '(Dpair x v) => (cf x).[v] +where "cf .[ v ]" := (subst cf v) : context_scope. + +Fixpoint abs@{i j} {ctx : context@{j}} : + forall {T : ctx -> Type@{i}}, (forall v, T v) -> @under@{i j} ctx T := + if ctx isn't Abs A ctxA then fun T : unit -> Type@{i} => @^~ tt else + fun T f x => abs (fun v => f [tele:= x, v]). + +Fixpoint wType_subst@{i j} {ctx : context@{j}} : + @under@{i j} ctx (fun=> Type@{j}) -> ctx -> wrappedType := + if ctx isn't Abs A ctxA then fun T _ => WrapType T else + fun cT '(Dpair x v) => wType_subst (cT x) v. + +Fixpoint join@{i} {ctx : context@{i}} : (ctx -> context@{i}) -> context@{i} := + if ctx isn't Abs A ctxA then @^~ tt else + fun K => [ctx x, ctxA x ++.v K [tele:= x, v]] +where "ctx ++. v ctx2" := (@join ctx (fun v => ctx2)) : context_scope. +Notation "ctx ++ ctx2" := (@join ctx (fun=> ctx2)) : context_scope. + +Definition extend@{i} ctx (cT : ctx -> Type@{i}) := ctx ++.v [ctx: cT v]. +Notation "ctx :+ cT" := (@extend ctx cT) : context_scope. + +Fixpoint join_tele@{i} {ctx} : + forall {K : ctx -> context} v, K v -> join@{i} K := + if ctx isn't Abs A ctxA then fun K 'tt w => w else + fun K '(Dpair x v) w => [tele:= x, v ++ w] +where "v ++ w" := (@join_tele _ _ v w) : telescope_scope. + +Fixpoint split_join@{i} {ctx} : forall {K}, ctx ++.v K v -> {dpair v, K v} := + if ctx isn't Abs A ctxA then (@Dpair Null@{i})^~ tt else fun K '(Dpair x u) => + let: Dpair v w := split_join u in [dpair:= [tele:= x, v], w]. + +Definition split_extend@{i} {ctx cT} (u : ctx :+ cT) : {dpair v, cT v} := + let: Dpair v w := split_join@{i} u in [dpair:= v, w.1d]. + +Lemma join_teleK@{i} ctx K v w : + @split_join@{i} ctx K (v ++ w) = [dpair:= v, w]. +Proof. by elim: ctx v => [|A ctxA IH] [] //= x v in K w *; rewrite IH. Defined. + +Definition extend_tele@{i} {ctx cT} v z : ctx :+ cT := + @join_tele@{i} ctx _ v [tele:= z]. +Notation "v :+ z" := (@extend_tele _ _ v z) : telescope_scope. + +Lemma extend_teleK@{i} ctx cT v z : + split_extend@{i} (v :+ z) = [dpair v : ctx, z : cT v]. +Proof. by rewrite /split_extend join_teleK. Defined. + +Variant depth := FullDepth | PartialDepth of nat. +Definition as_deep h k := + if k isn't PartialDepth k1 then true else + if h isn't PartialDepth h1 then false else h1 <= k1. +Notation "h <= k" := (as_deep h k) : telescope_scope. + +Fixpoint trunc_rec@{i} (ctx : context@{i}) h1 : context@{i} := + if ctx isn't Abs A ctxA then Null else if h1 isn't h.+1 then Null else + [ctx x, trunc_rec (ctxA x) h]. +Definition truncate@{i} ctx h := + if h is PartialDepth h1 then trunc_rec@{i} ctx h1 else ctx. +Notation "ctx `_ h" := (truncate ctx h) : context_scope. + +Fixpoint trunc_tele_rec@{i} {ctx : context} h1 : ctx -> trunc_rec@{i} ctx h1 := + if ctx isn't Abs A ctxA then fun=>tt else if h1 isn't h.+1 then fun=> tt else + fun v => [tele:= v.1d, @trunc_tele_rec (ctxA _) h v.2d]. +Definition truncate_tele@{i} {ctx : context@{i}} (v : ctx) h : ctx`_h := + if h is PartialDepth h1 then trunc_tele_rec h1 v else v. +Notation "v `_ n" := (truncate_tele v n) : telescope_scope. + +Fixpoint truncC_rec@{i} {ctx h1 k1} : + trunc_rec@{i} (trunc_rec ctx h1) k1 -> trunc_rec (trunc_rec ctx k1) h1 := + if ctx isn't Abs A ctxA then id else + if k1 isn't k.+1 then fun=> tt else if h1 isn't h.+1 then id else + fun v => [tele:= v.1d, @truncC_rec (ctxA _) h k v.2d]. +Definition truncC@{i} {ctx h k} : ctx`_h`_k -> ctx`_k`_h := + if k isn't PartialDepth k1 then id else if h isn't PartialDepth h1 then id else + truncC_rec@{i}. + +Lemma truncCK@{i} {ctx h k} : cancel (@truncC@{i} ctx h k) truncC. +Proof. +case: h k => [|h] [|k] //=; elim: ctx h k => // A ctxA IH [|h] [|k] /= [] // x v. +by rewrite IH. +Qed. + +Fixpoint truncV_rec@{i} {ctx h1} : trunc_rec@{i} ctx h1 -> option ctx := + if ctx isn't Abs A ctxA then Some else + if h1 isn't h.+1 then fun=> None else fun v => + omap (Dpair v.1d) (@truncV_rec (ctxA _) h v.2d). +Definition truncV@{i} {ctx h} : ctx`_h -> option ctx := + if h is PartialDepth h1 then @truncV_rec@{i} ctx h1 else Some. + +Notation "h >= v" := (isSome (truncV v`_h)) : telescope_scope. + +Lemma truncKV@{i} ctx h : ocancel (fun v => @truncV@{i} ctx h (v`_h)) id. +Proof. +case: h => //=; elim: ctx => [_ []|] //= A ctx IH [|h] [x v] //=. +by case: truncV_rec (IH x h v) => //= _ ->. +Qed. + +Lemma truncVK@{i} ctx h : ocancel (@truncV@{i} ctx h) (fun v => v`_h)%tele. +Proof. +case: h => //=; elim: ctx => [_ []|] //= A ctx IH [|h] // [x v] /=. +by case: truncV_rec (IH x h v) => //= _ ->. +Qed. + + +Fact truncE_P@{i} ctx h k (v : ctx`_h`_k) : (h <= k)%tele -> truncV@{i} v. +Proof. +case: h k v => [|h] [] //=; elim: ctx h => //= A ctx IH [|h] [|k] //= [x v] lehk. +by rewrite isSome_map IH. +Qed. + +Definition truncE@{i} {h k ctx} (lehk : (h <= k)%tele) (v : ctx`_h`_k) : ctx`_h := + (if truncV v is Some w as ow return ow -> _ then fun=> w else + fun ff => match notF ff with end) (truncE_P@{i} v lehk). + +Definition truncW@{i} {h k ctx} (lekh : (k <= h)%tele) (v : ctx`_h) : ctx`_k := + truncE@{i} lekh (truncC v`_k). + +Lemma truncE_K@{i} h k ctx (lehk : (h <= k)%tele) : + cancel (@truncE@{i} h k ctx lehk) (fun v => v`_k)%tele. +Proof. by rewrite /truncE => v; case: truncV (truncVK v) (truncE_P _ _). Qed. + +Lemma truncK@{i} h k ctx (lehk : (h <= k)%tele) : + cancel (fun v : ctx`_h => (v`_k)%tele) (@truncE@{i} h k ctx lehk). +Proof. by rewrite /truncE => v; case: truncV (truncE_P _ _) (truncKV k v). Qed. + +Definition Xtrunc@{i} h (ctx : context@{i}) (cT : ctx -> Type@{i}) : + ctx`_h -> ctx + (ctx :+ cT)`_h. +Proof. +case: h => /=; first by left. +do [fix IH 1] in ctx cT *; case: ctx => [|A ctxA] /= in cT *; first by left. +case=> [|h /= [x]]; first by right. +by case/(IH _ (fun v => cT [tele:= x, v])); [left | right]; exists x. +Defined. + +Definition truncX@{i} h (ctx : context@{i}) (cT : ctx -> Type@{i}) : + (ctx :+ cT)`_h -> ctx`_h. +Proof. +case: h ctx cT => [_ _ /split_extend[]|] //=; fix IHh 1 => -[|h] [|A ctxA] //= cT. +case=> x /IHh; apply: Dpair x. +Defined. + +Lemma truncX_tele@{i} h ctx cT v z : @truncX@{i} h ctx cT (v :+ z)`_h = (v`_h)%tele. +Proof. +case: h ctx cT v z => [*|] /=; first by rewrite extend_teleK. +by elim=> [|h IHh] /= [|A ctxA] //= cT [x v] z; rewrite IHh -/trunc_rec. +Qed. + +Lemma Xtrunc_eqV@{i} h (ctx : context@{i}) (cT : ctx -> Type@{i}) (v : ctx`_h) : + truncV v = Xtrunc cT v :> bool. +Proof. +case: h ctx cT v => //=; elim=> [|h IHh] [|A ctxA] //= cT [x v] /=. +by set cTx := fun u => cT _; rewrite isSome_map (IHh _ cTx); case: (_ v). +Qed. + +Record map@{i} (ctx1 ctx2 : context@{i}) := { + apply {h} : ctx1`_h -> ctx2`_h; + mapW {h k} v lekh : apply (@truncW h k ctx1 lekh v) = truncW lekh (apply v); + mapV {h} v : truncV (@apply h v) = truncV v :> bool +}. +Coercion apply : map >-> Funclass. + +Lemma map_truncV@{i} h ctx1 ctx2 (f : map@{i} ctx1 ctx2) v : + truncV (f h v) = truncV v :> bool. +Proof. exact: mapV. Qed. + +(* Lemma truncK@{i} h ctx (lehk : (h <= k)%tele) (v : ctx`_h) : *) + +(* +Definition map@{i} {S T : Type@{i}} {ctx} g (cf : ctx / S) : ctx / T := + abs (fun v => g cf.[v]). + +Definition map2@{i} {S T R : Type@{i}} {ctx} h (cf : ctx / S) (cg : ctx / T) := + abs (fun v => h cf.[v] cg.[v]) : ctx / R. + +Definition dmap@{i} {S : Type@{i}} {T : S -> Type@{i}} {R : Type@{i}} {ctx} + (g : forall x, T x -> R) (cf : ctx / S) := + let cg vz := let: Dpair v z := split_extend vz in g cf.[v] z in + abs cg : (ctx :+ (fun v => T cf.[v])) / R. + +Definition map_sum@{i} {S T R : Type@{i}} {ctx ctx2 : context@{i}} + (h : S -> T -> R) (cf : ctx / S) (cg : ctx2 / T) : (ctx ++ ctx2) / R := + let ch uv := let: Dpair u v := split_join uv in h cf.[u] cg.[v] in abs ch. +*) +(* Basic identities; most are transparent as they may be used for dependent *) +(* type transport, e.g., in subst_dmap below. *) + +Lemma subst_abs@{i j} ctx (T : ctx -> Type@{i}) (h : forall v, T v) v : + (abs@{i j} h).[v] = h v. +Proof. by elim: ctx v => [|A ctxA IH] /= [] // x v in T h *; apply: IH. Defined. + +Lemma congr_subst@{i} (ctx : context@{i}) (T : ctx -> Type@{i}) : + forall (cT1 cT2 : ctx /.v T v) v, cT1 =* cT2 -> cT1.[v] = cT2.[v]. +Proof. by elim: ctx T => [|A ctxA IH] T cT1 cT2 [] //= *; apply/IH. Defined. + +Lemma abs_subst@{i j} ctx (T : ctx -> Type@{i}) (cT : ctx /.v T v) : + abs@{i j} (fun v => cT.[v]) =* cT. +Proof. by elim: ctx T cT => /=. Defined. +(* +Lemma subst_map@{i} {S T : Type@{i}} {ctx} (g : S -> T) (cf : ctx / S) v : + (map@{i} g cf).[v] = g cf.[v]. +Proof. exact: subst_abs. Defined. + +Lemma subst_map2@{i} {S T R : Type@{i}} {ctx} + (h : S -> T -> R) (cf : ctx / S) (cg : ctx / T) v : + (map2@{i} h cf cg).[v] = h cf.[v] cg.[v]. +Proof. exact: subst_abs. Defined. + +Lemma subst_dmap@{i} {S : Type@{i}} {T : S -> Type@{i}} {R : Type@{i}} {ctx} + (g : forall x : S, T x -> R) (cf : ctx / S) v z : + (dmap@{i} g cf).[v :+ z] = g cf.[v] z. +Proof. by rewrite subst_abs extend_teleK. Defined. + +Lemma subst_sum@{i} {S T R : Type@{i}} {ctx ctx2} + (h : S -> T -> R) (cf : ctx / S) (cg : ctx2 / T) v w : + (map_sum@{i} h cf cg).[v ++ w] = h cf.[v] cg.[w]. +Proof. by rewrite subst_abs join_teleK. Defined. +*) + +Lemma unwrap_subst@{i j +} {ctx : context@{i}} (cT : ctx / Type@{j}) v : + wType_subst cT v = WrapType cT.[v]. +Proof. by elim: ctx v cT => [|A ctxA IH] [] //=. Qed. + +End Context. + +(* +Variant arg_of {A R} (f : A -> R) : R -> Type := Arg x : arg_of f (f x). +Notation arg_val y := (let: Arg x := y in x). +Arguments Arg {A R f}. + +Section LocalProperties. + +Context {A1 A2 A3 : Type}. +Context (d1 : mem_pred A1) (d2 : mem_pred A2) (d3 : mem_pred A3). + +Definition forall1 P := forall (x : A1), P x : Prop. +Definition forall2 P := forall (x : A1) (y : A2), P x y : Prop. +Definition forall3 P := forall (x : A1) (y : A2) (z : A3), P x y z : Prop. + +Definition all1pred := arg_of forall1. +Definition all2pred := arg_of forall2. +Definition all3pred := arg_of forall3. + +Definition for1_all x Q : all1pred Q -> Prop := fun '(Arg P) => P x. +Definition for2_all x y Q : all2pred Q -> Prop := fun '(Arg P) => P x y. +Definition for3_all x y z Q : all3pred Q -> Prop := fun '(Arg P) => P x y z. + +Definition in1_all Q : all1pred Q -> Prop := fun '(Arg P) => + forall x, in_mem x d1 -> P x. + +Definition in11_all Q : all2pred Q -> Prop := fun '(Arg P) => + forall x y, in_mem x d1 -> in_mem y d2 -> P x y. + +Definition in111_all Q : all3pred Q -> Prop := fun '(Arg P) => + forall x y z, in_mem x d1 -> in_mem y d2 -> in_mem z d3 -> P x y z. + +Lemma all2_and2 {P Q : A1 -> A2 -> Prop} : + (forall x y, P x y /\ Q x y) -> (forall x y, P x y) /\ (forall x y, Q x y). +Proof. by move=> /(_ _)/all_and2-/all_and2. Qed. + +Lemma all3_and2 {P Q : A1 -> A2 -> A3 -> Prop} : + (forall x y z, P x y z /\ Q x y z) -> + (forall x y z, P x y z) /\ (forall x y z, Q x y z). +Proof. by move=> /(_ _ _)/all_and2-/all2_and2. Qed. + +Lemma all2_and3 {P Q R : A1 -> A2 -> Prop} : + (forall x y, [/\ P x y, Q x y & R x y]) -> + [/\ forall x y, P x y, forall x y, Q x y & forall x y, R x y]. +Proof. by move=> /(_ _)/all_and3-/all_and3. Qed. + +Lemma all3_and3 {P Q R : A1 -> A2 -> A3 -> Prop} : + (forall x y z, [/\ P x y z, Q x y z & R x y z]) -> + [/\ forall x y z, P x y z, forall x y z, Q x y z & forall x y z, R x y z]. +Proof. by move=> /(_ _ _)/all_and3-/all2_and3. Qed. + +End LocalProperties. + +Arguments forall1 {A1} P /. +Arguments forall2 {A1 A2} P /. +Arguments forall3 {A1 A2 A3} P /. +Arguments for1_all {A1} x Q P : simpl never. +Arguments for2_all {A1 A2} x y Q P : simpl never. +Arguments for3_all {A1 A2 A3} x y z Q P : simpl never. +Notation "{ 'for' x , Q }" := (for1_all x Q (Arg _)) + (at level 0, format "{ '[' 'for' x , '/ ' Q ']' }", only printing) + : type_scope. +Notation "{ 'for' x & y , Q }" := (for2_all x y Q (Arg _)) + (at level 0, format "{ '[' 'for' x & y , '/ ' Q ']' }") : type_scope. +Notation "{ 'for' x & y & z , Q }" := (for3_all x y z Q (Arg _)) + (at level 0, format "{ '[' 'for' x & y & z , '/ ' Q ']' }") : type_scope. + +Definition in2_all {A1} d1 := @in11_all A1 A1 d1 d1. +Definition in3_all {A1} d1 := @in111_all A1 A1 A1 d1 d1 d1. +Definition in12_all {A1 A2} d1 d2 := @in111_all A1 A2 A2 d1 d2 d2. +Definition in21_all {A1 A2} d1 d2 := @in111_all A1 A1 A2 d1 d1 d2. + +Arguments in1_all {A1} d1 Q P : simpl never. +Arguments in2_all {A1} d1 Q P : simpl never. +Arguments in3_all {A1} d1 Q P : simpl never. +Arguments in11_all {A1 A2} d1 d2 Q P : simpl never. +Arguments in12_all {A1 A2} d1 d2 Q P : simpl never. +Arguments in21_all {A1 A2} d1 d2 Q P : simpl never. +Arguments in111_all {A1 A2 A3} d1 d2 d3 Q P : simpl never. + +Notation "{ 'in' d1 , Q }" := + (in1_all (mem d1) Q (Arg _)) : type_scope. +Notation "{ 'in' d1 & , Q }" := + (in2_all (mem d1) Q (Arg _)) : type_scope. +Notation "{ 'in' d1 & & , Q }" := + (in3_all (mem d1) Q (Arg _)) : type_scope. +Notation "{ 'in' d1 && , Q }" := + (in3_all (mem d1) Q (Arg _)) (only parsing) : type_scope. +Notation "{ 'in' d1 & d2 , Q }" := + (in11_all (mem d1) (mem d2) Q (Arg _)) : type_scope. +Notation "{ 'in' d1 & d2 & , Q }" := + (in12_all (mem d1) (mem d2) Q (Arg _)) : type_scope. +Notation "{ 'in' d1 & & d2 , Q }" := + (in21_all (mem d1) (mem d2) Q (Arg _)) : type_scope. +Notation "{ 'in' d1 && d2 , Q }" := + (in21_all (mem d1) (mem d2) Q (Arg _)) (only parsing) : type_scope. +Notation "{ 'in' d1 & d2 & d3 , Q }" := + (in111_all (mem d1) (mem d2) (mem d3) Q (Arg _)) : type_scope. + +Section PairProperties. + +Context {A} (d : mem_pred A). + +Definition dup1all2_with Q of @all2pred A A Q := A -> Q. +Definition dup2all1_with Q of @all1pred A Q := A -> A -> Q. + +Lemma undup1all2 {Q P} : @dup1all2_with Q P <-> Q. +Proof. by case: Q / P => /= P; split=> allP x //; apply: allP. Qed. + +Lemma undup2all1 {Q P} : @dup2all1_with Q P <-> Q. +Proof. by case: Q / P => /= P; split=> allP x //; apply: allP. Qed. + +Definition dup1all2_arg Q (P : all2pred Q) := + let: Arg P in arg_of _ Q := P return all3pred (dup1all2_with P) in + Arg (fun=> P). + +Lemma undup1all_in3 Q P : in3_all d _ (dup1all2_arg P) <-> in2_all d Q P. +Proof. by case: Q / P => P; split=> [Q x y d1x | Q _ x y _]; apply: (Q x). Qed. + +Definition dup2all1_arg Q (P : @all1pred A Q) := + let: Arg P in arg_of _ Q := P return all3pred (dup2all1_with P) in + Arg (fun _ _ => P). + +Lemma undup2all_in3 Q P : in3_all d _ (dup2all1_arg P) <-> in1_all d Q P. +Proof. +by case: Q / P => P; split=> [Q x ? | Q _ _ x _ _]; [apply: (Q x x) | apply: Q]. +Qed. + +Definition pair_all3_with Q1 Q2 : all3pred Q1 -> all3pred Q2 -> Prop := + fun '(Arg P1) '(Arg P2) => forall x y z : A, P1 x y z * P2 x y z. + +Lemma split_all3 {Q1 Q2 P1 P2} : @pair_all3_with Q1 Q2 P1 P2 <-> Q1 /\ Q2. +Proof. +case: Q1 / P1 => /= P1; case: Q2 / P2 => /= P2. +split=> [Q12 | [Q1 Q2] x y z]; last by split; move: x y z. +by split=> x y z; case: (Q12 x y z). +Qed. + +Definition split_all3_arg Q1 Q2 (P1 : all3pred Q1) (P2 : all3pred Q2) := + let: Arg P1 in arg_of _ Q1 := P1 return all3pred (pair_all3_with P1 P2) in + let: Arg P2 in arg_of _ Q2 := P2 + return all3pred (pair_all3_with (Arg P1) P2) in + Arg (fun x y z : A => P1 x y z * P2 x y z)%type. + +Lemma split_all_in3 {Q1 Q2 P1 P2} : + in3_all d (pair_all3_with P1 P2) (split_all3_arg P1 P2) + <-> in3_all d Q1 P1 /\ in3_all d Q2 P2. +Proof. +case: Q1 / P1 => P1; case: Q2 / P2 => P2 /=. +split=> [Q | [Q1 Q2]]; [split|] => x y z d_x d_y d_z; try by case: (Q x y z). +by split; move: x y z d_x d_y d_z. +Qed. + +End PairProperties. + +Arguments dup1all2_with {A} Q P. +Arguments dup2all1_with {A} Q P. +Arguments pair_all3_with {A} Q1 Q2 P1 P2. + +Notation dup1all2 Q := (dup1all2_with Q (Arg _)). +Notation dup2all1 Q := (dup2all1_with Q (Arg _)). +Notation pair_all3 Q1 Q2 := (pair_all3_with Q1 Q2 (Arg _) (Arg _)). + +*) + +Reserved Notation "{ 'for' x & y , P }" (at level 0, + format "'[hv' { 'for' x & y , '/ ' P } ']'"). +Reserved Notation "{ 'for' x & y & z , P }" (at level 0, + format "'[hv' { 'for' x & y & z , '/ ' P } ']'"). +Reserved Notation "{ 'in' <= S , P }" (at level 0, + format "'[hv' { 'in' <= S , '/ ' P } ']'"). + +Definition identify_source T : Type := T. +Definition identify_target T : Type := T. +Variant identical3 {T} x : T -> T -> Prop := Identical3 : @identical3 T x x x. +Structure identify {T} (x y : T) := + Identify {common_value :> identify_target T; _ : identical3 x y common_value}. + +Canonical trivial_identify {T} (x : identify_source T) := + Identify (@Identical3 T x). +Coercion trivial_identify : identify_source >-> identify. + +Section MoreLocalProperties. + +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 "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). +Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). +Local Notation ph := (phantom _). + +Definition prop_for2 (x : T1) (y : T2) P & ph {all2 P} := P x y. +Definition prop_for3 (x : T1) (y : T2) (z : T3) P & ph {all3 P} := P x y z. +Definition prop_within d P & ph {allA P} := forall A, sub_mem (mem A) d -> P A. + +Lemma for2E x y P phP : @prop_for2 x y P phP = P x y. Proof. by []. Qed. +Lemma for3E x y z P phP : @prop_for3 x y z P phP = P x y z. Proof. by []. Qed. + +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 MoreLocalProperties. + +Notation "{ 'for' x & y , P }" := + (prop_for2 x y (inPhantom P)) : type_scope. +Notation "{ 'for' x & y & z , P }" := + (prop_for3 x y z (inPhantom P)) : type_scope. +Notation "{ 'in' <= S , P }" := + (prop_within (mem S) (inPhantom P)) : type_scope. + +(* +Class identical_value {T} (x y : T) := IdenticalValue {}. +Instance duplicate_value {T} x : @identical_value T x x := IdenticalValue x x. +*) + +Section PairProperties. + +Context {T : Type} (d : mem_pred T). + +Local Notation "{ 'all1' P }" := (forall x : T, P x : Prop) (at level 0). +Local Notation "{ 'all2' P }" := (forall x y : T, P x y : Prop) (at level 0). +Local Notation "{ 'all3' P }" := (forall x y z : T, P x y z: Prop) (at level 0). + +Structure phantomProp (P : Prop) : Type := + PhantomProp {phantom_Prop :> Prop; _ : P = phantom_Prop}. +Canonical PropPhantom P := @PhantomProp P P erefl. +Local Notation ph := phantomProp. +Coercion phantom_of_Prop P phP : phantom Prop P := + let: PhantomProp Q defQ := phP in + let: erefl in _ = P := esym defQ return phantom Prop P in inPhantom Q. + +Ltac elimPh phP := (case: phP => phP; case: phP /). + +Definition prop_dup_body P (phP : ph {all1 P}) x y := + forall u : identify x y, P (common_value u). +Arguments prop_dup_body P phP x y / : clear implicits. +Local Notation prop_dup P phP := (forall x y, prop_dup_body P phP x y). + +Definition prop2_dup_body P (phP : ph {all2 P}) x y z := + forall u : identify y z, P x (common_value u). +Arguments prop2_dup_body P phP x y z / : clear implicits. +Local Notation prop2_dup P phP := (forall x y z, prop2_dup_body P phP x y z). + +Definition prop2_pair_body P Q (phP : ph {all2 P}) (_ : ph {all2 Q}) x y := + (P x y * Q x y)%type. +Arguments prop2_pair_body P Q phP phQ x y / : clear implicits. +Local Notation prop2_pair P Q phP phQ := + (forall x y, prop2_pair_body P Q phP phQ x y). + +Definition prop3_pair_body P Q (phP : ph {all3 P}) (_ : ph {all3 Q}) x y z := + (P x y z * Q x y z)%type. +Arguments prop3_pair_body P Q phP phQ x y z / : clear implicits. +Local Notation prop3_pair P Q phP phQ := + (forall x y z, prop3_pair_body P Q phP phQ x y z). + +Lemma prop_dupE P phP : prop_dup P phP <-> phP. +Proof. by elimPh phP; split=> P_ /= *; apply: P_. Qed. + +Lemma prop_in2_dup P phP : + prop_in2 d (inPhantom (prop_dup P phP)) <-> prop_in1 d phP. +Proof. by elimPh phP; split=> Pd x * => [|[_ []]]; apply Pd. Qed. + +Lemma prop2_dupE P phP : prop2_dup P phP <-> phP. +Proof. by elimPh phP; split=> P_ /= *; apply: P_. Qed. + +Lemma prop_in3_dup P phP : + prop_in3 d (inPhantom (prop2_dup P phP)) <-> prop_in2 d phP. +Proof. by elimPh phP; split=> Pd x * => [|[_ []]]; apply Pd. Qed. + +(* TODO: This used all_and. *) +Lemma prop2_pairE P Q phP phQ : prop2_pair P Q phP phQ <-> phP /\ phQ. +Proof. +elimPh phP; elimPh phQ; split=> [PQ|[]//]. +by split=> x y; move/(_ x y): PQ => []. +Qed. + +Lemma prop3_pairE P Q phP phQ : prop3_pair P Q phP phQ <-> phP /\ phQ. +Proof. +elimPh phP; elimPh phQ; split=> [PQ|[]//]. +by split=> x y z; move/(_ x y z): PQ => []. +Qed. + +Lemma prop_in2_pair P Q phP phQ : + prop_in2 d (inPhantom (prop2_pair P Q phP phQ)) + <-> prop_in2 d phP /\ prop_in2 d phQ. +Proof. +elimPh phP; elimPh phQ; split=> [PQ|[]]; last by split; auto. +by split=> x y xd yd; move/(_ x y xd yd): PQ => []. +Qed. + +Lemma prop_in3_pair P Q phP phQ : + prop_in3 d (inPhantom (prop3_pair P Q phP phQ)) + <-> prop_in3 d phP /\ prop_in3 d phQ. +Proof. +elimPh phP; elimPh phQ; split=> [PQ|[]]; last by split; auto. +by split=> x y z xd yd zd; move/(_ x y z xd yd zd): PQ => []. +Qed. + +End PairProperties. + +Notation prop_dup Q := + (forall x y, prop_dup_body (PropPhantom Q) x y). +Notation prop2_dup Q := + (forall x y z, prop2_dup_body (PropPhantom Q) x y z). +Notation prop_dup2 Q := (prop2_dup (prop_dup Q)). +Notation prop2_pair Q1 Q2 := + (forall x y, prop2_pair_body (PropPhantom Q1) (PropPhantom Q2)). +Notation prop3_pair Q1 Q2 := + (forall x y z, prop3_pair_body (PropPhantom Q1) (PropPhantom Q2) x y z). + +Section RelDefs. + +Variables (T : Type) (R : rel T). +Implicit Types (x y z : T) (A C : {pred T}). + +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 := prop3_pair (prop_dup2 (reflexive R)) (transitive R). + +Definition partial_order := prop3_pair preorder (prop2_dup (antisymmetric R)). + +Definition total_order := prop3_pair partial_order (prop2_dup (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_order}. + +Definition wo_chain C := {in <= C, well_order}. + +Lemma preorderE : preorder <-> reflexive R /\ transitive R. +Proof. by rewrite [preorder]prop3_pairE /= prop2_dupE /= prop_dupE. Qed. + +Lemma preorder_in A : + {in A & &, preorder} <-> {in A, reflexive R} /\ {in A & &, transitive R}. +Proof. by rewrite prop_in3_pair prop_in3_dup prop_in2_dup. Qed. + +Lemma partial_orderE : + partial_order <-> [/\ reflexive R, transitive R & antisymmetric R]. +Proof. +by rewrite [partial_order]prop3_pairE /= preorderE prop2_dupE; split=> [[]|] []. +Qed. + +Lemma partial_order_in A : + {in A & &, partial_order} + <-> [/\ {in A, reflexive R}, {in A & &, transitive R} + & {in A &, antisymmetric R}]. +Proof. by rewrite prop_in3_pair preorder_in prop_in3_dup; split=> [[]|] []. Qed. + +Lemma total_orderE : + total_order <-> [/\ reflexive R, transitive R, antisymmetric R & total R]. +Proof. +rewrite [total_order]prop3_pairE /= partial_orderE prop2_dupE /=. +by split=> [[]|] []. +Qed. + +Lemma total_order_in A : + {in A & &, total_order} + <-> [/\ {in A, reflexive R}, {in A & &, transitive R}, + {in A &, antisymmetric R} & {in A &, total R}]. +Proof. +by rewrite prop_in3_pair partial_order_in prop_in3_dup; split=> [[]|] []. +Qed. + +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; have Rtotal: {in C &, total R}. + move=> x y Cx Cy; have /Rwo[] := ne_cons x [::y]; first exact/allP/and3P. + by move=> z [] [] /or3P[] // /eqP-> /allP/and3P[] => [_|] ->; rewrite ?orbT. +have Rxx: {in C, reflexive R} by move=> x Cx; rewrite -[R x x]orbb Rtotal. +have Ranti: {in C &, antisymmetric R}. + move=> x y Cx Cy; 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. +suffices Rtr: {in C & &, transitive R} by apply/total_order_in. +move=> y x z Cy Cx Cz Rxy Ryz; pose A := [mem [:: x; y; z]]. +have /and4P[Ax Ay Az _]: all A _ := all_mem _. +have [] := Rwo A; first 1 [exact/allP/and4P | apply: ne_cons]. +move=> _ [[/or4P[]// /eqP-> /allP/and4P[// Ryx Rzy _ _]] _]. + by rewrite (Ranti x y) ?Rxy. +by rewrite (Ranti z y) ?Rzy. +Qed. + +Lemma well_order_total (T : eqType) (R : rel T) : well_order R -> total_order R. +Proof. by move=>/withinW/wo_chainW/in3T. Qed. + +(* Alternatively, one can deduce the localized variant from the global one. + +Lemma well_order_total (T : eqType) (R : rel T) : well_order R -> total_order R. +Proof. +have inU1l x (A : {pred T}): x \in xpredU1 x A by apply/predU1l. +have inU12r (x y : T): y \in xpred2 x y by apply/predU1r/eqxx. +have exU1 (x : T) A: nonempty (xpredU1 x A) by exists x; apply: inU1l. +move=> Rwo; have Rtotal: total R. + move=> x y; have /Rwo[z [[/pred2P/=xyz]]] := exU1 x (pred1 y). + by case: xyz orbC => [-> _ | -> ->] ->. +have Rxx: reflexive R by move=> x; have:= Rtotal x x; rewrite orbb. +have Ranti: antisymmetric R. + move=> x y /andP[Rxy Ryx]; have /Rwo[z [_ Uz]] := exU1 x (pred1 y). + by transitivity z; first apply/esym; apply/Uz; split=> [|_ /pred2P[]->] /=. +suffices Rtr: transitive R by apply/total_orderE. +move=> y x z Rxy Ryz; pose A := pred3 x y z. +have [Ax Ay Az]: [/\ A x, A y & A z] by rewrite /= !eqxx !orbT. +have /Rwo[t [[At minAt] _]]: exists t, A t by exists x. +case/predU1P: At => [-> -> //| /pred2P[]->] in minAt *. + by rewrite (Ranti x y) // Rxy minAt. +by rewrite (Ranti z y) // Ryz minAt. +Qed. + +Lemma well_order_total_in (T : eqType) (R : rel T) (C : {pred T}) : + {in <= C, well_order R} -> {in C & &, total_order R}. +Proof. +move=> Rwo; pose T' := {x | x \in C}; pose R' := relpre (val : T' -> T) R. +without loss u0: / T' by move=> IH x y z Cx; apply: IH (Cx); exists x. +have defR: {in C &, R =2 relpre (insubd u0) R'}. + apply/total_order_in; split=> [x Cx | y x z Cy Cx Cz | x y Cx Cy | x y Cx Cy]; + rewrite !defR //; [apply: R'xx | apply: R'tr | | apply: R'tot]. + by move/R'anti/(congr1 val); rewrite !insubdK. +apply/well_order_total=> A neA; pose B := [pred x in C | insubd u0 x \in A]. +have sAB u: u \in A -> val u \in B by rewrite inE (valP u) valKd. +have memB x: x \in B -> exists2 u, u \in A & x = val u. + by case/andP=> Cx Ax; exists (insubd u0 x); rewrite ?insubdK. +have /Rwo[? /andP[]//|_ [[/memB[w Aw ->] minBw] Uw]]: nonempty B. + by case: neA => u /sAB-Bu; exists (val u). +exists w; do 2?[split] => // [u Au | v [Av minAv]]; first exact/minBw/sAB. +by apply/val_inj/Uw; split=> [|_ /memB[u Au ->]]; [apply/sAB | apply/minAv]. +Qed. + +end alternative *) + +(******************************************************************************) + +Section Zorn. + +Fact dec_eqMixin {T} : Equality.mixin_of T. +Proof. exists (fun x y => `[< x = y >]) => x y; apply: asboolP. Qed. +Definition DecEqType {T} := EqType T dec_eqMixin. + +Lemma well_order_WF T (R : rel T) : + well_order R <-> antisymmetric R /\ well_founded (fun x y => ~~ R y x). +Proof. +set R' := fun x y => is_true _; split=> [Rwo | [Ranti Rwf]]. + split; first by have /total_orderE[] := @well_order_total DecEqType R Rwo. + pose A x := `[< ~ Acc R' x >]. + move=> x; absurd_not=> Ax; have{x Ax}: nonempty A by exists x; apply/asboolP. + case/Rwo=> x [[/asboolP-Ax minAx] _]; case: Ax; split=> y; rewrite /R'. + by contra=> Ay; apply: minAx; apply/asboolP. +move=> A [x Ax]; elim: x / (Rwf x) => x _ IHx in Ax *. +have [lbAx | /notP[y Ay /IHx]] := asboolP (lower_bound R A x); last exact. +by exists x; split=> // y [Ay lbAy]; apply: Ranti; rewrite lbAx ?lbAy. +Qed. + +Lemma Zorn's_lemma T (R : rel T) (S : {pred T}) : + {in S & &, preorder 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}. +- case/preorder_in=> 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 (@DecEqType T1) (relpre val R); last 1 first. + - by exists (val u) => // x Sx Rux; apply: (maxT1u (Sub x Sx)). + - by apply/preorderE; 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/preorderE=> 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_chainW/total_order_in[_ _ 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_chainW/total_order_in[_ _ 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 & &, preorder 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. +case/preorder_in=> 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 & &, preorder Rch}. + apply: in3W; apply/preorderE; split=> [X | X Y Z]; first exact/asboolP. + by move=> /asboolP-sXY /asboolP-sYZ; apply/asboolP=> x /sXY/sYZ. +case/Zorn's_lemma=> [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. +have{XXwo} /(@wo_chainW DecEqType)/total_order_in[_ _ _ XXch] := XXwo. +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=> //; first apply/total_order_in. +by split; first 1 [exact: (sub_in1 sDS) | exact: (sub_in3 sDS)]; + move=> x y _ /(in2D x)[//|X [/CSchXX/asboolP[Xch _ _] Xx Xy]]; + have /total_order_in[_ _ anti tot] := Xch; do [apply: anti | apply: tot]. +Qed. + +Theorem well_ordering_principle T : {R : rel T | well_order R}. +Proof. +have{T} [T ->]: {T1 : eqType | T = T1} by exists (@DecEqType 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 & &, preorder initR} by apply: in3W; apply/preorderE. +case/Zorn's_lemma=> [C pwoC Cch | [D R] /asboolP/=pwoR maxR]. + have{Cch} /(@wo_chainW DecEqType)/total_order_in[_ _ _ 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_chainW/total_order_in[_ _ 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.