Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?



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

--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec, Skype duke4701

→ Building & Exploring Web Based Environments.  Seville, Spain, 27 Jan–
  1 Feb 2013.  Deadline 2 Sep.  http://iaria.org/conferences2013/WEB13.html





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.