Email Gateway (Aug 22 2022 at 17:11): Email Gateway (Aug 22 2022 at 17:11):From: Dominique Unruh <unruh@ut.ee>
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.
Email Gateway (Aug 22 2022 at 17:12):From: Makarius <makarius@sketis.net>
On 25/05/18 21:03, Dominique Unruh wrote:
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?
The aspect of the context that is relevant here is Name.context /
Variable.names_of. That sub-context throws type and term variables into
one pot, and implicitly relies on other policies that ensure that they
are normally not in conflict.
As you can see in the Variable module, there are further intermediate
states of variables, corresponding to declare_names,
declare_constraints, declare_term etc. -- the "implementation" manual
explains some of this.
It is particularly important to develop an intuition how implicitly
declared type variables vs. explicitly fixed term variables give you
Hindley-Milner polymorphism in the end. That is the main purpose of the
whole affair of managing names formally.
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.
Goal.prove provides a programming interface that corresponds to Isar
"have props if asms for xs", but Goal.prove uses
Variable.add_fixes_direct without any implicit name invention. The names
that you provide need to be "free" in the sense that they can be fixed
in the current context, e.g. because they were invented properly beforehand.
Apart from these explicit term variables, you need to take care about
type variables occurring in the propositions: Variable.declare_term does
that, it ensures that the term is syntactically known to the context.
Makarius
Email Gateway (Aug 22 2022 at 17:22):From: Dominique Unruh <unruh@ut.ee>
Hi,
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.
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.
theory Test
imports Main
begin
lemma x: fixes c :: int assumes "c = d" shows "True" ..
context fixes a :: int begin
ML {*
val ctx = @{context}
val T = TFree(("a"),@{sort type}) (* Note the incorrect "a" instead of "'a"
*)
val l = Free(("l"),T)
val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (l,l)) (* prop = "l=l" *)
fun tac {context=ctx, ...} = ALLGOALS (simp_tac ctx)
val thm = Goal.prove ctx ["l"] [] prop tac (* proving prop *)
val _ = @{thm x} OF [thm] (* Fails with "no unifiers". But succeeds if
"fixes a" above is "fixes b" *)
*}
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 17:22):From: Makarius <makarius@sketis.net>
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
Last updated: Nov 21 2024 at 12:39 UTC