Merge pull request #197 from anandadalton/configure_sh

Remove conditional from configure.sh
coq-community · May 31, 2023 · 48735ca · 48735ca
2 parents ca47307 + ae9ab3a
commit 48735ca
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 20 deletions.
diff --git a/configure.sh b/configure.sh
@@ -4,16 +4,8 @@
 
 cp -f Make.in Make
 
-COQ_VERSION_LINE=$(coqc --version | head -1)
-COQ_VERSION=`echo $COQ_VERSION_LINE | sed 's/The Coq Proof Assistant, version 8\.\([^ +]*\).*/\1/'`
 DIRECTORIES="algebra complex coq_reals fta ftc liouville logic metrics model raster reals tactics transc order metric2 stdlib_omissions util classes ode"
 
-# Include constructive measure theory on version 8.12 and after
-if [ $COQ_VERSION -gt 11 ] ;
-then
-    find $DIRECTORIES -name "*.v" >>Make
-else
-    find $DIRECTORIES -name "*.v" | grep -v "stdlib/" >>Make
-fi
+find $DIRECTORIES -name "*.v" >>Make
 
 ${COQBIN}coq_makefile -f Make -o Makefile
diff --git a/reals/stdlib/CMTFullSets.v b/reals/stdlib/CMTFullSets.v
@@ -166,7 +166,7 @@ Proof.
   destruct xdf as [xnDiag cvDiag].
   assert (forall a b:nat, lt a b -> lt (diagPlane n a) (diagPlane n b)).
   { intros. unfold diagPlane. apply Nat.add_lt_le_mono. assumption.
-    apply Nat.Div0.div_le_mono. auto. apply Nat.mul_le_mono.
+    apply Nat.div_le_mono. auto. apply Nat.mul_le_mono.
     apply Nat.add_le_mono. apply Nat.le_refl. unfold lt in H0.
     apply (Nat.le_trans _ (S a)). apply le_S. apply Nat.le_refl. assumption.
     apply le_n_S. apply Nat.add_le_mono. apply Nat.le_refl. unfold lt in H0.

diff --git a/reals/stdlib/CMTIntegrableFunctions.v b/reals/stdlib/CMTIntegrableFunctions.v
@@ -434,13 +434,13 @@ Proof.
     apply (CRle_trans _ _ _ (CRabs_triang _ _)).
     setoid_replace (1 # n)%Q with ((1 # (2*n)) + (1 # (2*n)))%Q.
     apply le_S_n in H1. rewrite CR_of_Q_plus. apply CRplus_le_compat.
-    apply H. rewrite <- (Nat.div_mul N 2). apply Nat.Div0.div_le_mono.
+    apply H. rewrite <- (Nat.div_mul N 2). apply Nat.div_le_mono.
     auto. apply (Nat.le_trans (N*2) (N*2 + (S N0)*2)). apply Nat.le_add_r.
     apply (Nat.le_trans _ i). assumption.
     apply le_S. apply Nat.le_refl. auto.
     apply H0. assert (N0 = pred (S N0)). reflexivity.
     rewrite H2. apply Nat.pred_le_mono. rewrite <- (Nat.div_mul (S N0) 2).
-    apply Nat.Div0.div_le_mono. auto.
+    apply Nat.div_le_mono. auto.
     apply (Nat.le_trans _ (N*2 + (S N0)*2)).
     rewrite Nat.add_comm. apply Nat.le_add_r.
     apply (Nat.le_trans (N*2 + (S N0)*2) i). assumption. apply le_S. apply Nat.le_refl. auto.
@@ -453,11 +453,11 @@ Proof.
     apply (CRle_trans _ _ _ (CRabs_triang _ _)).
     setoid_replace (1 # n)%Q with ((1 # (2*n)) + (1 # (2*n)))%Q.
     apply le_S_n in H1. rewrite CR_of_Q_plus. apply CRplus_le_compat.
-    apply H. rewrite <- (Nat.div_mul N 2). apply Nat.Div0.div_le_mono.
+    apply H. rewrite <- (Nat.div_mul N 2). apply Nat.div_le_mono.
     auto. apply (Nat.le_trans (N*2) (N*2 + (S N0)*2)). apply Nat.le_add_r.
     apply (Nat.le_trans _ i). assumption. apply le_S. apply Nat.le_refl. auto.
     apply H0. rewrite <- (Nat.div_mul N0 2).
-    apply Nat.Div0.div_le_mono. auto.
+    apply Nat.div_le_mono. auto.
     apply (Nat.le_trans (N0*2) (N*2 + (S N0)*2)). rewrite Nat.add_comm.
     apply (Nat.le_trans (N0 * 2) (S N0 * 2)).
     apply Nat.mul_le_mono_r. apply le_S. apply Nat.le_refl.

diff --git a/reals/stdlib/CMTProductIntegral.v b/reals/stdlib/CMTProductIntegral.v
@@ -593,7 +593,8 @@ Proof.
       2: rewrite Nat.mul_1_l; reflexivity.
       intro abs. rewrite Nat.add_sub, abs, Nat.mul_0_r in H0. inversion H0.
       replace (i + length k)%nat with (i + 1*length k)%nat.
-      rewrite Nat.Div0.mod_add. reflexivity.
+      rewrite Nat.mod_add. reflexivity.
+      intro abs. rewrite Nat.add_sub, abs, Nat.mul_0_r in H0. inversion H0.
       rewrite Nat.mul_1_l. reflexivity.
     + clear IHl. simpl (list_prod (a :: l) k). rewrite app_nth1.
       2: rewrite map_length; exact l0.
@@ -1254,7 +1255,7 @@ Proof.
     pose proof (nth_list_prod
                   (FreeSubsets (length hn)) (FreeSubsets (length hn)) nil nil
                   (kg + kf * (length (FreeSubsets (length hn)))) H2).
-    rewrite Nat.div_add, Nat.Div0.mod_add, Nat.div_small, Nat.mod_small in H3.
+    rewrite Nat.div_add, Nat.mod_add, Nat.div_small, Nat.mod_small in H3.
     2: apply H0. 2: apply H0.
     symmetry. rewrite <- CRmult_1_r.
     apply CRmult_morph. rewrite <- CRmult_1_r.
@@ -1288,6 +1289,7 @@ Proof.
       simpl. destruct H0. rewrite H4.
       apply ProdIntegrableSubsetRight_match. apply inuniong. exact H1.
     + intros abs. destruct H. rewrite abs in H. inversion H.
+    + intros abs. destruct H. rewrite abs in H. inversion H.
   - (* Other points evaluate to zero *)
     intros. simpl.
     rewrite CRmult_assoc. rewrite (CRmult_morph _ _ _ (CReq_refl _) _ 0).

diff --git a/reals/stdlib/ConstructiveDiagonal.v b/reals/stdlib/ConstructiveDiagonal.v
@@ -285,7 +285,7 @@ Proof.
   assert (I = K).
   - destruct (Nat.lt_trichotomy I K).
     + exfalso. unfold lt in H0. assert ((S I) * S (S I) / 2 <= K * S K / 2)%nat.
-      apply Nat.Div0.div_le_mono.
+      apply Nat.div_le_mono. intro absurd. inversion absurd.
       apply Nat.mul_le_mono_nonneg. apply Nat.le_0_l. assumption. apply Nat.le_0_l.
       apply le_n_S. assumption. rewrite diagPlaneAbsNext in H1.
       apply (Nat.add_le_mono_l (I * S I / 2 + S I) (K * S K / 2) l) in H1.
@@ -298,7 +298,7 @@ Proof.
       assumption. apply Nat.le_refl.
     + destruct H0. assumption. exfalso.
       unfold lt in H0. assert ((S K) * S (S K) / 2 <= I * S I / 2)%nat.
-      apply Nat.Div0.div_le_mono.
+      apply Nat.div_le_mono. intro absurd. inversion absurd.
       apply Nat.mul_le_mono_nonneg. apply Nat.le_0_l. assumption. apply Nat.le_0_l.
       apply le_n_S. assumption. rewrite diagPlaneAbsNext in H1.
       apply (Nat.add_le_mono_l (K * S K / 2 + S K) (I * S I / 2) j) in H1.
@@ -433,7 +433,7 @@ Proof.
   rewrite des in H0. unfold diagPlane in H0. unfold diagPlane.
   subst p. rewrite Nat.add_0_l. ring. unfold diagPlane. rewrite Nat.add_0_l.
   rewrite Nat.add_0_l. remember (i + j)%nat. apply Nat.add_le_mono. assumption.
-  apply Nat.Div0.div_le_mono. auto. apply Nat.mul_le_mono_nonneg.
+  apply Nat.div_le_mono. auto. apply Nat.mul_le_mono_nonneg.
   apply Nat.le_0_l. assumption. apply Nat.le_0_l. apply le_n_S. assumption.
 Qed.
 
@@ -558,7 +558,7 @@ Proof.
   remember (S n + p)%nat as n0. assert (n <= n0)%nat.
   subst n0. simpl. apply le_S. rewrite <- (Nat.add_0_r n). rewrite <- Nat.add_assoc.
   apply Nat.add_le_mono_l. apply Nat.le_0_l.
-  apply Nat.add_le_mono. assumption. apply Nat.Div0.div_le_mono. auto.
+  apply Nat.add_le_mono. assumption. apply Nat.div_le_mono. auto.
   apply Nat.mul_le_mono. assumption. apply le_n_S. assumption.
   rewrite CRabs_minus_sym. apply H. apply Nat.le_refl.
   unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity.