## Stream: general

### Topic: more problems with coercions

#### Scott Morrison (Aug 06 2018 at 05:14):

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 (Aug 06 2018 at 05:15):

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

#### Scott Morrison (Aug 06 2018 at 05:15):

Here's my slightly minimised example:

#### Scott Morrison (Aug 06 2018 at 05:15):

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 (Aug 06 2018 at 05:16):

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

#### Scott Morrison (Aug 06 2018 at 05:16):

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

#### Mario Carneiro (Aug 06 2018 at 05:23):

You have to use dsimp

#### Mario Carneiro (Aug 06 2018 at 05:23):

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

#### Mario Carneiro (Aug 06 2018 at 05:24):

this messes up dsimp

ah..

#### Scott Morrison (Aug 06 2018 at 05:24):

I never knew that.

#### Scott Morrison (Aug 06 2018 at 05:25):

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

#### Mario Carneiro (Aug 06 2018 at 05:25):

You should always prove definitional theorems by rfl

#### Mario Carneiro (Aug 06 2018 at 05:26):

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

#### Scott Morrison (Aug 06 2018 at 05:26):

what does by refl do?

#### Mario Carneiro (Aug 06 2018 at 05:26):

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

#### Scott Morrison (Aug 06 2018 at 05:26):

surely that's the same thing

#### Scott Morrison (Aug 06 2018 at 05:27):

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

#### Scott Morrison (Aug 06 2018 at 05:27):

I guess I can check.

#### Mario Carneiro (Aug 06 2018 at 05:27):

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

#### Johan Commelin (Aug 06 2018 at 05:34):

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

#### Johan Commelin (Aug 06 2018 at 05:34):

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

#### Mario Carneiro (Aug 06 2018 at 06:05):

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

#### Mario Carneiro (Aug 06 2018 at 06:05):

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

#### Mario Carneiro (Aug 06 2018 at 06:06):

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 (Aug 06 2018 at 06:31):

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

Last updated: May 08 2021 at 04:14 UTC