simp documentation

Stream: general

[Simon Hudon]

@Kevin Buzzard I'm having a look at your recent PR. In "When it is unadvisable to use simp", why not use show instead of suffices?

[Kevin Buzzard]

I think that's kind of backwards

[Kevin Buzzard]

let's say you're a long way from a goal

[Kevin Buzzard]

and simp makes tiny progress

[Kevin Buzzard]

no wait

[Kevin Buzzard]

simp changes your goal slightly

[Kevin Buzzard]

it makes it into X

[Kevin Buzzard]

then suffices X, simpa [this] does the same thing

[Kevin Buzzard]

but show won't work

[Kevin Buzzard]

becuase X isn't defeq to the original goal

[Kevin Buzzard]

The idiom (is that the right word?) is that if simp changes your goal to X, then why not make a new goal and instantly close it with simp.

[Simon Hudon]

Good point. Then you can only choose show in the special case where the new goal is defeq to the old one.

[Simon Hudon]

It might be worth having a shortcut for suffices : (simplified thing), by simpa [this]

[Kevin Buzzard]

yeah, it's simp ;-)

[Kevin Buzzard]

simp to (simplified thing)?

[Mario Carneiro]

simpa was intended for basically exactly that use case. It's not exactly wasting that many keywords as it is

[Kevin Buzzard]

yeah but golf

[Mario Carneiro]

for golf, simpa [bla] using bla is even more effective

[Kevin Buzzard]

simp {answer := simplified thing}

[Mario Carneiro]

also, you can just write suffices : (simplified thing), {simpa}