John Hughes (Feb 28 2025 at 13:53): John Hughes (Feb 28 2025 at 13:53):(Apologies: the title should say "Locales" rather than "Locals".)
Here's a tiny theory illustrating a confusion about locales; I've trimmed it down from something larger, which explains some of the name choices.
theory Scratch
imports Complex_Main
begin
locale base_data =
fixes Points :: "'p set"
begin
end
locale plane1 =
base_data +
assumes
a1a: "⟦ P ∈ Points; Q ∈ Points⟧ ⟹ P = Q"
begin
end
locale plane2 =
base_data Points for Points :: "'p set" +
assumes
a1a: "⟦ P ∈ Points; Q ∈ Points⟧ ⟹ P = Q"
begin
end
locale both =
fixes Points :: "'p set"
assumes
a1a: "⟦ P ∈ Points; Q ∈ Points⟧ ⟹ P = Q"
begin
end
end
As you can see, in the base_data locale, Points is a 'p set . But if you check in plane1, it's become an 'a set. On the other hand, in plane2, it's still a 'p set.
I had mistakenly believed that when a locale was included in another, it was more or less like what I've written in the locale called both, in which both the fixes and assumes lines are in a single declaration.
I learned about the for keyword from an example someone gave me, and it's allowed me to finish up some proving, so I'm happy. But I'd like to understand what it's actually doing. Ballarin's revised tutorial on locales (https://isabelle.in.tum.de/doc/locales.pdf) is great, but it's actually a little reticent on the exact meaning of "for". Can anyone clarify for me the semantics of 'inclusion' vs 'inclusion using for'? One specific question: why, in plane1, do the types change at all in the first place?
Fabian Huch (Feb 28 2025 at 14:34):I don't know the fine points about locale syntax, but all three of your definitions are equivalent. The types are equal modulo alpha-renaming.
John Hughes (Feb 28 2025 at 15:07):Well... yes and no. I have a theorem (in the larger theory from which this is extracted and simplified) that I could not prove (indeed, in one version could not even state!) without the "for". It looked like this:
"∃(P :: 'p) (Q :: 'p) (R :: 'p) (S :: 'p).
P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ P ≠ S ∧ Q ≠ S ∧ R ≠ S ∧ P ∈ Points ∧
Q ∈ Points ∧ R ∈ Points ∧ S ∈ Points"
I attached the types to P, Q, R, and S as a way to ensure that they all had the same type, etc., because I so often get caught by type-stuff.
When I tried to state that theorem, Isabelle said this:
Type unification failed
Failed to meet type constraint:
Term:
λS. P ≠ Q ∧
P ≠ R ∧ Q ≠ R ∧ P ≠ S ∧ Q ≠ S ∧ R ≠ S ∧ P ∈ Points ∧ Q ∈ Points ∧ R ∈ Points ∧ S ∈ Points ::
'a ⇒ bool
Type: 'p ⇒ ??'a
Coercion Inference:
Local coercion insertion on the operand failed:
Cannot generate coercion from "'p" to "'a"
Now trying to infer coercions globally.
Coercion inference failed:
weak unification of subtype constraints fails
Given that 'p hasn't been mentioned since I defined the 'base' locale, where it's a parameter (more or less), I can't see why it can't be unified with 'a here. Changing the type from 'p to 'd, which has never been mentioned at all, gave the same results.
irvin (Feb 28 2025 at 15:09):Isabelle locales does not use the information about the name that you chose it alpha renames
irvin (Feb 28 2025 at 15:24):It assumes that they are separate unless you explicit do it using the for keyword see. It does rename when you do it in assumptions
locale A =
fixes A :: "'a set"
locale B =
fixes B :: "'a set"
locale C = A + B
locale D = A + B +
assumes "A = B"
In your larger example you probably have more than one distinct type variable, in which case there is a difference between a locale that has two distinct type variables and one that coincides both.
Fabian Huch (Feb 28 2025 at 15:29):E.g. if you have the two locales
locale A = fixes a::'a
locale B = fixes b :: 'b
Then you can either have one where those type variables do not coincide, which is the default:
locale C = A + B
Or you create one that extends A and B such that the type variable does coincide:
locale D = A a + B b for a :: "'c" and b :: "'c"
I think you're on to something here, although it's not quite this situation. I have two locales:
locale affine_plane_data =
fixes Points :: "'p set" and Lines :: "'l set" and meets :: "'p ⇒ 'l ⇒ bool"
fixes join:: "'p ⇒ 'p ⇒ 'l"
fixes find_parallel:: "'l ⇒ 'p ⇒ 'l"
begin
(definition of parallel, and || syntax for it)
end
and
locale affine_plane =
affine_plane_data Points Lines meets
for meets :: "'p ⇒ 'l ⇒ bool" and
Points :: "'p set" and
Lines :: "'l set" +
assumes
a1a: "⟦P ≠ Q; P ∈ Points; Q ∈ Points⟧ ⟹ join P Q ∈ Lines ∧ meets P (join P Q) ∧ meets Q (join P Q)" and
a1b: "⟦P ≠ Q; P ∈ Points; Q ∈ Points; meets P m; meets Q m⟧ ⟹ m = join P Q" and
a2a: "⟦ P ∈ Points; l ∈ Lines⟧ ⟹ find_parallel l P ∈ Lines" and
a2b: "⟦ P ∈ Points; l ∈ Lines⟧ ⟹ ( find_parallel l P) || l" and
a2c: "⟦ P ∈ Points; l ∈ Lines⟧ ⟹ meets P (find_parallel l P)" and
a2d: "⟦ P ∈ Points; l ∈ Lines; m ∈ Lines; m || l; meets P m⟧ ⟹ m = find_parallel l P" and
a3: "∃P Q R. P ∈ Points ∧ Q ∈ Points ∧ R ∈ Points ∧ P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ ¬ (collinear P Q R)"
begin
So there are indeed two type variables, 'p and 'l, but they're both in one locale. Within affine_plane, when I leave out the for clause, points and lines get types 'a and 'b rather than 'p and 'l, and the conflict I showed above arises.
Fabian Huch (Feb 28 2025 at 15:46):conflict from what assumption?
Fabian Huch (Feb 28 2025 at 15:52):Oh wait you mention syntax defined inside a locale
Fabian Huch (Feb 28 2025 at 15:52):That sounds sketchy
Fabian Huch (Feb 28 2025 at 15:52):This is probably your problem
irvin (Feb 28 2025 at 16:04):You should understand that your locales fixes the type variables with type based assumptions so you can't rename it
irvin (Feb 28 2025 at 16:05):By default isabelle renames the locales to use 'a ... so those are the ones fixed not 'p
irvin (Feb 28 2025 at 16:25):Is this your problem?
locale A = fixes
A :: "'l set"
assumes foo: "A = UNIV"
context A
begin
(*Works*)
lemma "A = (UNIV :: 'l set)"
by(fact foo)
end
(*implicit conversion of A to 'a set*)
locale B = A +
assumes bar"True"
context B
begin
(*Fails*)
lemma "A = (UNIV :: 'l set)"
by(fact foo)
end
Fabian Huch said:
This is probably your problem
Perhaps so. Manuel Eberl showed me how to do it. It's pretty useful, because writing the axioms for the affine plane becomes so much prettier.
I think that @Irvin 's example may be a minimal case of my problem, and it doesn't involve that syntax thing, so maybe the syntax is a red herring.
(Thanks for helping chase this down. It's all pretty baffling for a beginner.)
John Hughes (Feb 28 2025 at 16:41):irvin said:
Is this your problem?
locale A = fixes A :: "'l set" assumes foo: "A = UNIV" context A begin (*Works*) lemma "A = (UNIV :: 'l set)" by(fact foo) end (*implicit conversion of A to 'a set*) locale B = A + assumes bar"True" context B begin (*Fails*) lemma "A = (UNIV :: 'l set)" by(fact foo) end
I think that this DOES illustrate the problem. What's not clear to me is why, in context B, saying that A is UNIV for sets of some as-yet-unspecified type 'l is a problem -- why can't Isabelle say "Yeah, that's true if I unify 'l with 'a"? (The problem persists if you replace 'l with 'd, so it's not just the use of 'l in locale A that's a problem.)
Mathias Fleury (Feb 28 2025 at 16:44):I feel like adding such kind of unification would be extremely complicated and very error-prone
Mathias Fleury (Feb 28 2025 at 16:45):It would also break the thread model: independent lemmas cannot be executed in parallel anymore due to the unification
irvin (Feb 28 2025 at 16:47):You should understand that locales are type level for all and the 'a is fixed in context
irvin (Feb 28 2025 at 16:53):For example you can think of a locale theorem as something like.
Where in this case 'a is the a
for a. P a
. So similar to a normal for all where.
to prove !x. P x. You fix x and prove P x.
In this case 'a is fixed and 'l is not fixed
John Hughes (Feb 28 2025 at 17:04):Mathias Fleury said:
It would also break the thread model: independent lemmas cannot be executed in parallel anymore due to the unification
I clearly misunderstand type-inference/unification in Isabelle; I'll try to read more. My understanding was roughly "if you have some expression involving type-variables, unification tries to find an assignment of types consistent with these." So when you have x = (2::nat), Isabelle determines that the type of x, formerly unknown, must in fact be nat. But when I tried writing a lemma saying (x::'a) = (2::nat), it failed, so this is clearly not happening the way I thought.
By the way, I think it's hard for folks here to understand the possible depths of ignorance of beginners. You wrote about the "thread model," but in the text recommended for beginners (Programming and Proving), the word "thread" never appears. There's some mental model that experienced folks have that we beginners lack -- not because we forgot it, but because we never knew it.
irvin's remark, "You should understand that locales are type level for all and the 'a is fixed in context", is similar: I have no idea what "type level" means (I'm only guessing that it's a compound adjective!), what "for all" means here, etc.
irvin (Feb 28 2025 at 17:07):Works
lemma "⋀x. P x"
proof -
fix x
show "P x"
by sorry
qed
and This also
lemma "⋀x. P x"
proof -
fix y
show "P y"
by sorry
qed
but this does not work
lemma "⋀x. P x"
proof -
fix x
show "P y"
by sorry
qed
In your locale you have fixed it already
using the fixes
John Hughes (Feb 28 2025 at 17:16):I can see what's wrong with that forall example -- thanks very much for that clear illustration.
Unfortunately, I don't see the analogy with locales clearly yet. When you say "In your locale, you have fixed it already," what does it refer to, and where did I 'fix' it?
I'm sorry to be so obtuse here. You just have to imagine that you're trying to explain nuclear fusion to a jellyfish. :)
irvin (Feb 28 2025 at 17:17):locale A =
fixes A :: "'l set"
assumes foo: "A = UNIV"
begin
Here you have fixed A :: "'l set"
irvin (Feb 28 2025 at 17:18):Where the 'l is equivalent to the x
irvin (Feb 28 2025 at 17:19):The jedit has a query panel where you can see what's fixed in your context.
query > print context
John Hughes (Feb 28 2025 at 17:28):irvin said:
locale A = fixes A :: "'l set" assumes foo: "A = UNIV" beginHere you have fixed
A :: "'l set"
Right...but then 'l gets renamed to 'a when A is included in BB, which doesn't feel very "fixed" to me -- it still feels as if the type for A has a free parameter. I can make an instance of locale A in which 'l is, say int or real. Here's an example which works fine:
locale A =
fixes S :: "'l set"
assumes foo: "S = UNIV"
begin
print_theorems
end
lemma "A (UNIV::int set)"
using A_def by auto
lemma "A (UNIV::real set)"
using A_def by auto
So 'l doesn't seem quite "fixed" here. Or maybe I also don't know what "fixed" means in Isabelle. Sigh.
irvin (Feb 28 2025 at 17:29):It's fixed when you enter the context
John Hughes (Feb 28 2025 at 17:33):Thanks. I appreciate that. I think I need to go back and double check my assumptions about what I know about Isabelle before this will make sense to me, so I'm going to set this aside for a while and try to clear my head. I really appreciate your attempts to clarify things, and I hope that re-reading them will bring enlightenment, at which point I won't be able to recall why it seemed hard in the first place. :)
irvin (Feb 28 2025 at 17:36):To be fair i don't think i've done that great of an explanation. Perhaps someone else could provide a better explanation.
Mathias Fleury (Feb 28 2025 at 17:45):John Hughes said:
Mathias Fleury said:
It would also break the thread model: independent lemmas cannot be executed in parallel anymore due to the unification
I clearly misunderstand type-inference/unification in Isabelle; I'll try to read more. My understanding was roughly "if you have some expression involving type-variables, unification tries to find an assignment of types consistent with these." So when you have
x = (2::nat), Isabelle determines that the type ofx, formerly unknown, must in fact benat. But when I tried writing a lemma saying(x::'a) = (2::nat), it failed, so this is clearly not happening the way I thought.
Type-inference happens only when you state a lemma / definition / fun / term whatever. There is no propagation from the type inference to another statement.
There is only one exception to this rule, the pair:
fix x
assume `x = (0::nat)`
works (don't ask me why…)
John Hughes said:
Mathias Fleury said:
It would also break the thread model: independent lemmas cannot be executed in parallel anymore due to the unification
[...]
By the way, I think it's hard for folks here to understand the possible depths of ignorance of beginners. You wrote about the "thread model," but in the text recommended for beginners (Programming and Proving), the word "thread" never appears. There's some mental model that experienced folks have that we beginners lack -- not because we forgot it, but because we never knew it.
The fact that Isabelle can run proofs in parallel only works when you assume that statement do not interact: you parse a theorem and can use even if its own proof is not yet finished. Statements and proofs do not interact, so checking can be done in parallel.
There is obviously one exception here too: an apply scripts. If you have apply (rule XYZ) apply (rule STU), they cannot be done in parallel.
Exception in the exception
Mathias Fleury (Feb 28 2025 at 17:48):Ah now I see the difference you are having issues with:
locale test =
fixes f assume ‹f a b = a + b›
vs
definition f where ‹f a b = a + b›
I always see a locale as a module where you fix all information (both constant and type information). All information is fixed within the context. So it cannot change anymore.
Mathias Fleury (Feb 28 2025 at 17:51):It's like a parameterized module or a C++ template: you have a type and you have to work with it. You cannot specialize it.
Mathias Fleury (Feb 28 2025 at 17:54):In math it would like "let A be an algebra": you have an abstract algebra and you cannot decide in a theorem to let A be the real numbers. You would something like "let A be the algebra of real numbers" be the proof in not the "let A be an algebra" context anymore. You left it.
John Hughes (Feb 28 2025 at 18:08):"The fact that Isabelle can run proofs in parallel" -- even this "fact" was not obvious to me as a beginner. Indeed, getting Isabelle to run any one proof was so rare an experience that having it do two at once would have been a shock. :)
Your analogy with "an algebra" vs "the algebra of the reals" is helpful; perhaps a little bit of fog is clearing. As I said to irvin, I think I'll take all this and digest for a bit.
Once again, I'm much obliged for your help.
Last updated: Mar 09 2025 at 12:28 UTC