Email Gateway (Aug 22 2022 at 11:24): Email Gateway (Aug 22 2022 at 11:24):From: Lars Hupel <hupel@in.tum.de>
Dear list,
as you all know, the 'proof' command introduces a let-binding "?thesis"
according to the preceding statement. I have observed a situation where
there is a difference between "?thesis" and the expanded term. See the
attached theory file. In the last proof step, if you replace the literal
term with "?thesis", the simplifier fails to solve the proposition.
However, both look completely identical. I have no idea what's going on
there.
Cheers
Lars
Thesis.thy
Email Gateway (Aug 22 2022 at 11:24):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Lars,
If you disable eta-contraction in printing, with
declare [[eta_contract = false]]
you will see that the two terms are not exactly the same, which is enough to derail the simplification.
Jasmin
Email Gateway (Aug 22 2022 at 11:24):From: Lars Hupel <hupel@in.tum.de>
Hi Jasmin,
thanks for the investigation. Apparently spontaneous eta-contraction is a
tricky business. I just wonder why the 'induction' method appears to
eta-expand terms occurring in my goal.
Cheers
Lars
Email Gateway (Aug 22 2022 at 11:25):From: Tobias Nipkow <nipkow@in.tum.de>
On 09/09/2015 14:58, Lars Hupel wrote:
Hi Jasmin,
If you disable eta-contraction in printing, with
declare [[eta_contract = false]]
you will see that the two terms are not exactly the same, which is enough
to derail the simplification.thanks for the investigation. Apparently spontaneous eta-contraction is a
tricky business. I just wonder why the 'induction' method appears to
eta-expand terms occurring in my goal.
Induction performs resolution and resolution can eta-expand.
Tobias
Cheers
Lars
Last updated: Apr 26 2024 at 16:20 UTC