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



Hi Andreas,


> On 24 Apr 2015, at 2:03 am, Andreas Lochbihler <andreas.lochbihler at 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 at 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.
>> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.