Re: [isabelle] SELECT_GOAL and schematic variables



Unfortunately, this problem does not only affect the (admittedly
low-level) SELECT_GOAL, but also high-level proof scripts, as the
following example demonstrates:

  inductive P for x where I: "P x"
  lemma J: "P (\<lambda>_. R)" by (rule I)

  schematic_lemma "\<And>a b. P (?R a) \<or> P (?R)" "TERM ?R4"
    apply (rule disjI2, rule J) []
*** exception TYPE raised (line 109 of "envir.ML"):
*** Variable "?R4" has two distinct types
*** 'c
*** 'd

note that everything works fine without the [].

--
  Peter



On Fr, 2013-03-22 at 15:11 +0000, Lawrence Paulson wrote:
> I'm afraid that I really can't answer this question without a time machine.
> 
> In the early days, I must have introduced SELECT_GOAL in the context of some specific application where it worked fine. Then it got put in the standard libraries of tacticals and more or less forgotten. I know that a lot of derivations that involve new variables in sub-proofs can go wrong as you describe. The usual method of getting around such problems was to freeze variables prior to applying the tactic, thawing them afterwards. That was a hack, but it generally worked. My impression is that Makarius has replaced such trickery by more robust methods, but it's possible that quite a lot about old code is still there and running. I'm not sure about the current best practice for dealing with this sort of situation.
> 
> Larry Paulson
> 
> 
> On 21 Mar 2013, at 16:25, Peter Lammich <lammich at in.tum.de> wrote:
> 
> > Hi all,
> > 
> > I recently spotted down a problem with SELECT_GOAL and schematic
> > variables. If new schematic variables are produced in the proof of the
> > selected goal, their names may clash with existing schematics in the
> > outer proof state, resulting in unexpected error messages:
> > 
> >  inductive P for x where I: "P x"
> >  lemma J: "P (\<lambda>_. R)" by (rule I)
> > 
> >  schematic_lemma "\<And>a. P (?R a) \<or> P (?R)" "TERM ?R3"
> >    apply -
> >    apply (tactic {* SELECT_GOAL (
> >      rtac @{thm disjI2} 1 THEN rtac @{thm J} 1 
> >      (*THEN PRIMITIVE zero_var_indexes*)
> >      THEN print_tac "Proof state after inner tactic"
> >      ) 1
> >      *})
> > 
> > *** exception TYPE raised (line 109 of "envir.ML"):
> > *** Variable "?R3" has two distinct types
> > *** 'c
> > *** 'd
> > 
> > What happened here is that the tactic inside SELECT_GOAL produced the
> > proof state: "\<And>a b. P ?R3 \<or> P (\<lambda>_. ?R3)"
> > And when retrofitting this into the outer proof state, ?R3 happens to
> > clash with the ?R3 there.
> > 
> > 
> > Moreover, if one directly changes schematic variables that occur in the
> > selected goal, like the "zero_var_indexes" does in the commented out
> > line of the example, the unifier runs havoc and produces errors like:
> > 
> > *** mk_ff_list
> > *** At command "apply" (line 9 of
> > "/home/lammich/lehre/praktWS1112/cava/Libs/Refine/Autoref/Scratch.thy")
> > 
> > (I also got some exceptions about "Var name confusion" from the unifier,
> > that I cannot reproduce any more)
> > 
> > 
> > These observations result in two main questions:
> >  1. What are the conventions that tactics must stick to when
> > instantiating schematic variables? E.g. is it ok to do 
> >  PRIMITIVE zero_var_indexes or not?
> > 
> >  2. Is SELECT_GOAL implemented correctly and was never supposed to 
> > 	work with schematics, or should it be fixed?
> > 
> > 
> > Regards and thanks for any comments/workarounds on this,
> >  Peter
> > 
> > 
> > 
> 






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