## Stream: Beginner Questions

### Topic: Local homeomorphism

#### 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.

#### 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?

#### Wenda Li (Jun 29 2021 at 07:52):

``````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
``````

#### 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?

#### 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?

#### 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.

#### 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...

#### 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!

#### 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.

#### 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!

#### 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

#### 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.

#### 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!

#### 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 :-)

#### 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.

#### 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
``````

#### 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`

#### Nicolò Cavalleri (Jun 29 2021 at 11:16):

Thank you very much though!

Last updated: Sep 11 2024 at 16:22 UTC