Locria Cyber (Aug 16 2022 at 11:14): Locria Cyber (Aug 16 2022 at 11:14):I found the definition of axiomatic real numbers here.
Locria Cyber (Aug 16 2022 at 11:14):Is RInv R0 a point in R?
Locria Cyber (Aug 16 2022 at 11:19):What will happen if you define 0 * / 0 = 1?
Paolo Giarrusso (Aug 16 2022 at 11:53):https://coq.inria.fr/distrib/8.4pl5/stdlib/Coq.Reals.Raxioms.html# ensures that Rinv r is the inverse of r:
Axiom Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
beware that's the stdlib of Coq 8.4, you probably want https://coq.inria.fr/stdlib/ instead
Guillaume Melquiond (Aug 16 2022 at 12:02):Locria Cyber said:
What will happen if you define
0 * / 0 = 1?
If you set this equality as axiom, then you can trivially deduce False, since you also have the equality 0 * foo = 0 by virtue of zero being absorbing for the multiplication.
Last updated: Oct 05 2023 at 02:01 UTC