Zulip Chat Archive

Stream: new members

Topic: cases under equality


view this post on Zulip Pedro Minicz (Mar 03 2021 at 20:16):

What is the name of the tactic that turns goals of the form (a, b) = (c, d) into goals of the form a = c and b = d? I know a generic tactic that does this and that works for any constructor exists, but I forgot its name.

view this post on Zulip Pedro Minicz (Mar 03 2021 at 20:16):

I had no luck finding it on the documentation thus far.

view this post on Zulip Kevin Buzzard (Mar 03 2021 at 20:16):

extensionality -- ext . It's a general principle that says that objects are equal if they have the same "external properties" (e.g. in your case, the same first and second elements) even if they have been defined in different ways. https://en.wikipedia.org/wiki/Extensionality . An example of when you might not want to consider two extensionally equal objects to be equal would be two sorting algorithms, which might have different run times, but which both do the same thing to the same input.

view this post on Zulip Yakov Pechersky (Mar 03 2021 at 20:18):

Or congr in this particular case too

view this post on Zulip Pedro Minicz (Mar 03 2021 at 20:20):

Oh, congr (or ext) is exactly what I was looking for. I guess forgetting this stuff is what happens when you take a few months break from lean. Thanks everyone!

view this post on Zulip Pedro Minicz (Mar 03 2021 at 20:36):

Knowing the tactic name was all I needed to finish my first small proof in the last few months.

import tactic

-- https://www.youtube.com/watch?v=l1FCXUi6Vlw

namespace yoneda

class functor (f : Type  Type) : Type 1 :=
(map :  {α β : Type}, (α  β)  f α  f β)
(id_map :  {α : Type}, map (id : α  α) = id)
(comp_map :  {α β γ : Type} (g : α  β) (h : β  γ), map h  map g = map (h  g))

open yoneda.functor

class natural_transformation (f : Type  Type) (g : Type  Type) [functor f] [functor g] :=
(app :  (α : Type), f α  g α)
(naturality :  {α β : Type} (h : α  β), map h  app α = app β  map h)

open natural_transformation

@[reducible] def reader (ρ α : Type) : Type := ρ  α

instance {ρ : Type} : functor (reader ρ) :=
begin
  refine { map := _, id_map := _, comp_map := _ },
  { intros α β f g, exact f  g },
  { intros α, ext, simp },
  { intros α β γ g h, ext, simp }
end

def yoneda (f : Type  Type) [functor f] (α : Type) := natural_transformation (reader α) f

lemma yoneda_lemma (f : Type  Type) [functor f] (α : Type) : yoneda f α  f α :=
begin
  refine { to_fun := _, inv_fun := _, left_inv := _, right_inv := _ },
  { intro η,
    apply η.app,
    unfold reader,
    apply id },
  { intro x,
    refine { app := _, naturality := _ },
    { intros β g, exact map g x },
    { intros β γ g,
      ext y,
      rw [function.comp_app, function.comp_app],
      rw [function.comp_app (map g), yoneda.functor.comp_map],
      refl } },
  { intros η,
    cases η,
    congr,
    ext β g,
    have h := η_naturality g,
    simp [function.comp_app (map g), h, map] },
  { intros x,
    simp [yoneda.functor.id_map] }
end

end yoneda

view this post on Zulip Yakov Pechersky (Mar 03 2021 at 21:59):

Should yoneda_lemma be a def since an equiv is data?

import tactic

-- https://www.youtube.com/watch?v=l1FCXUi6Vlw

namespace yoneda

class functor (f : Type  Type) : Type 1 :=
(map :  {α β : Type}, (α  β)  f α  f β)
(id_map :  {α : Type}, map (id : α  α) = id)
(comp_map :  {α β γ : Type} (g : α  β) (h : β  γ), map h  map g = map (h  g))

open yoneda.functor

structure natural_transformation (f : Type  Type) (g : Type  Type) [functor f] [functor g] :=
(app :  (α : Type), f α  g α)
(naturality :  {α β : Type} (h : α  β), map h  app α = app β  map h)

open natural_transformation

@[reducible] def reader (ρ α : Type) : Type := ρ  α

instance {ρ : Type} : functor (reader ρ) :=
{ map := λ _ _, (),
  id_map := λ _, rfl,
  comp_map := λ _ _ _ _ _, rfl }

def yoneda (f : Type  Type) [functor f] (α : Type) := natural_transformation (reader α) f

def yoneda_lemma (f : Type  Type) [functor f] (α : Type) : yoneda f α  f α :=
{ to_fun := λ η, η.app _ id,
  inv_fun := λ x, { app := λ _, flip map x, naturality := λ _ _ _, by {
    ext,
    dsimp [flip],
    rw [function.comp_app (map _), functor.comp_map],
    refl } },
  left_inv := λ _, natur⟩, by {
    dsimp [flip],
    congr,
    ext,
    simp [function.comp_app (map _), natur, map] },
  right_inv := λ _, by simp [flip, functor.id_map] }

end yoneda

view this post on Zulip Scott Morrison (Mar 03 2021 at 22:05):

Yakov Pechersky said:

Should yoneda_lemma be a def since an equiv is data?

Yes. In the library yoneda_lemma is this equivalence, bundled with the fact that it is natural with respect to both f and α. If you used lemma here instead of def it wouldn't be possible to even state naturality.

view this post on Zulip Eric Wieser (Mar 03 2021 at 22:25):

Is tactic#injection related to the original question?

view this post on Zulip Eric Wieser (Mar 03 2021 at 22:25):

Ah, that for hypotheses not goals


Last updated: May 15 2021 at 23:13 UTC