ereal inverse + simplification mule and mule_def #1494
Conversation
|
I will not have time to push this PR forward, so @hoheinzollern please feel free to take ownership |
CohenCyril
changed the title
|
Refreshed for use in #1624 |
- this commit adds an implementation of the inverse for extended reals, `inve` a total involutive inversion function on `\bar R`, denoted `^-1` in the `ereal_scope` coinciding with `x^-1%R` when `x != 0` but such that `0^-1 = +oo` and `-oo^-1 = -oo`, - notation `x / y` in `ereal_scope` for `x / y = x * y^-1`/, - lemmas `inver`, `inveP`, `fine_invr`, `inve0`, `inve1`, `invey`, `invey`, `inveNy`, `inveK`, `invr_inj`, `inveN`, `inve_eq0`, `inve_ge0`, `inve_gt0`, - a predicate `inveM_def` with notation `x *^-1? y` defining a sufficient condition for the inverse and product to commute, - it changes `mule` to have special cases optimizing computation for +oo and -oo adn `mule_def` has been rewritten to optimize computation in several cases. - it adds a compatibility lemma `mule_defE` to bridge the former definition of `mule_def` with the new one.
I haven't had a look, but that sounds like there should be a dual version? What is the rationale for the choice? For addition, the rationale was making (max, adde) (resp. (min, dual_adde)) semirings. |
proux01
left a comment
proux01
left a comment
There was a problem hiding this comment.
Don't we want inve_le0 and inve_lt0 while at it?
I thought you agreed that there is no use for a dual version (#1494 (comment)) but maybe I miunderstood? The rationale is to make sure that the inverse is involutive. Moreover |
|
Yes, sorry, let's go without dual version for now (at least until we better understand why we would need it) |
Co-authored-by: Pierre Roux <[email protected]>
|
Additionally I fixed |
|
The last commit is an application of |
|
Looks good, CI seems happy, should I (squash) merge? |
- this commit adds an implementation of the inverse for extended reals, `inve` a total involutive inversion function on `\bar R`, denoted `^-1` in the `ereal_scope` coinciding with `x^-1%R` when `x != 0` but such that `0^-1 = +oo` and `-oo^-1 = -oo`, - notation `x / y` in `ereal_scope` for `x / y = x * y^-1`/, - lemmas `inver`, `inveP`, `fine_invr`, `inve0`, `inve1`, `invey`, `invey`, `inveNy`, `inveK`, `invr_inj`, `inveN`, `inve_eq0`, `inve_ge0`, `inve_gt0`, - a predicate `inveM_def` with notation `x *^-1? y` defining a sufficient condition for the inverse and product to commute, - it changes `mule` to have special cases optimizing computation for +oo and -oo adn `mule_def` has been rewritten to optimize computation in several cases. - it adds a compatibility lemma `mule_defE` to bridge the former definition of `mule_def` with the new one. Co-authored-by: Reynald Affeldt <[email protected]> Co-authored-by: Pierre Roux <[email protected]>
- this commit adds an implementation of the inverse for extended reals, `inve` a total involutive inversion function on `\bar R`, denoted `^-1` in the `ereal_scope` coinciding with `x^-1%R` when `x != 0` but such that `0^-1 = +oo` and `-oo^-1 = -oo`, - notation `x / y` in `ereal_scope` for `x / y = x * y^-1`/, - lemmas `inver`, `inveP`, `fine_invr`, `inve0`, `inve1`, `invey`, `invey`, `inveNy`, `inveK`, `invr_inj`, `inveN`, `inve_eq0`, `inve_ge0`, `inve_gt0`, - a predicate `inveM_def` with notation `x *^-1? y` defining a sufficient condition for the inverse and product to commute, - it changes `mule` to have special cases optimizing computation for +oo and -oo adn `mule_def` has been rewritten to optimize computation in several cases. - it adds a compatibility lemma `mule_defE` to bridge the former definition of `mule_def` with the new one. Co-authored-by: Reynald Affeldt <[email protected]> Co-authored-by: Pierre Roux <[email protected]>
4 participants
Motivation for this change
@hoheinzollern
Things done/to do
CHANGELOG_UNRELEASED.mdAutomatic note to reviewers
Read this Checklist and put a milestone if possible.