Coq QArith деление на ноль равно нулю, почему?

Question

Я заметил, что в определении рациональных чисел Кока инверсия нуля определяется как ноль. (Обычно деление на ноль не является четко определенным / законным / разрешенным.)

Require Import QArith.
Lemma inv_zero_is_zero: (/ 0) == 0. 
Proof. unfold Qeq. reflexivity. Qed.

Почему это так?

Может ли это вызвать проблемы в расчетах с рациональными или это безопасно?

Answer 1

Короткий ответ: да, это абсолютно безопасно.

Когда мы говорим, что деление на ноль не является четко определенным, мы имеем в виду, что ноль не имеет мультипликативного обратного. В частности, у нас не может быть функции, которая вычисляет мультипликативный обратный для нуля. Тем не менее, можно написать функцию, которая вычисляет мультипликативный обратный для всех других элементов и возвращает некоторое произвольное значение, когда такого обратного не существует (например, для нуля). Это именно то, что делает эта функция.

Определение этого обратного оператора везде означает, что мы сможем определить другие функции, которые вычисляют его, без необходимости явно утверждать, что его аргумент отличается от нуля, что делает его более удобным для использования. В самом деле, представьте, какой будет боль, если мы заставим эту функцию вернуть option вместо этого мы терпим неудачу, когда передаем ноль: нам нужно сделать весь код монадическим, что усложнит понимание и осмысление. У нас была бы аналогичная проблема, если бы написать функцию, которая требует доказательства того, что ее аргумент не равен нулю.

Так в чем же подвох? Что ж, при попытке доказать что-либо о функции, которая использует обратный оператор, нам нужно будет добавить явные гипотезы, говорящие, что мы передаем ей аргумент, отличный от нуля, или утверждаем, что ее аргумент никогда не может быть нулевым. Леммы об этой функции получают дополнительные предварительные условия, например,

forall q, q <> 0 -> q * (/ q) = 1

Многие другие библиотеки имеют такую ​​структуру, ср. например, определение аксиом поля в библиотеке алгебры MathComp.

В некоторых случаях мы хотим включить дополнительные предварительные условия, требуемые некоторыми функциями, в качестве ограничений уровня типа. Это то, что мы делаем, например, когда мы используем индексированные по длине векторы и безопасный get функция, которая может быть вызвана только для чисел, находящихся в границах. Итак, как мы решаем, какой из них использовать при проектировании библиотеки, то есть использовать ли расширенный тип с большим количеством дополнительной информации и предотвращать ложные вызовы определенных функций (как в случае с индексированием длины) или оставить эту информацию вне и требовать его в качестве явных лемм (как в мультипликативном обратном случае)? Ну, здесь нет однозначного ответа, и действительно нужно проанализировать каждый случай в отдельности и решить, какая альтернатива будет лучше для этого конкретного случая.