Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve compatibility lemmas in Rstruct #1235

Merged
merged 5 commits into from
May 31, 2024
Merged

Improve compatibility lemmas in Rstruct #1235

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
205c469
strengthen RinvE and RdivE; add Pos_to_natE and IZposRE
t6s May 30, 2024
9161ad9
doc
t6s May 30, 2024
5c392d4
review
affeldt-aist May 30, 2024
dbcb64c
fix
affeldt-aist May 30, 2024
7f24c49
fix for the CI
affeldt-aist May 31, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,12 @@
- in `measure.v`:
+ lemma `measurableID`

- in `mathcomp_extra.v`:
+ lemma `Pos_to_natE`

- in `Rstruct.v`:
+ lemma `IZRposE`

### Changed

- in `forms.v`:
Expand Down Expand Up @@ -136,6 +142,9 @@

### Generalized

- in `Rstruct.v`:
+ lemmas `RinvE`, `RdivE`

- in `constructive_ereal.v`:
+ `gee_pMl` (was `gee_pmull`)

Expand Down
10 changes: 10 additions & 0 deletions classical/mathcomp_extra.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -364,3 +364,13 @@ rewrite /Order.min/=; case: ifPn => xz; case: ifPn => yz; rewrite ?ltxx//.
Qed.

End order_min.

Section positive.

Lemma Pos_to_natE p : Pos.to_nat p = nat_of_pos p.
Proof.
by elim: p => //= p <-;
rewrite ?(Pnat.Pos2Nat.inj_xI,Pnat.Pos2Nat.inj_xO) NatTrec.doubleE -mul2n.
Qed.

End positive.
23 changes: 18 additions & 5 deletions theories/Rstruct.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
Require Import Rtrigo1 Reals.
From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum.
From HB Require Import structures.
From mathcomp Require Import mathcomp_extra.

Set Implicit Arguments.
Unset Strict Implicit.
Expand Down Expand Up @@ -456,20 +457,32 @@ Lemma RmultE x y : Rmult x y = x * y. Proof. by []. Qed.

Lemma RoppE x : Ropp x = - x. Proof. by []. Qed.

Lemma RinvE x : x != 0 -> Rinv x = x^-1.
Let neq0_RinvE x : x != 0 -> Rinv x = x^-1.
Proof. by move=> x_neq0; rewrite -[RHS]/(if _ then _ else _) x_neq0. Qed.

Lemma RdivE x y : y != 0 -> Rdiv x y = x / y.
Proof. by move=> y_neq0; rewrite /Rdiv RinvE. Qed.
Lemma RinvE x : Rinv x = x^-1.
Proof.
have [->| ] := eqVneq x R0; last exact: neq0_RinvE.
rewrite /GRing.inv /GRing.mul /= /Rinvx eqxx /=.
rewrite RinvImpl.Rinv_def; case: Req_appart_dec => //.
by move=> /[dup] -[] /RltP; rewrite Order.POrderTheory.ltxx.
Qed.

Lemma RdivE x y : Rdiv x y = x / y. Proof. by rewrite /Rdiv RinvE. Qed.

Lemma INRE n : INR n = n%:R.
Proof. elim: n => // n IH; by rewrite S_INR IH RplusE -addn1 natrD. Qed.

(**md Note that rewrites using the following lemma `IZRposE` are
systematically followed by a rewrite using the lemma `INRE`. *)
Lemma IZRposE (p : positive) : IZR (Z.pos p) = INR (nat_of_pos p).
Proof. by rewrite -Pos_to_natE INR_IPR. Qed.

Lemma RsqrtE x : 0 <= x -> sqrt x = Num.sqrt x.
Proof.
move => x0; apply/eqP; have [t1 t2] := conj (sqrtr_ge0 x) (sqrt_pos x).
rewrite eq_sym -(eqrXn2 (_: 0 < 2)%N t1) //; last by apply /RleP.
rewrite sqr_sqrtr // !exprS expr0 mulr1 -RmultE ?sqrt_sqrt //; by apply/RleP.
rewrite eq_sym -(eqrXn2 (_: 0 < 2)%N t1) //; last exact/RleP.
by rewrite sqr_sqrtr // !exprS expr0 mulr1 -RmultE ?sqrt_sqrt //; exact/RleP.
Qed.

Lemma RpowE x n : pow x n = x ^+ n.
Expand Down
Loading