Email Gateway (Aug 19 2022 at 08:13): Email Gateway (Aug 19 2022 at 08:13):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
Dear Isabelle experts,
somewhere in a proof that involves real numbers from the theory "Real" I
would like to infer "(x::real) >= 0" from "x > 0".
For now I solved the problem by introducing the following axiomatic "lemma":
lemma greater_zero_implies_greater_equal_zero [simp] :
fixes x::real
assumes "x > 0"
shows "x ≥ 0"
sorry
(Note that I am new to Isabelle, so there might be better ways of doing
this.)
I would be interested in some built-in rule, or a theory in the library,
that would simply do this inference for me.
I am less interested in writing my own proof of this in place of the
"sorry" above, as my overall formalisation is a higher-level applied one.
Cheers, and thanks in advance for any help,
Christoph
Email Gateway (Aug 19 2022 at 08:13):From: Brian Huffman <huffman@in.tum.de>
by (rule less_imp_le)
Email Gateway (Aug 19 2022 at 08:14):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
Dear Brian,
2012-08-10 10:15 Brian Huffman:
excellent, thanks a lot for your quick reply!
Generally, when similar situations occur in future: Is there any
documentation of such rules? In the manuals that come with Isabelle I
didn't find anything.
I see that this particular rule and similar ones are documented
reasonably well by the comments in src/Provers/order.ML So would you
generally suggest scanning the sources for applicable rules, or is there
a nicer overview?
Cheers, and thanks,
Christoph
Email Gateway (Aug 19 2022 at 08:14):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Freitag, den 10.08.2012, 12:08 +0200 schrieb Christoph LANGE:
Dear Brian,
2012-08-10 10:15 Brian Huffman:
somewhere in a proof that involves real numbers from the theory "Real" I
would like to infer "(x::real) >= 0" from "x > 0".…
by (rule less_imp_le)
excellent, thanks a lot for your quick reply!
Generally, when similar situations occur in future: Is there any
documentation of such rules? In the manuals that come with Isabelle I
didn't find anything.
The theories are documented in
http://isabelle.in.tum.de/dist/library/HOL/Orderings.html
but this is neither searchable nor very readable.
There are two better methods:
use find_theorems
like: find_theorems "_ > _ ==> _ >= _"
This is fast, but the result depends very strong on the pattern you
are searching for.
General rule: give a list of constants and not more:
find_theorems (200) "_ > _" "_ >= _" name: Ord
(the (200) tells find theorem to list the first 200 results)
use sledgehammer:
lemma "(x::real) > 0 --> x >= 0"
sledgehammer
This will now try to find a proof for this.
The proof will contain the necessary lemmas.
Johannes
I see that this particular rule and similar ones are documented
reasonably well by the comments in src/Provers/order.ML So would you
generally suggest scanning the sources for applicable rules, or is there
a nicer overview?Cheers, and thanks,
Christoph
Email Gateway (Aug 19 2022 at 08:14):From: Brian Huffman <huffman@in.tum.de>
Scanning the ML sources is probably not very useful. If you want to
familiarize yourself with the set of available theorems, it is better
to browse the .thy files in src/HOL (most lemmas about < and <= are in
Orderings.thy) or else browse the generated pdf documentation for
Isabelle/HOL (follow "document" or "outline" link from
https://isabelle.in.tum.de/dist/library/HOL/index.html).
If you are looking for a specific lemma, you should definitely learn
the "find_theorems" command. See e.g. section 3.1.11 of the "Tutorial
on Isabelle/HOL".
Email Gateway (Aug 19 2022 at 08:14):From: Lawrence Paulson <lp15@cam.ac.uk>
The real difficulty here is that you are using assumes/shows. Then the assumption "x > 0" isn't explicitly part of the subgoal and isn't visible to Isabelle's automation. The one exception is sledgehammer, which sees everything, and instantly finds a proof.
It would be better to state your problem more simply as follows:
lemma greater_zero_implies_greater_equal_zero [simp] :
fixes x::real
shows "x > 0 \<Longrightarrow> x \<ge> 0"
Or even more simply like this:
lemma greater_zero_implies_greater_equal_zero [simp] :
"(x::real) > 0 \<Longrightarrow> x \<ge> 0"
Then almost anything will solve it: auto, simp, arith, force. I suggest reserving assumes/shows for complicated theorems where there are many assumptions and they aren't all wanted at the same time.
Another remark: I'm not sure it's a good idea to declare something like this as a default simplification rule. It will be quite generally applicable, and could increase your simplification time or even (together with similarly general conditional rewrite rules) cause looping.
Larry Paulson
Email Gateway (Aug 19 2022 at 08:14):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
2012-08-10 12:22 Johannes Hölzl:
Am Freitag, den 10.08.2012, 12:08 +0200 schrieb Christoph LANGE:
2012-08-10 10:15 Brian Huffman:
by (rule less_imp_le)
…
Generally, when similar situations occur in future: Is there any
documentation of such rules? In the manuals that come with Isabelle I
didn't find anything.The theories are documented in
http://isabelle.in.tum.de/dist/library/HOL/Orderings.htmlbut this is neither searchable nor very readable.
Thanks! Grepping the *.thy source files has been very useful for me so
far. Actually the only reason why I ended up in the ML sources was that
in the theory sources there was a lot of "noise" from this rule being
_applied_, so I just overlooked the lemma.
There are two better methods:
Thanks a lot – very helpful. As a newbie, obviously, I knew neither of
them.
* use find_theorems
like: find_theorems "_ > _ ==> _ >= _"
^
I think here it expects a numeric argument
as said below; didn't work without.
…
General rule: give a list of constants and not more:
find_theorems (200) "_ > _" "_ >= _" name: Ord
(the (200) tells find theorem to list the first 200 results)
BTW in the documentation find_theorems is only mentioned in
prog-prove.pdf (just searched all files with pdfgrep), and there it says:
--- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< ---
Command find_theorems searches for specific theorems in the current theory.
Search criteria include pattern matching on terms and on names. For details
see the Isabelle/Isar Reference Manual [4].
--- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< ---
… but the reference manual does't mention it.
Generally, I had no idea that one can apply _any_ theorem using (rule
name_of_theorem). This wasn't obvious to me, and instead I had thought
that "rules" are something special that's built in at the level of "a
calculus for a logic".
* use sledgehammer:
lemma "(x::real) > 0 --> x >= 0"
sledgehammerThis will now try to find a proof for this.
The proof will contain the necessary lemmas.
Excellent, very helpful too!
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 08:14):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
2012-08-10 12:22 Brian Huffman:
Scanning the ML sources is probably not very useful.
Indeed – I realized my mistake (see my reply to Johannes where I
explained why I ran into this wrong direction).
If you are looking for a specific lemma, you should definitely learn
the "find_theorems" command. See e.g. section 3.1.11 of the "Tutorial
on Isabelle/HOL".
Nice!
I should really be using ProofGeneral _and_ jEdit side-by-side.
Shouldn't be a problem, as either editor notices when the other one has
changed the file, and offers reloading.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 08:14):From: Tobias Nipkow <nipkow@in.tum.de>
My mistake, will fix that, thanks!
Tobias
Email Gateway (Aug 19 2022 at 08:14):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
Dear Larry, dear all (some more general-interest comments below; search
for "objectives"),
2012-08-10 12:22 Lawrence Paulson:
The real difficulty here is that you are using assumes/shows. Then the assumption "x > 0" isn't explicitly part of the subgoal and isn't visible to Isabelle's automation.
Thanks, that's good to know. I really had thought that "assumes/shows"
is just syntactic sugar for certain more complex expressions within the
logic.
(Note: Don't be too worried when I say "I thought" or "I didn't know" or
"I had no idea" – I still need to learn a lot. Whenever I think that
something should really be presented in a more learnable way, I will
make it explicit, as in a bug report :-))
It would be better to state your problem more simply as follows:
lemma greater_zero_implies_greater_equal_zero [simp] :
fixes x::real
shows "x > 0 \<Longrightarrow> x \<ge> 0"Or even more simply like this:
lemma greater_zero_implies_greater_equal_zero [simp] :
"(x::real) > 0 \<Longrightarrow> x \<ge> 0"
Nice! I had no idea that one can omit the universal quantification of
x::real here.
Then almost anything will solve it: auto, simp, arith, force.
So from x::real these provers will know that it is a real number and
therefore an element of an ordered set?
I suggest reserving assumes/shows for complicated theorems where there are many assumptions and they aren't all wanted at the same time.
Thanks, that's good to know. One of the objectives of our project
(http://cs.bham.ac.uk/research/projects/formare/) is to teach ATP/ITP to
non-experts from application domains, economics in our case.
We are interested in formalising new theorems that haven't been
formalised before, but also re-formalising things that have been
formalised before, but in a way that doesn't "just get the proof done",
but in a way that we think we could teach to economists.
Therefore we would like to keep as closely as possible to paper textbook
style, and for this reason I thought "the more Isar syntactic sugar the
better".
We just got started with Isabelle (have done some formalisation in
Theorema before), but first public results can be expected soon.
Another remark: I'm not sure it's a good idea to declare something like this as a default simplification rule.
Thanks for the heads-up – indeed that approach resulted from the
misunderstanding; I didn't know that one can simply say (rule
name_of_lemma).
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 08:15):From: Dmitriy Traytel <traytel@in.tum.de>
I don't see the mistake. The Isabelle/Isar Reference Manual describes
find theorems on pages 163-165.
Dmitriy
Email Gateway (Aug 19 2022 at 08:15):From: Lars Noschinski <noschinl@in.tum.de>
On 10.08.2012 13:32, Tobias Nipkow wrote:
My mistake, will fix that, thanks!
find_theorems is explained on page 163 of the reference manual.
Christoph: Searching for text in these pdf manual is not reliable; for
example "fi" is turned into an fi-ligature (a single character), so it
does not turn up when searching for fi (two characters), at least for
some pdf readers.
It is far more reliable to look into the index at the end of the
reference manual.
-- Lars
Am 10/08/2012 13:24, schrieb Christoph LANGE:
BTW in the documentation find_theorems is only mentioned in prog-prove.pdf (just
searched all files with pdfgrep), and there it says:--- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< ---
Command find_theorems searches for specific theorems in the current theory.
Search criteria include pattern matching on terms and on names. For details
see the Isabelle/Isar Reference Manual [4].
--- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< ---… but the reference manual does't mention it.
Email Gateway (Aug 19 2022 at 08:15):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
2012-08-10 13:42 Dmitriy Traytel:
I don't see the mistake. The Isabelle/Isar Reference Manual describes
find theorems on pages 163-165.
Indeed – but strangely this text is not searchable. The underscore of,
e.g., find_theorems, is not represented as a usual underscore. You can
try it by searching the PDF for "find_theorems".
doc-src/IsarRef/Thy/Misc.thy doesn't contain anything suspicious, so I
suspect a bug in the document preparation implementation.
Is this list the right way to report bugs, or is there any better way?
Cheers, and thanks,
Christoph
Email Gateway (Aug 19 2022 at 08:15):From: Lars Noschinski <noschinl@in.tum.de>
On 10.08.2012 13:40, Christoph LANGE wrote:
Dear Larry, dear all (some more general-interest comments below; search
for "objectives"),2012-08-10 12:22 Lawrence Paulson:
The real difficulty here is that you are using assumes/shows. Then the
assumption "x > 0" isn't explicitly part of the subgoal and isn't
visible to Isabelle's automation.Thanks, that's good to know. I really had thought that "assumes/shows"
is just syntactic sugar for certain more complex expressions within the
logic.
You will get the same theorem in the end, but it is handled differently
in Isar; the assumptions will need to be used explicitly, e.g.
lemma greater_zero_implies_greater_equal_zero [simp] :
fixes x::real assumes "x > 0" shows "x \<ge> 0"
using assms by auto
I suggest reserving assumes/shows for complicated theorems where there
are many assumptions and they aren't all wanted at the same time.Thanks, that's good to know. One of the objectives of our project
(http://cs.bham.ac.uk/research/projects/formare/) is to teach ATP/ITP to
non-experts from application domains, economics in our case.We are interested in formalising new theorems that haven't been
formalised before, but also re-formalising things that have been
formalised before, but in a way that doesn't "just get the proof done",
but in a way that we think we could teach to economists.Therefore we would like to keep as closely as possible to paper textbook
style, and for this reason I thought "the more Isar syntactic sugar the
better".
This is entirely a matter of preference. I usually prefer structured
lemma statements.
-- Lars
Email Gateway (Aug 19 2022 at 08:15):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
2012-08-10 14:01 Lars Noschinski:
Christoph: Searching for text in these pdf manual is not reliable; for
example "fi" is turned into an fi-ligature (a single character), so it
does not turn up when searching for fi (two characters), at least for
some pdf readers.
Good point – I didn't realize, as I mainly use PDF viewers that support
them. But indeed I see that Adobe Reader doesn't.
This post might be helpful:
http://www.acsu.buffalo.edu/~jfernand/archives/2011/01/allow-adobe-reader-to-find-words-containing-ligatures.html
(note the link to glyphtounicode.tex is broken, but Google will find it,
and many TeX installations have it)
I'm not sure whether this solution is generally applicable, but maybe
the LaTeX-to-PDF creation workflow of Isabelle could be adapted to take
this fix into account. (This won't fix the unterscore problem yet.)
It is far more reliable to look into the index at the end of the
reference manual.
Uh – I hope I won't eventually have to _print_ the manual ;-)
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 08:15):From: Lawrence Paulson <lp15@cam.ac.uk>
On 10 Aug 2012, at 12:40, Christoph LANGE wrote:
So from x::real these provers will know that it is a real number and therefore an element of an ordered set?
Correct.
I didn't know that one can simply say (rule name_of_lemma).
That is one of the core ideas in Isabelle, going right back to 1986.
Your project sounds interesting. Good luck!
Larry
Email Gateway (Aug 19 2022 at 08:15):From: Makarius <makarius@sketis.net>
On Fri, 10 Aug 2012, Christoph LANGE wrote:
Indeed – but strangely this text is not searchable. The underscore of,
e.g., find_theorems, is not represented as a usual underscore. You can
try it by searching the PDF for "find_theorems".
doc-src/IsarRef/Thy/Misc.thy doesn't contain anything suspicious, so I
suspect a bug in the document preparation implementation.
See also this thread:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-May/msg00251.html
Is this list the right way to report bugs, or is there any better way?
You can post whatever you want on this list, as long as it refers to the
official Isabelle release -- normally the latest one, or one or two
versions behind.
It also helps to search the mailing list archives. See the links on the
Isabelle website front page.
BTW, after more than 25 years certain things in Isabelle are just as they
are to the good or to the confusion of new users. "Bugs" are very rare --
often it is just a misunderstanding what to expect.
Of course it always helps if you report your observations and share the
experience to get things the way you need them.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC