# 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.