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)".

For a start, simp should prove this, but unfortunately it does not. We will have
to add the right lemmas to automate this, thanks.

> 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.

The search button (`Find' or `Query'). In this case it is not so clear what to
search for. Certainly "floor", but that still gives you 75 lemmas, which you
would have to go through and see if they might be helpful.

> 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.

Not for me: presburger is instantaneous, as is arith (which tries linear
arithmetic first and only then presburger).

> 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. -Douglas

The 18,000 suggests you just typed find_theorems. Use the search facility
(`Find' or `Query') with appropriate selection criteria.

Tobias




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