Stream: Beginner Questions

Topic: Type overloading not working


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (May 06 2021 at 10:47):

when you're defining test_1, you're outside of the weird_topological_space

view this post on Zulip Jakub Kądziołka (May 06 2021 at 10:48):

Take a look at how group_hom is defined here

view this post on Zulip 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?

view this post on Zulip Jakub Kądziołka (May 06 2021 at 10:49):

you need to provide the implicit parameters of the locale somehow

view this post on Zulip Jakub Kądziołka (May 06 2021 at 10:49):

I assume that you want to have two topological spaces involved

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip Jakub Kądziołka (May 06 2021 at 11:36):

ah, ignore the ⊗, copy-paste mishap

view this post on Zulip 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?

view this post on Zulip Jakub Kądziołka (May 06 2021 at 11:53):

say for X (structure) and Y (structure) and add subscripts to invokations of nbhds

view this post on Zulip 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"

view this post on Zulip Nicolò Cavalleri (May 06 2021 at 12:03):

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"

view this post on Zulip Jakub Kądziołka (May 06 2021 at 12:09):

hmm, I do not understand why this is happening

view this post on Zulip 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 line

and at_mem_y : "y ∈ Y"

You mean this right?

view this post on Zulip 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"

view this post on Zulip Nicolò Cavalleri (May 06 2021 at 13:40):

What is happening in the parenthesis ("is'_openı _")? I mean what is that and what is its role?

view this post on Zulip 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"

view this post on Zulip Jakub Kądziołka (May 06 2021 at 14:49):

ctrl+click on partial_object -- it is just a record field carrier :: "'a set"

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Jakub Kądziołka (May 06 2021 at 14:54):

The carrier is your set S

view this post on Zulip Nicolò Cavalleri (May 06 2021 at 14:55):

What is the ' after "is" in is'_open?

view this post on Zulip 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 _

view this post on Zulip 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)"

view this post on Zulip Jakub Kądziołka (May 06 2021 at 14:58):

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

view this post on Zulip 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

view this post on Zulip 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 set instead 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

view this post on Zulip Nicolò Cavalleri (May 07 2021 at 00:02):

Thank you very much!!


Last updated: Sep 25 2022 at 23:25 UTC