Email Gateway (Aug 19 2022 at 13:37): Email Gateway (Aug 19 2022 at 13:37):From: Van Staden Stephan <stephan.vanstaden@inf.ethz.ch>
Dear all,
In Isabelle/jEdit 2013-2, the following locale works fine:
locale Test =
fixes pred :: "'a set ⇒ 'a rel ⇒ bool"
assumes a1: "pred S R"
(* assumes a2: "pred R S" *)
begin
lemma pred_is_UNIV: "pred A B"
by (metis a1)
end
However, uncommenting assumption a2 gives me the following error:
Type unification failed
Type error in application: incompatible operand type
Operator: pred :: 'a set ⇒ ('a × 'a) set ⇒ bool
Operand: R :: ('a × 'a) set
Page 2 of the locale tutorial seems to suggest that this is a bug. Or should I expect this behaviour?
Thanks in advance!
Stephan
Email Gateway (Aug 19 2022 at 13:38):From: John Wickerson <johnwickerson@cantab.net>
The error seems sensible to me. In a1, R is a relation, and in a2 it's a set. Or maybe I'm missing something?
John
Email Gateway (Aug 19 2022 at 13:38):From: Van Staden Stephan <stephan.vanstaden@inf.ethz.ch>
It's a free variable in each assumption. I would expect the assumptions to be:
(!!S R. pred S R) /\ (!!S R. pred R S)
but what happens is apparently:
(!!S R. pred S R /\ pred R S)
The question is whether the free variables in an assumption are local to the assumption or not. The locale tutorial suggests that they should be local, but maybe I'm wrong.
Thanks,
Stephan
Email Gateway (Aug 19 2022 at 13:38):From: Makarius <makarius@sketis.net>
The quantification in the first form is what happens logically, but
syntactically the "free" variables share the same scope of the whole
specification. Thus you need to use explicit binders, or evade the
problem by renaming variables apart.
Note that "Test" is a bad name for a locale: lower-case is normally used.
Likewise, theory names are usually capitalized words (in singular),
separated by underscore. (You did not show that in the example, but I
guess > 50% that you've had a lowercase test.thy here, or was it just
Scratch.thy?)
Makarius
Email Gateway (Aug 19 2022 at 13:38):From: bnord <bnord01@gmail.com>
Do you know anything about the intended audience for his development
that you think the "default" Isabelle style is appropriate for him? Or
is it just the objectively "best" style?
Best
Benedikt
Email Gateway (Aug 19 2022 at 13:38):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
For the record: I assume you're perfectly aware that conjunction (which is incidentally written &&& if you want the metalogic version) distributes over universal quantification. And since Isabelle magically transforms universals in schematics, you effectively get independent theorems "pred ?S ?R" and "pred ?R ?S", only that there's an additional type constraint that all occurrences of R (resp. S) have the same type.
The locales tutorial is not entirely clear on this point. If "means" refers to semantics, what is written there is not inaccurate.
Jasmin
Email Gateway (Aug 19 2022 at 13:38):From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
On 21.02.2014 17:33, Makarius wrote:
On Fri, 21 Feb 2014, Van Staden Stephan wrote:
It's a free variable in each assumption. I would expect the
assumptions to be:(!!S R. pred S R) /\ (!!S R. pred R S)
but what happens is apparently:
(!!S R. pred S R /\ pred R S)
The question is whether the free variables in an assumption are local
to the assumption or not. The locale tutorial suggests that they
should be local, but maybe I'm wrong.The quantification in the first form is what happens logically, but
syntactically the "free" variables share the same scope of the whole
specification. Thus you need to use explicit binders, or evade the
problem by renaming variables apart.
Thanks, okay, got it! But for the record I can add that it's not what I
expected.
Note that "Test" is a bad name for a locale: lower-case is normally
used. Likewise, theory names are usually capitalized words (in
singular), separated by underscore. (You did not show that in the
example, but I guess > 50% that you've had a lowercase test.thy here,
or was it just
Scratch.thy?)
Sorry, just wrote a quick and dirty example to show what I found
surprising. I don't know what it has to do with the issue really, but I
stored the example in Test.thy.
Thanks again,
Stephan
Email Gateway (Aug 19 2022 at 13:38):From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
It's this type constraint that surprised me. The post by Makarius
explains it, but as a user I would prefer to have complete separation.
Is there a compelling reason why it's implemented as it is?
Thanks,
Stephan
Email Gateway (Aug 19 2022 at 13:39):From: Peter Lammich <lammich@in.tum.de>
I frequently run into another instance of this problem, when writing
something like:
lemma foo:
"x & y --> x"
"x = y --> f x = f y"
Note that foo(2) is: "?x::bool = ?y ...", which is usually not
what was intended.
Email Gateway (Aug 19 2022 at 13:39):From: Lawrence Paulson <lp15@cam.ac.uk>
Clearly every instance of a variable in a single formula must have the same type, and it’s natural to expect that every instance in a list of formulas should also have the same type. The alternative would be very confusing for readers, also in informal mathematics.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:39):From: Makarius <makarius@sketis.net>
The observation by Larry is correct. He probably still remembers the time
when type-inference would only range over each term separately, causing
many strange effects and surprises.
When you write a simultaneous statement as above, or a long statement with
fixes/assumes/shows, the scope of free variables and their types ranges
over the whole clause. This is the intended way -- we have required many
years to get there.
A slightly different situation occurs in conceptually separate scopes that
happen to be written with free variables that share the type-inference
scope, but are logically separate. There are two main situations for
this: the 'obtains' statement with several disjuctive branches, and the
implicit quantification of locale expressions that were encountered here.
Here I would prefer to keep type-information separate, according to the
logical structure.
When I introduced the latter locale convenience about 12 years ago, I was
aware of the snag with type-inference, and also aware of the lack of any
systematic documentation of type-inference in the Isabelle manuals (even
until today). Approximately every 5 years some user stumbles over that
detail. The manuals could be improved at some point, but it is probably
more helpful to give more feedback about scopes and type-inference errors
in the Prover IDE.
Makarius
Email Gateway (Aug 19 2022 at 13:39):From: Makarius <makarius@sketis.net>
Locales in capitals and theories in lower-case probably stems from Java
(classes vs. packages), but the world is bigger than Java.
The objectively best style for Isabelle is the one devised by the people
who implemented qualified name spaces and locales, type classes and more
over the years. By observing the very simple scheme of Theory.locale.item
or Theory.class.item, you get more robust name space accesses for free
(there is no cost to follow a simple convention).
Just a few days ago, I have mentally revisited the situation for qualified
theory names (by the session name, which is also capitalized), and
completion in the Prover IDE for all these names. So that is still
relevant, even though people tend to become forgetful. Maybe I should
make the Prover IDE inform the user about naming conventions, just to save
time explaining them again and again.
Makarius
Email Gateway (Aug 19 2022 at 13:39):From: Makarius <makarius@sketis.net>
Feasibility and complexity of implementation. In order to move locales
once again some steps forward, one should probably give up rarely used old
features like 'defines' and 'constrains' (which have heavy weight and
little real applications).
Makarius
Email Gateway (Aug 19 2022 at 13:39):From: Van Staden Stephan <stephan.vanstaden@inf.ethz.ch>
Thanks for the explanations. It seems wise to keep it the way it is.
All the best,
Stephan
Email Gateway (Aug 19 2022 at 13:39):From: Makarius <makarius@sketis.net>
The 'defines' element predates proper 'definition (in loc)'. Having
axiomatic specifications that are intertwined with quasi-definitional ones
is conceptually very complex, and actually a mess. I know that people
sometimes do that, but one would have to look very closely if that is
really required: normally you should be able to pull out the auxiliary
definitions before the locale specifications. If we would have
understood localized definitions already in 1999, this problem would not
exist, because 'defines' would have never been introduced.
The 'constrains' element is easier to get rid of. I would like to see
some constructive proofs where you "need to constrain types", as you say.
This is usually just a workaround to specify locale type arguments, but if
that would be supported directly, the need would go away.
Anyway, we have just the default situation of inertia: after many years of
getting used to some not-quite-right feature, users find it hard to go
beyond it. This is why certain problems cannot be solved easily, and we
need to explain new users why some things are a bit odd.
Makarius
Email Gateway (Aug 19 2022 at 13:40):From: Makarius <makarius@sketis.net>
Maybe you have actually missed the important locale expression
improvements by Clemens Ballarin from Isabelle2009. See the NEWS, e.g.
this one:
- In locale expressions, instantiation replaces renaming. Parameters
must be declared in a for clause. To aid compatibility with previous
parameter inheritance, in locale declarations, parameters that are not
'touched' (instantiation position "_" or omitted) are implicitly added
with their syntax at the beginning of the for clause.
In most situations a locale expression suffix "for x :: T" can be used to
instantiate types in imports. I had cleaned up AFP in this respect
already some years ago, but in various newer entries old 'constrains'
seem to have come back. Time for spring cleaning?
Makarius
Email Gateway (Aug 19 2022 at 13:40):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Actually, yes this may do it. I’ve used it for new proofs, but somehow managed not to make the connection.
Let me try this out on the old proofs.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 13:40):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
I know one use case where constrains is more convenient than parameter instantiation with
for, namely to revert the renaming of type variables. I want type variables to have
sensible names like 'state, not just 'a, 'b, 'c, 'd. Unfortunately, locale inheritance
always renames them to 'a, 'b, 'c, etc., so I rename them back. Of course, this can be
done with a for clause, too. But a for clause drops the mixfix syntax associated with the
parameter, so would have to redeclare it; with constrains, I need not. And for consistency
reasons, I prefer not to redeclare notation if it's not necessary. And if locale
inheritance did not rename type variables, I'd not need constrains at all and be much happier.
Andreas
Email Gateway (Aug 19 2022 at 13:41):From: Makarius <makarius@sketis.net>
On Tue, 25 Feb 2014, Andreas Lochbihler wrote:
On 24/02/14 23:05, Makarius wrote:
The 'constrains' element is easier to get rid of. I would like to see
some constructive proofs where you "need to constrain types", as you
say. This is usually just a workaround to specify locale type
arguments, but if that would be supported directly, the need would go
away.
I know one use case where constrains is more convenient than parameter
instantiation with for, namely to revert the renaming of type variables.
I want type variables to have sensible names like 'state, not just 'a,
'b, 'c, 'd. Unfortunately, locale inheritance always renames them to 'a,
'b, 'c, etc., so I rename them back.
This is an old misunderstanding: there is no "locale inheritance", but
locale import within a certain language of locale expressions. That works
via Hindley-Milner type-inference, so the result typing is most-general
and in canonical form. Whence the (fortunate) renaming. Type-inference
was not there in very early versions of locales, which made them hardly
usable, and that was indeed unfortunate.
Of course, this can be done with a for clause, too. But a for clause
drops the mixfix syntax associated with the parameter, so would have to
redeclare it; with constrains, I need not. And for consistency reasons,
I prefer not to redeclare notation if it's not necessary. And if locale
inheritance did not rename type variables, I'd not need constrains at
all and be much happier.
Nothing of this is new in the argument, we've had that already several
years ago.
What you merely need here is some way to specified the implicit type
arguments of a locale explicitly. That would also help in situations of
"hidden polymorphism", i.e. locales with excess type parameters that are
not mentioned in any term parameter. The existing implementation is a bit
weak here: it emits a warning and leaves the user confused, hoping that
nothing bad happens later.
These fine-points could have been sorted out many years ago, if there
would not be this "lock-in" effect of early aspects of an implementation
that get stuck because users get used to them.
Makarius
Email Gateway (Aug 19 2022 at 13:59):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Just to confirm, “for” works fine in my old example. No constraints from here, then..
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Nov 21 2024 at 12:39 UTC