Stream: Beginner Questions

Topic: Local homeomorphism

view this post on Zulip Nicolò Cavalleri (Jun 28 2021 at 17:20):

Suppose I wanted to define the type of local homeomorphisms in the context of Abstract_topology. I cannot transform this:

definition is_chart :: "'a topology ⇒ 'e topology ⇒ 'a set ⇒ 'e set ⇒ ('a ⇒ 'e) ⇒ ('e ⇒ 'a)
  ⇒ bool" where
"is_chart Ta Te A E f g ≡ openin Ta A ∧ openin Te E ∧
  homeomorphic_maps (subtopology Ta A) (subtopology Te E) f g"

into a type with fixed topologies right? I mean using typedef with some trick.

view this post on Zulip Nicolò Cavalleri (Jun 28 2021 at 21:00):

I gave up on fixing the topologies, but why does this:

import Analysis.Abstract_topology

definition is_chart :: "'a topology ⇒ 'e topology ⇒ 'a set ⇒ 'e set ⇒ ('a ⇒ 'e) ⇒ ('e ⇒ 'a)
  ⇒ bool" where
"is_chart Ta Te A E f g ≡ openin Ta A ∧ openin Te E ∧
  homeomorphic_maps (subtopology Ta A) (subtopology Te E) f g"

typedef (overloaded) ('a, 'e) chart =
  "{(Ta::'a topology, Te::'e topology, A::'a set, E::'e set, f, g).
    is_chart Ta Te A E f g}"
  by (rule exI[where x="(discrete_topology, discrete_topology, {}, {}, (λx. undefined),
    (λx. undefined))"]) simp

setup_lifting type_definition_chart

not work?

view this post on Zulip Wenda Li (Jun 29 2021 at 07:52):

How about this one? 

typedef (overloaded) ('a, 'e) chart =
  "{(Ta::'a topology, Te::'e topology, A::'a set, E::'e set, f, g).
    is_chart Ta Te A E f g}"
  apply (rule exI[where x="(discrete_topology {}, discrete_topology {}, {},
          {}, (λx. undefined),(λx. undefined))"])
  unfolding is_chart_def homeomorphic_maps_def by auto

view this post on Zulip Nicolò Cavalleri (Jun 29 2021 at 10:45):

It works thank you very much! I am puzzeld though (apart from the fact that I forgot to add something after discrete_topology): if I write this

typedef (overloaded) ('a, 'e) chart =
  "{(Ta::'a topology, Te::'e topology, A::'a set, E::'e set, f, g).
    is_chart Ta Te A E f g}"
  apply (rule exI[where x="(discrete_topology {}, discrete_topology {}, {},
          {}, (λx. undefined),(λx. undefined))"])

and then I run sledgehammer it does not find a proof. Is it normal?

view this post on Zulip Nicolò Cavalleri (Jun 29 2021 at 10:47):

Also, setup_lifting type_definition_chart gives a warning 

Generation of a parametrized correspondence relation failed.
Reason:  No relator for the type "Abstract_Topology.topology" found.

but the code works fine. Should I worry about it?

view this post on Zulip Wenda Li (Jun 29 2021 at 10:59):

Nicolò Cavalleri said:

and then I run sledgehammer it does not find a proof. Is it normal?

Yes, it is normal. Sledgehammer is bad when the goal is of higher-order nature (i.e., functions as arguments). Generally, Sledgehammer is a bit unpredictable -- it may fail at some goal that appears easy to us, but sometimes it can exceed our expectation by succeeding on extremely challenging problems.

view this post on Zulip Nicolò Cavalleri (Jun 29 2021 at 10:59):

Also I wonder why the last lemma in this mwe

typedef (overloaded) ('a, 'e) chart =
  "{(Ta::'a topology, Te::'e topology, A::'a set, E::'e set, f, g).
    openin Ta A ∧ openin Te E ∧ homeomorphic_maps (subtopology Ta A) (subtopology Te E) f g}"
  apply (rule exI[where x="(discrete_topology {}, discrete_topology {}, {},
          {}, (λx. undefined),(λx. undefined))"])
  unfolding homeomorphic_maps_def by auto

setup_lifting type_definition_chart

lift_definition apply_chart::"('a, 'e) chart ⇒ 'a ⇒ 'e"
  is "λ(Ta, Te, A, E, f, g). f" .

declare [[coercion apply_chart]]

lift_definition inv_chart::"('a, 'e) chart ⇒ 'e ⇒ 'a"
  is "λ(Ta, Te, A, E, f, g). g" .

lift_definition source_topology::"('a, 'e) chart ⇒ 'a topology"
  is "λ(Ta, Te, A, E, f, g). Ta" .

lift_definition range_topology::"('a, 'e) chart ⇒ 'e topology"
  is "λ(Ta, Te, A, E, f, g). Te" .

lift_definition domain::"('a, 'e) chart ⇒ 'a set"
  is "λ(Ta, Te, A, E, f, g). A" .

lift_definition codomain::"('a, 'e) chart ⇒ 'e set"
  is "λ(Ta, Te, A, E, f, g). E" .


subsection ‹Properties›

lemma open_domain[intro, simp]: "openin (source_topology c) (domain c)"
  and open_codomain[intro, simp]: "openin (range_topology c) (codomain c)"
  and chart_homeomorphism: "homeomorphic_maps (subtopology (source_topology c) (domain c))
    (subtopology (range_topology c) (codomain c)) c (inv_chart c)"
  by (transfer, auto)+

lemma at_within_domain: "at x within domain c = at x" if "x ∈ domain c"
  by (rule at_within_open[OF that open_domain])

does not work...

view this post on Zulip Nicolò Cavalleri (Jun 29 2021 at 11:00):

Wenda Li said:

Nicolò Cavalleri said:

and then I run sledgehammer it does not find a proof. Is it normal?

Yes, it is normal. Sledgehammer is bad when the goal is of higher-order nature (i.e., functions as arguments). Generally, Sledgehammer is a bit unpredictable -- it may fail at some goal that appears easy to us, but sometimes it can exceed our expectation by succeeding on extremely challenging problems.

Ok thank you very much!

view this post on Zulip Wenda Li (Jun 29 2021 at 11:02):

Nicolò Cavalleri said:

Also, setup_lifting type_definition_chart gives a warning 

Generation of a parametrized correspondence relation failed.
Reason:  No relator for the type "Abstract_Topology.topology" found.

but the code works fine. Should I worry about it?

There might be a problem if you want to use the lift and transfer framework sometimes later. If you don't plan to use that framework, setup_lifting type_definition_chart is actually not necessary.

view this post on Zulip Nicolò Cavalleri (Jun 29 2021 at 11:03):

Wenda Li said:

Nicolò Cavalleri said:

Also, setup_lifting type_definition_chart gives a warning 

Generation of a parametrized correspondence relation failed.
Reason:  No relator for the type "Abstract_Topology.topology" found.

but the code works fine. Should I worry about it?

There might be a problem if you want to use the lift and transfer framework sometimes later. If you don't plan to use that framework, setup_lifting type_definition_chart is actually not necessary.

I do plan to use (you can see my use in the mwe) it but it works despite the warning!

view this post on Zulip Nicolò Cavalleri (Jun 29 2021 at 11:08):

Nicolò Cavalleri said:

Also I wonder why the last lemma in this mwe

...

does not work...

The problem is that these proofs should be super easy but Isabelle does not find them automatically and apparently I am not able to write any proof by hand, I can only use auto simp fastforce and sledgehammer

view this post on Zulip Wenda Li (Jun 29 2021 at 11:09):

Nicolò Cavalleri said:

I do plan to use (you can see my use in the mwe) it but it works despite the warning!

Yes, I just saw that. It is nice that transfer works so far. You may need to work out those relator stuff when it fails.

view this post on Zulip Nicolò Cavalleri (Jun 29 2021 at 11:11):

Wenda Li said:

Nicolò Cavalleri said:

I do plan to use (you can see my use in the mwe) it but it works despite the warning!

Yes, I just saw that. It is nice that transfer works so far. You may need to work out those relator stuff when it fails.

Yep I would not know how to do that because I do not know either abstract topology nor the transfer package but I will ask for help here in case!

view this post on Zulip Wenda Li (Jun 29 2021 at 11:12):

Nicolò Cavalleri said:

The problem is that these proofs should be super easy but Isabelle does not find them automatically and apparently I am not able to write any proof by hand, I can only use auto simp fastforce and sledgehammer

That is the idea of interactive theorem proving and the difference between us and those ATPs -- we can always learn to proceed when automation fails even though we may proceed at a mush slower pace :-)

view this post on Zulip Nicolò Cavalleri (Jun 29 2021 at 11:15):

Wenda Li said:

Nicolò Cavalleri said:

The problem is that these proofs should be super easy but Isabelle does not find them automatically and apparently I am not able to write any proof by hand, I can only use auto simp fastforce and sledgehammer

That is the idea of interactive theorem proving and the difference between us and those ATPs -- we can always learn to proceed when automation fails even though we may proceed at a mush slower pace :-)

Yeah actually I saw the problem in my proof... the theorem at_within_open does not apply here.

view this post on Zulip Wenda Li (Jun 29 2021 at 11:15):

As for

lemma at_within_domain: "at x within domain c = at x" if "x ∈ domain c"
  by (rule at_within_open[OF that open_domain])

Your at_within_open[OF that open_domain] is not valid. The proof can be fixed if you can prove open (domain c) (I am not sure if it is provable or not):

lemma at_within_domain: "at x within domain c = at x" if "x ∈ domain c"
proof -
  have "open (domain c)" sorry
  then show ?thesis using at_within_open[OF that] by auto
qed

view this post on Zulip Nicolò Cavalleri (Jun 29 2021 at 11:16):

Wenda Li said:

As for

lemma at_within_domain: "at x within domain c = at x" if "x ∈ domain c"
  by (rule at_within_open[OF that open_domain])

Your at_within_open[OF that open_domain] is not valid. The proof can be fixed if you can prove open (domain c) (I am not sure if it is true or not):

lemma at_within_domain: "at x within domain c = at x" if "x ∈ domain c"
proof -
  have "open (domain c)" sorry
  then show ?thesis using at_within_open[OF that] by auto
qed

No I think it is not true but hopefully I should manage to recover a proof if someone who knows well Abstract topology will answer me in the thread Filters in abstract topology

view this post on Zulip Nicolò Cavalleri (Jun 29 2021 at 11:16):

Thank you very much though!

Last updated: Dec 30 2024 at 16:22 UTC