Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Higher-order matching against schematic variables

Email Gateway (Aug 18 2022 at 16:29):

From: Michael Chan <mchan@inf.ed.ac.uk>
Hi all,

I have a question with higher-order matching against schematic
variables. I can't figure out why the pattern trm1 can't be matched
against lem if lem was "A x y --> x y = 0". However, if the RHS contains
constants instead, e.g., "A x y --> g a = 0", a matcher is found. Since
x and y have the same types of g and a respectively, how come there
isn't a matcher in the former case? A difference is that x and y are
schematic variables, but why can't schematic variables be matched against?

Here's the code:

locale A =
fixes f :: "nat => nat"
and a :: nat
assumes ax: "f a = 0"

consts
g :: "nat => nat"
a :: nat

lemma lem: "A x y --> x y = 0"
sorry

ML {*

val trm1 = term_of @{cpat "?P --> (?f::((?'a=>?'b)=>?'c)) ?stuff = ?v"};
val trm2 = Thm.prop_of @{thm lem};

val mtch_seq = let
val init = Envir.empty 0
val ctxt = @{context}
val (Const ("Trueprop",_) $ trm2) = Thm.prop_of (ProofContext.get_thm
ctxt "lem")
in
Unify.matchers @{theory} [(trm1,trm2)]
end;

val seq as SOME (mtch,_) = nthseq 0 mtch_seq;
pretty_env @{context} (Envir.term_env mtch);
*}

Thanks
Michael

Email Gateway (Aug 18 2022 at 16:29):

From: Michael Chan <mchan@inf.ed.ac.uk>
On 18/11/10 16:07, Lawrence Paulson wrote:

I can't see the answer to this, but something complicated is going on when you match (?f::((?'a=>?'b)=>?'c)) ?stuff against x y where x :: nat => nat.

Thanks, Larry. Indeed, even without the predicate, it gives the same
problem when using that pattern, i.e.

lemma lem: "g a = 0"
sorry

vs

lemma lem: "(x::nat=>nat) y = 0"
sorry

Now, if we instead use a simpler pattern:

val trm1 = term_of @{cpat "(?f::?'a=>?'b) ?stuff = ?v"};

matching it against "g a = 0" gives 4 matchers:

1. [?f::nat => nat := %a::nat. a, ?v::nat := 0::nat, ?stuff::nat := g a]

2. [?f::nat => nat := g, ?v::nat := 0::nat, ?stuff::nat := a]

3. [?f::?'a => nat := %b::?'a. g a, ?v::nat := 0::nat,
   ?stuff::?'a := ?stuff::?'a]

4. [?f::?'a => ?'b := g, ?v::?'b := 0::nat, ?stuff::?'a := a]

But matching it against "(x::nat=>nat) y = 0", gives only 1 matcher:

1. [?f::?'a => ?'b := ?x::nat => nat, ?v::?'b := 0::nat,
   ?stuff::?'a := ?y::nat]

which is of the same shape of the first lemma's 4th matcher.

Perhaps the higher-order matcher somehow fails, since 1. and 3. should
be returned by it. 2. is essentially 4., but with the schematic type
variables instantiated. Now, is 4. a valid matcher even when ?'a and ?'b
can be clearly instantiated (to become 2.)? If it is valid, isn't it
redundant to have a separate matcher with the type variables uninstantiated?

Thanks
Michael

Larry Paulson

On 18 Nov 2010, at 13:37, Michael Chan wrote:

Hi all,

I have a question with higher-order matching against schematic variables. I can't figure out why the pattern trm1 can't be matched against lem if lem was "A x y --> x y = 0". However, if the RHS contains constants instead, e.g., "A x y --> g a = 0", a matcher is found. Since x and y have the same types of g and a respectively, how come there isn't a matcher in the former case? A difference is that x and y are schematic variables, but why can't schematic variables be matched against?

Here's the code:

locale A =
fixes f :: "nat => nat"
and a :: nat
assumes ax: "f a = 0"

consts
g :: "nat => nat"
a :: nat

lemma lem: "A x y --> x y = 0"
sorry

ML {*

val trm1 = term_of @{cpat "?P --> (?f::((?'a=>?'b)=>?'c)) ?stuff = ?v"};
val trm2 = Thm.prop_of @{thm lem};

val mtch_seq = let
val init = Envir.empty 0
val ctxt = @{context}
val (Const ("Trueprop",_) $ trm2) = Thm.prop_of (ProofContext.get_thm ctxt "lem")
in
Unify.matchers @{theory} [(trm1,trm2)]
end;

val seq as SOME (mtch,_) = nthseq 0 mtch_seq;
pretty_env @{context} (Envir.term_env mtch);
*}

Thanks
Michael

--
Postal Address: School of Informatics, University of Edinburgh,
Room 2.05, Informatics Forum, 10 Crichton Street,
Edinburgh EH8 9AB, UK.
Telephone Number: +44-131-651-3077,
Fax Number: +44-131-650-6899,
Email: M.Chan@ed.ac.uk
Web Page: http://homepages.inf.ed.ac.uk/mchan/

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Email Gateway (Aug 18 2022 at 16:30):

From: Michael Chan <mchan@inf.ed.ac.uk>

Perhaps the higher-order matcher somehow fails, since 1. and 3. should
be returned by it. 2. is essentially 4., but with the schematic type
variables instantiated. Now, is 4. a valid matcher even when ?'a and ?'b
can be clearly instantiated (to become 2.)? If it is valid, isn't it
redundant to have a separate matcher with the type variables
uninstantiated?

I can confirm that the first lemma's matcher 4. and the second lemma's
only matcher are results of the FO matcher. So, I guess the above
question becomes: how come the FO matcher doesn't instantiate the type
variables? Of course, this is a different question to why the HO matcher
doesn't return matchers to the second lemma.

Michael

Thanks
Michael

Larry Paulson

On 18 Nov 2010, at 13:37, Michael Chan wrote:

Hi all,

I have a question with higher-order matching against schematic
variables. I can't figure out why the pattern trm1 can't be matched
against lem if lem was "A x y --> x y = 0". However, if the RHS
contains constants instead, e.g., "A x y --> g a = 0", a matcher is
found. Since x and y have the same types of g and a respectively, how
come there isn't a matcher in the former case? A difference is that x
and y are schematic variables, but why can't schematic variables be
matched against?

Here's the code:

locale A =
fixes f :: "nat => nat"
and a :: nat
assumes ax: "f a = 0"

consts
g :: "nat => nat"
a :: nat

lemma lem: "A x y --> x y = 0"
sorry

ML {*

val trm1 = term_of @{cpat "?P --> (?f::((?'a=>?'b)=>?'c)) ?stuff = ?v"};
val trm2 = Thm.prop_of @{thm lem};

val mtch_seq = let
val init = Envir.empty 0
val ctxt = @{context}
val (Const ("Trueprop",_) $ trm2) = Thm.prop_of (ProofContext.get_thm
ctxt "lem")
in
Unify.matchers @{theory} [(trm1,trm2)]
end;

val seq as SOME (mtch,_) = nthseq 0 mtch_seq;
pretty_env @{context} (Envir.term_env mtch);
*}

Thanks
Michael

--
Postal Address: School of Informatics, University of Edinburgh,
Room 2.05, Informatics Forum, 10 Crichton Street,
Edinburgh EH8 9AB, UK.
Telephone Number: +44-131-651-3077,
Fax Number: +44-131-650-6899,
Email: M.Chan@ed.ac.uk
Web Page: http://homepages.inf.ed.ac.uk/mchan/

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Last updated: Nov 21 2024 at 12:39 UTC