Zulip Chat Archive

Stream: mathlib4

Topic: suffices syntax

Yury G. Kudryashov (Jul 26 2023 at 13:58):

Curently, tactic mode allows both

suffices 0 < a by simpa

and

suffices : 0 < a
· simpa

Should we drop one of the versions?

Adam Topaz (Jul 26 2023 at 14:08):

What’s wrong with having both?

Anatole Dedecker (Jul 26 2023 at 14:09):

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

Anatole Dedecker (Jul 26 2023 at 14:10):

~~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 (Jul 26 2023 at 14:14):

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

Ruben Van de Velde (Jul 26 2023 at 14:14):

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 (Jul 26 2023 at 14:17):

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

Ruben Van de Velde (Jul 26 2023 at 14:32):

Right, but these features should be orthogonal

Yury G. Kudryashov (Jul 26 2023 at 15:29):

My main concern about two syntaxes is inconsistency.

Mario Carneiro (Jul 26 2023 at 18:42):

the core-preferred way to write it is

suffices 0 < a by
  simpa

Mario Carneiro (Jul 26 2023 at 18:42):

(notwithstanding one line golf)

Mario Carneiro (Jul 26 2023 at 18:43):

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 (Jul 26 2023 at 18:46):

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

Ruben Van de Velde (Jul 26 2023 at 19:22):

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 (Jul 26 2023 at 19:38):

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

Yury G. Kudryashov (Jul 26 2023 at 19:40):

But not suffices : 0 < a by ...

Eric Wieser (Aug 07 2023 at 16:05):

the core-preferred way to write it is

Does core have similar opinions on have?

Kevin Buzzard (Aug 07 2023 at 18:20):

Yury G. Kudryashov said:

But not suffices : 0 < a by ...

but suffices 0 < a by is fine and shorter!

Last updated: Dec 20 2023 at 11:08 UTC