Zulip Chat Archive

Stream: general

Topic: more problems with coercions


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

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

view this post on Zulip Scott Morrison (Aug 06 2018 at 05:15):

Here's my slightly minimised example:

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

view this post on Zulip Scott Morrison (Aug 06 2018 at 05:16):

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

view this post on Zulip Scott Morrison (Aug 06 2018 at 05:16):

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

view this post on Zulip Scott Morrison (Aug 06 2018 at 05:20):


view this post on Zulip Mario Carneiro (Aug 06 2018 at 05:23):

You have to use dsimp

view this post on Zulip Mario Carneiro (Aug 06 2018 at 05:23):

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

view this post on Zulip Mario Carneiro (Aug 06 2018 at 05:24):

this messes up dsimp

view this post on Zulip Scott Morrison (Aug 06 2018 at 05:24):

ah..

view this post on Zulip Scott Morrison (Aug 06 2018 at 05:24):

I never knew that.

view this post on Zulip Scott Morrison (Aug 06 2018 at 05:25):

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

view this post on Zulip Mario Carneiro (Aug 06 2018 at 05:25):

You should always prove definitional theorems by rfl

view this post on Zulip Mario Carneiro (Aug 06 2018 at 05:26):

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

view this post on Zulip Scott Morrison (Aug 06 2018 at 05:26):

what does by refl do?

view this post on Zulip Mario Carneiro (Aug 06 2018 at 05:26):

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

view this post on Zulip Scott Morrison (Aug 06 2018 at 05:26):

surely that's the same thing

view this post on Zulip Scott Morrison (Aug 06 2018 at 05:27):

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

view this post on Zulip Scott Morrison (Aug 06 2018 at 05:27):

I guess I can check.

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

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

view this post on Zulip Johan Commelin (Aug 06 2018 at 05:34):

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

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

view this post on Zulip Mario Carneiro (Aug 06 2018 at 06:05):

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

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

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