I don't get `simp`

Stream: general

[Kevin Buzzard]

I have been doing a lot of mathematics in Lean recently -- not plumbing, but high-level stuff, API-making. I never tag anything with simp though, because I don't know how simp works. My favourite tactic is rfl and a lot of my proofs are of the form rw [A,B,C], show X, rw [D,E,F], show Y, rwa [G,H]. I have no feeling as to whether G and H should be simp lemmas, or even if the assertion that Y is equal to the thing I changed into Y with the show command should be a simp lemma, even though the proof is rfl.

Yesterday Patrick was frustrated because some complete triviality which to a mathematician's eyes looks like the statement $1/x = 1/x$ could not be proved with refl or simp, so he formalised a statement which would suffice for his purposes and asked me if I could prove it for him (because like doing these little puzzles and Patrick has no time for them).

lemma thing_which_will_do {α : Type*} [division_ring α] (x : units α) :
  (x : α)⁻¹ = x.inv := sorry

I tried simp and it didn't work, so I opened up the division ring API and had a look. Note that I say this, but there is no division ring API really, there are a bunch of lemmas which might be in the division ring namespace, or might ask for division ring instances using type class inference, or they might be in completely different namespaces like the semiring namespace but they apply to division rings anyway even though this is not explicitly noted in mathlib (should it be?) and they're scattered around, but I know my way around now. A mathematician-sanitised version of #print prefix division_ring would be really nice, we don't care much about recursors and assertions about size_of, we just want to see universal properties and basic lemmas. What I guess I would like to have access to is some sort of "mathematician's API for division rings in Lean", where we get to see once and for all what we are supposed to be using. I would also need a "mathematician's API for units of a ring in Lean" I think -- but once I have these, will I see x.inv in them? This could also be written as ((x⁻¹ : units α) : α). Is this somehow the "correct" way to access the inv field for a unit?

Here is my proposed proof of Patrick's lemma.

import algebra.field

@[simp]
lemma units.coe_inv' {α : Type*} [division_ring α] (x : units α) :
  ((x⁻¹ : units α) : α) = x⁻¹ := by simp

-- Should the only simp lemma mentioning x.inv be that x.inv is ((x⁻¹ : units α) : α) ?

lemma thing_which_will_do {α : Type*} [division_ring α] (x : units α) :(x : α)⁻¹ = x.inv :=
-- by simp #exit -- doesn't work
(units.coe_inv' _).symm -- why doesn't simp work yet?

I can't get simp to work. I am unclear about whether we should need the lemma at all. How does all this work? Not understanding how to use simp properly in my own API's is bad; I would like to learn how to write better API's. Are there rules saying what should and should not go into a simp lemma? How come I can prove units.coe_inv' using simp but I can't prove the lemma in the form Patrick gave to me using simp? How do I make simp work better for me?

[Jesse Michael Han]

simp lemmas will trigger on a syntactic match, so if one hasn't been careful with sticking to a canonical form, a change is sometimes required:

lemma thing_which_will_do {α : Type*} [division_ring α] (x : units α) :
  (x : α)⁻¹ = x.inv :=
by {change _ = ↑(x⁻¹), simp}

[Jesse Michael Han]

i'm not sure if it would be feasible to try to have simp lemmas trigger on successful unification instead of a syntactic match. it would make simp a lot slower, and for definitionally-provable simp lemmas it would naiively just try them over and over again.

maybe a tactic which just attempts to rewrite subterms to all the definitionally equal things it can think of would be useful for these kinds of situations. (we should call it dblast)

[Kevin Buzzard]

simp lemmas will trigger on a syntactic match, so if one hasn't been careful with sticking to a canonical form, a change is sometimes required:

Well I didn't write division rings and I didn't write units. How do I find out the canonical form of (x : α)⁻¹ = x.inv?

[Jesse Michael Han]

the convention is set by whoever wrote the library (like how mathlib prefers le over ge, so that ge goals must be changed to le before simp will work, or how finset.to_set is superceded by the uparrow coercion notation in most lemmas). i think for now one has to just poke around in the library and look at the simp lemmas to see what the conventions are.

[Kevin Buzzard]

I see, so there is no formal place to read the canonical notation? And is it always there, or sometimes do different people use different competing canonical notation?

[Jesse Michael Han]

maybe it wouldn't be hard to write a tool which checks what the preferred definitionally-equivalent version of a given term is in the imported libraries. but right now, i think the task of ensuring uniform conventions falls to the mathlib maintainers.

sometimes, if you aren't careful in writing a library, you find yourself with two different families of simp lemmas with different conventions, and then things become very unpleasant (this has happened to me)

[Mario Carneiro]

in this case the preference is for (x : α)⁻¹

[Mario Carneiro]

they should be defeq btw

[Mario Carneiro]

oh wait, nvm, it's defeq to (x⁻¹ : α) but the other way around depends on division_ring axioms

[Kevin Buzzard]

Right. I know how to prove it. The question is whether simp should prove it, or whether we should not even be formulating the statement this way at all, or something else?

[Patrick Massot]

I think Jesse and Mario are trying to answer the question. Once we know what is favored by the library, we must hunt for the bad simp lemma that brought a forbidden form

[Kevin Buzzard]

Are there simp lemmas of the form bad way to say something = good way to say it?

[Kevin Buzzard]

e.g is x.inv = (x⁻¹ : units alpha)) a simp lemma? That's saying that a bad way is a good way (if x is a unit). I think.

[Mario Carneiro]

yes

[Jesse Michael Han]

in this case i don't see why not (i don't see how marking it simp would throw it into a loop)

[Kevin Buzzard]

And simp would never apply them in reverse to get an unconventional thing?

[Mario Carneiro]

right

[Kevin Buzzard]

I see. So Patrick the onus seems to be on us to find out why we thought we needed this lemma.

[Mario Carneiro]

If you never write the bad way and no simp lemma generates it, then this bad way fixing lemma will never be invoked. So it is often omitted

[Mario Carneiro]

It's good documentation though, since it indicates that the bad way is a bad way according to the local convention. Otherwise you have to know the mind of the author

[Wojciech Nawrocki]

Personally I think of simp as being not much more than a system which automatically applies rewrites to bring expressions from, like you called it, a "bad form" to a "good form". Sometimes having just a single simp makes things a bit restrictive, since depending on context "good form" might mean different things. Something I ended up doing as an experiment was to create a new simp attribute with run_cmd mk_simp_attr ``sop_form [``simp]. What this does is allow you to tag lemmas with @[sop_form] instead of @[simp] and then simp with sop_form will apply all rewrites tagged with sop_form (sop stands for sum-of-products, as this grouping of lemmas was meant to bring expressions to a SOP form).