Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Equational reasoning with "undefined" expressions


view this post on Zulip Email Gateway (Jul 11 2022 at 12:47):

From: Dominique Unruh <unruh@ut.ee>
Hello,

The calculational reasoning feature of Isabelle/Isar (commands "also"
and "finally") is very useful for many complex calculations but I
repeatedly found one area where it is hard to use.

Namely, when working with potentially undefined expressions (e.g.,
limits, series, integrals, suprema, division by zero, etc.).

(Side note: I am aware that Isabelle/HOL is total. I do not wish to
resurrect the discussion whether things such as division by zero should
have a fixed default value or not. When I say "undefined", I mean it in
the sense of "the limit doesn't exist" etc. in common mathematical
parlance, irrespective of how the HOL-constant is precisely defined.
Also, my meaning of "undefined" has nothing to do with the existing
HOL-constant "undefined".)

For example, in a mathematical proof involving series, I may have a
calculation saying \ \sum_{ }^{ }f_i\le\sum_{ }^{ }g_i\le\sum_{ }^{
}h_i=z, with a comment explaining something like "here the left series
exist because the right one exists". Or somewhat more formally, we
consider each of the series as an expression that can be a number, or
"undefined", and we interpret x\le y as meaning "if /y/ is defined, then
/x/ is defined and x\le y".

When translating such proofs to Isabelle/HOL, I very often end up having
to do the calculation twice. I do one part of the proof that has a
sequence of steps of the form "summable h_i \implies summable g_i". And
then once these are established, I do the steps "\sum_{ }^{
}g_i\le\sum_{ }^{ }h_i" etc. This increases duplication and reduces
readability a lot. Especially when I have nested series (where the
summands of a series might also be series that are potentially
undefined), things get hard to read).

Instead of this, one could recreate what is implicitly done in the
mathematical proof as follows:

* One rewrites the expressions \sum_{ }^{ }g_i (of type real) into
expressions of type "real option", returning None if the series does
not exist (or any of the summands does not exist).
(Essentially, treating the computation as something that happens in
the maybe-monad.)

* One defines a relation \le' on "real option" that has the meaning
"smaller-equal, and left is defined if right is" as described above.

There are two problems with that. First, one needs to define a lot of
new relations (e.g., "smaller, left if right", "smaller-equal, right if
left", "..., right if and only if left", etc.) I think this would not be
a big one problem (e.g., one could have second order constants such as
"left_if_right" mapping \le into \le' and define some appropriate
syntactic sugar for readability).

The second problem is more substantial: Rewriting an expression of type
"real" (or any other type involved in calculational reasoning) into
"real option" is difficult. (Not conceptually difficult but difficult to
do correctly.) \sum_{ }^{ }g_i would be replaced by "if summable g_i
then Some \sum_{ }^{ }g_i else None". (This can be made more readable
with a new constant "series_lifted", of course.) And even worse,
something like \sum_i^{ }\left(g_i+\sum_j^{ }h_{ij}\right) becomes a
very unreadable term since it is None if any of the inner series diverge
or if the outer one diverges.

I would like to resolve these difficulties, and my idea is the following:

* Write an ML function "lift: term -> term" that transforms normal
expressions (e.g., of type real) to "lifted" expression (of type
"real option").
This function would of course need some configuration, e.g., to know
that "series :: (nat real -> real)" is something that can return
something "undefined" and under what conditions this happens.
This is the hard part and needs careful thinking about the details,
I think.

* Add some syntactic sugar and parse/print translations so that this
function would be applied when parsing terms.
(E.g., "\sum_{ }^{ }g_i\ \left[\le\right]_{\leftarrow}\ \sum_{ }^{
}h_i" might be replaced by something like "series_lifted g_i \le'
series_lifted h'" on parsing and translated back on printing, where
"series_lifted" is what the ML-function lift returns.)

* Add a bunch of additional lemmas to ease working with these things.
(E.g., trans-rules for constants such as \le'. And wrapper-lemmas
expressing existing results in terms of "series_lifted" etc., e.g.)

Before I set out on this endeavor, I would like to hear from others
whether there are other, better approaches to deal with calculational
reasoning in these situations. Or whether there are existing
implementations of this or a similar idea (in Isabelle, or in other
provers).

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Jul 12 2022 at 08:51):

From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Dear Dominique,

just an observation: what you propose reminds me of what I suggested
years ago for Matita/Coq

Claudio Sacerdoti Coen and Enrico Zoli. “A Note on Formalising
Undefined Terms in Real Analysis”. In: PATE’07 (2007), p. 3. url:
https://www.cs.unibo.it/˜sacerdot/PAPERS/pate07.pdf.

Indeed one needs multiple relations, but the interesting part is that
one observes in practice in real-world proofs very long zig-zags of the
form <<<<< >>>>>> <<<<<< >>>> etc. where > means "if lhs is defined,
rhs is" and < the opposite. This allows to provide explicit proofs of
definedness only at the peaks of the zig-zags, like mathematicians do
informally.

At the time there were not many easy ways to automate what we proposed
in Coq/Matita, but I think that nowadays it should be much simpler to
do, letting the system infer automatically what decorations to use for
relations and for the lemmas.

Since you are reviving my interest into that, please let me know if you
plan to actually work on that for Isar.

Cheers,
C.S.C.


Last updated: Jul 15 2022 at 23:21 UTC