Nicolò Cavalleri (May 06 2021 at 10:41): Nicolò Cavalleri (May 06 2021 at 10:41):I have the following code, which is not the original but just a mwe to recreate the problem I have:
theory Scratch
imports Main
begin
locale weird_topological_space = fixes S :: "'a set" and is_open :: "'a set ⇒ bool"
assumes open_space [simp, intro]: "is_open S" and open_empty [simp, intro]: "is_open {}"
and open_imp_subset: "is_open U ⟹ U ⊆ S"
and open_inter [intro]: "⟦is_open U; is_open V⟧ ⟹ is_open (U ∩ V)"
and open_union [intro]: "⋀F::('a set) set. (⋀x. x ∈ F ⟹ is_open x) ⟹ is_open (⋃x∈F. x)"
begin
definition nbhds :: "'a ⇒ 'a filter"
where "nbhds a = (INF S∈{S. is_open S ∧ a ∈ S}. principal S)"
end
definition pippo :: "'a ⇒ 'a filter"
where "pippo a = (INF S∈{S. a ∈ S}. principal S)"
locale test_1 =
fixes f :: "'a ⇒ 'b" and x :: 'a and y :: 'b
assumes has_derivative_hd: "filterlim f (nbhds y) (nbhds x)"
(* Type unification failed
Type error in application: incompatible operand type
Operator: nbhds :: 'b ⇒ 'b filter
Operand: x :: 'a *)
locale test_2 =
fixes f :: "'a ⇒ 'b" and x :: 'a and y :: 'b
assumes has_derivative_hd: "filterlim f (pippo y) (nbhds x)"
locale test_3 =
fixes f :: "'a ⇒ 'b" and x :: 'a and y :: 'b
assumes has_derivative_hd: "filterlim f (pippo y) (pippox)"
end
and for some reason test 2 and 3 work, whereas test 1 does not. It is as if for some reason the function is_open does not allow the function nbhds to change type in different instances.
Does anybody know why?
Jakub Kądziołka (May 06 2021 at 10:47):as you can see by the identifier being blue, the nbhds in test_1 is a free variable, it does not refer to the definition in weird_topological_space
Jakub Kądziołka (May 06 2021 at 10:47):when you're defining test_1, you're outside of the weird_topological_space
Jakub Kądziołka (May 06 2021 at 10:48):Take a look at how group_hom is defined here
Nicolò Cavalleri (May 06 2021 at 10:49):Ok ops that was a stupid mistake, sorry I am not used to Isabelle colors! How can I use it outside?
Jakub Kądziołka (May 06 2021 at 10:49):you need to provide the implicit parameters of the locale somehow
Jakub Kądziołka (May 06 2021 at 10:49):I assume that you want to have two topological spaces involved
Jakub Kądziołka (May 06 2021 at 10:50):if you only needed one, you could do locale test_1 = weird_topological_space + and nbhds would be in scope
Jakub Kądziołka (May 06 2021 at 10:51):if you do need two, you'll need to give explicit names to the topological spaces and then use nbhds⊗⇘T⇙ and nbhds⊗⇘U⇙ (again, see the group_hom example
Nicolò Cavalleri (May 06 2021 at 11:14):Thank you very much for your help! I am trying to imitate the example you linked. Now it recognizes nbhds but it still have a type overloading problem: if I replace test_1 above with
locale test_1 =
X?: weird_topological_space X + Y?: weird_topological_space Y
for X and Y +
fixes f :: "'a ⇒ 'b" and x :: 'a and y :: 'b
assumes at_mem_x : "x ∈ X"
and at_mem_y : "y ∈ Y"
and lim: "filterlim f (nbhds x) (nbhds y)"
(* Type unification failed
Type error in application: incompatible operand type
Operator: (∈) y :: 'b set ⇒ bool
Operand: Y :: 'a set *)
I get the above error. What am I doing wrong this time? Again it is as if it forces both topological spaces to be built on the same type
Nicolò Cavalleri (May 06 2021 at 11:24):Also I am not sure what the symbols in nbhds⊗⇘T⇙ are! Is it something important? I can't find anything about this notation in the online tutorial on locales!
Lukas Stevens (May 06 2021 at 11:26):This is like \<sub> but you are allowed to use multiple characters (\<bsub> ...\<esub>). Additionally, you are allowed to use parameters inside this notation, which is not allowed for \<sub>. The notation is not displayed correctly but there are patches for jEdit flying around @Mohammad Abdulaziz?
Jakub Kądziołka (May 06 2021 at 11:36):ah, ignore the ⊗, copy-paste mishap
Nicolò Cavalleri (May 06 2021 at 11:52):Nicolò Cavalleri said:
I get the above error. What am I doing wrong this time? Again it is as if it forces both topological spaces to be built on the same type
@Jakub Kądziołka do you by chance know anything about this?
Jakub Kądziołka (May 06 2021 at 11:53):say for X (structure) and Y (structure) and add subscripts to invokations of nbhds
Nicolò Cavalleri (May 06 2021 at 12:00):I added (structure), but as for subscripts, the error comes out even if I remove the line about nbhds: it comes out for the line
and at_mem_y : "y ∈ Y"
Also I tried to add subscripts your way, with \<bsub> and \<esub> but Isabelle does not seem to recognize them, it says Inner syntax error⌂
Failed to parse prop. I don't really know how subscripts work in isabelle and they don't appear to be in any tutorial: neither prog-prove nor "A proof Assistant for Higher-Order Logic"
Jakub Kądziołka (May 06 2021 at 12:09):hmm, I do not understand why this is happening
Nicolò Cavalleri (May 06 2021 at 12:10):Nicolò Cavalleri said:
I added
(structure), but as for subscripts, the error comes out even if I remove the line about nbhds: it comes out for the lineand at_mem_y : "y ∈ Y"
You mean this right?
Jakub Kądziołka (May 06 2021 at 12:18):Looks like locales with multiple parameters aren't behaving like they should. I'd suggest posting on the mailing list. Meanwhile you can package up your topological space into a record like HOL-Algebra does:
theory Scratch
imports Main "HOL-Algebra.Congruence"
begin
record 'a weird_topological_space = "'a partial_object" +
is_open :: "'a set ⇒ bool" ("is'_openı _")
locale weird_topological_space = fixes S (structure)
assumes open_space [simp, intro]: "is_open (carrier S)"
begin
end
locale test_1 =
X?: weird_topological_space X + Y?: weird_topological_space Y
for X (structure) and Y (structure) +
fixes f :: "'a ⇒ 'b" and x y
assumes at_mem_x : "x ∈ carrier X"
and at_mem_y : "y ∈ carrier Y"
What is happening in the parenthesis ("is'_openı _")? I mean what is that and what is its role?
Nicolò Cavalleri (May 06 2021 at 13:45):Also do you know about somewhere where I can read more about how are locales related to records? I don't really understand what is going on and I can't manage to get rid of the carriers, I mean I'd just like to write S :: 'a set instead of "'a partial_object"
Jakub Kądziołka (May 06 2021 at 14:49):ctrl+click on partial_object -- it is just a record field carrier :: "'a set"
Jakub Kądziołka (May 06 2021 at 14:49):using this common definition lets you use HOL-Algebra and your definitions without having to disambugate the meaning of carrier
Jakub Kądziołka (May 06 2021 at 14:53):Nicolò Cavalleri said:
What is happening in the parenthesis
("is'_openı _")? I mean what is that and what is its role?
Right. The motivation is that is_open needs an argument which is the record (topological space) itself. This is the role of the structure mechanism:
fixes X (structure) or for X (structure) (with optional type signature before the parenthesis), it can be used as a subscript in a place corresponding to a ı in notation Jakub Kądziołka (May 06 2021 at 14:54):The carrier is your set S
Nicolò Cavalleri (May 06 2021 at 14:55):What is the ' after "is" in is'_open?
Jakub Kądziołka (May 06 2021 at 14:56):the ' is an escape character — unescaped, an underscore indicates an argument. Think if _ then _ else _
Jakub Kądziołka (May 06 2021 at 14:56):BTW, I realized why your earlier example wasn't working. This works:
locale test_1 =
X?: weird_topological_space X open_in_X + Y?: weird_topological_space Y open_in_Y
for X open_in_X Y and open_in_Y +
fixes f :: "'a ⇒ 'b" and x :: 'a and y :: 'b
assumes at_mem_x : "x ∈ X"
and at_mem_y : "y ∈ Y"
and lim: "filterlim f (Y.nbhds y) (X.nbhds x)"
note that you need to do for <set> and <open predicate for that set>, and provide both to weird_topological_space, as only both values at once can define a topological space
Jakub Kądziołka (May 06 2021 at 14:59):This is why records are so common — a record is essentially a tuple where its elements have been named
Jakub Kądziołka (May 06 2021 at 15:00):Nicolò Cavalleri said:
Also do you know about somewhere where I can read more about how are locales related to records? I don't really understand what is going on and I can't manage to get rid of the carriers, I mean I'd just like to write
S :: 'a setinstead of"'a partial_object"
I guess I wrote some notes on how and why abstract structures like these are defined by Isabelle as they are: https://github.com/NieDzejkob/isabelle-math-contests/blob/master/NOTES.md#abstract-algebra
Nicolò Cavalleri (May 07 2021 at 00:02):Thank you very much!!
Last updated: Oct 13 2024 at 01:36 UTC