rewriting posnum #511

CohenCyril · 2022-01-09T18:13:04Z

Generalizing posnum and nonneg and linking the two
TODO:

add support for inequalities in extended reals (done in Non negative extended reals #375 )
discuss construction of orderType on signs (c.f., commented Section Order)
add a comment to signed_intro
fix two problems in the application of le_num
add a nonzero structure to detect that `|x| > 0 when x != 0

CohenCyril · 2022-01-09T18:14:06Z

proux01 · 2022-01-11T12:31:15Z

I had a quick look, this looks great.
I'd like to do a more careful review, but this will probably have to wait for a few more days.

theories/sequences.v

proux01

Sorry for the delay, here are some comments after a careful reading
of the code. I still need to

do the doc
do the extended reals

so more comments will come later.

Main comment: in abstract interpretation, we would say that the abstract domain (>=0, <=0) doesn't have the property of the best abstraction, which causes a bunch of issues (should 0 be considered >=0 or <=0 ? both abstractions are not comparable), the usual fix is to add a 0 in the lattice (as (meet <=0 >=0) so that 0 now has a best abstraction). I could offer a commit with that change if you want.

Comments on entire files

measure.v and normedtype.v: replace all %:nngnum by %:num?
nngnum.v and posnum.v: shouldn't we just remove these files?

theories/landau.v

theories/signed.v

proux01 · 2022-01-25T13:18:08Z

Previously, a posnum was also a nonneg thanks to that Canonical instance in posnum.v

Canonical posnum_nngnum x := Nonneg.NngNum x%:num (posnum_ge0 x).

it seems we have a regression here (c.f. comments above on one and inv).

CohenCyril · 2022-01-25T14:01:04Z

Thank you for your thorough review @proux01, this is much appreciated. I will try to address all your comments.
My main objective on this pass was to be able to cover everything posnum and nnegnum were covering before, some holes are voluntary in this first past others not.

Main comment: in abstract interpretation, we would say that the abstract domain (>=0, <=0) doesn't have the property of the best abstraction, which causes a bunch of issues (should 0 be considered >=0 or <=0 ? both abstractions are not comparable), the usual fix is to add a 0 in the lattice (as (meet <=0 >=0) so that 0 now has a best abstraction). I could offer a commit with that change if you want.

Yes, I noticed this very late and this additional would make sense.
However in practical cases, it is very easy to get around this tricky corner case, e.g. by using addr0 or mulr0 to remove 0 altogether from the guilty goal, and I guess that's why it was not a problem at all.
Naturally, I'm not opposed to adding this case of course!

Comments on entire files

nngnum.v and posnum.v: shouldn't we just remove these files?

Yes, I kept these two files as a stub in order to transition smoothly between the new and old code, especially to anticipate a compat with unmerged PRs. But they should disappear in the long run.

measure.v and normedtype.v: replace all %:nngnum by %:num?

I'm not completely sure, this will show up more precisely later in my answer to detailed comments, but the rough reason is that we may not want to rely on an arbitrary signed number, as we may want to guide the resolution a little bit.

theories/signed.v

proux01 · 2022-01-29T14:53:19Z

Yes, I noticed this very late and this additional would make sense. However in practical cases, it is very easy to get around this tricky corner case, e.g. by using addr0 or mulr0 to remove 0 altogether from the guilty goal, and I guess that's why it was not a problem at all.

I'm not worried about 0 + _ or 0 * _ but I'm less confident about things like min 0 _ or max 0 _.

Naturally, I'm not opposed to adding this case of course!

Here it is: https://github.com/proux01/analysis/commits/posnum_wip (this branch also adresses all my comments above we agreed upon)

proux01 · 2022-02-05T12:00:06Z

I added the doc I promised, so AFAICT, the remaining TODOs are:

should notations such as %:pos and %:nng be in ring_scope? (that would allow for similar notations in ereal_scope in ereal.v)
discuss construction of orderType on signs (c.f., commented Section Order)
add a comment to signed_intro
fix two problems in the application of le_num (don't know which ones)
add a nonzero structure to detect that `|x| > 0 when x != 0 (not sure to grasp the details)

Extended reals are handled separately in #375

proux01 · 2022-02-07T16:45:44Z

@CohenCyril I generalized (c.f. last commit) what was already done for nat to infer some sign information based on the type when no canonical instance matches the head symbol. In particular, I added a "top" catch-all that states that everything is in {compare x0 & ?=0 & >?<0 }. This enables things like abse x (in #375 ) or max 0 x to infer >=0 even when nothing is known about x.

The main drawback is that canonical structure inference no longer unfolds anything (since the catch-all triggers before).
Thus a few more unfolding are needed. This seems an acceptable trade-off to me, but you may not share my opinion (see last commit for example of impact).

Apart from the few points above (and adding still more canonical instances, but that's endless), I consider this and #375 ready.

CohenCyril · 2022-02-07T20:10:58Z

The main drawback is that canonical structure inference no longer unfolds anything (since the catch-all triggers before).
Thus a few more unfolding are needed. This seems an acceptable trade-off to me, but you may not share my opinion (see last commit for example of impact).

Yes indeed, I think that's a good trade-off.

theories/signed.v

proux01 · 2022-03-02T08:05:31Z

Thanks @affeldt-aist or the review. @CohenCyril do you agree if I rebase (and squash a bit/tidy the history) this in order to move towards merging?

It was requiring an exact abstract value, now any more-precise abstract value also works. For instance `unify AnySign NonNeg` was failing because NonNeg was too precise, whereas `unify_r AnySign NonNeg` now works. This is currently useless because one was only asking for most-precise abstract values, but should become useful in the future.

`expr%:nng` was failing when `expr%:pos` was working because the more precise type `{posnum _}` was infered instead of `{nonneg _}`.

Otherwise, we didn't know wether 0 should be abstracted as >=0 or <=0. The former made max(0, _) fail to be recognized as <=0 while the latter would break min(0, _) similarly.

Previously e%:sgn was failing when an unknown (or no, i.e., for which no canonical instance is registered) operation was encountered in the expression e, now some sign information can be inferred from the type of the unknown sub expression. This is generalizing the canonical instance already existing for the type nat. This is needed in #375 to be able to infer that `|x|%E is non negative when nothing is known on x.

Generalize min and max signed instances from numDomainType to porderType. This way, they can be used for extended reals.

This way, they can also be used for extended reals for instance.

proux01 · 2022-03-05T13:41:21Z

Since there was no opposition, I rebased (thanks @affeldt-aist for the initial rebase!).
A few points remain (c.f. initial PR description on top), but none of them is blocking.
I would argue in favor of merging (and adding issues to remember those points). @CohenCyril WDYT?

affeldt-aist

I committed a few simplifications that I observed when doing the rebase for PR #559 .

CohenCyril · 2022-03-05T16:07:06Z

"Pull request authors cannot approve their own pull request", still I'm in favor.

proux01 · 2022-03-05T17:14:05Z

Looks everyone agrees, let's merge then.

CohenCyril mentioned this pull request Jan 9, 2022

Non negative extended reals #375

Merged

5 tasks

CohenCyril commented Jan 11, 2022

View reviewed changes

theories/sequences.v Outdated Show resolved Hide resolved

proux01 reviewed Jan 25, 2022

View reviewed changes