Email Gateway (Aug 19 2022 at 16:33): Email Gateway (Aug 19 2022 at 16:33):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hello,
I have the theory:
theory test imports Main
begin
definition "F = top"
lemma A: "F (f o g) (n::nat) = top"
apply auto
sorry
lemma B: "F (f o g) (n::nat) = top"
apply (induction n)
apply auto
sorry
end
The question is why in lemma A, auto fails as expected, while in lemma B
auto
changes (f o g) into (λa. f (g a)). How can I prevent this change?
Best regards,
Viorel Preoteasa
Email Gateway (Aug 19 2022 at 16:33):From: Tobias Nipkow <nipkow@in.tum.de>
The culprit is comp_apply: (f ∘ g) a = f (g a) which you can of course remove:
apply(auto simp del: comp_apply)
How to find out? Put "using [[simp_trace_new mode=full]]" in front of your
simp/auto command.
Tobias
smime.p7s
Email Gateway (Aug 19 2022 at 16:33):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
It works if I add "del: comp_apply", but I still do not understand why?
My term does not contain "(f o g) a", so comp_apply does not seem to match
any sub-term. I tried before to remove comp_def which is applicable
to (f o g), but then I got the warning that comp_def is not a simp rule.
It is also strange that the rule comp_apply becomes applicable only
after induction.
Viorel
Email Gateway (Aug 19 2022 at 16:33):From: Tobias Nipkow <nipkow@in.tum.de>
Terms are eta-contracted before printing and rule application (eg in induction)
may eta-expand terms. If you always want to see the uncontracted version:
declare [[eta_contract=false]]
Tobias
smime.p7s
Email Gateway (Aug 19 2022 at 16:33):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Thank you. This explains it.
Viorel
Last updated: Apr 25 2024 at 04:18 UTC