Re: [isabelle] Handling of invalid type variable names on ML level



Dear Makarius,

thank you for the explanation. I was not aware the Variable.variant_fixes
and friends are also for type variables, this is useful to know. (Perhaps
the implementation manual should mention this more explicitly.)

Concerning my original confusion: I was wondering how it can be that fixing
the variable "a" influences the behavior of the (invalid) type variable
"a". I think the answer is that, while type and regular variables are
separate, the table that remembers what variables are fixed is shared by
type and regular variables. Thus fixing the regular variable *a* also fixes
the (invalid) type variable *a*. Is that correct?

I will try to follow your programming guidelines. But one thing is unclear
to me in that context: Goal.prove has an argument xs (instantiated with
["l"] in my example). I thought I can use xs with a hardcoded name because
Goal.prove will locally fix that variable. Is that incorrect? If it's
incorrect, I don't understand how the argument xs can be used, because if I
get a fresh name via Variable.variant_fixes and supply this name in the
argument xs, then I get an error that the variable is already fixed. So, I
see no way how to use the xs argument. (Of course, I can always avoid using
that argument by using Variable.export after creating a theorem using
Goal.prove, but then what is xs for?)

Best wishes,
Dominique.




On 25 May 2018 at 13:44, Makarius <makarius at sketis.net> wrote:

> On 25/05/18 16:51, Dominique Unruh wrote:
> >
> > I am not sure the following situation should be considered a bug or not,
> > since it occurs only when using Isabelle incorrectly. But I feel that it
> > probably indicates that invalid input is not detected in time, and it may
> > lead to very hard to understand problems (starting from a typo). So I
> just
> > explain the problem and leave it to the Isabelle-experts to decide
> whether
> > it indicates a real problem or not.
>
> This preface already points in the direction of a "general user error",
> or rather a mismatch of expectations vs. the reality of how the system
> works.
>
>
> > The problem is exhibited by the theory below. But in a nutshell, we have
> > the following situation:
> >
> >    - It is possible to prove a theorem with a type variable called *a*
> (not
> >    *'a*). I understand that I should not do that, of course. But there is
> >    no error when proving the theorem.
> >    - Then, if we try to use OF with that theorem, we get unexpected
> >    failures. But only if *a* is the name of a fixed variable (not type
> >    variable).
> >
> > I guess that type variable *a* should probably just be rejected when
> trying
> > to prove the theorem. But even if not, it is surprising that the
> existence
> > of a fixed variable *a* makes a difference since I would have assumed
> that
> > free variables and free type variables have completely independent name
> > spaces.
>
> There are many different notions of names, variables, contexts etc. and
> a lot of system infrastructure to help getting Isabelle/ML tool
> implementations right. The "implementation" manual explains some of this
> -- beyond that it is important to find good examples and study them
> carefully.
>
> In general, the programming interfaces are much less typed than one
> might expect. As a start you should think of Isabelle/ML is a variant of
> LISP with a few static types to avoid utter nonsense. It is important to
> observe certain disciplines and high-level ideas -- the system often
> does not check or cannot check for that.
>
> For type and term variables, it is usually already an error if literal
> names appear in the ML text. There are operations to invent fresh
> variables relative to a certain context -- and using them is mandatory
> to make things work in arbitrary contexts. So it is unlikely to make a
> typo of "a" vs. "'a" in ML, because both are already wrong as literal
> variable names in the source.
>
>
> > val ctx = @{context}
>
> First note that there are hard and fast naming conventions for certain
> basic Isabelle/ML types (see chapter 0 in the "implementation" manual),
> in particular the value above needs to be called "ctxt". Otherwise there
> is no chance to understand the source in more complex situations, when
> there is a serious problem with contexts (the present example is not
> serious yet). The Highlighter of Isabelle/jEdit can be helpful here,
> when sources are written in a standard form.
>
> > fun tac {context=ctx, ...} = ALLGOALS (simp_tac ctx)
>
> At this spot you are binding the same name "ctx" again: this shadowing
> makes it difficult to understand and change the sources later. Anyway,
> the forward definition of "tac" is better inlined into the Goal.prove
> invocation, it makes the source more readable and robust.
>
> Here is that snippet in standard form, optimized for readability:
>
> ML ‹
> val ctxt = @{context}
> val T = TFree ("a", @{sort type})
> val l = Free ("l", T)
> val thm =
>   Goal.prove ctxt ["l"] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (l, l)))
>     (fn {context = ctxt', ...} => ALLGOALS (simp_tac ctxt'))
> ›
>
> Now the development of the local ctxt into ctxt' becomes clear: the
> latter is the "eigen-context" of the goal statement.
>
>
> After inspecting contexts, I routinely look at variables and terms vs.
> these contexts. Above Goal.prove is applied to some proposition that is
> not declared in the context (e.g. with Variable.declare_term). Omitting
> that in real applications can lead to really confusing situations with
> the implicit Hindley-Milner polymorphism and other corner cases.
>
> See also section "6.1 Variables" in the "implementation" manual,
> including its minimal examples. With that you might produce fresh
> type/term variables robustly, such that the whole question from the
> start disappears.
>
>
>         Makarius
>



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