more problems with coercions

Stream: general

[Scott Morrison]

So... I've been trying to implement @Mario Carneiro's suggestion that I define the coercion allowing F X for a functor F on an object X, and define a @[simp] lemma unfolding the coercion.

[Scott Morrison]

I immediately run into trouble, however, where simp fails to apply the simp lemma, because a motive is not correct:

[Scott Morrison]

Here's my slightly minimised example:

[Scott Morrison]

namespace category_theory

universes u v

meta def obviously := `[skip]

class category (Obj : Type u) : Type (max u (v+1)) :=
(Hom     : Obj → Obj → Type v)
(id      : Π X : Obj, Hom X X)
(comp    : Π {X Y Z : Obj}, Hom X Y → Hom Y Z → Hom X Z)
(id_comp : ∀ {X Y : Obj} (f : Hom X Y), comp (id X) f = f . obviously)
(comp_id : ∀ {X Y : Obj} (f : Hom X Y), comp f (id Y) = f . obviously)
(assoc   : ∀ {W X Y Z : Obj} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z), comp (comp f g) h = comp f (comp g h) . obviously)

notation `𝟙` := category.id -- type as \b1
infixr ` ≫ `:80 := category.comp -- type as \gg
infixr ` ⟶ `:10 := category.Hom -- type as \h

attribute [simp] category.id_comp category.comp_id category.assoc

universes u₁ v₁ u₂ v₂ u₃ v₃

structure Functor (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [category.{u₂ v₂} D] : Type (max u₁ v₁ u₂ v₂) :=
(obj           : C → D)
(map           : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y)))
(map_id        : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
(functoriality : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) . obviously)

attribute [simp] Functor.map_id Functor.functoriality

infixr ` ↝ `:70 := Functor       -- type as \lea -- unfortunately ⇒ (`\functor`) is taken by core.

namespace Functor

section
variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
include 𝒞 𝒟

instance : has_coe_to_fun (C ↝ D) :=
{ F   := λ F, C → D,
  coe := λ F, F.obj }

@[simp] lemma unfold_obj_coercion (F : C ↝ D) (X : C) : F X = F.obj X := by refl
end

section
variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C] {D : Type u₂} [𝒟 : category.{u₂ v₂} D] {E : Type u₃} [ℰ : category.{u₃ v₃} E]
include 𝒞 𝒟 ℰ

set_option trace.check true

definition comp (F : C ↝ D) (G : D ↝ E) : C ↝ E :=
{ obj    := λ X, G (F X),
  map    := λ _ _ f, G.map (F.map f),
  map_id := begin
             intros,
             simp, /- why didn't that unfold the coercion? -/
             rw unfold_obj_coercion F X /- oh. -/
            end,
  functoriality := begin intros, simp end }
end

end Functor

end category_theory

[Scott Morrison]

(Being told my motive is not correct always makes me feel very guilty.)

[Scott Morrison]

Hopefully I'm just doing something dumb here...

[Scott Morrison]

---

[Mario Carneiro]

You have to use dsimp

[Mario Carneiro]

is there a reason you use by refl instead of rfl to prove rfl-lemmas?

[Mario Carneiro]

this messes up dsimp

[Scott Morrison]

ah..

[Scott Morrison]

I never knew that.

[Scott Morrison]

Okay. That should fix my problems, but wow, gross! :-)

[Mario Carneiro]

You should always prove definitional theorems by rfl

[Mario Carneiro]

because lean reads that specially: A = B := rfl means A === B

[Scott Morrison]

what does by refl do?

[Mario Carneiro]

It proves the theorem normally, so you just end up learning A = B

[Scott Morrison]

surely that's the same thing

[Scott Morrison]

but isn't the proof term the same either way?

[Scott Morrison]

I guess I can check.

[Mario Carneiro]

it is, but the literal token rfl is used by the lean parser to add the @[_refl_lemma] attribute

[Johan Commelin]

It really is a pity that refl and rfl have such important but subtle distinctions, while only differing by one letter.

[Johan Commelin]

And then rfl (without e) adds @[_refl_lemma] (with e)!

[Mario Carneiro]

to be fair, one is a tactic and one is a term, so they differ by more than one letter

[Mario Carneiro]

although you shouldn't confuse rfl with eq.refl either

[Mario Carneiro]

similarly there is iff.rfl and iff.refl, etc. The naming convention has rfl have an implicit argument and refl has an explicit arg

[Scott Morrison]

Thanks for explaining this rfl vs refl thing. Switching to rfl really helps, both here and elsewhere. :-)