Email Gateway (Aug 18 2022 at 13:39): Email Gateway (Aug 18 2022 at 13:39):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear members of Isabelle users,
My name is Bogdan Grechuk, I am mathematician interested in formalization of mathematics. My main mathematical dream is that automated theorem provers will become much more convenient and attractive for mathematicians, and as a result basically all mathematics will be formalized. I have read much about the area, but had no direct experience of working with automated theorem provers before. From June 9 to July 3, I am invited for an academic visit by the Mathematical Reasoning Group at University of Edinburgh. The purpose of this visit was to do some simple formalization in Isabelle to understand the state of the area.
First I thought I would formalize something from my research area. However, the library turned out not reach far enough for this purpose. In particular, I did not find the notion of convex function there. As a result, I decided to introduce this notion and prove the main properties of convex functions. I hope these results will be added to Isabelle library. I am attaching the “thy” file I have developped. Could you please confirm that these results are indeed new to Isabelle and tell me whether they can be added to the library? If so, please tell me what should I do in the remaining week of my visit to improve the formalisation? May be I need to rename some things, or add more comments, or try to develop shorter proofs, or would it be better to formalize some more results about convex functions? I would appreciate any comments or suggestions.
Below I also add some further remarks which may be interesting for the developers of Isabelle. First is the description of my file, containing some explanation of what exactly I formalized and why. Second is the description of my first experience of working with Isabelle, which includes some comments and suggestions about what I would like to see in the system.
Sincerely,
Bogdan Grechuk.
*** Description of Convexity.thy ***
My aim was to introduce the notion of convex function real -> real. To do this, I needed some basic theory. First, I did not want to introduce separate definitions for convex functions on (-infty, infty), (a, infty), (a,b) etc., therefore I introduced the notion of real interval, which generalizes all the types of intervals mentioned above. By definition, real interval is just any convex subset of real line. I have started my theory file with some lemmas about real intervals, which I need later. In particular, I have proved here that (-infty, infty), (a, infty), (-infty, b), and (a,b) are real intervals.
Then I introduced the notion of non-decreasing function on real intervals, and proved that differentiable function is non-decreasing if and only if its derivative is non-negative.
After this preparation, I introduced the notion of convex function on a real interval. First, I proved some simple properties of convex functions, namely, that linear functions are convex, that sum of convex functions are convex, that f(g(x)) is convex if f() convex and g() linear, or if f() convex increasing and g() convex, and that the global maximum of convex function on [a, b] is f(a) or f(b).
Then I proved some properties of convex functions connected with derivatives.
First, I proved that graph of convex function is above all the tangents, and used this fact to prove that if the first derivative of convex function at some point is 0, that this point is a global minimum. Then I proved that (twice) differentiable function is convex on an interval if and only if its first derivative is non-decreasing on this interval, and also if and only if its second derivative is non-negative.
Clearly, these theorems provide a powerful tool of proving convexity of different functions. As an example, I used them to prove that -ln(x) is a convex function on (0, infty).
Finally, I use the summation over finite set theorems to prove that for convex function f we have alpha_1 f(x_1)+...+aplha_n f(x_n) >= f(alpha_1 x_1 +...aplha_n x_n), if aplha_i>=0 with sum 1, and use this to prove the famous Geometric-Arithmetic Mean Inequality.
*** Working with Isabelle ***
In this part I would like to describe the impression about my first experience of working with Isabelle, what I liked and used most, and what improvements I would like to see most. I hope this feedback may be useful to you.
My first impression is that the proofs are too detailed, and the simplifier is not powerful enough. For example, it took me 4 lines and about 15 minutes to prove obvious identity a(cx + (1-c)y)+b=c(ax+b)+(1-c)(a*y+b) --- I read that, in some other systems, identities like this can be done in one line. May be, I just did not find the correct way? What I used is “simp” or “auto”, and they are not able to solve this directly. When I tried to prove something interesting, it was unpleasant to spend time on simplification like this. And I am sure that improvement simp up to (at least) such a level should be possible.
On the positive side, I really like that when I formulate simple lemma, the system tell me that “The current goal could be solved directly with:” and then gives suggestions. Very often I used this instead of search for the correct lemma. Sometimes its hard to find lemmas in the library: to use search by name I need to guess part of name, to use search by expression I need to study syntax... It is much easier just type the lemma you want, and look at the suggestions. This should prevent users from reproving known theorems.
Unfortunately, this works only when I formulate lemmas. In particular, when I write
lemma “(a :: real)(b+c)=ab+a*c”
--- I have many suggestions. However, when I type
proof-
have “(a :: real)(b+c)=ab+a*c”
--- I have no suggestions.
As a result, sometimes, when I need to prove some fact and I type it after “have”, and finally prove it in many lines, I later discover that it could be proved directly with an existing lemmas... I think, if you develop a mechanism how to suggest relevant lemmas when I type “lemma”, it should be easy to extend this to the case of a subgoal in the proof, such as those formulated after have.
If something can be proved directly by auto or something without any lemmas, it would be nice if system also tells me this.
Also, unfortunately, this the suggestions mechanism does not work if I slightly reformulate the lemma.
For example, I had a huge problem when I tried to prove that two functions f and g are the same functions. I proved that for every argument y we have f(y)=g(y), and then wanted to conclude that f=g by auto, but it did not work. So, I needed absolutely trivial (for me) lemma “(!y. f(y)=g(y)) --> f=g” but I had no idea how to prove it. When I formulated this lemma, the system gave me no suggestions. I had no idea where to find something relevant in the library. Finally, I asked for help, and was shown the axiom “ext” in Theory HOL, which was exactly what I need, and my lemma was proved in one line “by (auto intro: ext)”. However, from the beginning, no hint to use “ext” was given.
I think this the suggestions mechanism is a BRILLIANT idea. If you develop it up to the level where the system will recognize reformulations and direct corollaries, all the process of proof will be extremely comfortable for mathematicians – just divide the problem you want into prove by simpler subgoals, and follow the suggestions how to prove each of them! I think this suggestions system would then replace “theorem search”. When the library becomes larger, this becomes more and more important. Ideally, a mathematician may have no idea that fact (or subfact) he wanted to prove is already known! I hope, in the future, mathematicians will use formal theorem provers in order to avoid reproving of already known results. All this is closely related with the famous problem of search of mathematical results, in the internet, to get something relevant.
But to achieve this, the system should recognize that what I type is just a reformulation of a known lemma. Also, the next step would be if system could recognize facts which follow from two lemmas. This already would be extremely beautiful and useful, and would really help in actually proving theorems, not only in formalization of known results.
I have also some minor comments and suggestions, but probably would prefer to leave them for future communication.
Email Gateway (Aug 18 2022 at 13:39):From: Makarius <makarius@sketis.net>
I've played a bit with your theory, looking mainly at the first definition
and lemma. The outcome is in the attachment.
Here are some general notes on producing structured Isabelle/Isar theories
and proofs.
* For most basic human readability of the sources, lines should not be
too long (80-100 chars). Some spaces should be inserted between
mathematical operators (like Knuth would do for you in TeX).
* The hierachical structure can be emphasized by indentation. Proof
General will do most of the work for you, if you press TAB frequently.
* Use explicit naming for local facts sparsely, only as required. It is
best to come up with meaningful names in the first place, but there
are many ways to avoid names and (often confusing) name references.
In particular:
. Isar proof elements 'with', 'then', 'moreover', 'ultimately' etc.
allow to refer to "recent" facts without explicit pointers.
. Facts can be referenced literally, e.g. a < b (ASCII backquotes)
. Meaningless names can be as simple as 1, 2, 3, or more
mathematical , , -- the latter also has the advantage that
with more than four *'s you will notice that names need to be
cleaned up.
. There is no need to prefix letters to meaningless names. Note
that the way facts were introduced (assume/have/obtain/show) does
not really matter for the proof, and it changes as the proof is
maintained (thus some a1 would have to be renamed to h7 and other
labels shifted).
* Use direct Isar context elements, instead of simulating them via
logical connectives. Isar proofs are like a block structured
mathematical notepad, you can work like this:
{
assume "a < b"
then have A ...
from a < b have B ...
}
No need to encode it as "a < b --> A" and "a < b --> B".
In the proof of cont_interval I've achieved this by using rule
linorder_cases for the overall outline. (Admittedly it is hard to
figure out which rule is required. At some point Isar will support
direct case splitting written in the text, without having to guess
suitable inference rules.)
* Unfolding primitive definitions in the middle of a proof can be
avoided if standard introduction and elimination rules are proved once
and for all. BTW, rule_format is essentially a legacy feature from
the times before structured Isar proofs, even before the times
where Isabelle could handle structured rule statements (with pure !!
and ==>) uniformly.
* Note that "obtain alpha = ..." is just a local definition. No proof
required here.
Makarius
Convexity.thy
Email Gateway (Aug 18 2022 at 13:39):From: Johannes Hölzl <johannes.hoelzl@gmx.de>
Hi,
I looked through some of your proofs, and have some suggestions:
Instead of introducing real_interval and using it for proofs as
"real_interval S", you could also use the interval notation "{a .. b}".
And write "x : {a..b}" instead of "real_interval S" "x : S". There is a
lot of support in the simplifier, and hopefully the proofs get easier
when using them.
<< def x == "..." >> instead of
<< obtain x where "x = ..." by auto >>
the theorem is then called x_def.
You can also introduce patterns using
<< let ?x = "..." >>
They are just used by parsing, and not seen by the theorem prover
core.
you can use ´finite I´ instead of a1 (i.e. write the proposition of
the theorem in ´...´)
use useful names for theorems instead of a1, h12, ...
(proof writing is programming!)
do you know about "moreover" and "ultimately" to collect theorems?
you often write << apply (rule R) apply auto done >>
this can often be done by << by (auto intro: R) >>
sometimes we need to instantiate: R[of ...]
prefer meta-level syntax (i.e. "!! x. ...", "P ==> Q"), over HOL
level syntax ("! x. ...", "P --> Q"). Meta-level synatx is easier to
work with, e.g. when using thm[of ...] or thm[OF ...] and sometimes the
proof methods seem to work better with them.
incr_funct_deriv2: you can do contraction proofs using
<<
lemma P
proof (rule ccontr)
assume "~ P"
...
show False
qed
>
do you know about "then", "hence" and "thus"?
instead of "from this" -> "then"
instead of "from this have" -> "then have" -> "hence"
instead of "from this show" -> "thus"
this are just abreviations, use them as you like
Probably you know it already:
The Isabelle tutorial:
http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf
I made the experience that it can be very helpful to read it a second
time after doing proving in Isabelle/Isar.
I hope this tips were helpful to you.
Best regards,
Johannes
Last updated: May 03 2024 at 12:27 UTC