Skip to content

Commit

Permalink
Adapt to coq/coq#18164
Browse files Browse the repository at this point in the history
  • Loading branch information
@Villetaneuse
Villetaneuse committed Nov 8, 2023
1 parent a6158dc commit 5c94a75
Show file tree
Hide file tree
Showing 22 changed files with 193 additions and 276 deletions.
37 changes: 14 additions & 23 deletions algebra/COrdFields2.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
34 changes: 16 additions & 18 deletions algebra/CRings.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand All @@ -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)).
Expand Down
27 changes: 13 additions & 14 deletions algebra/Expon.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand All @@ -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.

Expand All @@ -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.
Expand Down
22 changes: 8 additions & 14 deletions complex/NRootCC.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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 |- *.
Expand Down
8 changes: 4 additions & 4 deletions ftc/CalculusTheorems.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down
Loading

0 comments on commit 5c94a75

Please sign in to comment.