Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Potential bug regarding non-permanent thinning


view this post on Zulip Email Gateway (Feb 11 2022 at 02:07):

From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Hi!

I’d like to report another potential buggy behavior, this time about
thinning being non-permanent.

Consider the following code:

lemma "A ⟹ B ⟹ C ⟹ D"
apply (
match premises in a [thin]: _ ⇒ ‹
match premises in b [thin]: _ ⇒ ‹
succeed


)
oops

After the application of the proof method, the goal is C ⟹ D, as
expected.

Now let’s add some superfluous matching:

lemma "A ⟹ B ⟹ C ⟹ D"
apply (
match premises in a [thin]: _ ⇒ ‹
match ("()") in "()" ⇒ ‹
match premises in b [thin]: _ ⇒ ‹
succeed



)
oops

This time, the generated goal is not C ⟹ D, but B ⟹ C ⟹ D, which it
shouldn’t be.

Let’s add some debugging code:

lemma "A ⟹ B ⟹ C ⟹ D"
apply (
match premises in a [thin]: _ ⇒ ‹
match ("()") in "()" ⇒ ‹
match premises in b [thin]: _ ⇒ ‹
match premises in prems: _ (multi) ⇒ ‹
print_fact prems




)
oops

We get C as the content of prems, which is correct, while the
generated goal is still B ⟹ C ⟹ D.

Apparently, the removal of B from the list of premises, while being
locally observable, is not reflected outside of the match invocation
that performs the superfluous matching. Changing this match invocation
to use a different term or a fact as its match target leads to the same
outcome. However, if premises or conclusion is used as the match
target of this match invocation, the generated goal is again C ⟹ D.
It seems that match invocations that don’t perform subgoal focusing
introduce some sort of barrier that the effect of thinning cannot
transcend.

All the best,
Wolfgang


Last updated: Jul 15 2022 at 23:21 UTC