port of classical from lspace_master

CHANGELOG_UNRELEASED.md

@@ -26,6 +26,16 @@
 - in `lebesgue_integral_approximation.v`:
   + lemma `measurable_prod`
 
+- in `boolp.v`:
+  + lemmas `orW`, `or3W`, `or4W`
+
+- in `classical_sets.v`:
+  + lemmas `set_cst`, `image_nonempty`
+
+- in `unstable.v`:
+  + lemmas `eq_exists2l`, `eq_exists2r`
+  + module `ProperNotations` with notations `++>`, `==>`, `~~>`
+
 ### Changed
 
 - in `pi_irrational`:

classical/boolp.v

@@ -341,6 +341,30 @@ Proof. by rewrite /asbool; case: pselect=> h; constructor. Qed.
 Lemma asboolW (P : Prop) : `[<P>] -> P.
 Proof. by case: asboolP. Qed.
 
+Lemma orW A B : A \/ B -> A + B.
+Proof.
+have [|NA] := asboolP A; first by left.
+have [|NB] := asboolP B; first by right.
+by move=> AB; exfalso; case: AB.
+Qed.
+
+Lemma or3W A B C : [\/ A, B | C] -> A + B + C.
+Proof.
+have [|NA] := asboolP A; first by left; left.
+have [|NB] := asboolP B; first by left; right.
+have [|NC] := asboolP C; first by right.
+by move=> ABC; exfalso; case: ABC.
+Qed.
+
+Lemma or4W A B C D : [\/ A, B, C | D] -> A + B + C + D.
+Proof.
+have [|NA] := asboolP A; first by left; left; left.
+have [|NB] := asboolP B; first by left; left; right.
+have [|NC] := asboolP C; first by left; right.
+have [|ND] := asboolP D; first by right.
+by move=> ABCD; exfalso; case: ABCD.
+Qed.
+
 (* Shall this be a coercion ?*)
 Lemma asboolT (P : Prop) : P -> `[<P>].
 Proof. by case: asboolP. Qed.

classical/classical_sets.v

@@ -1242,6 +1242,13 @@ Notation bigcupM1l := bigcupX1l (only parsing).
 #[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to bigcupX1r.")]
 Notation bigcupM1r := bigcupX1r (only parsing).
 
+Lemma set_cst {T I} (x : T) (A : set I) :
+   [set x | _ in A] = if A == set0 then set0 else [set x].
+Proof.
+apply/seteqP; split=> [_ [i +] <-|t]; first by case: ifPn => // /eqP ->.
+by case: ifPn => // /set0P[i Ai ->{t}]; exists i.
+Qed.
+
 Section set_order.
 Import Order.TTheory.
 
@@ -1532,6 +1539,9 @@ Proof. by move=> b [x [Aa Ba <-]]; split; apply: imageP. Qed.
 Lemma nonempty_image f A : f @` A !=set0 -> A !=set0.
 Proof. by case=> b [a]; exists a. Qed.
 
+Lemma image_nonempty f A : A !=set0 -> f @` A !=set0.
+Proof. by move=> [x] Ax; exists (f x), x. Qed.
+
 Lemma image_subset f A B : A `<=` B -> f @` A `<=` f @` B.
 Proof. by move=> AB _ [a Aa <-]; exists a => //; apply/AB. Qed.
 
@@ -1654,6 +1664,8 @@ Proof. by rewrite preimage_false; under eq_fun do rewrite inE. Qed.
 
 End image_lemmas.
 Arguments sub_image_setI {aT rT f A B} t _.
+Arguments subset_set1 {_ _ _}.
+Arguments subset_set2 {_ _ _ _}.
 
 Lemma image2_subset {aT bT rT : Type} (f : aT -> bT -> rT)
     (A B : set aT) (C D : set bT) : A `<=` B -> C `<=` D ->

classical/unstable.v

@@ -442,3 +442,39 @@ Proof.
 move=> lt_mn i; rewrite big_nat [ltRHS]big_nat ltr_sum//.
 by apply/hasP; exists m; rewrite ?mem_index_iota leqnn lt_mn.
 Qed.
+
+
+Lemma eq_exists2l (A : Type) (P P' Q : A -> Prop) :
+  (forall x, P x <-> P' x) ->
+  (exists2 x, P x & Q x) <-> (exists2 x, P' x & Q x).
+Proof.
+by move=> eqQ; split=> -[x p q]; exists x; move: p q; rewrite ?eqQ.
+Qed.
+
+Lemma eq_exists2r (A : Type) (P Q Q' : A -> Prop) :
+  (forall x, Q x <-> Q' x) ->
+  (exists2 x, P x & Q x) <-> (exists2 x, P x & Q' x).
+Proof.
+by move=> eqP; split=> -[x p q]; exists x; move: p q; rewrite ?eqP.
+Qed.
+
+Declare Scope signature_scope.
+Delimit Scope signature_scope with signature.
+
+Import -(notations) Morphisms.
+Arguments Proper {A}%_type R%_signature m.
+Arguments respectful {A B}%_type (R R')%_signature _ _.
+
+Module ProperNotations.
+
+Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature))
+  (right associativity, at level 55) : signature_scope.
+
+Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
+  (right associativity, at level 55) : signature_scope.
+
+Notation " R ~~> R' " := (@respectful _ _ (Program.Basics.flip (R%signature)) (R'%signature))
+  (right associativity, at level 55) : signature_scope.
+
+Export -(notations) Morphisms.
+End ProperNotations.