Robert Soeldner (Dec 30 2022 at 20:00): Robert Soeldner (Dec 30 2022 at 20:00):Is there a way to debug, why by assumption fails?
I see a strange error while trying to prove a statement which is also an assumption:
image.png
image.png
Jan van Brügge (Jan 01 2023 at 16:50):You can try supply [[unify_trace_failure]] by assumption. This is probably because a type is not fixed correctly
Robert Soeldner (Jan 01 2023 at 17:53):Indeed, you are right:
The following types do not unify:
('x, 'x, 'y, 'y) pre_morph ⇒ (nat, nat, nat, nat) pre_morph
('ab, 'ab, 'ac, 'ac) pre_morph ⇒ (nat, nat, nat, nat) pre_morph
Still, this was copy\paste of an assumption. Why does it behave like this? It took me significant time until I've add type annotations ^^
Robert Soeldner (Jan 01 2023 at 18:02):Additionally, where can I find the docs of unify_trace_failure ? Isar-ref does not list it.
Mathias Fleury (Jan 02 2023 at 07:02):Robert Soeldner said:
Indeed, you are right:
The following types do not unify: ('x, 'x, 'y, 'y) pre_morph ⇒ (nat, nat, nat, nat) pre_morph ('ab, 'ab, 'ac, 'ac) pre_morph ⇒ (nat, nat, nat, nat) pre_morphStill, this was copy\paste of an assumption. Why does it behave like this? It took me significant time until I've add type annotations ^^
why it behaves like this: Isabelle tries to find the most general possible type, so it does not restrict type to appear in the current goal
Mathias Fleury (Jan 02 2023 at 07:03):Unification is mentioned in 5.8 of https://isabelle.in.tum.de/dist/Isabelle2022/doc/tutorial.pdf, but the name of the flag is not given
Wolfgang Jeltsch (Jan 05 2023 at 01:54):By the way, Isar applies assumption automatically if there are goals left (that’s at least roughly how it is); so you should be able to replace by assumption by the trivial .-proof.
Last updated: Apr 27 2024 at 12:25 UTC