simp

Stream: general

[Sebastien Gouezel]

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]

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]

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]

it might be that you want to rewrite a - b = 0 to a <= b but that's a different rule

[Sebastien Gouezel]

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]

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]

gaargh got it

rewrite tactic failed, motive is not type correct

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Johan Commelin]

In mathlib it would be F.obj, I guess

[Kevin Buzzard]

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]

What should I have called F.val? I was just making it all up.

[Johan Commelin]

There is already a definition of presheaf in mathlib

[Kevin Buzzard]

I know.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

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