## Stream: general

### Topic: simp canonize

#### Simon Hudon (Jan 22 2019 at 17:28):

I'm trying to get rid of some simp loops and I just realized that there is a part of it I don't understand and it seems to be getting into a loop. Here is the trace that Lean prints for it:

[simplify.canonize]
category_theory.types
==>
category_theory.types
[simplify.canonize]
category_theory.types
==>
category_theory.types
[simplify.canonize]
_inst_2
==>
_inst_2
[simplify.canonize]
category_theory.types
==>
category_theory.types
[simplify.canonize]
category_theory.types
==>
category_theory.types
[simplify.canonize]
_inst_2
==>
_inst_2


How do I prevent it from looping? I tried simp [-category_theory.types] and it doesn't work.

#### Johan Commelin (Jan 22 2019 at 17:36):

But category_theory.types isn't even marked as [simp]. How come the simplifier is using it?

#### Simon Hudon (Jan 22 2019 at 18:36):

I am puzzled too. My tentative answer is that it comes from the canonize phase of simp which I did not know of. It seems like a phase where class instances are reduced but I can't say more. @Sebastian Ullrich, would you care to enlighten us?

#### Simon Hudon (Jan 22 2019 at 20:49):

Update: using set_option trace.debug.dsimplify true and using dsimp instead of simp, I managed to find the offender which was unrelated to canonize

MWE

#### Simon Hudon (Jan 22 2019 at 23:21):

import category_theory.category
import category_theory.types

universes u

class comonad (w : Type u → Type u)
extends functor w :=
(extract : Π {α}, w α → α)
(extend : Π {α β}, (w α → β) → w α → w β)

def Cokleisli (m) [comonad.{u} m] := Type u

instance {m} [comonad.{u} m] : category.{u} (Cokleisli m) := sorry

def copipe {w α β γ} [comonad w] (f : w α → β) (g : w β → γ) : (w α → γ) :=
g ∘ extend f

infix  =>= :55 := copipe

instance Cokleisli.category {m} [comonad m] : category (Cokleisli.{u} m) :=
{ hom := λ α β, m α → β,
id := λ α, extract,
comp := λ X Y Z f g, f =>= g,
id_comp' := sorry,
comp_id' := sorry,
assoc' := sorry }

@[simp] lemma Cokleisli.comp_def {m : Type* → Type*} [comonad m] (α β γ : Cokleisli m)
(xs : α ⟶ β) (ys : β ⟶ γ) :
xs ≫ ys = xs =>= ys := sorry

variables {α β : Type u}

example {m} [comonad m] (f : α ⟶ m α) (g : m α ⟶ α) : f ≫ g = 𝟙 _ :=
by { simp, }
-- deep recursion was detected at 'expression replacer' (potential
-- solution: increase stack space in your system)


#### Simon Hudon (Jan 22 2019 at 23:22):

If you comment out Cokleisli.comp_def, the error disappears

Last updated: May 13 2021 at 06:15 UTC