diff --git a/algebra/COrdFields2.v b/algebra/COrdFields2.v index c10ec1ff..c13f0b27 100644 --- a/algebra/COrdFields2.v +++ b/algebra/COrdFields2.v @@ -1008,33 +1008,24 @@ Proof. auto. Qed. -Lemma even_power_pos : forall n, even n -> forall x : R, x [#] [0] -> [0] [<] x[^]n. +Lemma even_power_pos : forall n, Nat.Even n -> forall x : R, x [#] [0] -> [0] [<] x[^]n. Proof. - intros. - elim (even_2n n H). intros m y. - replace n with (2 * m). - astepr ((x[^]2)[^]m). - apply nexp_resp_pos. - apply pos_square. auto. - rewrite y. unfold Nat.double in |- *. lia. + intros n Hn x Hx; apply Nat.Even_double in Hn as ->; unfold Nat.double. + astepr ((x[^]2)[^](Nat.div2 n)). + - apply nexp_resp_pos, pos_square; exact Hx. + - astepr ((x[^]2)[^](Nat.div2 n)); [reflexivity |]. + now rewrite nexp_mult, <-Nat.double_twice. Qed. - -Lemma odd_power_cancel_pos : forall n, odd n -> forall x : R, [0] [<] x[^]n -> [0] [<] x. +Lemma odd_power_cancel_pos : forall n, Nat.Odd n -> forall x : R, [0] [<] x[^]n -> [0] [<] x. Proof. - intros n H x H0. - induction n as [| n Hrecn]. - generalize (to_Codd _ H); intro H1. - inversion H1. - apply mult_cancel_pos_rht with (x[^]n). - astepr (x[^]S n). auto. - apply less_leEq; apply even_power_pos. - inversion H. auto. - apply un_op_strext_unfolded with (nexp_op (R:=R) (S n)). - cut (0 < S n). intro. - astepr ZeroR. - apply Greater_imp_ap. auto. - auto with arith. + intros n [m Hm]%to_Codd x. simpl. intros H. + apply mult_pos_imp in H as [[H1 H2] | [H1 H2]]. + - exact H2. + - exfalso. apply less_imp_ap in H2. + apply (even_power_pos m) in H2; [| now apply Ceven_to]. + apply less_antisymmetric_unfolded with (1 := H1). + exact H2. Qed. Lemma plus_resp_pos : forall x y : R, [0] [<] x -> [0] [<] y -> [0] [<] x[+]y. diff --git a/algebra/CRings.v b/algebra/CRings.v index cc480bfb..f4f1776a 100644 --- a/algebra/CRings.v +++ b/algebra/CRings.v @@ -1099,34 +1099,32 @@ Proof. Qed. Hint Resolve zero_nexp: algebra. -Lemma inv_nexp_even : forall (x : R) n, even n -> [--]x[^]n [=] x[^]n. +Lemma inv_nexp_even : forall (x : R) n, Nat.Even n -> [--]x[^]n [=] x[^]n. Proof. intros x n H. - elim (even_2n n); try assumption. - intros m H0. - rewrite H0. unfold Nat.double in |- *. - astepl ( [--]x[^]m[*] [--]x[^]m). - astepl (( [--]x[*] [--]x) [^]m). - astepl ((x[*]x) [^]m). - Step_final (x[^]m[*]x[^]m). + rewrite (Nat.Even_double _ H). + unfold Nat.double in |- *. + astepl ( [--]x[^](Nat.div2 n)[*] [--]x[^](Nat.div2 n)). + astepl (( [--]x[*] [--]x) [^](Nat.div2 n)). + astepl ((x[*]x) [^](Nat.div2 n)). + Step_final (x[^](Nat.div2 n)[*]x[^](Nat.div2 n)). Qed. Hint Resolve inv_nexp_even: algebra. Lemma inv_nexp_two : forall x : R, [--]x[^]2 [=] x[^]2. Proof. intro x. - apply inv_nexp_even. - auto with arith. + now apply inv_nexp_even; exists 1. Qed. Hint Resolve inv_nexp_two: algebra. -Lemma inv_nexp_odd : forall (x : R) n, odd n -> [--]x[^]n [=] [--] (x[^]n). +Lemma inv_nexp_odd : forall (x : R) n, Nat.Odd n -> [--]x[^]n [=] [--] (x[^]n). Proof. - intros x n H. - inversion H; clear H1 H n. - astepl ( [--]x[*] [--]x[^]n0). - astepl ( [--]x[*]x[^]n0). - Step_final ( [--] (x[*]x[^]n0)). + intros x [| n] H; [apply Nat.odd_spec in H; discriminate H |]. + apply Nat.Odd_succ in H. + astepl ( [--]x[*] [--]x[^]n). + astepl ( [--]x[*]x[^]n). + Step_final ( [--] (x[*]x[^]n)). Qed. Hint Resolve inv_nexp_odd: algebra. @@ -1146,14 +1144,14 @@ Proof. Qed. Hint Resolve nexp_two: algebra. -Lemma inv_one_even_nexp : forall n : nat, even n -> [--][1][^]n [=] ([1]:R). +Lemma inv_one_even_nexp : forall n : nat, Nat.Even n -> [--][1][^]n [=] ([1]:R). Proof. intros n H. Step_final (([1]:R) [^]n). Qed. Hint Resolve inv_one_even_nexp: algebra. -Lemma inv_one_odd_nexp : forall n : nat, odd n -> [--][1][^]n [=] [--] ([1]:R). +Lemma inv_one_odd_nexp : forall n : nat, Nat.Odd n -> [--][1][^]n [=] [--] ([1]:R). Proof. intros n H. Step_final ( [--] (([1]:R) [^]n)). diff --git a/algebra/Expon.v b/algebra/Expon.v index d0069537..ea3ca6f0 100644 --- a/algebra/Expon.v +++ b/algebra/Expon.v @@ -200,10 +200,10 @@ Proof. apply nexp_resp_nonneg; assumption. Qed. -Lemma nexp_resp_leEq_neg_even : forall n, even n -> +Lemma nexp_resp_leEq_neg_even : forall n, Nat.Even n -> forall x y : R, y [<=] [0] -> x [<=] y -> y[^]n [<=] x[^]n. Proof. - do 2 intro; pattern n in |- *; apply even_ind. + do 2 intro; pattern n in |- *; apply even_ind; [| | assumption]. intros; simpl in |- *; apply leEq_reflexive. clear H n; intros. astepr (x[^]n[*]x[*]x); astepl (y[^]n[*]y[*]y). @@ -215,30 +215,29 @@ Proof. astepr (y[^]2); apply sqr_nonneg. auto. astepl (y[^]2); astepr (x[^]2). + assert (E : Nat.Even 2) by (now exists 1). eapply leEq_wdr. - 2: apply inv_nexp_even; auto with arith. + 2: apply inv_nexp_even; assumption. eapply leEq_wdl. - 2: apply inv_nexp_even; auto with arith. + 2: apply inv_nexp_even; assumption. apply nexp_resp_leEq. - astepl ([--] ([0]:R)); apply inv_resp_leEq; auto. - apply inv_resp_leEq; auto. - auto. + astepl ([--] ([0]:R)); apply inv_resp_leEq; assumption. + apply inv_resp_leEq; assumption. Qed. -Lemma nexp_resp_leEq_neg_odd : forall n, odd n -> +Lemma nexp_resp_leEq_neg_odd : forall n, Nat.Odd n -> forall x y : R, y [<=] [0] -> x [<=] y -> x[^]n [<=] y[^]n. Proof. - intro; case n. - intros; exfalso; inversion H. - clear n; intros. + intro; case n; [intros [x H]; rewrite Nat.add_1_r in H; discriminate H |]. + clear n; intros n H%Nat.Odd_succ x y Hy Hxy. astepl (x[^]n[*]x); astepr (y[^]n[*]y). rstepl ([--] (x[^]n[*][--]x)); rstepr ([--] (y[^]n[*][--]y)). apply inv_resp_leEq; apply mult_resp_leEq_both. eapply leEq_wdr. - 2: apply inv_nexp_even; inversion H; auto. + 2: { apply inv_nexp_even; inversion H; assumption. } apply nexp_resp_nonneg; astepl ([--] ([0]:R)); apply inv_resp_leEq; auto. astepl ([--] ([0]:R)); apply inv_resp_leEq; auto. - apply nexp_resp_leEq_neg_even; auto; inversion H; auto. + apply nexp_resp_leEq_neg_even; auto; inversion H. apply inv_resp_leEq; auto. Qed. @@ -258,7 +257,7 @@ Qed. Hint Resolve nexp_distr_recip: algebra. -Lemma nexp_even_nonneg : forall n, even n -> forall x : R, [0] [<=] x[^]n. +Lemma nexp_even_nonneg : forall n, Nat.Even n -> forall x : R, [0] [<=] x[^]n. Proof. do 2 intro. pattern n in |- *; apply even_ind; intros. diff --git a/complex/NRootCC.v b/complex/NRootCC.v index b36c14d1..c582261f 100644 --- a/complex/NRootCC.v +++ b/complex/NRootCC.v @@ -127,18 +127,12 @@ Proof. apply sqrt_sqr. Qed. -Lemma nroot_I_nexp_aux : forall n, odd n -> {m : nat | n * n = 4 * m + 1}. +Lemma nroot_I_nexp_aux : forall n, Nat.Odd n -> {m : nat | n * n = 4 * m + 1}. Proof. - intros n on. - elim (odd_S2n n); try assumption. - intros n' H. - rewrite H. - exists (n' * n' + n'). - unfold Nat.double in |- *. - ring. + intros n [m ->]%Nat.Odd_OddT; exists (m * m + m); ring. Qed. -Definition nroot_I (n : nat) (n_ : odd n) : CC := II[^]n. +Definition nroot_I (n : nat) (n_ : Nat.Odd n) : CC := II[^]n. Lemma nroot_I_nexp : forall n n_, nroot_I n n_[^]n [=] II. Proof. @@ -181,7 +175,7 @@ Proof. Qed. Hint Resolve nroot_I_nexp: algebra. -Definition nroot_minus_I (n : nat) (n_ : odd n) : CC := [--] (nroot_I n n_). +Definition nroot_minus_I (n : nat) (n_ : Nat.Odd n) : CC := [--] (nroot_I n n_). Lemma nroot_minus_I_nexp : forall n n_, nroot_minus_I n n_[^]n [=] [--]II. Proof. @@ -964,7 +958,7 @@ Section NRootCC_4_ap_real. Variables a b : IR. Hypothesis b_ : b [#] [0]. Variable n : nat. -Hypothesis n_ : odd n. +Hypothesis n_ : Nat.Odd n. (* begin hide *) Let c := a[+I*]b. @@ -1042,7 +1036,7 @@ Proof. apply to_Codd. assumption. apply nrootCC_3'_degree. - rewrite (odd_double n). auto with arith. + rewrite (Nat.Odd_double n). auto with arith. assumption. Qed. @@ -1258,7 +1252,7 @@ and [(odd n)]; define [c' := (a[+I*]b) [*]II := a'[+I*]b']. Variables a b : IR. Hypothesis a_ : a [#] [0]. Variable n : nat. -Hypothesis n_ : odd n. +Hypothesis n_ : Nat.Odd n. (* begin hide *) Let c' := (a[+I*]b) [*]II. @@ -1303,7 +1297,7 @@ Qed. End NRootCC_4_ap_imag. -Lemma nrootCC_4 : forall c, c [#] [0] -> forall n, odd n -> {z : CC | z[^]n [=] c}. +Lemma nrootCC_4 : forall c, c [#] [0] -> forall n, Nat.Odd n -> {z : CC | z[^]n [=] c}. Proof. intros. pattern c in |- *. diff --git a/ftc/CalculusTheorems.v b/ftc/CalculusTheorems.v index a45de32c..edbb9f77 100644 --- a/ftc/CalculusTheorems.v +++ b/ftc/CalculusTheorems.v @@ -682,11 +682,11 @@ Qed. real power preserves the less or equal than relation! *) -Lemma nexp_resp_leEq_odd : forall n, odd n -> forall x y : IR, x [<=] y -> x[^]n [<=] y[^]n. +Lemma nexp_resp_leEq_odd : forall n, Nat.Odd n -> forall x y : IR, x [<=] y -> x[^]n [<=] y[^]n. Proof. - intro; case n. - intros; exfalso; inversion H. - clear n; intros. + intros [| n] H x y H'; + [destruct H as [m H]; rewrite Nat.add_1_r in H; discriminate H |]. + apply Nat.Odd_succ in H. astepl (Part (FId{^}S n) x I). astepr (Part (FId{^}S n) y I). apply Derivative_imp_resp_leEq with realline I (nring (R:=IR) (S n) {**}FId{^}n). diff --git a/logic/CLogic.v b/logic/CLogic.v index c0d41d99..d739abf6 100644 --- a/logic/CLogic.v +++ b/logic/CLogic.v @@ -48,7 +48,6 @@ Require Export Coq.Arith.Compare_dec. Require Export CoRN.logic.CornBasics. Require Export Coq.ZArith.ZArith. Require Export Coq.setoid_ring.ZArithRing. -Require Export Coq.Arith.Div2. Require Export Coq.Arith.Wf_nat. From Coq Require Import Lia. @@ -474,72 +473,57 @@ with Ceven : nat -> CProp := | Ceven_O : Ceven 0 | Ceven_S : forall n : nat, Codd n -> Ceven (S n). -Lemma Codd_even_to : forall n : nat, (Codd n -> odd n) /\ (Ceven n -> even n). +Lemma Codd_even_to : forall n : nat, (Codd n -> Nat.Odd n) /\ (Ceven n -> Nat.Even n). Proof. simple induction n. split. intro H. inversion H. intro. - apply even_O. + now exists 0. intros n0 H. elim H; intros H0 H1. split. intro H2. inversion H2. - apply odd_S. + apply Nat.Odd_succ. apply H1. assumption. intro H2. inversion H2. - apply even_S. + apply Nat.Even_succ. apply H0. assumption. Qed. -Lemma Codd_to : forall n : nat, Codd n -> odd n. +Lemma Codd_to : forall n : nat, Codd n -> Nat.Odd n. Proof. intros n H. elim (Codd_even_to n); auto. Qed. -Lemma Ceven_to : forall n : nat, Ceven n -> even n. +Lemma Ceven_to : forall n : nat, Ceven n -> Nat.Even n. Proof. intros n H. elim (Codd_even_to n); auto. Qed. -Lemma to_Codd_even : forall n : nat, (odd n -> Codd n) and (even n -> Ceven n). +Lemma to_Codd_even : forall n : nat, (Nat.Odd n -> Codd n) and (Nat.Even n -> Ceven n). Proof. - simple induction n. - split. - intro H. - exfalso. - inversion H. - intro H. - apply Ceven_O. - intros n0 H. - elim H; intros H0 H1. - split. - intro H2. - apply Codd_S. - apply H1. - inversion H2. - assumption. - intro H2. - apply Ceven_S. - apply H0. - inversion H2. - assumption. + induction n as [| n IH]; split. + - intros H%Nat.odd_spec; discriminate H. + - intros _; exact Ceven_O. + - now intros H%Nat.Odd_succ; apply IH in H; apply Codd_S. + - now intros H%Nat.Even_succ; apply IH in H; apply Ceven_S. Qed. -Lemma to_Codd : forall n : nat, odd n -> Codd n. +Lemma to_Codd : forall n : nat, Nat.Odd n -> Codd n. Proof. intros. elim (to_Codd_even n); auto. Qed. -Lemma to_Ceven : forall n : nat, even n -> Ceven n. +Lemma to_Ceven : forall n : nat, Nat.Even n -> Ceven n. Proof. intros. elim (to_Codd_even n); auto. @@ -691,21 +675,18 @@ We begin by proving that this case distinction is decidable. Next, we prove the usual results about sums of even and odd numbers: *) -Lemma even_plus_n_n : forall n : nat, even (n + n). +Lemma even_plus_n_n : forall n : nat, Nat.Even (n + n). Proof. - intro n; induction n as [| n Hrecn]. - auto with arith. - replace (S n + S n) with (S (S (n + n))). - apply even_S; apply odd_S; apply Hrecn. - rewrite plus_n_Sm; simpl in |- *; auto. + intros n; replace (n + n) with (Nat.double n) by reflexivity. + now rewrite Nat.double_twice; exists n. Qed. Lemma even_or_odd_plus : forall k : nat, {j : nat & {k = j + j} + {k = S (j + j)}}. Proof. - intro k. - elim (even_odd_dec k); intro H. - elim (even_2n k H); intros j Hj; exists j; auto. - elim (odd_S2n k H); intros j Hj; exists j; auto. + intros k; destruct (Nat.EvenT_OddT_dec k) as [[x H] | [x H]]; exists x; + replace (x + x) with (Nat.double x) by reflexivity; rewrite Nat.double_twice. + - now left. + - now right; rewrite <-Nat.add_1_r. Qed. (** Finally, we prove that an arbitrary natural number can be written in some canonical way. @@ -715,11 +696,14 @@ Lemma even_or_odd_plus_gt : forall i j : nat, i <= j -> {k : nat & {j = i + (k + k)} + {j = i + S (k + k)}}. Proof. intros i j H. - elim (even_or_odd_plus (j - i)). - intros k Hk. - elim Hk; intro H0. - exists k; left; rewrite <- H0; auto with arith. - exists k; right; rewrite <- H0; auto with arith. + destruct (even_or_odd_plus (j - i)) as [k [Hk | Hk]]; exists k. + destruct (Nat.eq_dec k 0) as [-> | I]. + - left; rewrite Nat.add_0_r; rewrite Nat.add_0_r in Hk. + now apply Nat.sub_0_le in Hk; apply Nat.le_antisymm. + - left; apply Nat.add_sub_eq_nz in Hk; [| now intros [C _]%Nat.eq_add_0]. + exact (eq_sym Hk). + - right; apply Nat.add_sub_eq_nz in Hk; [| now intros C]. + exact (eq_sym Hk). Qed. End Odd_and_Even. @@ -1007,36 +991,33 @@ results for [CProp]-valued predicates: Lemma even_induction : forall P : nat -> CProp, P 0 -> - (forall n, even n -> P n -> P (S (S n))) -> - forall n, even n -> P n. -Proof. - intros P H H0 n. - pattern n in |- *; apply lt_wf_rect. - clear n. - intros n H1 H2. - induction n as [| n Hrecn]. - auto. - induction n as [| n Hrecn0]. - exfalso; inversion H2; inversion H4. - apply H0. - inversion H2; inversion H4; auto. - apply H1. - auto with arith. - inversion H2; inversion H4; auto. + (forall n, Nat.Even n -> P n -> P (S (S n))) -> + forall n, Nat.Even n -> P n. +Proof. + intros P H0 H n; induction n as [n IH] using Wf_nat.lt_wf_rect. + destruct n as [| n]. + - intros _; exact H0. + - destruct n as [| n]. + + intros C%Nat.even_spec; discriminate C. + + intros Hn; apply ->Nat.Even_succ_succ in Hn. + apply H; [exact Hn |]. + apply IH; [| exact Hn]. + apply Nat.lt_trans with (1 := Nat.lt_succ_diag_r n). + exact (Nat.lt_succ_diag_r _). Qed. Lemma odd_induction : forall P : nat -> CProp, P 1 -> - (forall n, odd n -> P n -> P (S (S n))) -> - forall n, odd n -> P n. + (forall n, Nat.Odd n -> P n -> P (S (S n))) -> + forall n, Nat.Odd n -> P n. Proof. - intros P H H0 n; case n. - intro H1; exfalso; inversion H1. - clear n; intros n H1. - pattern n in |- *; apply even_induction; auto. - intros n0 H2 H3; auto with arith. - inversion H1; auto. + intros P H1 H [| n] Hn. + - apply Nat.odd_spec in Hn; discriminate Hn. + - apply (even_induction (fun n => P (S n))). + + exact H1. + + now intros k Hk; apply H, Nat.Odd_succ. + + now apply Nat.Odd_succ. Qed. Lemma four_induction : @@ -1064,23 +1045,23 @@ Proof. pattern m in |- *; apply lt_wf_rect; auto with arith. Qed. -Lemma odd_double_ind : forall P : nat -> CProp, (forall n, odd n -> P n) -> +Lemma odd_double_ind : forall P : nat -> CProp, (forall n, Nat.Odd n -> P n) -> (forall n, 0 < n -> P n -> P (Nat.double n)) -> forall n, 0 < n -> P n. Proof. cut (forall n : nat, 0 < Nat.double n -> 0 < n). intro. intro. intro H0. intro H1. intro n. pattern n in |- *. apply lt_wf_rect. intros n0 H2 H3. - generalize (even_odd_dec n0). intro H4. elim H4. + generalize (Nat.Even_Odd_dec n0). intro H4. elim H4. intro. - rewrite (even_double n0). + rewrite (Nat.Even_double n0). apply H1. apply H. - rewrite <- (even_double n0). assumption. + rewrite <- (Nat.Even_double n0). assumption. assumption. apply H2. apply Nat.lt_div2. assumption. - rewrite (even_double n0) in H3. + rewrite (Nat.Even_double n0) in H3. apply H. assumption. assumption. assumption. @@ -1211,31 +1192,16 @@ completeness's sake. *) Lemma even_ind : forall P : nat -> Prop, - P 0 -> (forall n, even n -> P n -> P (S (S n))) -> forall n, even n -> P n. -Proof. - intros P H H0 n. - pattern n in |- *; apply lt_wf_ind. - clear n. - intros n H1 H2. - induction n as [| n Hrecn]. - auto. - induction n as [| n Hrecn0]. - exfalso; inversion H2; inversion H4. - apply H0. - inversion H2; inversion H4; auto. - apply H1. - auto with arith. - inversion H2; inversion H4; auto. -Qed. + P 0 -> (forall n, Nat.Even n -> P n -> P (S (S n))) -> forall n, Nat.Even n -> P n. +Proof. now intros P; apply even_induction. Qed. +(* NOTE: this statement is not consistent with odd_induction, is it intended? *) Lemma odd_ind : forall P : nat -> Prop, - P 1 -> (forall n, P n -> P (S (S n))) -> forall n, odd n -> P n. + P 1 -> (forall n, P n -> P (S (S n))) -> forall n, Nat.Odd n -> P n. Proof. - intros P H H0 n; case n. - intro H1; exfalso; inversion H1. - clear n; intros n H1. - pattern n in |- *; apply even_ind; auto. - inversion H1; auto. + intros P H1 H n Hn; apply odd_induction; [exact H1 | |]. + - now intros k _; apply H. + - exact Hn. Qed. Lemma nat_complete_double_ind : diff --git a/logic/CornBasics.v b/logic/CornBasics.v index 73c248bc..8ef30b0c 100644 --- a/logic/CornBasics.v +++ b/logic/CornBasics.v @@ -47,9 +47,6 @@ From Coq Require Export ZArith. From Coq Require Import Lia. -Require Export Coq.Arith.Even. -Require Export Coq.Arith.Max. -Require Export Coq.Arith.Min. Require Export CoRN.stdlib_omissions.List. Require Import Coq.Logic.Eqdep_dec. Require Import Coq.Setoids.Setoid. diff --git a/metric2/Compact.v b/metric2/Compact.v index 9684722b..c0a32f53 100644 --- a/metric2/Compact.v +++ b/metric2/Compact.v @@ -26,7 +26,6 @@ Require Export CoRN.metric2.Complete. Require Import CoRN.logic.Classic. Require Import Coq.QArith.Qpower. Require Import Coq.QArith.Qround. -Require Import Coq.Arith.Div2. Set Implicit Arguments. diff --git a/ode/SimpleIntegration.v b/ode/SimpleIntegration.v index 5938fa52..1314f123 100644 --- a/ode/SimpleIntegration.v +++ b/ode/SimpleIntegration.v @@ -10,7 +10,7 @@ Require Import CoRN.metric2.Metric. Require Import CoRN.metric2.UniformContinuity. Require Import CoRN.model.reals.CRreal. Require Import - CoRN.stdlib_omissions.List Coq.Numbers.Natural.Peano.NPeano Coq.Unicode.Utf8 + CoRN.stdlib_omissions.List Coq.Unicode.Utf8 Coq.QArith.QArith Coq.QArith.Qabs CoRN.model.totalorder.QposMinMax CoRN.util.Qsums CoRN.model.metric2.Qmetric CoRN.model.setoids.Qsetoid (* Needs imported for Q_is_Setoid to be a canonical structure *) diff --git a/reals/Bridges_LUB.v b/reals/Bridges_LUB.v index 0ae42232..034190a8 100644 --- a/reals/Bridges_LUB.v +++ b/reals/Bridges_LUB.v @@ -649,7 +649,7 @@ Proof. apply Nat.le_add_r. apply U_conversion_rate2 with (m := S (N + 3)). apply le_n_S. - apply le_plus_r. + apply Nat.le_add_l. assumption. apply Archimedes'. (* Note the use of Archimedean Property of R1 *) Qed. @@ -956,7 +956,7 @@ Proof. assumption. apply H3. apply Nat.le_trans with (m := N1 + N2). - apply le_plus_r. + apply Nat.le_add_l. assumption. unfold B in |- *. cut (SeqLimit U_as_CauchySeq (Lim U_as_CauchySeq)). @@ -1057,7 +1057,7 @@ Proof. assumption. apply a0. apply Nat.le_trans with (m := N1 + N2). - apply le_plus_r. + apply Nat.le_add_l. assumption. unfold B in |- *. cut (SeqLimit U_as_CauchySeq (Lim U_as_CauchySeq)). diff --git a/reals/Bridges_iso.v b/reals/Bridges_iso.v index d74307ae..18302778 100644 --- a/reals/Bridges_iso.v +++ b/reals/Bridges_iso.v @@ -577,7 +577,7 @@ Proof. Intros. Left. Intros. - Rewrite <- (le_n_O_eq m H2). + Rewrite <- (Nat.le_0_r m H2). Assumption. Intro. Right. @@ -593,7 +593,7 @@ Proof. Apply H. Apply Nat.le_trans with m:=N. Assumption. - Apply le_n_Sn. + Apply Nat.le_succ_diag_r. Intro. Case (H (S N)). Apply le_n. @@ -626,7 +626,7 @@ Proof. Split. Apply Nat.le_trans with m:=N. Assumption. - Apply le_n_Sn. + Apply Nat.le_succ_diag_r. Assumption. Qed. *) @@ -1419,10 +1419,10 @@ Proof. apply a. apply Nat.le_trans with (m := m). assumption. - apply le_plus_r. + apply Nat.le_add_l. apply AbsSmall_minus. apply a. - apply le_plus_r. + apply Nat.le_add_l. Qed. @@ -1658,7 +1658,7 @@ Proof. apply leEq_wdr with (y := sup (tail_seq g N)). change (sup_tail (k + N)[<=]sup_tail N) in |- *. apply sup_tail_decrease. - apply le_plus_r. + apply Nat.le_add_l. apply eq_symmetric_unfolded. assumption. apply less_leEq. @@ -1724,7 +1724,7 @@ Proof. apply leEq_transitive with (y := nring (R:=OF) k). apply less_leEq; assumption. apply nring_leEq. - apply le_plus_r. + apply Nat.le_add_l. apply Greater_imp_ap. apply pos_div_two. assumption. diff --git a/reals/OddPolyRootIR.v b/reals/OddPolyRootIR.v index 9f8faa15..5e20a6a2 100644 --- a/reals/OddPolyRootIR.v +++ b/reals/OddPolyRootIR.v @@ -171,7 +171,7 @@ Qed. Hint Resolve flip_coefficient: algebra. -Lemma flip_odd : forall (p : RX) n, odd n -> monic n p -> monic n (flip p). +Lemma flip_odd : forall (p : RX) n, Nat.Odd n -> monic n p -> monic n (flip p). Proof. unfold monic in |- *. unfold degree_le in |- *. intros. @@ -207,24 +207,24 @@ Variable R : COrdField. Let RX := (cpoly R). (* end hide *) -Lemma oddpoly_pos : forall (p : RX) n, odd n -> monic n p -> {x : R | [0] [<=] p ! x}. +Lemma oddpoly_pos : forall (p : RX) n, Nat.Odd n -> monic n p -> {x : R | [0] [<=] p ! x}. Proof. - intros. + intros p n H1 H2. apply cpoly_pos with n; auto. - elim H. intros. auto with arith. + destruct H1 as [m ->]; rewrite Nat.add_1_r; exact (Nat.lt_0_succ _). Qed. Lemma oddpoly_pos' : forall (p : RX) a n, - odd n -> monic n p -> {x : R | a [<] x | [0] [<=] p ! x}. + Nat.Odd n -> monic n p -> {x : R | a [<] x | [0] [<=] p ! x}. Proof. - intros. - elim (Ccpoly_pos' _ p a n). intros x H1 H2. - exists x; assumption. - elim H; auto with arith. - assumption. + intros p a n H1 H2. + elim (Ccpoly_pos' _ p a n). + - intros x Hx Hp; exists x; assumption. + - destruct H1 as [m ->]; rewrite Nat.add_1_r; exact (Nat.lt_0_succ _). + - assumption. Qed. -Lemma oddpoly_neg : forall (p : RX) n, odd n -> monic n p -> {x : R | p ! x [<=] [0]}. +Lemma oddpoly_neg : forall (p : RX) n, Nat.Odd n -> monic n p -> {x : R | p ! x [<=] [0]}. Proof. intros. elim (oddpoly_pos _ _ H (flip_odd _ _ _ H H0)). intro x. intros. @@ -289,7 +289,7 @@ Section OddPoly_Root. ** Roots of polynomials of odd degree Polynomials of odd degree over the reals always have a root. *) -Lemma oddpoly_root' : forall f n, odd n -> monic n f -> {x : IR | f ! x [=] [0]}. +Lemma oddpoly_root' : forall f n, Nat.Odd n -> monic n f -> {x : IR | f ! x [=] [0]}. Proof. intros. elim (oddpoly_neg _ f n); auto. intro a. intro H1. @@ -304,7 +304,7 @@ Proof. apply monic_apzero with n; auto. Qed. -Lemma oddpoly_root : forall f n, odd n -> degree n f -> {x : IR | f ! x [=] [0]}. +Lemma oddpoly_root : forall f n, Nat.Odd n -> degree n f -> {x : IR | f ! x [=] [0]}. Proof. intros f n H H0. elim (oddpoly_root' (poly_norm _ f n H0) n); auto. @@ -318,7 +318,7 @@ Proof. unfold odd_cpoly in |- *. intros f H. elim H. clear H. intro n. intros H H0. - cut (odd n). + cut (Nat.Odd n). intro. elim (oddpoly_root f n H1 H0). intros. exists x. auto. apply Codd_to. diff --git a/reals/Q_dense.v b/reals/Q_dense.v index a375a85a..20fa4961 100644 --- a/reals/Q_dense.v +++ b/reals/Q_dense.v @@ -719,7 +719,7 @@ Proof. apply Nat.le_add_r. apply G_conversion_rate2 with (m := S (N + 3)). apply le_n_S. - apply le_plus_r. + apply Nat.le_add_l. assumption. apply Q_is_archemaedian. (* Note the use of Q_is_archemaedian *) Qed. @@ -908,7 +908,7 @@ Proof. apply G_conversion_rate_resp_x. apply Nat.le_trans with (m := S (N + 3)). apply le_n_S. - apply le_plus_r. + apply Nat.le_add_l. assumption. apply Archimedes'. Qed. diff --git a/reals/Series.v b/reals/Series.v index 60791287..74d2425e 100644 --- a/reals/Series.v +++ b/reals/Series.v @@ -1004,9 +1004,8 @@ Proof. eapply eq_transitive_unfolded. apply nexp_plus. apply inv_one_odd_nexp. - cut (n + S (n + (m + m)) = S (n + n + (m + m))); [ intro | rewrite <- plus_n_Sm; auto with arith ]. - rewrite H0. - auto with arith. + replace (n + S (n + (m + m))) with (2 * (n + m) + 1) by ring; + now exists (n + m). astepl ([1][*]x (S (S (n + (m + m))))). rstepr ( [--][1][^]n[*][--][1][^]S (S (n + (m + m))) [*]x (S (S (n + (m + m))))). apply mult_wdl. @@ -1014,9 +1013,8 @@ Proof. eapply eq_transitive_unfolded. apply nexp_plus. apply inv_one_even_nexp. - cut (n + S (S (n + (m + m))) = S (S (n + n + (m + m)))); [ intro | lia ]. - rewrite H0. - auto with arith. + replace (n + S (S (n + (m + m)))) with (2 * (S (n + m))) by ring; + now exists (S (n + m)). unfold Sum in |- *; simpl in |- *. unfold Sum1 in |- *; simpl in |- *. rational. @@ -1041,9 +1039,8 @@ Proof. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. apply nexp_plus. apply inv_one_odd_nexp. - cut (n + S (n + (m + m)) = S (n + n + (m + m))); [ intro | rewrite <- plus_n_Sm; auto with arith ]. - rewrite H0. - auto with arith. + replace (n + S (n + (m + m))) with (2 * (n + m) + 1) by ring; + now exists (n + m). apply pos_x. eapply eq_transitive_unfolded. apply eq_symmetric_unfolded; apply ring_dist_unfolded. @@ -1081,9 +1078,7 @@ Proof. eapply eq_transitive_unfolded. apply nexp_plus. apply inv_one_odd_nexp. - cut (n + S n = S (n + n)); [ intro | auto with arith ]. - rewrite H1. - auto with arith. + replace (n + S n) with (2 * n + 1) by ring; now exists n. unfold Sum, Sum1 in |- *; simpl in |- *; rational. cut (n + S (S m + S m) = S (S (n + S (m + m)))); [ intro | simpl in |- *; repeat rewrite <- plus_n_Sm; auto with arith ]. @@ -1106,19 +1101,15 @@ Proof. astepl ([1][*]x (S (n + S (m + m)))); apply mult_wdl. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded; [ apply nexp_plus | apply inv_one_even_nexp ]. - cut (n + S (n + S (m + m)) = S (S (n + n + (m + m)))); - [ intro | simpl in |- *; repeat rewrite <- plus_n_Sm; auto with arith ]. - rewrite H0. - auto with arith. + replace (n + S (n + S (m + m))) with (2 * (n + m + 1)) by ring; + now exists (n + m + 1). eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply mult_assoc_unfolded. rstepl ( [--][1][*]x (S (S (n + S (m + m))))); apply mult_wdl. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded; [ apply nexp_plus | apply inv_one_odd_nexp ]. - cut (n + S (S (n + S (m + m))) = S (S n + S n + (m + m))); [ intro - | simpl in |- *; repeat rewrite <- plus_n_Sm; simpl in |- *; auto with arith ]. - rewrite H0. - auto with arith. + replace (n + S (S (n + S (m + m)))) with (2 * (n + m + 1) + 1) by ring; + now exists (n + m + 1). apply mult_wdr. unfold Sum, Sum1 in |- *; simpl in |- *; rational. Qed. @@ -1158,10 +1149,8 @@ Proof. apply less_leEq; apply pos_one. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. apply nexp_plus. - cut (n + S (n + S (m + m)) = n + n + (S m + S m)); [ intro - | simpl in |- *; repeat rewrite <- plus_n_Sm; simpl in |- *; auto with arith ]. - rewrite H0; apply inv_one_even_nexp. - auto with arith. + replace (n + S (n + S (m + m))) with (2 * (n + m + 1)) by ring. + apply inv_one_even_nexp; now exists (n + m + 1). apply pos_x. apply plus_resp_leEq. apply alternate_lemma3. @@ -1224,7 +1213,7 @@ Proof. astepr ZeroR; apply leEq_reflexive. simpl in |- *; unfold ABSIR in |- *; apply eq_reflexive_unfolded. apply eq_symmetric_unfolded; assumption. - elim (even_odd_dec N); intro. + destruct (Nat.Even_Odd_dec N) as [HE | HO]. apply AbsIR_wd. eapply eq_transitive_unfolded. apply seq_part_sum_n; auto; apply Nat.lt_le_trans with N; auto. @@ -1254,16 +1243,8 @@ Proof. 2: apply eq_symmetric_unfolded; apply mult_assoc_unfolded. apply mult_wdl. astepl (OneR[*][--][1][^]i). - apply mult_wdl. - apply eq_symmetric_unfolded. - rstepl ( [--]OneR[^]1[*][--][1][^]N). - eapply eq_transitive_unfolded. - apply nexp_plus. - apply inv_one_even_nexp. - simpl in |- *. - auto with arith. - exists (S N'). - auto with arith. + now apply mult_wdl; rewrite inv_one_odd_nexp, cg_inv_inv by assumption. + exists (S N'); [exact (Nat.lt_0_succ _) |]. intros. astepr (x m[-][0]); apply HN'; auto with arith. Qed. diff --git a/reals/fast/CRartanh_slow.v b/reals/fast/CRartanh_slow.v index 703128c6..0e9a6dc5 100644 --- a/reals/fast/CRartanh_slow.v +++ b/reals/fast/CRartanh_slow.v @@ -369,10 +369,9 @@ csetoid_replace (ArTanH_series_coef (S (Nat.double n))[*]A) (inj_Q IR (Str_nth n (artanhSequence a))). rational. unfold ArTanH_series_coef. - case_eq (even_odd_dec (S (Nat.double n))); intros H. - elim (not_even_and_odd _ H). - constructor. - apply even_plus_n_n. + case_eq (Nat.Even_Odd_dec (S (Nat.double n))); intros H. + elim (Nat.Even_Odd_False _ H). + now rewrite <-Nat.add_1_r, Nat.double_twice; exists n. intros _. eapply eq_transitive; [|apply inj_Q_wd; simpl;symmetry;apply Str_nth_artanhSequence]. @@ -416,11 +415,11 @@ csetoid_replace (ArTanH_series_coef (S (Nat.double n))[*]A) apply nexp_wd. rational. unfold ArTanH_series_coef. -case_eq (even_odd_dec (Nat.double n)). +case_eq (Nat.Even_Odd_dec (Nat.double n)). intros _ _. rational. intros o. -elim (fun x=> not_even_and_odd _ x o). +elim (fun x=> Nat.Even_Odd_False _ x o). apply even_plus_n_n. Qed. diff --git a/reals/fast/CRsin.v b/reals/fast/CRsin.v index e216fcd0..84758fab 100644 --- a/reals/fast/CRsin.v +++ b/reals/fast/CRsin.v @@ -366,23 +366,15 @@ Proof. apply bin_op_wd_unfolded. + destruct (even_or_odd_plus n') as [m [Hm|Hm]]; simpl. rational. - elim (not_even_and_odd n'). - apply (even_mult_l 2 n). - repeat constructor. - rewrite Hm. - constructor. - replace (m + m)%nat with (2*m)%nat by lia. - apply (even_mult_l 2 m). - repeat constructor. + elim (Nat.Even_Odd_False n'); + [ now apply (Nat.Even_mul_l 2 n); exists 1%nat | + now exists m; rewrite Hm, Nat.add_1_r; simpl; rewrite Nat.add_0_r]. + destruct (even_or_odd_plus (S n')) as [m [Hm|Hm]]; simpl. - elim (not_even_and_odd (S n')). + elim (Nat.Even_Odd_False (S n')). rewrite Hm. replace (m + m)%nat with (2*m)%nat by lia. - apply (even_mult_l 2 m). - repeat constructor. - constructor. - apply (even_mult_l 2 n). - repeat constructor. + now apply (Nat.Even_mul_l 2 m); exists 1%nat. + subst n'; exists n; ring. inversion Hm. unfold n' in H1. replace m with n by lia. diff --git a/reals/iso_CReals.v b/reals/iso_CReals.v index f035358c..3ff8d8f6 100644 --- a/reals/iso_CReals.v +++ b/reals/iso_CReals.v @@ -99,7 +99,7 @@ Proof. assumption. apply H5. apply Nat.le_trans with (m := N1 + N2). - apply le_plus_r. + apply Nat.le_add_l. assumption. apply H1. apply div_resp_pos. @@ -296,7 +296,7 @@ Proof. apply shift_minus_less; rstepr (Lim g); auto. elim (H6 (N1 + N2)); intros. rstepl ([--]((Lim g[-]y) [/]ThreeNZ)); auto. - apply le_plus_r. + apply Nat.le_add_l. elim (H3 (N1 + N2)); intros. apply inv_cancel_leEq. rstepr ((Lim g[-]y) [/]ThreeNZ); rstepl (g (N1 + N2)[-]y); auto. @@ -336,7 +336,7 @@ Proof. elim (a (N1 + N2)); intros. apply inv_cancel_leEq. rstepr ((y[-]Lim g) [/]ThreeNZ); rstepl (g (N1 + N2)[-]Lim g); auto. - apply le_plus_r. + apply Nat.le_add_l. elim (H3 (N1 + N2)); intros. rstepl ([--]((y[-]Lim g) [/]ThreeNZ)); auto. apply Nat.le_add_r. @@ -389,7 +389,7 @@ Proof. assumption. apply H7. apply Nat.le_trans with (m := N1 + N2). - apply le_plus_r. + apply Nat.le_add_l. assumption. apply H4. apply pos_div_two. @@ -444,7 +444,7 @@ Proof. apply AbsSmall_minus. apply H6. apply Nat.le_trans with (m := N1 + N2). - apply le_plus_r. + apply Nat.le_add_l. assumption. apply eq_transitive_unfolded with (y := CS_seq IR g m[-]CS_seq IR h m[+](Lim h[-]Lim g)). rational. @@ -604,7 +604,7 @@ Proof. assumption. apply H5. apply Nat.le_trans with (m := N1 + N2). - apply le_plus_r. + apply Nat.le_add_l. assumption. apply (ax_Lim _ _ (crl_proof IR) h). apply pos_div_two. @@ -772,7 +772,7 @@ Proof. apply a. apply Nat.le_add_r. apply H2. - apply le_plus_r. + apply Nat.le_add_l. apply Lim_Cauchy. Qed. diff --git a/stdlib_omissions/Z.v b/stdlib_omissions/Z.v index d5ee48ce..598314b8 100644 --- a/stdlib_omissions/Z.v +++ b/stdlib_omissions/Z.v @@ -1,5 +1,5 @@ -Require Import Coq.ZArith.ZArith Coq.Numbers.Natural.Peano.NPeano CoRN.stdlib_omissions.P. +Require Import Coq.ZArith.ZArith CoRN.stdlib_omissions.P. Require Import Lia. (*Require Import NSigNAxioms. was added in the trunk branch*) diff --git a/transc/ArTanH.v b/transc/ArTanH.v index 9a826543..b485ea1e 100644 --- a/transc/ArTanH.v +++ b/transc/ArTanH.v @@ -315,16 +315,15 @@ Proof. Qed. (** PowerSeries for the Inverse Hyperbolic Tangent Function. *) -Lemma ArTanH_series_coef_lemma : forall (R:COrdField) n, odd n -> (nring (R:=R) n)[#][0]. +Lemma ArTanH_series_coef_lemma : forall (R:COrdField) n, Nat.Odd n -> (nring (R:=R) n)[#][0]. Proof. - intros R [|n] H. - exfalso. - inversion H. + intros R [|n] H%Nat.Odd_OddT; + [destruct H as [k H]; rewrite Nat.add_1_r in H; discriminate H |]. apply nringS_ap_zero. Qed. Definition ArTanH_series_coef (n:nat) := -match (even_odd_dec n) with +match (Nat.Even_Odd_dec n) with | left _ => [0] | right H => [1][/](nring n)[//](ArTanH_series_coef_lemma IR n H) end. @@ -349,10 +348,11 @@ Proof. Log_series_coef n[*]([1][-]x[-][1])[^]n)[=] ArTanH_series_coef n[*]nexp IR n (x[-][0])). unfold ArTanH_series_coef. destruct n as [|n]. - destruct (even_odd_dec 0) as [A|A]; try inversion A. - simpl; rational. + destruct (Nat.Even_Odd_dec 0) as [A|A]; + [simpl; rational | + exfalso; destruct A as [k B]; rewrite Nat.add_1_r in B; discriminate B ]. rstepl (Half (R:=IR)[*] (Log_series_coef (S n)[*](x[^]S n[-]([--]x)[^]S n))). - destruct (even_odd_dec (S n)) as [A|A]; unfold cg_minus. + destruct (Nat.Even_Odd_dec (S n)) as [A|A]; unfold cg_minus. csetoid_rewrite (inv_nexp_even _ x _ A). rational. csetoid_rewrite (inv_nexp_odd _ x _ A). @@ -361,7 +361,8 @@ Proof. apply mult_wd;[|change (x[^]S n[=](x[+][--][0])[^]S n); rational]. unfold Log_series_coef. apply div_wd; try apply eq_reflexive. - csetoid_rewrite (inv_nexp_even IR [1] _ (even_S _ A)). + apply Nat.Even_succ in A. + csetoid_rewrite (inv_nexp_even IR [1] _ A). algebra. Qed. diff --git a/transc/PowerSeries.v b/transc/PowerSeries.v index 47db6f8e..498a2fa5 100644 --- a/transc/PowerSeries.v +++ b/transc/PowerSeries.v @@ -446,7 +446,7 @@ Proof. elim Hk; simpl in |- *; intro. eapply leEq_wdl; [ apply less_leEq; apply pos_one | apply eq_symmetric_unfolded; apply AbsIRz_isz ]. apply eq_imp_leEq. - elim (even_odd_dec k); intro. + elim (Nat.Even_Odd_dec k); intro. apply eq_transitive_unfolded with (AbsIR [1]). apply AbsIR_wd; astepl ([--]OneR[^]k); apply inv_one_even_nexp; auto. apply AbsIR_eq_x; apply less_leEq; apply pos_one. @@ -464,7 +464,7 @@ Proof. elim even_or_odd_plus; intros k Hk; simpl in |- *. elim Hk; simpl in |- *; intro. apply eq_imp_leEq. - elim (even_odd_dec k); intro. + elim (Nat.Even_Odd_dec k); intro. apply eq_transitive_unfolded with (AbsIR [1]). apply AbsIR_wd; astepl ([--]OneR[^]k); apply inv_one_even_nexp; auto. apply AbsIR_eq_x; apply less_leEq; apply pos_one. diff --git a/transc/SinCos.v b/transc/SinCos.v index b84a2272..3f693ed7 100644 --- a/transc/SinCos.v +++ b/transc/SinCos.v @@ -184,7 +184,7 @@ Proof. apply mult_wdr. rewrite b. eapply eq_transitive_unfolded. - 2: apply inv_nexp_odd; apply odd_S; apply even_plus_n_n. + 2: apply inv_nexp_odd; apply Nat.Odd_succ; apply even_plus_n_n. apply nexp_wd; rational. Qed. diff --git a/util/Qsums.v b/util/Qsums.v index eeb5ea71..72a84fd3 100644 --- a/util/Qsums.v +++ b/util/Qsums.v @@ -1,5 +1,5 @@ Require Import - CoRN.stdlib_omissions.List Coq.Numbers.Natural.Peano.NPeano + CoRN.stdlib_omissions.List Coq.QArith.QArith Coq.QArith.Qabs CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric