Search code examples
coqcoq-tactic

Field tactic with partial inverse function

Coq defines the multiplicative inverse function 1/x as a total function R -> R, both in Rdefinitions.v and in Field_theory.v. The value 1/0 is left undefined, all calculation axioms ignore it.

However this is a problem in constructive mathematics, because all total functions R -> R must be continuous. And we cannot connect the positive and negative infinities at zero. Therefore the constructive inverse is rather a partial function :

Finv : forall x : R, (0 < x \/ x < 0) -> R

This is for example how it is defined in the C-CoRN library.

Now is there a way to use the field tactic with those partial inverse functions ? A direct Add Field does not work.

Solution

  • The answer is no. The Add Field command relies on a function of type R -> R that represents the inverse and such a function cannot be defined constructively.