Re: [isabelle] Difficulties with "setsum"

On 22/04/2015 21:17, Lars Hupel wrote:
lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3"

if both sides can be evaluated to the same value, you can discharge the
goal by "eval".

Note that 'eval' does not go through the kernel and is generally
considered bad style (except for maybe exploratory purposes).

I disagree. I have seen too many people wasting their time trying to achieve something by "pure inference" that eval will do without blinking an eye. There is no evidence that the evaluator is less reliable than the inference kernel. Of course in this example you may as well use code_simp, but the latter can be prohibitively slow.


Fortunately, there's an alternative:

   lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3"
   by code_simp

This sets uses the same code equations as 'eval' (as far as I know), but
goes through the kernel (by invoking the simplifier).


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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