wlog syntax

Stream: mathlib4

[Yury G. Kudryashov]

I think that we should change wlog syntax from

wlog h : Even a generalizing a
· -- proof assuming this : ∀ a, Even a → goal and h : ¬ (Even a)
-- proof assuming h : Even a

to

wlog h : Even a generalizing a by
  -- proof assuming this  : ∀ a, Even a → goal and h : ¬ (Even a)
-- proof assuming h : Even a

similarly to suffices. What do you think?

[Yaël Dillies]

I don't like the new suffices syntax because it clashes with my idea of making by have very low precedence so that it behaves more like fun

[Ruben Van de Velde]

I'm still hoping for wlog to solve the first goal on its own, and I wonder if this would get in the way

[Yury G. Kudryashov]

I don't care about suffices ... by/wlog ... by vs suffices ... := by/wlog ... := by but I think that the current "create 2 goals" syntax is worse than both.

[Thomas Murrills]

I’m reminded of this discussion; while the focus is slightly different, if we eventually have standard syntax for dealing with side goals, that might present a natural choice of syntax here

[Thomas Murrills]

Yaël Dillies said:

I don't like the new suffices syntax because it clashes with my idea of making by have very low precedence so that it behaves more like fun

Hmm, would you mind clarifying what you mean here? I would have thought the fact that the following tactics have to be indented would give it this behavior, which probably means I’m misinterpreting!

[Yaël Dillies]

I wish for foo by simp to be valid syntax for foo (by simp), just as foo fun _ => _ is valid syntax for foo (fun _ => _)

[Eric Wieser]

I guess suffices could be adapted to suffices foo from by tac to make this precedence work

[Yaël Dillies]

Yes, you have mentioned that before and I like it

[Eric Wieser]

Have I?

[Yaël Dillies]

Ah no, you had suggested something different but similar in spirit: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/suffices.20syntax/near/422673695