From 24a446c0ae1a0438591217431d0dc608fc6a31c0 Mon Sep 17 00:00:00 2001
From: Columbus240 <8899730+Columbus240@users.noreply.github.com>
Date: Tue, 6 Aug 2024 11:21:58 +0200
Subject: [PATCH] Fix errors when using coq v8.19.2

The changes in the stdlib regarding `Nat` broke some proofs.
---
 theories/Topology/Completeness.v             |  2 +-
 theories/Topology/TietzeExtension.v          |  2 +-
 theories/Topology/UniformTopology.v          |  1 -
 theories/Topology/UrysohnsLemma.v            | 46 ++++++++++----------
 theories/ZornsLemma/ReverseMath/ReverseCSB.v |  2 +-
 5 files changed, 27 insertions(+), 26 deletions(-)

diff --git a/theories/Topology/Completeness.v b/theories/Topology/Completeness.v
index 79c69a00..fc3088f4 100644
--- a/theories/Topology/Completeness.v
+++ b/theories/Topology/Completeness.v
@@ -54,7 +54,7 @@ intros y Hy.
 inversion Hy; subst; clear Hy.
 rename x0 into n. clear Hx d_metric.
 constructor.
-destruct (le_or_lt N n).
+destruct (Nat.le_gt_cases N n).
 - apply Rlt_le_trans with 1; auto.
   unfold Rmax.
   destruct (Rle_dec _ _); lra.
diff --git a/theories/Topology/TietzeExtension.v b/theories/Topology/TietzeExtension.v
index fd110c64..cf580681 100644
--- a/theories/Topology/TietzeExtension.v
+++ b/theories/Topology/TietzeExtension.v
@@ -1,6 +1,6 @@
 Require Export RTopology SeparatednessAxioms.
 Require Import RFuncContinuity UniformTopology ContinuousFactorization.
-From Coq Require Import Description Max Psatz ClassicalChoice.
+From Coq Require Import Description Psatz ClassicalChoice.
 From ZornsLemma Require Import Proj1SigInjective.
 Require Import UrysohnsLemma.
 
diff --git a/theories/Topology/UniformTopology.v b/theories/Topology/UniformTopology.v
index b310166f..65037839 100644
--- a/theories/Topology/UniformTopology.v
+++ b/theories/Topology/UniformTopology.v
@@ -2,7 +2,6 @@ Require Export MetricSpaces.
 Require Import FunctionalExtensionality.
 Require Export Completeness.
 Require Import Description.
-Require Import Max.
 Require Import Psatz.
 Require Import Lra.
 From Coq Require ProofIrrelevance.
diff --git a/theories/Topology/UrysohnsLemma.v b/theories/Topology/UrysohnsLemma.v
index 346ad113..f2928a9a 100644
--- a/theories/Topology/UrysohnsLemma.v
+++ b/theories/Topology/UrysohnsLemma.v
@@ -185,8 +185,6 @@ Qed.
 
 Require Export TopologicalSpaces.
 Require Export InteriorsClosures.
-Require Import Div2.
-Require Import Even.
 Require Import Arith.
 Require Export RTopology.
 
@@ -226,12 +224,12 @@ destruct n as [|].
   red; intros; constructor.
 Qed.
 
-Definition expand_U_dyadic (f:nat->Ensemble X)
+Definition expand_U_dyadic (f:nat -> Ensemble X)
   (Hopen: forall n:nat, open (f n))
   (Hincr: forall n:nat, Included (closure (f n)) (f (S n)))
   (n:nat) : Ensemble X :=
-if (even_odd_dec n) then f (div2 n) else
-let m := div2 n in proj1_sig
+if (Nat.Even_Odd_dec n) then f (Nat.div2 n) else
+let m := Nat.div2 n in proj1_sig
   (normal_sep_fun (closure (f m)) (f (S m))
      (closure_closed _) (Hopen _) (Hincr _)).
 
@@ -240,7 +238,7 @@ Lemma expand_U_dyadic_open: forall f Hopen Hincr n,
 Proof.
 intros.
 unfold expand_U_dyadic.
-destruct even_odd_dec.
+destruct Nat.Even_Odd_dec.
 - apply Hopen.
 - destruct normal_sep_fun.
   simpl.
@@ -254,22 +252,28 @@ Proof.
 intros.
 unfold expand_U_dyadic.
 simpl.
-destruct even_odd_dec.
+destruct Nat.Even_Odd_dec.
 - destruct normal_sep_fun.
   simpl.
   destruct n.
   + simpl.
     apply a.
-  + rewrite <- odd_div2.
+  + rewrite <- Nat.Odd_div2.
     * apply a.
-    * now inversion e.
+    * apply Nat.Even_succ.
+      exact e.
 - simpl.
-  destruct normal_sep_fun.
+  destruct normal_sep_fun as [x [Hx0 [Hx1 Hx2]]].
   simpl.
-  destruct o.
-  rewrite even_div2.
-  + now apply a.
-  + trivial.
+  destruct n.
+  { (* ~ Nat.Odd 0 *)
+    contradict o. clear.
+    intros []. lia.
+  }
+  apply Nat.Odd_succ in o.
+  rewrite Nat.Even_div2.
+  + exact Hx2.
+  + exact o.
 Qed.
 
 Definition packaged_expand_U_dyadic :
@@ -325,14 +329,12 @@ simpl.
 unfold expand_U_dyadic.
 change ((m + (m + 0))%nat) with ((2*m)%nat).
 rewrite div2_double.
-assert (forall m:nat, even (2*m)).
-{ induction m0.
-  { constructor. }
-  replace ((2 * S m0)%nat) with ((S (S (2 * m0)))%nat) by ring.
-  constructor.
-  now constructor. }
-destruct even_odd_dec; trivial.
-now contradiction not_even_and_odd with ((2 * m)%nat).
+assert (forall m:nat, Nat.Even (2*m)).
+{ intros ?. apply Nat.Even_mul_l.
+  exists 1%nat. reflexivity.
+}
+destruct Nat.Even_Odd_dec; trivial.
+now contradiction Nat.Even_Odd_False with (2 * m)%nat.
 Qed.
 
 Lemma U_dyadic_open: forall x:dyadic_rational,
diff --git a/theories/ZornsLemma/ReverseMath/ReverseCSB.v b/theories/ZornsLemma/ReverseMath/ReverseCSB.v
index 4e6b9a9c..4a23574d 100644
--- a/theories/ZornsLemma/ReverseMath/ReverseCSB.v
+++ b/theories/ZornsLemma/ReverseMath/ReverseCSB.v
@@ -342,7 +342,7 @@ Proof.
           rewrite Nat.ltb_ge in Heqb.
           rewrite Nat.le_succ_r in Heqb.
           destruct Heqb; auto.
-          apply lt_not_le in Heqb0.
+          apply Nat.lt_nge in Heqb0.
           contradiction.
         }
         rewrite H1. assumption.