Email Gateway (Feb 11 2022 at 02:07): 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: Jan 04 2025 at 20:18 UTC