Coq определяет мультипликативную обратную функцию 1/x как общую функцию R -> R, как в Rdefinitions.v, так и в Field_theory.v.Значение 1/0 остается неопределенным, все аксиомы вычислений игнорируют его.
Однако это проблема конструктивной математики, поскольку все суммарные функции R -> R должны быть непрерывными.И мы не можем соединить положительную и отрицательную бесконечность в ноль.Следовательно, конструктивная обратная функция - это, скорее, частичная функция:
Finv : forall x : R, (0 < x \/ x < 0) -> R
Вот, например, как она определена в библиотеке C-CoRN .
Теперь естьспособ использовать тактику field с этими частичными обратными функциями?Прямая Add Field не работает.