suffices syntax

Stream: mathlib4

[Yury G. Kudryashov]

Curently, tactic mode allows both

suffices 0 < a by simpa

and

suffices : 0 < a
· simpa

Should we drop one of the versions?

[Adam Topaz]

What’s wrong with having both?

[Anatole Dedecker]

Was the second one introduced recently? I remember trying it 2 weeks ago and it didn't work

[Anatole Dedecker]

The problem with the second one is that writing name : type := proof strongly suggests that proof : type, wherehas here proof is a proof of the goal with the added hypothesis name : type...

[Yury G. Kudryashov]

@Anatole Dedecker There was a typo in the second one. Fixed.

[Ruben Van de Velde]

I believe one is from core and one from mathlib; it's pretty annoying that they have significantly different syntax. The first one also allows suffices foo from term

[Adam Topaz]

But they have different reasons for being used. In the second you can optionally name the hypothesis.

[Ruben Van de Velde]

Right, but these features should be orthogonal

[Yury G. Kudryashov]

My main concern about two syntaxes is inconsistency.

[Mario Carneiro]

the core-preferred way to write it is

suffices 0 < a by
  simpa

[Mario Carneiro]

(notwithstanding one line golf)

[Mario Carneiro]

refactoring this was considered for mathport but it's just a bit too tricky to do reliably so I left it for after the port / via linter

[Mario Carneiro]

it really only exists for backward compatibility with lean 3, same thing with have; tac

[Ruben Van de Velde]

Mario Carneiro said:

the core-preferred way to write it is

suffices 0 < a by
  simpa

With no way to rename the hypothesis? I guess I don't particularly mind, but it seems a strange limitation when you're used to the lean3 version

[Mario Carneiro]

you can write suffices h : 0 < a by ... too

[Yury G. Kudryashov]

But not suffices : 0 < a by ...

[Eric Wieser]

the core-preferred way to write it is

Does core have similar opinions on have?

[Kevin Buzzard]

Yury G. Kudryashov said:

But not suffices : 0 < a by ...

but suffices 0 < a by is fine and shorter!

[Filippo A. E. Nuccio]

I am sorry to resurrect this stream, but I have seen #10534 by @Eric Wieser and I see that the doc concerning suffices is still the old one, saying

Given a main goal ctx ⊢ t, suffices h : t' from e replaces the main goal with ctx ⊢ t', e must have type t in the context ctx, h : t'.

The variant suffices h : t' by tac is a shorthand for suffices h : t' from by tac. If h : is omitted, the name this is used.

I wanted to create a PR, but I realise that I find the indenting requirement very odd: the goal that needs to be fixed after suffices is the original one, so it is not a side goal, yet indentation is required. Isn't this opposite to what I read here :

When new goals arise as side conditions or steps, they are indented and preceded by a focusing dot · (inserted as \.); the dot is not indented.

?

[Riccardo Brasca]

Related discussion. I don't know a reasonable way of writing a proof that uses suffices. (I see there are tricks to make it OK, but it would be nice to have an official workflow.)

[Filippo A. E. Nuccio]

And coherent, official doc!

[Yaël Dillies]

Also the new suffices notation is inconsistent with the new have notation

[Yaël Dillies]

In particular, the by is not separated from the rest of the term which to me is really really bad because I was independently hoping we could make by have the same precedence as fun (there are so many $ by everywhere), and that new suffices syntax seems to be conflicting with this.

[Eric Wieser]

Should it be suffices h : foo => instead?

[Yaël Dillies]

That would make more sense than currently at least

[Yaël Dillies]

Also because we need a colon to put binders before, the same way the have syntax does it

[Riccardo Brasca]

Maybe we can discuss this in the lean4 stream? All these tactics are in core, and even if we can modify the standard behavior it's probably a good idea to follow what core does.

[Filippo A. E. Nuccio]

Eric Wieser said:

Should it be suffices h : foo => instead?

Well, already having the colon would be a great advance (it makes more type-theoretic sense). I also do not understand the indentation of the dot that should be used: the first goal that one approaches is not a side goal , just the first one. It should be possible to work on it withoug indentation.

[Filippo A. E. Nuccio]

Riccardo Brasca said:

Maybe we can discuss this in the lean4 stream? All these tactics are in core, and even if we can modify the standard behavior it's probably a good idea to follow what core does.

Or to ask for some modification in core...