3 ms·
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
by e79 6y ago
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?
- thaumasiotes 6y agoWell, 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.)
- zozbot234 6y agoThat'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.
- thaumasiotes 6y ago...yes?