Stream: Coq users

Topic: What is `RInv R0`


view this post on Zulip Locria Cyber (Aug 16 2022 at 11:14):

I found the definition of axiomatic real numbers here.

view this post on Zulip Locria Cyber (Aug 16 2022 at 11:14):

Is RInv R0 a point in R?

view this post on Zulip Locria Cyber (Aug 16 2022 at 11:19):

What will happen if you define 0 * / 0 = 1?

view this post on Zulip 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

view this post on Zulip 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: Feb 01 2023 at 11:04 UTC