*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Use of simp add:*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Fri, 29 Aug 2014 10:02:33 +0200*In-reply-to*: <a0620071dd0259b7efc7c@[192.168.1.2]>*References*: <a0620071dd0259b7efc7c@[192.168.1.2]>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Icedove/24.6.0

On 29.08.2014 05:22, W. Douglas Maurer wrote: > I would appreciate some kind of strategy to determine what to write > after simp add: when proving a simple fact. This first came up for me > when I was trying to prove "floor (9.5::real) = (9::int)" and "ceiling > (9.5::real) = (10::int)". Here try0 was no help; it tried simp, auto, > fast, fastforce, force, blast, metis, linarith, and presburger, and > then reported no proof found. Quite by accident, I found out how to do > these; you type simp add: floor_unique or simp add: ceiling_unique . > I'd like to know how to find rules like floor_unique and > ceiling_unique in other cases. In this case, my approach would have been to use find_theorems to look for "floor _ = _". If the property could also be computed (there are no variables in this goal), you can also try code_simp/normalization/eval -- these methods use a different setup of rewrite rules aimed at generation of executable code instead of proving. > The one I'm concerned about now is "(2::nat)*x ~= 3", which arose for > me as an unproved subgoal. Yes, I know I can prove this one by > presburger, because try0 told me so, but that seems like using an > elephant to crush a flea; presburger took forever to find a proof. It shouldn't take long -- on my machine, presburger is almost instantaneous on this goal (additional premises may slow it down, though). > I've also tried find_theorems, but that said it found over 18,000 > theorems and none of the first few looked promising. I'm sure there's > a much simpler way of proving that "(2::nat)*x ~= 3", and I'm sure > that many people on the mailing list know what it is, but what I'd > really appreciate is some hints on how to find something like this. find_theorems is often the right approach. However, if you need to give it a query, otherwise it lists all theorems (which is not going to be useful). The simples queries consist of a number of term patterns (like "_ * _"); another very useful query is "intro" which lists all applicable introduction rules. The reference manual has a full list of options. Another way to discover lemmas is using sledgehammer and inspecting the proofs (especially if you give it the isar_proofs option). For me, it gives the proof by (metis Suc_numeral even_mult_two_ex monoid_mult_class.mult.right_neutral odd_Suc_mult_two_ex semiring_norm(5)) The interesting lemmas here are even_mult_two_ex and odd_Suc_mult_two_ex. However, due to the existential, they are not well-suited for simp and auto. The goal "2*x ~= 3" is a bit tricky for automated tools: The reasoning is that 2*x is even and 3 is odd. However, neither "even" nor "odd" is mentioned in the goal. A rule like "even x ==> odd y ==> x ~= y" could introduce these constants. However, looking at the theorems for "even" and "odd" [1], none of the existing theorems suggests itself. We can easily prove it ourselves, though: lemma even_odd_neq_nat: "⋀x y :: nat. even x ⟹ odd y ⟹ x ≠ y" by auto Giving this lemma to simp easily solves the goal. -- Lars [1] There is some oddity in find_theorems. Searching for "odd" will not yield any lemmas, you will need to write "odd _". This is somehow related to odd being an abbreviation for "~ even" and possibly warrants some closer investigation from the developers.

**References**:**[isabelle] Use of simp add:***From:*W. Douglas Maurer

- Previous by Date: Re: [isabelle] Use of simp add:
- Next by Date: [isabelle] Call for participation : VTSA 2014
- Previous by Thread: Re: [isabelle] Use of simp add:
- Next by Thread: [isabelle] Call for participation : VTSA 2014
- Cl-isabelle-users August 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list