Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with simplifier trace (part 2)

view this post on Zulip Email Gateway (Aug 18 2022 at 13:15):

From: Christoph Feller <c_feller@informatik.uni-kl.de>
Hallo,

I got the same problem as before just at another place. This time I
supply an actual subtrace. This part gets repeated over and over.
Simplifier depth is set to 3. Why do I think this trace is strange?
Well the simplifier tries to use the rule in the first line/block (of
the trace). So it has to show both assumption. It instantiates ?s1 and
?st with the same value and then finds that it can simplify the second
assumption to False (see line/block six). But then the trace continues
with "succeeded", with no indication why it succeeded and I don't want
it to - but I've no way to find the reason for this success.

By the way, if I delete st_in_st_not_ref (see line/block five) from
the simpset the simplifier doesn't loop.

Can anyone make sense of this?

[1]Applying instance of rewrite rule "local.P.st_in_st_stypv":
[| ?st1 st_in_prog P; (?s1, ?st1) : st_in_st |] ==>
Concrete_AST_w_st.stypv P ?s1 ?v1 == Concrete_AST_w_st.stypv P ?st1
?v1

[1]Trying to rewrite:
[| ?st1 st_in_prog P; ([n] v := T Unary unary_op exp, ?st1) : st_in_st|]
==> Concrete_AST_w_st.stypv P [n] v := T Unary unary_op exp v ==
Concrete_AST_w_st.stypv P ?st1 v

[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
?st1 st_in_prog P

[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
([n] v := T Unary unary_op exp, [n] v := T Unary unary_op exp) : st_in_st

[2]Applying instance of rewrite rule "local.P.st_in_st_not_ref":
(?st1, ?st1) : st_in_st == False

[2]Rewriting:
([n] v := T Unary unary_op exp, [n] v := T Unary unary_op exp) :
st_in_st == False

[1]SUCCEEDED
Concrete_AST_w_st.stypv P [n] v := T Unary unary_op exp v ==
Concrete_AST_w_st.stypv P [n] v := T Unary unary_op exp v

Thanks,

Christoph Feller

view this post on Zulip Email Gateway (Aug 18 2022 at 13:19):

From: Tobias Nipkow <nipkow@in.tum.de>
I suspect the problem is here:

[1]Trying to rewrite:
[| ?st1 st_in_prog P; ([n] v := T Unary unary_op exp, ?st1) : st_in_st|]
==> Concrete_AST_w_st.stypv P [n] v := T Unary unary_op exp v ==
Concrete_AST_w_st.stypv P ?st1 v

You have a premise with an uninstantiated higher-order variable. The
simplifier probably managed to instantiate ?st1 with something that
returns False, eg %_ _. False.

The simplifier is not predictable on rules with higher-order variables
in the premises that are not in the conclusion. You have given it the
license to replace such variables with anything...

Tobias

Christoph Feller schrieb:

Hallo,

I got the same problem as before just at another place. This time I
supply an actual subtrace. This part gets repeated over and over.
Simplifier depth is set to 3. Why do I think this trace is strange?
Well the simplifier tries to use the rule in the first line/block (of
the trace). So it has to show both assumption. It instantiates ?s1 and
?st with the same value and then finds that it can simplify the second
assumption to False (see line/block six). But then the trace continues
with "succeeded", with no indication why it succeeded and I don't want
it to - but I've no way to find the reason for this success.

By the way, if I delete st_in_st_not_ref (see line/block five) from
the simpset the simplifier doesn't loop.

Can anyone make sense of this?

[1]Applying instance of rewrite rule "local.P.st_in_st_stypv":
[| ?st1 st_in_prog P; (?s1, ?st1) : st_in_st |] ==>
Concrete_AST_w_st.stypv P ?s1 ?v1 == Concrete_AST_w_st.stypv P ?st1
?v1

[1]Trying to rewrite:
[| ?st1 st_in_prog P; ([n] v := T Unary unary_op exp, ?st1) : st_in_st|]
==> Concrete_AST_w_st.stypv P [n] v := T Unary unary_op exp v ==
Concrete_AST_w_st.stypv P ?st1 v

[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
?st1 st_in_prog P

[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
([n] v := T Unary unary_op exp, [n] v := T Unary unary_op exp) : st_in_st

[2]Applying instance of rewrite rule "local.P.st_in_st_not_ref":
(?st1, ?st1) : st_in_st == False

[2]Rewriting:
([n] v := T Unary unary_op exp, [n] v := T Unary unary_op exp) :
st_in_st == False

[1]SUCCEEDED
Concrete_AST_w_st.stypv P [n] v := T Unary unary_op exp v ==
Concrete_AST_w_st.stypv P [n] v := T Unary unary_op exp v

Thanks,

Christoph Feller

view this post on Zulip Email Gateway (Aug 18 2022 at 13:24):

From: Christoph Feller <c_feller@informatik.uni-kl.de>
On Wed, Apr 1, 2009 at 11:20, Tobias Nipkow <nipkow@in.tum.de> wrote:

I suspect the problem is here:

[1]Trying to rewrite:
[| ?st1 st_in_prog P; ([n] v := T Unary unary_op exp, ?st1) : st_in_st|]
==> Concrete_AST_w_st.stypv P [n] v := T Unary unary_op exp v ==
Concrete_AST_w_st.stypv P ?st1 v

You have a premise with an uninstantiated higher-order variable. The
simplifier probably managed to instantiate ?st1 with something that
returns False, eg %_ _. False.

I just used infix notation for st_in_prog which I shouldn't have done
as it's obviously quite misleading. It should be:

[1]Trying to rewrite:
[| st_in_prog P ?st1; ([n] v := T Unary unary_op exp, ?st1) : st_in_st|]
==> Concrete_AST_w_st.stypv P [n] v := T Unary unary_op exp v ==
Concrete_AST_w_st.stypv P ?st1 v

where ?st1 is a statement i.e. a base value.

[...]

Under these circumstances I would conclude that at least the tracing
algorithm isn't as helpful as it should be. Am I right?

Christoph

Last updated: May 03 2024 at 04:19 UTC