Still don't understand simp

Stream: general

[Kevin Buzzard]

I still don't understand simp. I tried

example (c : ℕ) (H : 0 + 0 + c = 0) : c = 0 := by simp [H]

fully expecting it to work, and it didn't. So I switched to by simp at H;assumption which works fine -- but I feel like I'm missing a trick. What is the correct way to solve this goal? I know I could prove it using zero_add a couple of times -- is best practice to spell out the proof in full or use automation?

[Kevin Buzzard]

The moment I try zero_add in term mode I find myself in triangle hell.

[Chris Hughes]

simpa using h

[Chris Hughes]

simp * at *

[Kevin Buzzard]

simpa using h

Do I need an import for this?

[Mario Carneiro]

just the usual

[Kevin Buzzard]

That's happening to me more and more. Is there any way I can import every mathlib tactic automatically?

[Mario Carneiro]

import tactic.interactive gets the main tactics, but advanced tactics have their own imports, in particular ring and finish

[Kevin Buzzard]

Is there any reason I shouldn't import ring always?

[Mario Carneiro]

if you don't need it, don't import it

[Mario Carneiro]

and you shouldn't overuse it anyway, it's slow

[Kevin Buzzard]

if you don't need it, don't import it

Why not? If I don't use it, it doesn't even matter

[Mario Carneiro]

it adds a spurious dependency, which is probably a bigger problem for me than for you

[Mario Carneiro]

Of course, adding additional dependencies also slows down startup and recompile times

[Kevin Buzzard]

Even if I never use them?

[Kevin Buzzard]

They're compiled on sight?

[Mario Carneiro]

of course, how would it know if you have used the file unless it compiles the dependency?

[Mario Carneiro]

the way you are supposed to signal what you depend on is in your import list

[Kevin Buzzard]

How about I don't import it, and every time I use it a little pop-up appears saying "I see you're using ring. Do you want to import tactic.ring?"

[Mario Carneiro]

how would it know that ring exists?

[Kevin Buzzard]

and same for simpa and tactic.interactive

[Kevin Buzzard]

how would it know that ring exists?

Because I just tell it, using a "snippet" or something?

[Kevin Buzzard]

"I see that you just deleted the last occurrence of simpa. Do you want me to unimport it again?"

[Kevin Buzzard]

"I see that you used simp. Do you want me to replace that argument with what Lean actually did?"

[Mario Carneiro]

hm, I suppose one option is to somehow generate an "index" of all definitions in mathlib and their locations, and then store this info in some file with no dependencies and use it for hints

[Mario Carneiro]

Import analysis like that is very expensive

[Kevin Buzzard]

I'm basically asking for some sort of tactic manager I think.

[Kevin Buzzard]

I just have no idea about what is possible.

[Kevin Buzzard]

Does simpa !? only? (* | [(* | (- id | expr)), ...]?) (with id*)? (using expr)? tactic.simp_config_ext? actually mean something? Where can I learn about what it means?

[Mario Carneiro]

It is hard to get the analysis exactly right without just recompiling the current file, and if it's not exactly right then there is the possibility of incorrect hints, which will get old fast

[Mario Carneiro]

yes, it's a description of the parsing of arguments following simpa

[Kevin Buzzard]

I want it to be a regex but I can't make sense of it

[Mario Carneiro]

Basically ? means that the previous thing may or may not be present, and * means zero or more of the previous thing

[Sebastian Ullrich]

It's a pseudorex

[Kevin Buzzard]

oh is it just a regex but using stuff I don't know?

[Kevin Buzzard]

Aah thanks!

[Mario Carneiro]

| means alternatives

[Mario Carneiro]

i.e. a | b means parse a or parse b

[Kevin Buzzard]

and expr is some kind of variable? Or you want something of type expr?

[Mario Carneiro]

expr means parse an expression

[Mario Carneiro]

and id means parse an identifier

[Kevin Buzzard]

I thought that h was a name in simpa using h, not an expr

[Mario Carneiro]

nope, look for simpa using show in mathlib and you will find several larger examples

[Mario Carneiro]

it's a nice way to say "use this term, but clean it up first"

[Kevin Buzzard]

so what's with?

[Kevin Buzzard]

I just apply these things at random usually.

[Mario Carneiro]

most of the args are just passed to simp as is

[Kevin Buzzard]

I have a list of "incantations formed with simp or simpa which have worked for me in the past"

[Mario Carneiro]

that includes ! and with

[Mario Carneiro]

the with arg of simp allows you to simplify with custom simp sets, like functor_norm

[Mario Carneiro]

I don't use it much at all

[Kevin Buzzard]

What does simpa [this] do? Does that not even parse?

[Chris Hughes]

The same as simp [this], assumption

[Kevin Buzzard]

example (c : ℕ) (H : 0 + 0 + c = 0) : c = 0 := by simpa -- fails
example (c : ℕ) : 0 + 0 + c = 0 → c = 0 := by simpa -- works

If you'd told me one works and one failed I would have guessed the other way around.

[Chris Hughes]

The second one is simplified to c=0 -> c=0. The first one doesn't simplify H

[Kevin Buzzard]

example : ∀ (y : ℕ), (λ (c : ℕ), 0 + 0 + c = 0) y → y = 0 := by simp

[Kevin Buzzard]

I wouldn't have dreamed of applying simp to that because it's not an equality. Am I using simp completely wrong?

[Mario Carneiro]

Actually simpa [this] is a bit funny - it's more like have this' := this, simp [this] at this', simp [this], exact this'

[Mario Carneiro]

for the first example you want by simpa using H

[Mario Carneiro]

The using argument of simpa is pretty important. It's not really optional, it just has a default value of this

[Mario Carneiro]

so by simpa where there is no this in the context is kind of pointless

[Chris Hughes]

One nice feature of simp I discovered today, is it doesn't let you make horrible simp lemma. I tried to prove forall x : zmod 2, x = -x and it didn't let me make it simp

[Kevin Buzzard]

If you try it again you might get banned

[Kevin Buzzard]

"no more simp for you for a week"

[Mario Carneiro]

your use of simp to prove that is valid but a bit funny and doesn't generalize well

[Mario Carneiro]

I would do intros y H; simpa using H

[Mario Carneiro]

simp {contextual := tt} often works in these situations, but I don't think it simplifies the assumptions first