Email Gateway (Aug 18 2022 at 12:25): Email Gateway (Aug 18 2022 at 12:25):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
Hi Peter,
Peter Lammich wrote:
Consider the following subgoal
- "!!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 bIn 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 bSomething 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
Email Gateway (Aug 18 2022 at 12:25):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Peter Lammich wrote:
Some years ago I wrote some code based on the "conversionals" of HOL, to
do this sort of thing more easily. Thus, for example,
Goal "!!x y a b. f ((x = y) = (a = b)) = P x y a b" ;
by ((Conv.CONV_TAC o Conv.TDSTOP_CONV) (eqc eq_commute)) ;
(applies conversions top-down, but stopping (ie, not descending into a
resulting term upon success)
!!x y a b. P x y a b = f ((x = y) = (a = b))
by ((Conv.CONV_TAC o Conv.TOPDN_CONV) (eqc eq_commute)) ;
(applies conversions top down)
!!x y a b. f ((b = a) = (y = x)) = P x y a b
by ((Conv.CONV_TAC o Conv.BUSTOP_CONV) (eqc eq_commute)) ;
(applies conversions bottom up, stopping upon any success)
!!x y a b. f ((a = b) = (x = y)) = P x y a b
With these, I usually don't need the following, which makes a conversion
succeed only the first and third times it would otherwise have succeeded).
by ((Conv.CONV_TAC o Conv.TOPDN_CONV o Conv.NTH_CONV [1,3]) (eqc
eq_commute)) ;
Incidentally, I found my code doesn't work with schematic variables (I
don't know why), so to use it you'd have to wrap your goal in
freeze_thaw. Which would presumably solve your problem anyway.
But if you're interested in my code, it's at
http://users.rsise.anu.edu.au/~jeremy/isabelle/2005/gen/{conv.ML,eq_conv.ML}
Regards,
Jeremy
Last updated: May 03 2024 at 04:19 UTC