Style: hypothesis left of colon vs pattern matching

Stream: mathlib4

[Michael Rothgang]

Here's a style guideline question that arose in #30508: should there be an exception to the "hypotheses left of colon" rule for pattern matching? More concretely, several changes in the PR are of the following kind, changing

lemma listSum_le [AddLeftMono S] (l : List R) : abv l.sum ≤ (l.map abv).sum := by
  induction l with
  | nil => simp
  | cons head tail ih => exact (abv.add_le ..).trans <| add_le_add_left ih (abv head)

by

lemma listSum_le [AddLeftMono S] : ∀ l : List R, abv l.sum ≤ (l.map abv).sum
  | [] => by simp
  | a :: l => by grw [List.map_cons, List.sum_cons, List.sum_cons, abv.add_le, listSum_le]

which includes a golf (that I like), but also moves hypotheses "right of the colon" by introducing a \forall quantifier in the theorem type. On the other hand, that introduction enables golfing the proof by a line, because pattern matching becomes available.

I'd like to have a general vibe check: should this be an exception to the style guide, or do we consider saving one line not desirable?

[Michael Rothgang]

(I personally don't feel strongly, but feel we should not knowingly violate our style guide.)

[Yakov Pechersky]

I think the former is still preferable because it might get golfed into an induction <;> grind call

[Aaron Liu]

I didn't like this change because it gives you a match and it messes up the equations

[Chris Henson]

Yakov Pechersky said:

I think the former is still preferable because it might get golfed into an induction <;> grind call

Concretely, you could write:

import Mathlib

variable {R S : Type*} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S)

lemma AbsoluteValue.listSum_le' [AddLeftMono S] (l : List R) : abv l.sum ≤ (l.map abv).sum := by
  induction l <;> grind [map_zero, le_refl, listSum_le]

[Yaël Dillies]

My concern is that disallowing this would completely forbid pattern-matching in proofs, which seems unreasonable

[Yaël Dillies]

I don't disagree that there may be further golfs available in specific cases

[Aaron Liu]

Yaël Dillies said:

My concern is that disallowing this would completely forbid pattern-matching in proofs, which seems unreasonable

I'm not saying you can't match I'm saying I don't like when you unname the hypotheses as a result of putting the match in that spot

[Aaron Liu]

and of course by you I mean everyone

[Yaël Dillies]

What do you mean by "unname"? There is no hypothesis anymore, you directly call the lemma recursively (and so it is "named" like the lemma).

[Aaron Liu]

it means the name of the hypothesis gets erased

[Yaël Dillies]

I don't understand what you are talking about. Can you show an example?

[Aaron Liu]

Here like this

theorem k1 (n : Nat) (hn : n ≠ 0) : 0 < n :=
  Nat.zero_lt_of_ne_zero hn

#check k1 (n := Nat.succ 2) (hn := Nat.succ_ne_zero 2)

theorem k2 : (n : Nat) → n ≠ 0 → 0 < n
  | _, hn => Nat.zero_lt_of_ne_zero hn

-- uhoh
#check k2 (n := Nat.succ 2) (hn := Nat.succ_ne_zero 2)

[Yaël Dillies]

1. This is not what Michael and I are talking about. There is no hn-like hypothesis in any of the code snippets above, except yours.
2. This is easily fixable without getting rid of the pattern-matching:

theorem k1 (n : Nat) (hn : n ≠ 0) : 0 < n :=
  Nat.zero_lt_of_ne_zero hn

#check k1 (n := Nat.succ 2) (hn := Nat.succ_ne_zero 2)

theorem k2 : (n : Nat) → (hn : n ≠ 0) → 0 < n
  | _, hn => Nat.zero_lt_of_ne_zero hn

-- works
#check k2 (n := Nat.succ 2) (hn := Nat.succ_ne_zero 2)

[Aaron Liu]

1. Ok it doesn't apply to this case specifically but this is a minor annoyance I have come across
2. but unfortunately no one writes like that (or at least, not that I've seen anywhere) and I think it sets off an unused variable linter (after I tested, it doesn't seem to be?)

[Yaël Dillies]

Aaron Liu said:

unfortunately no one writes like that

That you can complain about. But we shouldn't ban pattern-matching because people sometimes misuse it!

[Yaël Dillies]

Chris Henson said:

Yakov Pechersky said:

I think the former is still preferable because it might get golfed into an induction <;> grind call

Concretely, you could write:

import Mathlib

variable {R S : Type*} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S)

lemma AbsoluteValue.listSum_le' [AddLeftMono S] (l : List R) : abv l.sum ≤ (l.map abv).sum := by
  induction l <;> grind [map_zero, le_refl, listSum_le]

Your suggestion got me confused for a very long time: It is not valid, because you renamed listSum_le to listSum_le' in the statement but not in the proof. Therefore all that grind does is apply the existing lemma from mathlib!

[Yaël Dillies]

In fact, none of the proofs in #30508 that Michael is concerned about can be proved with induction ... <;> grind [...]. This is expected, since grind doesn't know about generalised rewriting, and this is a PR about grw and gcongr.

[Jovan Gerbscheid]

I left a comment at the PR which is now #30632. Although your matching style might be nice in some situations, I think there is also value in keeping the proof (and statement) style consistent throughout mathlib, and sticking to the induction tactic.

[Yaël Dillies]

In fact, a lot of proofs already use pattern-matching. This is the default in all List files for example. I therefore do not buy this consistency argument.

[Jovan Gerbscheid]

Maybe, but I'd say that matching on lists feels a bit different from matching on natural numbers.

[Michael Rothgang]

My reading is that your stance, @Jovan Gerbscheid, is "matching on lists is fine, but use induction for natural numbers, please"? Is that a correct reading? @Yaël Dillies What do you think here?

[Michael Rothgang]

I don't really have a horse in this race; I'm sympathetic to a consistency argument --- but am not sure if matching on natural numbers is used more commonly than induction. (For lists, it might well be, in which case I'm happy to go with it!)

[Jovan Gerbscheid]

Yes. If you are proving a list lemma where the list is the main object of study, and if it is very obvious that the proof should go by induction, then I think that is comparatively a better situation to do a proof using recursion and an implicit match.

But for proofs with natural numbers, I think it is cleaner to have an explicit induction tactic. This comes with the added benefits that the proof is more flexible (you can add a tactic before induction, you can do induction n <;> grind) and that the theorem headers look consistent.

[Yakov Pechersky]

There is also the case to be made that more proofs can use fun_induction