# Zulip Chat Archive

## Stream: general

### Topic: simp

#### Sebastien Gouezel (Nov 24 2018 at 10:59):

I was really surprised by the following `simp`

behavior. There is a lemma in `ennreal`

that reads

@[simp] lemma sub_eq_zero_of_le (h : a ≤ b) : a - b = 0

It can be improved to

@[simp] lemma sub_eq_zero_iff_le : a - b = 0 ↔ a ≤ b

(following the general rule: if there is an equivalence, don't state the implication). From what I understand of the simplifier, the second version should be strictly stronger than the first. For the first one, if there is a goal `a - b = 0`

, the simplifier checks if it knows that `a ≤ b`

and if yes it closes the goal. For the second one, if there is a goal `a - b = 0`

, then it is reduced to `a ≤ b`

. Then if this fact is known to the simplifier it will reduce to `true`

and will be closed.

It turns out I am wrong: if I remove the first lemma and add the second instead, then some proofs break. I would like to understand why, and what it means on the way we should state simp lemmas.

#### Mario Carneiro (Nov 24 2018 at 11:03):

Having the second one as a rewrite lemma means that if `a - b = 0`

appears in the statement, then it can be replaced by `a <= b`

. Having the first means that if simp can prove `a <= b`

then it can replace `a - b`

in the goal with `0`

. That means that things like `(a - b) + b = b`

will simplify as well, where the iff version won't trigger

#### Mario Carneiro (Nov 24 2018 at 11:04):

generally speaking it is important to view a simp lemma as `conditions -> LHS => RHS`

, and modifications like this change the structure of the rewrite

#### Mario Carneiro (Nov 24 2018 at 11:05):

it might be that you want to rewrite `a - b = 0`

to `a <= b`

but that's a different rule

#### Sebastien Gouezel (Nov 24 2018 at 11:07):

Yes, of course. I was thinking of the lemma `lemma foo (h : a ≤ b) : (a - b = 0) ↔ true`

, but this is a different rewrite rule.

#### Kevin Buzzard (Dec 16 2019 at 11:38):

I've never worried too much about `simp`

but I am trying to write some code using the category theory library and I want to get basic automation working on it (my co-authors have always done this for me in the past).

I don't know if this is enough context, but $X$ is a topological space, $C$ is a category, and after I write this:

@[simp, refl] lemma val_eq_coe {ℱ : presheaf X C} {U : opens X} : ℱ.val U = ℱ U := rfl

(trying to train `simp`

to change the non-canonical `ℱ.val`

back into the coe-to-fun version `⇑ℱ`

) it still gets stuck, e.g. `simp`

will not solve this:

ℱ : presheaf X C, U : opens X ⊢ 𝟙 (ℱ.val U) = 𝟙 (⇑ℱ U)

I've never tried to train `simp`

before. Sorry for the hopefully basic questions.

#### Kevin Buzzard (Dec 16 2019 at 11:40):

gaargh got it

rewrite tactic failed, motive is not type correct

#### Kevin Buzzard (Dec 16 2019 at 11:42):

Can I define a new equality which is equality up to motives not being type correct?

#### Johan Commelin (Dec 16 2019 at 11:44):

@Kevin Buzzard Is this mathlib? Or are you working on another repo?

#### Kevin Buzzard (Dec 16 2019 at 11:45):

dunfold coe_fn has_coe_to_fun.coe, simp

works!

Johan -- It's my first day off in weeks and I'm just writing sheaves of categories on a topological space in the mundane way to teach myself about how to use categories in Lean.

#### Johan Commelin (Dec 16 2019 at 11:46):

Sure, but I'm confused. I don't know what `F.val`

means

#### Johan Commelin (Dec 16 2019 at 11:46):

And as far as I know mathlib also doesn't have a coe2fun for presheaves

#### Johan Commelin (Dec 16 2019 at 11:46):

In mathlib it would be `F.obj`

, I guess

#### Kevin Buzzard (Dec 16 2019 at 11:48):

structure topological_space.presheaf (X : Type w) [topological_space X] (C : Type u) [𝒞 : category.{v} C] := (val : Π (U : opens X), C) -- ℱ (res : ∀ (U V) (HVU : V ⊆ U), val U ⟶ val V) (Hid : ∀ (U), res U U (set.subset.refl U) = 𝟙 (val U)) (Hcomp : ∀ (U V W) (HWV : W ⊆ V) (HVU : V ⊆ U), res U W (set.subset.trans HWV HVU) = res U V HVU ≫ res V W HWV)

#### Kevin Buzzard (Dec 16 2019 at 11:48):

What should I have called `F.val`

? I was just making it all up.

#### Johan Commelin (Dec 16 2019 at 11:49):

There is already a definition of `presheaf`

in mathlib

#### Kevin Buzzard (Dec 16 2019 at 12:04):

I know.

#### Kevin Buzzard (Dec 16 2019 at 12:04):

I am teaching myself category theory by re-inventing the wheel.

#### Kevin Buzzard (Dec 16 2019 at 12:04):

I am already stuck ;-) I'll start another thread.

#### Reid Barton (Dec 16 2019 at 16:11):

I've never worried too much about

`simp`

but I am trying to write some code using the category theory library and I want to get basic automation working on it (my co-authors have always done this for me in the past).I don't know if this is enough context, but $X$ is a topological space, $C$ is a category, and after I write this:

@[simp, refl] lemma val_eq_coe {ℱ : presheaf X C} {U : opens X} : ℱ.val U = ℱ U := rfl(trying to train

`simp`

to change the non-canonical`ℱ.val`

back into the coe-to-fun version`⇑ℱ`

) it still gets stuck, e.g.`simp`

will not solve this:

ℱ : presheaf X C,

U : opens X

⊢ 𝟙 (ℱ.val U) = 𝟙 (⇑ℱ U)

I've never tried to train `simp` before. Sorry for the hopefully basic questions.

Use `dsimp`

Last updated: Dec 20 2023 at 11:08 UTC