wlog for 5 variables

Stream: general

[Huỳnh Trần Khanh]

I guess to prove this theorem we need to do WLOG on a, b, c, d, e to get a < b < c < d < e. But in order to pull this off do I have to list all 120 permutations of the variables?

import Mathlib
theorem sumsumsum (a b c d e : ℕ) (hq : Even a ∧ Even b ∧ Even c ∧ Even d ∧ Even e) (he : [a, b, c, d, e].Nodup) (hf : ∀ x ∈ [a, b, c, d, e], x < 10) : a + b + c + d + e = 20 := by
  -- challenge: actually prove it
  -- do I have to do 120 wlogs for 120 permutations?
  sorry

[Huỳnh Trần Khanh]

I can do this for 3 variables because there are only 6 possible permutations

[Sébastien Gouëzel]

Can you try instead to do it for an arbitrary number of variables? (To avoid being distracted by irrelevant details)

[Junyan Xu]

You might want to work with tuples Fin 5 → ℕ and make use of docs#Tuple.sort which returns a monotone tuple (docs#Tuple.monotone_sort). You can prove the result for monotone tuples and show the truth of the statement is invariant under permutations.

[Huỳnh Trần Khanh]

I've decided to sacrifice computer time instead of human time :joy: by brute forcing all possible combinations

import Mathlib
set_option maxHeartbeats 999999999

theorem sumsumsum (a b c d e : ℕ) (hq : 2 ∣ a ∧ 2 ∣ b ∧ 2 ∣ c ∧ 2 ∣ d ∧ 2 ∣ e) (he : (a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ a ≠ e) ∧ (b ≠ c ∧ b ≠ d ∧ b ≠ e) ∧ (c ≠ d ∧ c ≠ e) ∧ d ≠ e) (hf : ∀ x ∈ [a, b, c, d, e], x < 10) : a + b + c + d + e = 20 := by
  obtain ⟨w, we, y, u, i⟩ := hq
  have s := hf a (by norm_num)
  have Q := hf b (by norm_num)
  have E := hf c (by norm_num)
  have K := hf d (by norm_num)
  have X := hf e (by norm_num)
  have pre1 : a = 0 ∨ a = 2 ∨ a = 4 ∨ a = 6 ∨ a = 8 := by omega
  have pre2 : b = 0 ∨ b = 2 ∨ b = 4 ∨ b = 6 ∨ b = 8 := by omega
  have pre3 : c = 0 ∨ c = 2 ∨ c = 4 ∨ c = 6 ∨ c = 8 := by omega
  have pre4 : d = 0 ∨ d = 2 ∨ d = 4 ∨ d = 6 ∨ d = 8 := by omega
  have pre5 : e = 0 ∨ e = 2 ∨ e = 4 ∨ e = 6 ∨ e = 8 := by omega
  obtain rfl | rfl | rfl | rfl | rfl := pre1
  all_goals obtain rfl | rfl | rfl | rfl | rfl := pre2
  all_goals norm_num at *
  all_goals obtain rfl | rfl | rfl | rfl | rfl := pre3
  all_goals norm_num at *
  all_goals obtain rfl | rfl | rfl | rfl | rfl := pre4
  all_goals norm_num at *
  all_goals obtain rfl | rfl | rfl | rfl | rfl := pre5
  all_goals norm_num at *

of course I did slightly optimize the code a little bit so it doesn't take too long to run but yeah

[Kevin Buzzard]

You've been talking about your experiences with Rocq/Coq recently: would this have been easier in Rocq? This is a nice example of something which is human-obvious but quite annoying to formalize if you take the naive approach. It also emphasizes the fact that Lean sometimes thinks 120 is a big number (whereas if I were writing code in magma and realised I wanted to iterate over all elements in the symmetric group S_5 I would just write the loop and not think twice, because magma thinks 120 is a very small number).

[Huỳnh Trần Khanh]

yeah unfortunately both Lean and Rocq/Coq struggle with this. and yeah both Lean and Rocq/Coq think 120 is a big number in tactic mode :pensive: which is why in the past when working on this internal project I wrote recursive definitions to do the computation separately from the proof but then it slowed me down as justifiying the correctness of the definition takes much longer... so now I'm pragmatic and just let Lean spend 1 minute to run. better than wasting an hour

[Mario Carneiro]

lol, I work on a project that took that "pragmatic" approach a long time ago, and now I and everyone else who works on the project wastes an hour building it

[Mario Carneiro]

that's absolutely not a good tradeoff

[Mario Carneiro]

here's a less brute force proof, using Sébastien Gouëzel 's advice

theorem sumsum (l : List ℕ) (hq : ∀ x ∈ l, 2 ∣ x)
    (he : l.Nodup) (hf : ∀ x ∈ l, x < 2*l.length) : l.sum = ∑ x : Fin l.length, x.1 * 2 := by
  generalize hn : l.length = n
  obtain ⟨l', rfl⟩ : ∃ l' : List (Fin n), l = l'.map fun x => x.1 * 2 := by
    use l.attach.map fun ⟨x, h⟩ => ⟨x / 2, have := hf _ h; by omega⟩
    simp []; rw [List.map_congr_left (g := id), List.map_id]
    intro x h; have := hq _ h; simp []; omega
  simp at *
  replace he := List.Nodup.of_map _ he
  let S : Finset (Fin n) := ⟨⟦l'⟧, he⟩
  show ∑ x ∈ S, ↑x * 2 = _
  simp [Finset.eq_of_subset_of_card_le (Finset.subset_univ S) (by simp [S, hn])]

theorem sumsumsum (a b c d e : ℕ) (hq : 2 ∣ a ∧ 2 ∣ b ∧ 2 ∣ c ∧ 2 ∣ d ∧ 2 ∣ e)
    (he : (a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ a ≠ e) ∧ (b ≠ c ∧ b ≠ d ∧ b ≠ e) ∧ (c ≠ d ∧ c ≠ e) ∧ d ≠ e)
    (hf : ∀ x ∈ [a, b, c, d, e], x < 10) : a + b + c + d + e = 20 := by
  have := sumsum [a,b,c,d,e] (by simpa using hq) (by simpa using he) (by simpa using hf)
  simpa [add_assoc] using this

[Bhavik Mehta]

I made an attempt earlier, but only today figured out how to make it work. So here's a more brute force proof, which just checks all the options. Mario's proof is better, and Sébastien's advice is excellent: do what they say, not what I did. That said:

import Mathlib

-- Increase this value from 128 to 4194985 = 2 ^ 22 + 681
set_option synthInstance.maxSize 4194985

theorem sumsumsum (a b c d e : ℕ) (hq : Even a ∧ Even b ∧ Even c ∧ Even d ∧ Even e)
    (he : [a, b, c, d, e].Nodup) (hf : ∀ x ∈ [a, b, c, d, e], x < 10) : a + b + c + d + e = 20 := by
  suffices
      ∀ a < 10, Even a → ∀ b < 10, Even b → ∀ c < 10, Even c → ∀ d < 10, Even d → ∀ e < 10, Even e →
      ¬a = b → ¬a = c → ¬a = d → ¬a = e → ¬b = c → ¬b = d → ¬b = e → ¬c = d → ¬c = e → ¬d = e →
      a + b + c + d + e = 20 by simp_all
  decide

Note I had to increase the synth instance size to $2^{22} + 681$, and making it any smaller breaks the proof. The default is $128$.
The proof is not massively slow though, the profiler says it takes 5 seconds, while Mario's takes 1.5 seconds.

[Aaron Liu]

With decide +kernel it takes half as long

[Bhavik Mehta]

"If true (default: false), then use only kernel reduction when reducing the Decidable instance. This is more efficient, since the default mode reduces twice", so the 2x speedup makes perfect sense

[Bhavik Mehta]

Kevin Buzzard said:

Lean sometimes thinks 120 is a big number

Also note that this proof is iterating through about $5 ^ 5$ options, so even if the 120 is too much, 3125 isn't!

[Bhavik Mehta]

Here are two more proofs. One of them only needs the maxSize to be increased to 1695, but takes around 30 seconds. The other needs the maxSize to be increased over 4 million again, but runs in under a second.

The general idea is that with some massaging, you can make it decidable and get decide to do the case-bash, but the size of the Decidable instance and the speed of the Decidable instance are very sensitive to how the expression is massaged. (The second one is entirely unsurprising, but the first one was unexpected to me).

import Mathlib

set_option trace.profiler true

set_option synthInstance.maxSize 4194985 in
-- takes about 2.5 seconds
theorem sumsumsum (a b c d e : ℕ) (hq : Even a ∧ Even b ∧ Even c ∧ Even d ∧ Even e)
    (he : [a, b, c, d, e].Nodup) (hf : ∀ x ∈ [a, b, c, d, e], x < 10) : a + b + c + d + e = 20 := by
  suffices
      ∀ a < 10, Even a → ∀ b < 10, Even b → ∀ c < 10, Even c → ∀ d < 10, Even d → ∀ e < 10, Even e →
      ¬a = b → ¬a = c → ¬a = d → ¬a = e → ¬b = c → ¬b = d → ¬b = e → ¬c = d → ¬c = e → ¬d = e →
      a + b + c + d + e = 20 by simp_all
  decide +kernel

set_option synthInstance.maxSize 1695 in
-- takes about 30 seconds
theorem sumsumsum1 (a b c d e : ℕ) (hq : Even a ∧ Even b ∧ Even c ∧ Even d ∧ Even e)
    (he : [a, b, c, d, e].Nodup) (hf : ∀ x ∈ [a, b, c, d, e], x < 10) : a + b + c + d + e = 20 := by
  suffices
      ∀ a < 10, ∀ b < 10, ∀ c < 10, ∀ d < 10, ∀ e < 10,
        Even a ∧ Even b ∧ Even c ∧ Even d ∧ Even e →
        [a, b, c, d, e].Nodup → a + b + c + d + e = 20 by simp_all
  decide +kernel

set_option synthInstance.maxSize 4126569 in
-- takes about 0.9 seconds
theorem sumsumsum2 (a b c d e : ℕ) (hq : Even a ∧ Even b ∧ Even c ∧ Even d ∧ Even e)
    (he : [a, b, c, d, e].Nodup) (hf : ∀ x ∈ [a, b, c, d, e], x < 10) : a + b + c + d + e = 20 := by
  suffices
      ∀ a < 10, Even a →
      ∀ b < 10, Even b → ¬a = b →
      ∀ c < 10, Even c → ¬a = c → ¬b = c →
      ∀ d < 10, Even d → ¬a = d → ¬b = d → ¬c = d →
      ∀ e < 10, Even e → ¬a = e → ¬b = e → ¬c = e → ¬d = e →
      a + b + c + d + e = 20 by simp_all
  decide +kernel