natural logarithm for extended real numbers #1649
Conversation
|
Note that the last commit changes the definition of Lemma lne_div : {in `]0, +oo] &, {morph lne : x y / x / y >-> x - y}}.instead of Lemma lne_div x y :
0 < x -> 0 < y -> lne (x * (fine y)^-1%:E) = lne x - lne y.(fyi: @CohenCyril) @jmmarulang It looks a bit better but is it as useful to you? |
affeldt-aist
changed the title
affeldt-aist
force-pushed
the
jairo_lne
branch
2 times, most recently
from
05f39b0 to
bc4f303
Compare
affeldt-aist
force-pushed
the
jairo_lne
branch
2 times, most recently
from
ceceff0 to
c30e735
Compare
|
This PR has been discussed, already been approved, CI errors seem unrelated, and comments have been addressed. @jmmarulang and @hoheinzollern , you may want to take a last look before squash-merge. @proux01 there is a minor fix in |
proux01
left a comment
proux01
left a comment
There was a problem hiding this comment.
Indeed I have a comment
| by apply: contraTT => /norP[]; apply: mule_neq0. | ||
| by apply: contraTT => /norP[]; exact: mule_neq0. |
There was a problem hiding this comment.
not really, I tend to use exact instead of apply to conclude because we gain the coloring.
There was a problem hiding this comment.
I generally agree, but here it is redundant with the by at the beginning of the line, so the color is more distracting than anything.
reals/constructive_ereal.v
Outdated
| Notation "0" := (@GRing.zero (\bar _)) : ereal_scope. | ||
| Notation "1" := (1%R%:E : dual_extended _) : ereal_dual_scope. | ||
| Notation "1" := (1%R%:E) : ereal_scope. | ||
| Notation "- 1" := ((-1)%R%:E) : ereal_scope. |
There was a problem hiding this comment.
I'm really not sure we want that: this introduces a special case for - 1 that becomes (- 1)%:E whereas - 2 remains - 2%:E. So - <n> is - <n>%:E, except when <n> is 1 where it is (- <n>)%:E. That can be a surprising exception.
There was a problem hiding this comment.
Indeed. On the other hand, - 1 is also a notation in ssralg.v, this PR provides an example that looks more natural with this notation, and it also helped us spotting an error in the definition of mulN1e, so it is not entirely negative imo. This is true that this is an exceptional case but given the many N1 lemmas, it seems to me that we already treat it as a special case. I am not sure what to do but I lean a bit towards the special notation. :-/
There was a problem hiding this comment.
I didn't even think about the notation priority thing, that makes it even worse :( if - 1 * n and - 2 * n are not parsed the same way.
And yes -1 is a notation in ssralg.v but so is - <n>, the - 1 is only to have - GRing.one.
There was a problem hiding this comment.
Notation reverted, but they led to reintroduce 1%E's. :-/ (even though the notation is defined by Notation "- x" := (oppe x%E) : ereal_scope.)
There was a problem hiding this comment.
Strange, that might be a bug in Rocq? We should probably minimize it.
There was a problem hiding this comment.
Trying to minimize:
From mathcomp Require Import all_ssreflect all_algebra.
Declare Scope ereal_scope.
Local Open Scope ring_scope.
Variant extended {R : Type} := EFin of R.
Notation "r %:E" := (@EFin _ r%R) (format "r %:E").
Notation "1" := (1%R%:E) : ereal_scope.
Axiom oppe : forall {R : zmodType}, @extended R -> @extended R.
Delimit Scope ereal_scope with E.
Notation "- x" := (oppe x%E) : ereal_scope.
Local Open Scope ereal_scope.
Axiom R : numDomainType.
Fail Check - 1 : @extended R.
(* The command has indeed failed with message:
The term "-1" has type
"GRing.Zmodule.sort
(join_GRing_Ring_between_GRing_SemiRing_and_GRing_Zmodule ?t)"
while it is expected to have type "extended".
*)
Check - 1%E : @extended R.There was a problem hiding this comment.
Trying to minimize:
Thanks, nice first step
From mathcomp Require Import all_ssreflect all_algebra.
We now need to get rid of that to report it as a Rocq bug.
But I'm now wondering whether it's really a bug.
In fact it's probably not. And our solution would be to add a small Number Notation in ereal scope. Will try that in a separate PR.
I agree but let me rebase it to be extra safe. |
|
@affeldt-aist CI green, I let you squash / merge at your convenience |
Thanks! (I wait a bit for input by the other participants to the conversation.) |
|
So, apparently I was right to want to get green CI but this wasn't enough. This PR ended up in a strange situation where this doesn't compile on MC master with Rocq <= 9.1, a combination we didn't test since we only test MC master on Rocq master. |
* add lne * ln -oo = -oo * fix mulN1e --------- Co-authored-by: jmmarulang <[email protected]>
5 participants
Motivation for this change
closes draft PR #1613
@jmmarulang : I have duplicated your PR to avoid pushing on your master
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers