[FOM] 618: Adventures in Formalization 4

[Dominic Mulligan]

After discussing with Freek Wiedijk offline and performing some digging of
my own, I feel the post I made earlier, quoted below, needs some
refinement, and Harvey has a point when it comes to how division is handled
in some proof assistants. Namely:

  * Agda handles division how I claimed, by giving the division function a
dependent type and requiring a proof that the denominator is non-zero. Note
the proof argument is implicit, meaning Agda will try to infer the
denominator is non-zero itself, only requiring an explicit proof if that
fails.
  * Coq has multiple axiomatisations and constructions of the reals, both
classical and constructive. The standard library implementation defines 1/0
to be an unknown but defined number. The CCorn library implements the
constructive reals and requires an explicit non-zero proof provided by the
user when calling the division function.
  * Mizar and HOL Light define 1/0 = 0 explicitly.

So, it seems like there's multiple different approaches in use, and whether
1/0=0 or not depends on the particular proof assistant, and even on the
particular library in use. Hope this clears things up.

Dominic
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150917/87ca9dc2/attachment.html>