Update for Coq v8.19, drop support of v8.15 and earlier

.github/workflows/coq-ci.yml

@@ -16,13 +16,10 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.19'
           - 'coqorg/coq:8.18'
           - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.16'
-          - 'coqorg/coq:8.15'
-          - 'coqorg/coq:8.14'
-          - 'coqorg/coq:8.13'
-          - 'coqorg/coq:8.12'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

README.md

@@ -36,7 +36,7 @@ and results of general topology in Coq.
   - stop-cran ([**@stop-cran**](https://github.com/stop-cran))
   - Columbus240 ([**@Columbus240**](https://github.com/Columbus240))
 - License: [GNU Lesser General Public License v2.1 or later](LICENSE)
-- Compatible Coq versions: Coq 8.12 or later (use the corresponding branch or release for other Coq versions)
+- Compatible Coq versions: Coq 8.16 or later (use the corresponding branch or release for other Coq versions)
 - Additional dependencies:
   - Zorn's Lemma (set library that is part of this repository)
 - Coq namespace: `Topology`

coq-topology.opam

@@ -16,7 +16,7 @@ and results of general topology in Coq.
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {(>= "8.12" & < "8.19~") | (= "dev")}
+  "coq" {(>= "8.16" & < "8.20~") | (= "dev")}
   "coq-zorns-lemma" {= version}
 ]
 

coq-zorns-lemma.opam

@@ -17,7 +17,7 @@ was as support for the Topology library.
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {(>= "8.12" & < "8.19~") | (= "dev")}
+  "coq" {(>= "8.16" & < "8.20~") | (= "dev")}
 ]
 
 tags: [

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.

theories/Topology/RFuncContinuity.v

@@ -311,7 +311,7 @@ assert (forall x:R, -1 < x / (1 + Rabs x) < 1).
   { pose proof (Rabs_pos x). lra. }
   apply and_comm, Rabs_def2.
   unfold Rdiv.
-  rewrite Rabs_mult, Rabs_Rinv; try lra.
+  rewrite Rabs_mult, Rabs_inv; try lra.
   rewrite (Rabs_right (1 + Rabs x)); [ | now left ].
   pattern 1 at 2.
   replace 1 with ((1 + Rabs x) * / (1 + Rabs x)) by (field; lra).

theories/Topology/RationalsInReals.v

@@ -25,7 +25,7 @@ Proof.
       apply lt_0_IZR in H0.
       now apply Z.lt_gt.
     - pattern eps at 2.
-      rewrite <- Rinv_involutive; auto with real;
+      rewrite <- Rinv_inv; auto with real;
         apply Rinv_lt_contravar; auto with real;
         apply Rmult_lt_0_compat; auto with real;
         apply Rlt_trans with (/ eps); auto with real.

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.
 
@@ -548,7 +548,7 @@
 split; intros.
 - apply continuous_composition with (1:=H) (2:=H1).
 - apply continuous_composition with (1:=H0) (2:=H1).
 Qed.
 
 Lemma Tietze_extension_func_continuous: continuous Tietze_extension_func.
 Proof.

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.

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,

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.