Showing topological_space_eq "manually"

Stream: maths

[Golol]

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]

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]

In fact refl will not prove this goal

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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

[Golol]

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]

There are surely shorter term-style proofs

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

[Mario Carneiro]

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₃