## Stream: maths

### Topic: Showing topological_space_eq "manually"

#### Golol (Oct 18 2020 at 16:27):

This is the definition of a topological space.

@[protect_proj] structure topological_space (α : Type u) :=
(is_open        : set α → Prop)
(is_open_univ   : is_open univ)
(is_open_inter  : ∀s t, is_open s → is_open t → is_open (s ∩ t))
(is_open_sUnion : ∀s, (∀t∈s, is_open t) → is_open (⋃₀ s))


I want to show the following lemma

lemma topological_space_eq {X Y : topological_space α} : (X.is_open = Y.is_open) -> X = Y


by explicitly constructing a proof of X = Y, not just typing refl and letting lean do it.
To do this I want to show that X.is_open_inter = Y.is_open_inter, X.is_open_sUnion = Y.is_open_sUnion and X.is_open_univ = Y.is_open_univ. Then I can apply topological_space.mk and since I have proofs that all the arguments are equal, as well as that X is the result of applying the constructor, I should be able to get a proof (using eq.rec_on a bit).
My problem is that

lemma test {X Y : topological_space α} : (X.is_open = Y.is_open) -> X.is_open_univ = Y.is_open_univ


does not typecheck since lean says that the two types at the end are different.
How could I get around this?

#### Mario Carneiro (Oct 18 2020 at 16:35):

note that refl is not a magic tool, it proves a very particular set of things. In particular, when refl is the proof, the proof is literally rfl, or eq.refl _ - there is no lower level proof

#### Mario Carneiro (Oct 18 2020 at 16:35):

In fact refl will not prove this goal

#### Mario Carneiro (Oct 18 2020 at 16:37):

The proof of this theorem is actually intro h; cases X; cases Y; cases h; refl, which should give you a hint as to how to proceed

#### Golol (Oct 18 2020 at 16:53):

Could you then explain how this proof works?

lemma topological_space_eq : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g
| ⟨a, _, _, _⟩ ⟨b, _, _, _⟩ rfl := rfl


We start by using recursion on topological space to assume that f and g are outputs of the constructor for certain inputs. But what does the first rfl do, and why is it trivial to Lean that all the arguments are identical?

#### Mario Carneiro (Oct 18 2020 at 16:57):

that's the same proof as I just described, but written with the equation compiler

#### Mario Carneiro (Oct 18 2020 at 16:58):

the first two tuples are doing cases X; cases Y and the rfl on the left is doing cases h, and the rfl on the right is the finishing refl

#### Mario Carneiro (Oct 18 2020 at 16:59):

Once you have done cases on everything, all the props become definitionally equal by proof irrelevance

#### Golol (Oct 18 2020 at 19:57):

Thanks a lot, I did the tactics proof and looked at the proof term:

theorem topological_space_eq2 : ∀ (α : Type u) (X Y : topological_space α), X.is_open = Y.is_open → X = Y :=
λ (α : Type u) (X Y : topological_space α) (h : X.is_open = Y.is_open),
X.cases_on
(λ (X_is_open : set α → Prop) (X_is_open_univ : X_is_open univ)
(X_is_open_inter : ∀ (s t : set α), X_is_open s → X_is_open t → X_is_open (s ∩ t))
(X_is_open_sUnion : ∀ (s : set (set α)), (∀ (t : set α), t ∈ s → X_is_open t) → X_is_open (⋃₀ s))
(h :
{is_open := X_is_open,
is_open_univ := X_is_open_univ,
is_open_inter := X_is_open_inter,
is_open_sUnion := X_is_open_sUnion}.is_open =
Y.is_open),
Y.cases_on
(λ (Y_is_open : set α → Prop) (Y_is_open_univ : Y_is_open univ)
(Y_is_open_inter : ∀ (s t : set α), Y_is_open s → Y_is_open t → Y_is_open (s ∩ t))
(Y_is_open_sUnion :
∀ (s : set (set α)), (∀ (t : set α), t ∈ s → Y_is_open t) → Y_is_open (⋃₀ s))
(h :
{is_open := X_is_open,
is_open_univ := X_is_open_univ,
is_open_inter := X_is_open_inter,
is_open_sUnion := X_is_open_sUnion}.is_open =
{is_open := Y_is_open,
is_open_univ := Y_is_open_univ,
is_open_inter := Y_is_open_inter,
is_open_sUnion := Y_is_open_sUnion}.is_open),
h.dcases_on
(λ (a : Y_is_open = X_is_open),
eq.rec
(λ (Y_is_open_univ : X_is_open univ)
(Y_is_open_inter : ∀ (s t : set α), X_is_open s → X_is_open t → X_is_open (s ∩ t))
(Y_is_open_sUnion :
∀ (s : set (set α)), (∀ (t : set α), t ∈ s → X_is_open t) → X_is_open (⋃₀ s))
(h :
{is_open := X_is_open,
is_open_univ := X_is_open_univ,
is_open_inter := X_is_open_inter,
is_open_sUnion := X_is_open_sUnion}.is_open =
{is_open := X_is_open,
is_open_univ := Y_is_open_univ,
is_open_inter := Y_is_open_inter,
is_open_sUnion := Y_is_open_sUnion}.is_open)
(H_2 :
h ==
eq.refl
{is_open := X_is_open,
is_open_univ := X_is_open_univ,
is_open_inter := X_is_open_inter,
is_open_sUnion := X_is_open_sUnion}.is_open),
eq.refl
{is_open := X_is_open,
is_open_univ := X_is_open_univ,
is_open_inter := X_is_open_inter,
is_open_sUnion := X_is_open_sUnion})
a.symm
Y_is_open_univ
Y_is_open_inter
Y_is_open_sUnion
h)
(eq.refl
{is_open := Y_is_open,
is_open_univ := Y_is_open_univ,
is_open_inter := Y_is_open_inter,
is_open_sUnion := Y_is_open_sUnion}.is_open)
(heq.refl h))
h)
h


I basically spent all day trying to find this proof lol. There are surely shorter term-style proofs but now I see why tactics are important...

#### Mario Carneiro (Oct 18 2020 at 20:40):

There are surely shorter term-style proofs

well yes, the first proof you posted is term-style

#### Mario Carneiro (Oct 18 2020 at 20:47):

but here's a shorter term mode proof using only rec_ons

lemma topological_space_eq' : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g :=
λ f, topological_space.cases_on f $λ a a₁ a₂ a₃, λ g, topological_space.cases_on g$ λ b b₁ b₂ b₃,
λ h : a = b, (eq.rec_on h \$ λ _ _ _, rfl) b₁ b₂ b₃


Last updated: May 19 2021 at 00:40 UTC