## 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

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