Merge pull request #202 from Villetaneuse/rm_arith_files

Adapt to coq/coq#18164
coq-community · Nov 10, 2023 · 79e7ee7 · 79e7ee7
2 parents a6158dc + 7d6c53e
commit 79e7ee7
Show file tree

Hide file tree

Showing 22 changed files with 228 additions and 303 deletions.
diff --git a/algebra/COrdFields2.v b/algebra/COrdFields2.v
@@ -1008,33 +1008,27 @@ Proof.
  auto.
 Qed.
 
-Lemma even_power_pos : forall n, 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.
-Qed.
-
-
-Lemma odd_power_cancel_pos : forall n, 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.
+Lemma even_power_pos : forall n, Nat.Even n -> forall x : R, x [#] [0] -> [0] [<] x[^]n.
+Proof.
+ intros n Hn x Hx.
+ destruct (even_or_odd_plus n) as [k [Hk | Hk]].
+ - astepr ((x[^]2)[^](k)).
+   apply nexp_resp_pos, pos_square; exact Hx.
+   astepr ((x[^]2)[^](k)); [reflexivity |].
+   now rewrite nexp_mult, Hk; replace (2 * k) with (k + k) by lia.
+ - exfalso; apply (Nat.Even_Odd_False n); [exact Hn |].
+   exists k; lia.
+Qed.
+
+Lemma odd_power_cancel_pos : forall n, Nat.Odd n -> forall x : R, [0] [<] x[^]n -> [0] [<] x.
+Proof.
+ 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
@@ -1099,34 +1099,31 @@ 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).
+ intros x n [k H].
+ replace (2 * k) with (k + k) in H by lia; rewrite H.
+ astepl ( [--]x[^](k)[*] [--]x[^](k)).
+ astepl (( [--]x[*] [--]x) [^](k)).
+ astepl ((x[*]x) [^](k)).
+ Step_final (x[^](k)[*]x[^](k)).
 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 +1143,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
@@ -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
@@ -127,18 +127,15 @@ 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 H; destruct (even_or_odd_plus n) as [m [Hm | ->]].
+ - exfalso; apply (Nat.Even_Odd_False n); [| exact H].
+   exists m; rewrite Hm; ring.
+ - 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 +178,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 +961,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,8 +1039,7 @@ Proof.
   apply to_Codd.
   assumption.
  apply nrootCC_3'_degree.
- rewrite (odd_double n). auto with arith.
-  assumption.
+ destruct n_ as [k ->]; rewrite Nat.add_1_r; exact (Nat.lt_0_succ _).
 Qed.
 
 End NRootCC_4_solutions.
@@ -1258,7 +1254,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 +1299,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
@@ -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).