Email Gateway (Aug 18 2022 at 10:15): Email Gateway (Aug 18 2022 at 10:15):From: Peter Lammich <peter.lammich@uni-muenster.de>
In the following example:
locale A =
fixes X
defines "X==[1::nat]"
lemma (in A) test: "[] ~= X"
apply safe
The subgoal presented to me is: False.
I expected something like: [] = X ==> False, but I get just False.
The same is with auto. The reason seems to be the defined variable X of
the locale.
In some more complex proofs, this forces me to very often fold/unfold
symbol definitions in my locales (to prevent auto or safe making such
transformations), and this makes the proof scripts more confusing.
Is this behaviour of safe and auto the intended one ?
Is there any workaround to use a defined variable like X, but prevent
safe/auto from making such steps ?
Thanks in advance for any help
-- Peter Lammich
Email Gateway (Aug 18 2022 at 10:15):From: Lawrence Paulson <lp15@cam.ac.uk>
At the moment, any assumption like []=X is deleted after replacing X
by []. As you've noticed, that isn't helpful if constrained by a
locale. We could investigate whether anything can be done about it.
Larry
Last updated: May 03 2024 at 08:18 UTC