The Coq mailing list

[Florian Steinberg <florian.steinberg AT inria.fr>]

Hi.

Here is another advantage of the choice to have the functions be defined 
on all of the reals and have lemmas that explicitly the values have 
certain properties: It means that you have very few different types 
involved that have potentially inconsistent naming systems for their 
lemmas, which can be a hassle. And, as you've probably already noticed, 
you can conveniently dismiss most of the additional goals that are 
generated by a use of lra.

Unfortunatelly, this approach also has some non-straight forward 
negative consequences. Here are some problems that I believe exist due 
to this choice of conventions and that gave me some headaches recently:

- The Mean Value Theorem in the standard library is currently formulated 
in such a way that it takes a function on the reals and an interval 
[a,b] and you have to prove that the function is differentiable in any 
point of the interior and that the end points a and b are points of 
continuity. The latter seems to assume that functions are constantly 
extended outside of [a,b]... If your function is not like that, you will 
have to first modify the function to be able to apply the mean value 
theorem even though the MVT in its usual formulation (i.e. using 
continuity on [a,b] instead of continuity on R for each element of [a, 
b]) could be applied to the restriction of the function to the interval 
right away. I needed the MVT for an application and ran into this 
problem. I modified (but also weakened) its statement for that, you can 
find it in a file called "mean_value_theorem" in the repository 
"youngsinequaltiy" on my github account if you are interested.

- The Function x |-> |x|^p can be defined via Rpower (Rabs x) p but this 
will give you a wrong value in zero. (I wanted to use this function to 
define lp spaces so the value in zero is very important for me). Rpower 
x y is defined through the exponential function which always returns 
strictly positive values, so it always takes strictly positive values. 
Note that this is even-though the function x |-> |x|^p can be 
continuously extended to 0 in zero 0 for any 0 < p.

And maybe one more thing... Another common workaround for partial 
functions apart from using total functions, dependent types or option 
types is to use relations with a proof of determinism. It is often a lot 
easier to describe the graph of a function and give a proof that it is 
never the case that two different return values are assigned to the same 
input, in particular if limits are involved in the definition of a 
function. If I am not mistaken, Coquelicot makes a considerable effort 
to prove that the axioms of the reals from the standard library are 
actually strong enough to allow you to translate from such a relation to 
a total function, so you can kind of switch back and forth between the 
concepts ... the convention is to name relation that corresponds to a 
function named f with is_f and the best example in my opinion is the 
limit function itself (Joseph already gave a pointer to that) or, if you 
prefer to have a function R -> R, the definition of the exponential 
function. The translation between relations and functions is called iota 
in Coquelicot and you there is a theorem iota_correct that allows you to 
conclude stuff about the function values under the assumption that you 
can prove that the value is contained in the domain of the relation 
(unfortunately the later often turns out problematic constructively as 
you have to prove an existential statement). This seems to be related to 
the concepts of multivalued-functions which are very popular in fields 
like computable analysis and function realizability. The main difference 
between relations and multivalued functions is how composition works, 
the one for multi-valued functions is more complicated than the 
composition of relations which already involves an existential statement 
... so this will not completely get you rid of the problems with 
compositionality that Theo mentioned either. Also functional analysis 
has some applications for multivalued-functions but I am not sure if 
that's related.

And finally... Can someone comment on how these problems are dealt with 
in mathcomp-analysis? I take that it assumes enough axioms, so you do 
not have to deal with the partial equivalence relations and in my 
experience math-comp does the consistent naming of lemmas very well, so 
maybe the combination of these makes the use of dependent types more 
accessible? But you'd still get the dependent type errors in rewriting, 
right? There is heavy use of dependent types in mathcomp (ordinals, 
subgroups, polynomials etc..), so maybe they provide a consistent way to 
deal with issues of this kind? I am not sure what the current state of 
the mathcomp-analysis project is, I think it is still in its beta phase 
or something... but if you want to do classical analysis it might be 
worth checking out. I mean... you are not using CoRN... you've lost hope 
for executability anyway, right? Oh, and there was a related question on 
the ssreflect mailing list recently, so that may be worth checking out.

Best,

Florian

On 01/02/2019 11:54, Théo Zimmermann wrote:
> Dear Michael,
>
> This design question is fundamentally the same (but in a more complex
> case) as the choice of defining 1/0=0 in the natural number domain.
> This is something that incidentally continues to confuse beginners not
> just in Coq but in other pure functional languages as well
> (https://discourse.elm-lang.org/t/integer-division-by-zero/2923). The
> alternatives are indeed dependently-typed functions (as highlighted by
> Joseph), but also functions returning values of type option. In both
> case, this breaks composability and is thus inconvenient.
>
> The three solutions (dependently-typed functions, functions which
> return an option and total functions) are all weird compared to the
> usual “undefined” behavior of math. So it seems to me that the ideal
> solution would be to actually emulate this “undefined” behavior by
> raising an exception. Pierre-Marie Pédrot has worked on adding
> exceptions to CIC without breaking consistency and has a plugin to do
> that (that I've never tried). I don't know how far we are from having
> exceptions in mainline Coq...
>
> Théo
>
> Le ven. 1 févr. 2019 à 10:38, Soegtrop, Michael
> <michael.soegtrop AT intel.com>
>  a écrit :
> > Dear Joseph,
> >
> >
> >
> > thanks for the detailed explanation of the design considerations!
> >
> >
> >
> > So in short the story is that all real functions with domain restrictions are 
> > extended to total functions over the complete R by returning some value which 
> > is convenient in most situations. E.g. for asin I could return –PI/2 or PI/2 
> > for out of domain arguments, so that I can prove that the function is 
> > everywhere continuous and that the result of asin is limited to –PI/2 to PI/2 
> > without requiring domain restrictions. And when it comes to proving that my 
> > definition of asin has a certain taylor expansion or derivative, I limit the 
> > argument range of asin to –1 … 1. Or alternatively I could return 1/0 for out 
> > of range asin, which possibly would allow me to prove that the derivative of 
> > asin x equals 1/sqrt(1-x^2) everywhere, but then I would need a domain 
> > restriction for the lemma which shows that asin x is bounded.
> >
> > This design leads to that one can prove:
> >
> >
> >
> > Require Import Reals.
> >
> > Require Import Psatz.
> >
> > Open Scope R_scope.
> >
> >
> >
> > Lemma sqrt_minus_one_is_zero: sqrt (-1) = 0.
> >
> > Proof.
> >
> >    unfold sqrt.
> >
> >    destruct (Rcase_abs (-1)) as [H|H].
> >
> >    - reflexivity.
> >
> >    - contradict H; lra.
> >
> > Qed.
> >
> >
> >
> > I am not sure if I like that one can prove sqrt(-1) = 0, even if this does 
> > not lead to a prove of that x=0 solves x²=-1. It is an interesting system – a 
> > bit weird, but I guess one gets used to it over time. As I said, in practice 
> > the reals as defined in Coq are very convenient to use and I understand that 
> > one has to pay some price for that (like sqrt(-1)=0).
> >
> >
> >
> > Best regards,
> >
> >
> >
> > Michael
> >
> >
> >
> > Intel Deutschland GmbH
> > Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> > Tel: +49 89 99 8853-0, www.intel.de
> > Managing Directors: Christin Eisenschmid
> > Chairperson of the Supervisory Board: Nicole Lau
> > Registered Office: Munich
> > Commercial Register: Amtsgericht Muenchen HRB 186928