Email Gateway (Aug 18 2022 at 15:05): Email Gateway (Aug 18 2022 at 15:05):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,
I have the following locale definition:
locale test =
fixes none :: "'index"
begin;
primrec
label:: "('a => 'index) => ('a list) => ('a => 'index)" where
"label lbl [] = lbl" |
"label lbl (y # S) = label (lbl(y := none)) S";
lemma first: "f x = none ==> f = label (f(x := i)) [x]";
by auto;
lemma second: "none = f x ==> f = label (f(x := i)) [x]";
apply auto;
The first lemma is proved by auto as one would expect, however the second
lemma is transformed into
f = test.label (f x) (f(x := i)) [x]
where test.label :: 'index => ('a => 'index) => 'a list => 'a => 'index
At first I had big problems understanding why label would have the
first parameter of type 'index, then I figured out that this extra
parameter
is the parameter none fixed by the locale. This fact can also be deduced
from how second lemma was transformed by auto.
Within a locale I would expect the fixed parameters to behave as
constants.
Even if they are treated as variable in second lemma I would expect
that the definition label can still be applied to test.label (f x) (f(x
:= i)) [x]
with (f x) instead on none. If that would be the case, then second lemma
should be discharged automatically.
Trying to apply the definition of label manually (unfold ...) (rule ...)
or (simp add: ...) does not change the goal
How do I prove f = test.label (f x) (f(x := i)) [x] ? I can prove
second lemma using by (case_tac "f x = none", auto) but the statement
" f = test.label (f x) (f(x := i)) [x]" occurs in a much more involved
result, and I cannot control how the simplifications are done before
getting this "unprovable" goal.
Best regards,
Viorel
Email Gateway (Aug 18 2022 at 15:05):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Viorel,
the matter is: internally, "label" (in test) is represented as
"test.label none". Therefore the assumption "none = f x" rewrites this
to "test.label (f x)" (c.f. also
http://www4.in.tum.de/~wenzelm/papers/local-theory.pdf). You could call
this a misbehaviour of the simplifier.
Once "test.label none" has been unfolded to "test.label (f x)", the
local theorems (in test) are not applicable any more. The global
foundational theorems test.label.simps etc. could be used; however I do
recommend to avoid that unfolding from the very beginning.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 15:05):From: Brian Huffman <brianh@cs.pdx.edu>
On Wed, Apr 14, 2010 at 5:37 AM, Florian Haftmann
<florian.haftmann@informatik.tu-muenchen.de> wrote:
Hi Viorel,
locale test =
fixes none :: "'index"
begin;primrec
label:: "('a => 'index) => ('a list) => ('a => 'index)" where
...
lemma second: "none = f x ==> f = label (f(x := i)) [x]";
apply auto;the matter is: internally, "label" (in test) is represented as
"test.label none". Therefore the assumption "none = f x" rewrites this
to "test.label (f x)" (c.f. also
http://www4.in.tum.de/~wenzelm/papers/local-theory.pdf). You could call
this a misbehaviour of the simplifier.
It seems that inside the locale, "label == test.label none" is
registered as a local abbreviation. As such, its argument ("none")
is still visible to the simplifier.
Is there any reason why "label == test.label none" could not be
implemented instead as a local definition? I'm thinking of how the
"def" command works within a proof script: This adds a definition that
is unfolded when the lemma is exported, but within the proof, the
simplifier just sees an opaque constant.
If locally-defined constants were treated this way in locales, I think
the behavior would cause many fewer surprises for users.
This same issue has been brought up on this list before, nearly two years ago:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2008-June/msg00089.html
At the time, I recommended using a congruence rule as a quick
workaround to prevent the simplifier from tampering with hidden
parameters of locally-defined constants. But I think a "def"-like
mechanism is a better solution.
Email Gateway (Aug 18 2022 at 15:05):From: Alexander Krauss <krauss@in.tum.de>
Brian Huffman wrote:
This unfortunately does not work in general, since "def" in proofs
cannot support polymorphism.
Alex
Email Gateway (Aug 18 2022 at 15:05):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hello Viorel,
the definition of label in your locale test produces only one global
constant called test.label that takes all locale parameters on which the
definition depends (in your case "none") as extra parameters.
When you are inside the context of the locale, you merely see
abbreviations of the global constants with the parameters instantiated
to the fixed locale parameters, i.e. there is no local version of the
label constant.
lemma second: "none = f x ==> f = label (f(x := i)) [x]";
apply auto;[...]
f = test.label (f x) (f(x := i)) [x]
Here, the simplifier rewrites "none" to "f x", so the local abbreviation
"label == test.label none" no longer applies.
This is why you see the global constant. Unfortunately, auto also
removes the equation "none = f x" from the assumptions because it thinks
that it would not be needed any more.
- Even if they are treated as variable in second lemma I would expect
that the definition label can still be applied to test.label (f x) (f(x
:= i)) [x]
with (f x) instead on none. If that would be the case, then second lemma
should be discharged automatically.
Just like with the constants, there are local and global versions of the
theorem. For label, label.simps refers to the local version where none
is fixed as parameter. Since your goal involves the global version of
label after auto has been applied, you must also use the global version
test.label.simps for reasoning.
Fortunately, your locale does not assume anything. Hence, the global
version of the defining theorem are not guarded by any locale predicate
and you can use them freely for reasoning.
- How do I prove f = test.label (f x) (f(x := i)) [x] ? I can prove
second lemma using by (case_tac "f x = none", auto) but the statement
" f = test.label (f x) (f(x := i)) [x]" occurs in a much more involved
result, and I cannot control how the simplifications are done before
getting this "unprovable" goal.
Instead of using auto, you could first tell the simplifier not to use
the assumptions, which leaves the local version intact.
apply(simp (no_asm_use))
In a second step, use again the simplifier to solve the remaining goal.
Hope this helps,
Andreas
Email Gateway (Aug 18 2022 at 15:06):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,
Thank you all for answering my question. It seems that this is a
delicate issue.
Applying a rule (auto) in local context which takes you out from the
local context,
although well motivated by the implementation, seem strange to the new user
which may not be aware of the internals. On the other hand if auto changes
the goal into a global goal, why the global simplification rules are not
used here. If auto would use these simplification rules (test.label.simps),
then this goal will be solved automatically. Moreover, I suppose
(test.label.simps) are always applicable when (label.simps) are
applicable, and using (test.label.simps) in auto would always
yield better results. If the final result contains "test.label none"
then the abbreviation would replace it back by label.
Another way I would imagine is that you would not allow results
which take you out of the local theory. Whenever you get out
of the locale you stop the proof and search for alternatives.
After all that is what you want with a locale.
I have figured out that avoiding unfolding "test.label none" to
"test.label (f x)", would let me
progress with the prof. However, as I already mentioned, this is not a good
option in my case because this problem occurs in a context where the
goal has many
components, and auto solves all except the one from this example. It
would be much
easier for me to use the global rule instead of splitting the goal
little by little and make
sure the unfolding "test.label none" to "test.label (f x)" does not occur.
Best regards,
Viorel
Email Gateway (Aug 18 2022 at 15:06):From: Brian Huffman <brianh@cs.pdx.edu>
The workaround using congruence rules that I mentioned before will do
just that: It will prevent simp or auto from rewriting "test.label
none" to "test.label (f x)".
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2008-June/msg00089.html
Here's the rule you would want to use in your case (note that there is
no assumption corresponding to subterm "n"):
lemma label_cong [cong]: "f = g ==> xs = ys ==> test.label n f xs =
test.label n g ys"
by simp
By placing this lemma (with its [cong] attribute) before your other
proofs, "test.label none" should never have its argument rewritten by
the simplifier.
Hope this helps,
Email Gateway (Aug 18 2022 at 15:07):From: Brian Huffman <brianh@cs.pdx.edu>
On Mon, Apr 19, 2010 at 1:40 AM, Viorel Preoteasa
<viorel.preoteasa@abo.fi> wrote:
Hello Brian,
The trick seems to work for the test theory, but it does not work
for my real theory. Also using the global simplification rule does not
work for me either because I have assumptions in the locale. I have
succeeded to strip down the example for which the cong approach
does not work. In the third and forth lemmas the definition label
is expanded to test.label and the proofs fail.
...
lemma third:
"tl a = [] ==> f (hd a) = none
==> f = label (f(hd a := i)) a";
apply auto;
sorry;lemma forth:
"? y ys . a = y # ys ==> f (hd a) = none
==> f = label (f(hd a := i)) a";
apply auto;
sorry;
I see what is going on here. The congruence rule successfully prevents
the simplifier from rewriting "label" to "test.label", but with
lemmas "third" and "forth" it is not the simplifier that is causing
the problem. Try replacing "apply auto" with either "apply safe" or
"apply clarify", and you will get the same result.
This unhelpful behavior of "safe" (which is included as part of what
"auto" does) in the context of locales has been noted before on the
mailing list:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2007-February/msg00075.html
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2007-February/msg00076.html
Unfortunately, while it has been acknowledged as a problem, it seems
that nothing has been done about it.
Email Gateway (Aug 18 2022 at 15:07):From: Brian Huffman <brianh@cs.pdx.edu>
Yes, try the following:
apply (auto) [1]
In general, "apply (<tactic>) [n]" restricts the tactic to act only on
the first n subgoals.
Email Gateway (Aug 18 2022 at 15:07):From: Makarius <makarius@sketis.net>
Here I really need to insist that the Isar category of "method" is not
called "tactic". One of the very characteristics of Isar proof methods is
the stylized access to the underlying goal structure, without the
traditional goal addressing of tactics.
The method combinator [...] above works quite differently from tactial
goal addressing: it singles out a section of the goal state, applies the
proof method, and retrofits the result.
Makarius
Email Gateway (Aug 18 2022 at 15:07):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello Brian,
The trick seems to work for the test theory, but it does not work
for my real theory. Also using the global simplification rule does not
work for me either because I have assumptions in the locale. I have
succeeded to strip down the example for which the cong approach
does not work. In the third and forth lemmas the definition label
is expanded to test.label and the proofs fail.
Best regards,
Viorel
locale test =
fixes none :: "'index"
begin;
primrec
label:: "('a => 'index) => ('a list) => ('a => 'index)" where
"label lbl [] = lbl" |
"label lbl (y # l) = label (lbl(y := none)) l";
lemma first: "f x = none ==> f = label (f(x := i)) [x]";
by auto;
lemma label_cong [cong]: "f = g ==> xs = ys ==> test.label n f xs =
test.label n g ys"
by simp
lemma second: "none = f x ==> f = label (f(x := i)) [x]";
by auto;
lemma third:
"tl a = [] ==> f (hd a) = none
==> f = label (f(hd a := i)) a";
apply auto;
sorry;
lemma forth:
"? y ys . a = y # ys ==> f (hd a) = none
==> f = label (f(hd a := i)) a";
apply auto;
sorry;
end;
Brian Huffman wrote:
Email Gateway (Aug 18 2022 at 15:08):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello Brian,
Thank you for your answer. I have succeeded with one theorem, but
I am struggling with the next one now. It is quite difficult to get it
to work. I have many parameters in the theories, and many definitions
depending on one or more parameters. As you already said, and also
discovered by myself while trying to prove the results, even safe
and clarify expand the definitions in the undesired way. What is
even worse is that these apply to all sub-goals, not only to the first one.
Is there a way of applying a rule (auto, safe, clarify, unfold) only
to the first goal (the same way as simp works)?
Best regards,
Viorel
Last updated: Apr 19 2024 at 20:15 UTC