Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2015-RC1: Rule instantiation in Eisbach

Email Gateway (Aug 22 2022 at 09:18):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Eisbach developers,

First of all, thanks for designing and implementing Eisbach. Unfortunately, I am
struggling with instantiating variables in rules when I write my own proof methods in Eisbach.

Abstractly,

1. I select a rule R by matching a list L of theorems against a term, and
2. then instantiate a variable in R with a term obtained by matching the conclusion
   against a pattern.

Unfortunately, I always get the error "More instantiations than variables in theorem"
although all the theorems in the list L contain at least one variable. I do not know where
this error comes from. Below is a small example:

theory Scratch imports Main "~~/src/HOL/Eisbach/Eisbach_Tools" begin

consts foo :: "'a ⇒ 'a ⇒ 'a ⇒ bool"
lemma my_thms: "foo x y z ⟹ z ∧ y" "foo x y y ⟹ x ∧ z" sorry

lemma "⋀z. A z ∧ B"
apply(
match concl in "f x y" for f x y ⇒ ‹
match my_thms in R:"PROP P ⟹ f u v" for P u v ⇒ ‹
rule R[of x]
›
›
)
oops

end

Thanks for any help,
Andreas

PS: I am trying to build something similar to the apply_split method in the Eisbach paper
presented at ITP2014.

Email Gateway (Aug 22 2022 at 09:23):

From: Daniel Matichuk <daniel.matichuk@nicta.com.au>
Hi Andreas,

Unfortunately the ITP paper is slightly out of date, specifically regarding rule instantiation. The "match" method is now meant to guard rule instantiation at run-time by ensuring that the matched theorem(s) has
the correct slots available. This is done by using meta-quantifiers in your patterns. Specifically the semantics of a match are that a "for-fixed" variable may match anything, whereas a meta-quantified variable
must match against a schematic. So in your example, assuming you wish to instantiate "P", your pattern should be "!!P. PROP P ==> f u v" for u v". This statically ensures that any matched rule can be instantiated appropriately (so the failure occurs in the match, rather than the rule instantiation).
The motivation for this requirement is perhaps more clear when using match to define an Eisbach method, rather than when used in-place.

It's also worth noting that a pattern like "f x y" for f x y will produce a large set of possible matches, due to "match" using the unifier internally. The usual best-practice approach is to add type annotations to your pattern to restrict the matches.
There is some argument for extending the match pattern language to support more precise term deconstruction, but I'm waiting to see more use cases before adding more complexity.

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

Email Gateway (Aug 22 2022 at 09:23):

From: Makarius <makarius@sketis.net>
It would be interesting to explore the question if/how the new "rewrite"
method facilities could be re-used here.

Makarius

Email Gateway (Aug 22 2022 at 09:23):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Daniel,

Thanks for the reply. Unfortunately, I cannot get this to work at all. Your suggested
pattern "!!P. PROP P ==> f u v" raises a type error. After several failed attempts, I am
now stuck at the following where something really strange happens.

lemma "⋀z. A z ∧ B"
apply(
match concl in "f x y" for f x y ⇒ ‹
match my_thms in R:"⋀x :: _ :: type. P x ⟹ f u v" for P u v ⇒ ‹
print_fact R,
print_fact R[of undefined],
rule R[of undefined]
›
›
)

If I name the bound variable to be matched by a schematic, print_fact R outputs something
like foo ?x ?y ?x ⟹ ?x ∧ ?y whereas the matched rule is "foo x y z ⟹ z ∧ y", i.e., it
unifies x with z. If I rename the bound variable !!x to !!z, the rule stays in its general
form. Still, the method still fails, because the variable instantiations are done in a
strange order (not in the order in which they occur in the theorem).

I do not know the form of the assumption of my matched theorem in my real use case, I just
know that there is a variable in the assumptions and that I want to instantiate the first
one. How can I express this in Eisbach? I tried to play with "!!x :: _ :: type. PROP P x
==> PROP Q" but this did not match anything I tried.

Best,
Andreas

Email Gateway (Aug 22 2022 at 09:24):

From: Daniel Matichuk <daniel.matichuk@nicta.com.au>
Hi Andreas,

On 24 Apr 2015, at 2:03 am, Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch> wrote:

Hi Daniel,

Thanks for the reply. Unfortunately, I cannot get this to work at all. Your suggested pattern "!!P. PROP P ==> f u v" raises a type error. After several failed attempts, I am now stuck at the following where something really strange happens.

lemma "⋀z. A z ∧ B"
apply(
match concl in "f x y" for f x y ⇒ ‹
match my_thms in R:"⋀x :: _ :: type. P x ⟹ f u v" for P u v ⇒ ‹
print_fact R,
print_fact R[of undefined],
rule R[of undefined]
›
›
)

If I name the bound variable to be matched by a schematic, print_fact R outputs something like foo ?x ?y ?x ⟹ ?x ∧ ?y whereas the matched rule is "foo x y z ⟹ z ∧ y", i.e., it unifies x with z. If I rename the bound variable !!x to !!z, the rule stays in its general form.

It's likely you've uncovered an issue with variable clashes here, picking a fresh name for the bound variable seems to result in the expected behaviour. I imagine I've overlooked some schematic index management somewhere, I'll look into it ASAP.

Still, the method still fails, because the variable instantiations are done in a strange order (not in the order in which they occur in the theorem).

The method instantiations are done in the order that they are declared in the match. So in your example "undefined" will be bound to whatever x matches against, regardless of the form of the actual rule.
It is precisely equivalent to writing "R[where x=undefined]".

I do not know the form of the assumption of my matched theorem in my real use case, I just know that there is a variable in the assumptions and that I want to instantiate the first one. How can I express this in Eisbach? I tried to play with "!!x :: _ :: type. PROP P x ==> PROP Q" but this did not match anything I tried.

The notion of the "first" schematic is not something that can be described with a match pattern. Again, this is perhaps some indication that a more expressive pattern language is needed.
Your pattern should backtrack over all possible ways some "P" can be bound such that "x" is bound to a schematic from the theorem, within these backtracking options will be the one that happens to be first.

However I believe this backtracking is not happening in your specific example, and I think it's actually a related issue to the other one. Bear with me while I investigate.

Best,
Andreas

On 23/04/15 03:48, Daniel Matichuk wrote:

Hi Andreas,

Unfortunately the ITP paper is slightly out of date, specifically regarding rule instantiation. The "match" method is now meant to guard rule instantiation at run-time by ensuring that the matched theorem(s) has
the correct slots available. This is done by using meta-quantifiers in your patterns. Specifically the semantics of a match are that a "for-fixed" variable may match anything, whereas a meta-quantified variable
must match against a schematic. So in your example, assuming you wish to instantiate "P", your pattern should be "!!P. PROP P ==> f u v" for u v". This statically ensures that any matched rule can be instantiated appropriately (so the failure occurs in the match, rather than the rule instantiation).
The motivation for this requirement is perhaps more clear when using match to define an Eisbach method, rather than when used in-place.

It's also worth noting that a pattern like "f x y" for f x y will produce a large set of possible matches, due to "match" using the unifier internally. The usual best-practice approach is to add type annotations to your pattern to restrict the matches.
There is some argument for extending the match pattern language to support more precise term deconstruction, but I'm waiting to see more use cases before adding more complexity.

On 20 Apr 2015, at 10:49 pm, Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch> wrote:

Dear Eisbach developers,

First of all, thanks for designing and implementing Eisbach. Unfortunately, I am struggling with instantiating variables in rules when I write my own proof methods in Eisbach.

Abstractly,
1. I select a rule R by matching a list L of theorems against a term, and
2. then instantiate a variable in R with a term obtained by matching the conclusion against a pattern.

Unfortunately, I always get the error "More instantiations than variables in theorem" although all the theorems in the list L contain at least one variable. I do not know where this error comes from. Below is a small example:

theory Scratch imports Main "~~/src/HOL/Eisbach/Eisbach_Tools" begin

consts foo :: "'a ⇒ 'a ⇒ 'a ⇒ bool"
lemma my_thms: "foo x y z ⟹ z ∧ y" "foo x y y ⟹ x ∧ z" sorry

lemma "⋀z. A z ∧ B"
apply(
match concl in "f x y" for f x y ⇒ ‹
match my_thms in R:"PROP P ⟹ f u v" for P u v ⇒ ‹
rule R[of x]
›
›
)
oops

end

Thanks for any help,
Andreas

PS: I am trying to build something similar to the apply_split method in the Eisbach paper presented at ITP2014.

---

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

Last updated: Nov 21 2024 at 12:39 UTC