Re:Division by zero in type theory: a FAQ
by e79 on Monday July 06, 2020 @01:36PM
(#23750389)
What would “halt and catch fire” look like for a proof assistant? If I’m trying to prove a theorem that performs division over the reals, would it then have to mechanically prove that there cannot exist any inputs that would result in division by zero? Isn’t that then itself a theorem that I’d have to explicitly define using tactics?
[ Parent
| on HN ]
Re:Division by zero in type theory: a FAQ
by thaumasiotes on Monday July 06, 2020 @04:37PM
(#23752479)
Well, if you're doing a proof and (for example) you want to cancel x in the numerator of a fraction with x in the denominator, you then apply the constraint x ≠ 0 to every subsequent step of the proof.
(You may then do a separate proof in the case that x = 0, if you want to prove something for all x including 0.)
That's actually needed for a real proof. One should keep in mind that y = ax is not injective if a=0, so that "cancel a variable" step you're thinking of is most likely incorrect without that side-condition.
Re:Division by zero in type theory: a FAQ
by thaumasiotes on Monday July 06, 2020 @05:24PM
(#23752937)
...yes?