Skip to content

is_derive1_sqrt lemma #1679

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

Merged
affeldt-aist merged 2 commits into from
Jul 7, 2025
Merged

is_derive1_sqrt lemma #1679

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
48cfb88
add derive1_sqrt
yosakaon Jul 7, 2025
3aab2e4
sqrK
affeldt-aist Jul 7, 2025
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
6 changes: 6 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,12 @@

### Added

- in `unstable.v`:
+ lemma `sqrK`

- in `realfun.v`:
+ instance `is_derive1_sqrt`

### Changed

### Renamed
Expand Down
3 changes: 3 additions & 0 deletions classical/unstable.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -483,3 +483,6 @@ Notation " R ~~> R' " := (@respectful _ _ (Program.Basics.flip (R%signature)) (R

Export -(notations) Morphisms.
End ProperNotations.

Lemma sqrK {K : rcfType} : {in Num.pos, cancel (@Num.sqrt K) (fun x => x ^+ 2)}.
Proof. by move=> r r0; rewrite sqr_sqrtr// ltW. Qed.
Comment on lines +487 to +488
Copy link
Member

@CohenCyril CohenCyril Jul 7, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks redundant with sqr_sqrt, (and slightly weaker since Num.pos can be weakened to Num.nneg).
If kept, it should be generalized and renamed sqrtK (the prefix of a K lemma is the section / thing being cancelled)

Copy link
Member

@affeldt-aist affeldt-aist Jul 7, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry for having been too hasty, will fix asap in a new PR.

Copy link
Member

@CohenCyril CohenCyril Jul 7, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(an in the long run, we should actually replace sqr_sqrt which has an equivalent statement written in an expanded way and which name is not as canonical as sqrtK)

20 changes: 20 additions & 0 deletions theories/realfun.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1763,6 +1763,26 @@ Unshelve. all: by end_near. Qed.

End is_derive_inverse.

Global Instance is_derive1_sqrt {K : realType} (x : K) : 0 < x ->
is_derive x 1 Num.sqrt (2 * Num.sqrt x)^-1.
Proof.
move=> x0.
rewrite -[x]sqrK//; apply: (@is_derive_inverse _ (fun x => x ^+ 2)).
- near=> z; rewrite sqrtr_sqr gtr0_norm//.
have [xz|zx|->] := ltgtP z (Num.sqrt x); last 2 first.
by rewrite (lt_trans _ zx)// sqrtr_gt0.
by rewrite sqrtr_gt0.
move: xz; near: z; exists (Num.sqrt x / 2) => /=.
by rewrite divr_gt0 // sqrtr_gt0 x0.
move=> r/= => /[swap] rx; rewrite gtr0_norm ?subr_gt0//ltrBlDl -ltrBlDr.
apply: le_lt_trans.
by rewrite subr_ge0 ger_pMr ?sqrtr_gt0// invf_le1// ler1n.
- by near=> z; exact: exprn_continuous.
- rewrite !sqrK//; split; first exact: exprn_derivable.
by rewrite exp_derive expr1 scaler1.
- by rewrite mulf_neq0// gt_eqF// sqrtr_gt0 exprn_gt0// sqrtr_gt0.
Unshelve. all: by end_near. Qed.

#[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) =>
(eapply is_deriveV; first by []) : typeclass_instances.

Expand Down