Menu
▾
▴
#399 Loosen WD condition on exponent
The WD for e^n is currently 0≤e ∧ 0≤n.
While it can make sense to reject negative powers (they can be written as 1/e^(-n) instead and it avoids having a more complex exponent definition) there is no reason to reject negative bases: the definition of e^n is the same whether e is positive or negative.
Therefore, we could limit the WD of e^n to 0≤n.
Before making any change, we should check that it would be compatible with external provers: Atelier B (
ppandml) and SMT solvers. It might not be worth the change if that makes the translation to these provers much more cumbersome.The proposed change is indeed compatible with Atelier B provers.
However, if we change the WD condition, then we may introduce regressions in proofs. Currently, the WD condition ensures that
e^nis non-negative. If we allow for negative bases, this will no longer be true (need to check that either base is non-negative or exponent is even).Therefore introducing such a change should be studied with care.