Re: [isabelle] Use of simp add:



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.




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