Полевая тактика с частичной обратной функцией - PullRequest
1 голос
/ 21 марта 2019

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 не работает.

1 Ответ

2 голосов
/ 22 марта 2019

Ответ - нет.Команда Add Field основана на функции типа R -> R, которая представляет обратное, и такую ​​функцию нельзя определить конструктивно.

...