Re: [isabelle] Problem with schematic variables, subst and flex-flex pairs



Hi Peter,

Peter Lammich wrote:
Consider the following subgoal

1. "!!x y a b. f ((x = y) = (a = b)) = ?P x y a b" now, I do: apply
(subst (1 3) eq_commute)

and get: goal (1 subgoal): 1. !!x y a b. f ((y = x) = (b = a)) = ?P6
x x x y y y a a a b b b flex-flex pairs: %x y a b. ?P6 x x x y y y a
a a b b b =?= %x y a b. ?P4 x x y y a a b b

In my concrete proof, ?P also occurs in other subgoals, it is the
result of applying exI to a goal of the form EX P. a1=P & a2=P. The
list of flex-flex pairs and newly introduced schematics with duplicate parameters gets very long until Isabelle only spits out
tons of trace output and does not terminate any more.

What happens here?

I think this is caused by Isabelle doing gratuitous lifting of
parameters as it applies substitution. Lifting is necessary if some part of the proof state not under the bound parameters also contains the meta-variable (also called schematic variables) - which is the general assumption when Isabelle performs resolution.

If you do fix your parameters to free variables, then you get something
more reasonable:

lemma "(A ?P) ==> f ((x = y) = (a = b)) = ?P x"
apply (subst (1 3) eq_commute)
...
fixed variables: A, f, x, y, a, b
goal (lemma, 1 subgoal):
 1. A ?P ==> f ((y = x) = (b = a)) = ?P2 x
flex-flex pairs:
  ?P2 x =?= ?P1 x
  ?P1 x =?= ?P x

But, depending on your context (other subgoals, assumptions etc), that
may give incorrect results as it allows meta-variables to capture the
bounds (which are being represented as Frees) - if the meta-variable
also occurs outside of the scope of the parameters and is instantiated
to a term containing the bound variable, you end up with a badly formed
instantiation w.r.t. the context.

However, I think something funny is going on in the substitution tactic here: there seems to be an extra flex-flex pair, and I didn't think that
was necessary, and is probably also the reason for the duplication of
the bound variables... I remember doing lifting by hand very carefully, but it seems the code has changed slightly... I also vaguely recall not being sure if I could get rid of extra lifting in the tactic without doing something very different... actually I think I remember discussing it in 2004... I'll look through my old email and I'll have a think about it again... thanks for reminding me of the issue :)

Is there a way to get rid of introducing new schematics during subst,
and get the desired subgoal: 1. !!x y a b. f ((y = x) = (b = a)) = ?P
x y a b

Something that simplifies the subgoal after each substitution step
would also be ok.

In the meantime, if you can't just fix the parameters, a horrible hack is to instantiate your meta-variables to lambda terms that throw away duplicated arguments. You then simply apply this after substitution.

best,
lucas

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






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