A small problem about Reals for teaching. In Reals, the inverse of 0 is 0. This is ultra-nice because this convention keeps the inverse involutive and odd. This removes many assumptions in theorems. There has been a nice simplification work in 8.16, deprecating some theorems and introducing new ones without non-zero conditions.

This is however a small issue for a mathematical course. I don't feel like teaching that the inverse of 0 is 0 to first year undergrads. Also if I want to prove for instance that `forall x, / (/ x) = x`

I don't want the students to spend time on the case `x = 0`

.

I could write down my own file to Require during the classes but then there would be other technical problems. (But maybe in the end, this is the true problem that needs to be solved...)

I don't think you need to tell the students that `/ 0`

is `0`

. Any proof that works in a setting where `/ 0`

is left unspecified still works the same when `/ 0`

is set to a specific value.

The only difference is that a theorem such as `exists x, /x = 0`

becomes provable. But I do not think that your lecture is about provability and/or satisfiability, so it does not really matter.

The kind of problem I could encounter is:

- in a first file about Reals as a field

```
(** exercise: prove this. *)
Lemma Rinv_inv : forall x, x <> 0 -> / (/ x) = x.
...
```

- then in another file (say, about inequalities),

```
Require Import RIneq.
Lemma foo: bar.
Search (/ (/ _)). (** professor! why has the condition disappeared?! *)
```

but there's still a chance they won't notice.

In that case, I would presumably tell them the following: "the Coq developers arbitrarily decided to define `/0`

as `0`

, so the equality `/ (/ x) = x`

happens to also hold for `x = 0`

, which makes the side condition superfluous".

Yes, it's probably the best decision. Thanks.

FWIW, you could blacklist lemmas from Search in your wrapper library.

But I wonder how many would benefit from formalizing Rinv_partial : R -> option R, relating that to the inverse (they coincide outside of 0) and stating some lemmas about it (to see the clutter that motivates using a total function instead).

(Clever?) students might still wonder about the mismatch, or realize that they can't trust a formalized Coq theorem about the completed inverse to apply about the partial inverse. Even if no inverse operation is _directly visible_ in the statement. I don't know of a good solution, other than ignoring on-paper maths or just stating the strange convention in papers on the results.

OTOH, I _think_ that on-paper theorems are always provable in Coq, but I wonder if contravariance throws a spanner, ...

(I also wonder about `x <> 0 -> x/y*y^2 <> 0`

: if you inferred quantifier `∀ y ∈ R <> 0`

instead of `∀ y ∈ R`

, that'd become provable on paper but not in Coq. But while such "domain inference" applies to partial functions, I'm not sure if anybody extends it to unstated quantifiers...)

There's a blog post about this (in Lean) here, and a comment by @Neel Krishnaswami at here that having `0 - n = 0`

is "correct" in a mathematical sense backed up by category theory. Is there similar category theory to back up how division should be defined on 0?

I do not know if you consider universal algebras to be a notion of category theory, but if so, then yes, universal algebras give rise to "meadows" (which have the property `0 = /0`

) when applied to fields.

Paolo Giarrusso said:

(I also wonder about

`x <> 0 -> x/y*y^2 <> 0`

: if you inferred quantifier`∀ y ∈ R <> 0`

instead of`∀ y ∈ R`

, that'd become provable on paper but not in Coq. But while such "domain inference" applies to partial functions, I'm not sure if anybody extends it to unstated quantifiers...)

To be honest I'm not sure there would be a consensus among math teachers to write the condition `∀ y ∈ R <> 0`

or not. Some would say that it's (a bit magically) implied by the fact that the quotient is _written_, some would not. I'm not sure partial functions have a clear semantics in everyday maths.

Last updated: Oct 13 2024 at 01:02 UTC