Non negative extended reals #375
Conversation
|
I have a version, in one of my workdirs that is supposed to cover everything (non negative, negative, positive, non positive, extended or not, symmetric on multiplication). I just did not have time to finish it :'( |
cf #511 |
|
Thanks, I'll rebase on top of it. |
Do you understand how to do it with minimal duplication? |
|
I hope so. I'll ask if I run into trouble (but if I understand correctly, that should mostly be a few canonical instances and a spec inductive with two cases (+oo or non negative real)). |
I expect that most (if not all) |
I do not understand this bit... |
Something similar to nonneg_spec in #511 |
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. lignes
* Make unify more generic
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.
* Make 1%:nng work
`expr%:nng` was failing when `expr%:pos` was working because the more
precise type `{posnum _}` was infered instead of `{nonneg _}`.
* Add =0 to the abstract domain
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.
* No need to declare reality_cond a local coercion
* Add Arguments for the sake of uniformity
* Generalize min and max
Generalize min and max signed instances from numDomainType to
porderType. This way, they can be used for extended reals.
* Generalize morphism lemmas
This way, they can also be used for extended reals for instance.
* No need for P to be a canonical projection
* Add sign inference on type as a last resort
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.
Co-authored-by: Pierre Roux <pierre@roux01.fr>
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.
|
Rebased and ready for review (this is mostly a bunch of canonical instances). |
I have this file in another development, don't know whether it may be worth having it in analysis?This is now rebased on top of #511
TODO:
ereal_supandereal_inf