Zulip Chat Archive

Stream: maths

Topic: Showing topological_space_eq "manually"


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

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

view this post on Zulip Mario Carneiro (Oct 18 2020 at 16:35):

In fact refl will not prove this goal

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

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

view this post on Zulip Mario Carneiro (Oct 18 2020 at 16:57):

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

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

view this post on Zulip Mario Carneiro (Oct 18 2020 at 16:59):

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

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

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

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