Generalize exp_ineq1 and add exp_ineq1_le, which holds forall Reals.

[shinnar]

Adds exp_ineq2, the negative counterpart to exp_ineq1.
Adds exp_ineq, which holds for all reals (but is a <= instead of a <).

Rpower currently defines exp_ineq1 : forall x:R, 0 < x -> 1 + x < exp x.
This PR adds the corresponding lemma for negative R: exp_ineq2 : forall x:R, 0 > x -> 1 + x < exp x
and the (slightly weaker) version for all R: exp_ineq : forall x:R, 1 + x <= exp x
These minor additions are nice to add for completeness, and are useful for users.

This proof was mostly done by Barry Trager (@bmtrager), and is being submitted with his permission (and at his request).

Kind: documentation / bug fix / feature / performance / infrastructure.
library addition / minor feature

Fixes / closes #????

• Added / updated test-suite

• Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

[Zimmi48]

This proof was mostly done by Barry Trager (@bmtrager), and is being submitted with his permission (and at his request).

Note that you can use Co-authored-by: to credit them. See https://github.blog/2018-01-29-commit-together-with-co-authors/

Also, this addition to the standard library, as any addition, will need a changelog entry. See https://github.com/coq/coq/tree/master/doc/changelog#how-to-add-an-entry

[retzger77]

Thank 🧒

…

On Sun, 6 Dec 2020, 16:45 Laurent Théry, ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In theories/Reals/Rpower.v <#13582 (comment)>: > @@ -233,6 +233,44 @@ Proof. apply H. Qed. +Lemma exp_gt1 (x : R) : 0 < x -> 1 < exp x. +Proof. + intro xgt. + generalize (exp_ineq1 x xgt); intros. + apply Rlt_trans with (r2 := 1+x); lra. +Qed. + +Lemma exp_ineq2 (x : R) : 0 > x -> 1 + x < exp x. Maybe we should only have exp_ineq1 be : Lemma exp_ineq1 (x : R) : x <> 0 -> 1 + x < exp x. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#13582 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ARDLQ5OWAU3W5K562WN3PZTSTOYI7ANCNFSM4UO76WNQ> .

[shinnar]

should I update the PR as suggested above? Note that I believe it would be a (minorly) breaking change (hence the original proposal).

[thery]

exp_ineq1 should not be much used, so generalize it to the whole line except zero should be ok.

[Zimmi48]

It turns out that there is one external project among the ones we test in CI that was using this lemma (https://gitlab.inria.fr/coquelicot/coquelicot/-/blob/master/theories/ElemFct.v#L604). Since his maintainer is also a maintainer of the real library, let's ping him here (@silene).

What are the paths to making a backward-compatible fix for this project possible? A #[ deprecated(since="8.14", note="Use exp_ineq1_pos instead.") ] Notation exp_ineq1 := exp_ineq1_pos.?

Note that in the current state of this PR (as opposed to the initial state), the type of changelog entry should be Changed instead of Added.

[thery]

Looks like @silene could use the new exp_ineq!.
To be backward compatible one possibility is to replace
by apply Rlt_le, exp_ineq1
with
apply Rlt_le, exp_ineq1; lra or
apply Rlt_le, exp_ineq1; auto with real if one doesn't want to import lra.

[thery]

Maybe we could get rid of the _neg and _pos theorems that are not so useful and directly prove ineq1

Lemma exp_ineq1 : forall x : R, x <> 0 -> 1 + x < exp x.
Proof.
assert (Hd : forall c : R,
           derivable_pt_lim (fun x : R => exp x - (x + 1)) c (exp c - 1)).
  intros.
  apply derivable_pt_lim_minus; [apply derivable_pt_lim_exp | ].
  replace (1) with (1 + 0) at 1 by lra.
  apply derivable_pt_lim_plus;
    [apply derivable_pt_lim_id | apply derivable_pt_lim_const].
intros x xdz; destruct (Rtotal_order x 0)  as [xlz|[xez|xgz]].
- destruct (MVT_cor2 _ _ x 0 xlz (fun c _ => Hd c)) as [c [HH1 HH2]].
  rewrite exp_0 in HH1.
  assert (H1 : 0 < x * exp c - x); [| lra].
  assert (H2 : x * exp 0  < x * exp c); [| rewrite exp_0 in H2; lra].
  apply Rmult_lt_gt_compat_neg_l; auto.
  now apply exp_increasing.
- now case xdz.
- destruct (MVT_cor2 _ _ 0 x xgz (fun c _ => Hd c)) as [c [HH1 HH2]].
  rewrite exp_0 in HH1.
  assert (H1 : 0 < x * exp c - x); [| lra].
  assert (H2 : x * exp 0  < x * exp c); [| rewrite exp_0 in H2; lra].
  apply Rmult_lt_compat_l; auto.
  now apply exp_increasing.
Qed.

[thery]

ok I've submitted the overlay for coquelicot #4. As soon as @silene accepts it I think we can merge
Ps: @shinnar I've modified the proof of exp_ineq1 in my comment I think it looks more symmetrical now

[shinnar]

@thery updated. Given that the current form of the proof is yours, should I include some form of attribution in the commit message? If so, what?

[Zimmi48]

One way is to put a "with help from" or "with review of Laurent Théry" in the changelog entry.

[thery]

@shinnar the proof is yours I have just reshaped it.

[shinnar]

@shinnar the proof is yours I have just reshaped it.

@thery Would you like to be included in the changelog? I amended it to read
"by Avi Shinnar and Barry Trager, with help from Laurent Théry", which seems appropriate.
If you would prefer to not be credited, I can revert the change.

[thery]

fine with me, thanks for your contribution!

[thery]

ok the overlay is in coquelicot #4, so we can merge

[thery]

@coqbot: merge now

[coqbot-app]

@thery: You can't merge the PR because you're not among the assignees.

[thery]

@coqbot: merge now

[olaure01]

The white line an final parenthesis seem to generate errors when adding new changelogs after this one (see for example CI errors in #13671 ).
If I am right and since this is already merged, what is the best way to make a modification? create an adhoc new PR?

[Zimmi48]

Yes, you are right about the diagnosis. You can either open an ad hoc PR or fix it in your own PR, especially if your own PR shouldn't take too long to merge.