From 551189ef1a28690ad729eed4338fd63a73c87a7a Mon Sep 17 00:00:00 2001 From: Ana Dalton Date: Tue, 30 May 2023 13:09:05 -0700 Subject: [PATCH 1/3] Remove conditional from configure.sh The conditional doesn't work in all bashes (doesn't work in mine, GNU bash, version 5.2.15(1)-release (x86_64-pc-linux-gnu) Moreover we don't even support versions of Coq that low anymore, so there's no need. --- configure.sh | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/configure.sh b/configure.sh index 92ab2e98c..fae7a0895 100755 --- 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 From a3e9b987500ea4575f29d3ea9ae5fa053e10642b Mon Sep 17 00:00:00 2001 From: Ana Dalton Date: Tue, 30 May 2023 13:48:04 -0700 Subject: [PATCH 2/3] Revert "'Deprecate Nat.div_le_mono for Div0.div_le_mono'" This reverts commit 09f771924e911acd5fb3d2fea8289980d9ea0ec8. It seems that older versions of Coq do not have these modules and therefore this is a breaking change. I do not know why CI didn't catch this. --- reals/stdlib/CMTFullSets.v | 2 +- reals/stdlib/CMTIntegrableFunctions.v | 8 ++++---- reals/stdlib/ConstructiveDiagonal.v | 8 ++++---- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/reals/stdlib/CMTFullSets.v b/reals/stdlib/CMTFullSets.v index 46c71c4b8..ae5240789 100644 --- 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 index 395f14870..82044286e 100644 --- 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/ConstructiveDiagonal.v b/reals/stdlib/ConstructiveDiagonal.v index 97b096c09..840c8dcb9 100644 --- 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. From ae9ab3ae5e2e451767947a8b3ed957c9ebaca1ce Mon Sep 17 00:00:00 2001 From: Ana Dalton Date: Tue, 30 May 2023 13:55:17 -0700 Subject: [PATCH 3/3] Revert "'Deprecate Nat.mod_add for Nat.Div0.mod_add'" This reverts commit 7e39c789778465b5f785d211827731cfdb4529c6. Nat.Div0 modules are too modern for versions of Coq 8.16 and below. --- reals/stdlib/CMTProductIntegral.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/reals/stdlib/CMTProductIntegral.v b/reals/stdlib/CMTProductIntegral.v index 7eb41f989..c171e4e9a 100644 --- 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).