cases under equality

Stream: new members

[Pedro Minicz]

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.

[Pedro Minicz]

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

[Kevin Buzzard]

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.

[Yakov Pechersky]

Or congr in this particular case too

[Pedro Minicz]

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!

[Pedro Minicz]

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

[Yakov Pechersky]

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

[Scott Morrison]

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.

[Eric Wieser]

Is tactic#injection related to the original question?

[Eric Wieser]

Ah, that for hypotheses not goals