port to mc2

math-comp · Feb 10, 2024 · 15f5a59 · 15f5a59
1 parent 190b8ac
commit 15f5a59
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 12 deletions.
diff --git a/classical/boolp.v b/classical/boolp.v
@@ -98,8 +98,6 @@ Proof. by have [propext _] := extensionality; apply: propext. Qed.
 
 Ltac eqProp := apply: propext; split.
 
-Ltac eqProp := apply: propext; split.
-
 Lemma funext {T U : Type} (f g : T -> U) : (f =1 g) -> f = g.
 Proof. by case: extensionality=> _; apply. Qed.
 
@@ -636,9 +634,6 @@ Proof. by rewrite -[_ /\ _]notE not_andE 2!notE. Qed.
 Lemma not_orP (P Q : Prop) : ~ (P \/ Q) <-> ~ P /\ ~ Q.
 Proof. by rewrite not_orE. Qed.
 
-Lemma not_orP (P Q : Prop) : ~ (P \/ Q) <-> ~ P /\ ~ Q.
-Proof. by rewrite not_orE. Qed.
-
 Lemma not_implyE (P Q : Prop) : (~ (P -> Q)) = (P /\ ~ Q).
 Proof. by rewrite propeqE not_implyP. Qed.
 

diff --git a/classical/wochoice.v b/classical/wochoice.v
@@ -107,7 +107,7 @@ Qed.
 
 Section Zorn.
 
-Lemma Zorn's_lemma T (R : rel T) (S : {pred T}) :
+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}}.
@@ -117,7 +117,7 @@ suffices{T R S} Zorn (T : eqType) (R : rel T) (Well := wo_chain R) :
   {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 (@classicType_eqType T1) (relpre val R); last 1 first.
+  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)].
@@ -239,7 +239,7 @@ 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 (@classicType_eqType {pred T})): XXwo => XXch.
+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.
@@ -261,9 +261,9 @@ move=> x y xD /(in2D x)-/(_ xD) [X [/CSchXX/asboolP[Xch _ _] Xx Xy]].
 exact: Xch.
 Qed.
 
-Theorem well_ordering_principle T : {R : rel T | well_order R}.
+Theorem well_ordering_principle (T : eqType) : {R : rel T | well_order R}.
 Proof.
-have{T} [T ->]: {T1 : eqType | T = T1} by exists (@classicType_eqType T).
+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 >].
@@ -278,7 +278,7 @@ have initRtr: transitive initR.
 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 (classicType_eqType ({pred T} * rel T))) {}Cch := Cch.
+  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.
@@ -289,7 +289,7 @@ case=> [C pwoC Cch | [D R] /asboolP/=pwoR maxR].
       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) //=.
+      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.