Email Gateway (Aug 22 2022 at 17:34): Email Gateway (Aug 22 2022 at 17:34):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
Dear all,
***Description:
**Which Eisbach functionality ?
Eisbach matching, namely:
(match conclusion in _" ⇒ _)
The bug is related to matching conclusions in proof goals that comes with
schematic variables.
**Example:
If the conclusion of the proof goal is of the form ⦃?ps5⦄_⦃_⦄ then:
apply (match conclusion in ⦃?ps5⦄_⦃_⦄ " ⇒ succeed) -->This WORKS FINE
However, If the conclusion of the proof goal is of the form ⦃ ?ps2.5 ⦄_⦃_⦄ or
⦃ ?p⇩5 ⦄_⦃_⦄ then:
apply (match conclusion in ⦃ ?ps2.5 ⦄_⦃_⦄ " ⇒ succeed) -->
This WILL NOT WORK because of ?ps2.5
apply (match conclusion in ⦃ ?p⇩5 ⦄_⦃_⦄ " ⇒ succeed)
This WILL NOT WORK because of ?p⇩5
In Other words If you have a schematic variable coming from a "fact" that
uses a free variable with
an underscore like " p⇩5 " or the "fact" uses a free variable followed by a
numeral like " p5 ", Eisbach will not manage to
match it. This is because of the generated schematic variable by Isabelle
after using the "fact" will have the form " ?p⇩5 " and "?p2.5"
respectively.
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 17:34):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
Hi again,
I just figure out it has nothing to do with schematic variables.
However, the bug is even worst. Namely:
1) apply ((match conclusion
in "⦃_⦄_⦃_⦄" ⇒ ‹succeed›), rule H)
2)apply ((match conclusion
in "⦃_⦄_⦃_⦄" ⇒ ‹ rule H ›) )
(1) Here (1) works fine and (2) does NOT work!
For me (1) and (2) should always behave the same!
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 17:34):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Yakoub,
Eisbach's match does not like schematic variables in goal states much. match works similar
to the subgoal command, which turns all schematic variables into goal parameters, i.e.,
they cannot be instantiated afterwards any more. This is by design because it removes the
interdependency between different goals and therefore allows for parallel proof
processing. If you want to work with goals with schematics in them, don't use match or
subgoal.
Best,
Andreas
Email Gateway (Aug 22 2022 at 17:49):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
Hi Andreas,
Is it a side-effect of the tactics match and subgoal on Isabelle state?
Or match and subgoal see schematic variables differently?
Best,
Yakoub.
2018-06-08 1:22 GMT-04:00 Andreas Lochbihler <mail@andreas-lochbihler.de>:
Email Gateway (Aug 22 2022 at 17:49):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Yakoub,
match and subgoal both internally use a function called Subgoal.FOCUS to zoom in on a
single subgoal. This function turns all schematic variables in the goal state into goal
parameters that cannot be instantiated until the FOCUS is removed again. If you must
instantiate schematic variables, you simply cannot use match or subgoal.
Andreas
Last updated: Nov 21 2024 at 12:39 UTC