what is the fastest way to prove this

Stream: general

[Kenny Lau]

p q t : ℕ+,
xp xq : ℤ,
m n : ℕ,
hm : ↑t = ↑p * m,
hn : ↑t = ↑q * n,
hpqt : xp * ↑m = xq * ↑n
⊢ xp * ↑q = xq * ↑p

[Chris Hughes]

Best I could do. It's not easy to keep it short.

example {p q t : ℕ+} {xp xq : ℤ} {m n : ℕ} (hm : (t : ℕ) = ↑p * m) (hn : (t : ℕ) = ↑q * n)
    (hpqt : xp * m = xq * n) : xp * q = xq * p :=
have hm0 : (m : ℤ) ≠ 0 := int.coe_nat_ne_zero.2 (λ h, lt_irrefl (0 : ℕ) (trans_rel_left
    (<) t.2 (by rwa [h, mul_zero] at hm))),
have hm' : (t : ℤ) = p * m := show ((t : ℕ) : ℤ) = p * m, from hm.symm ▸ by simp,
have hn' : (t : ℤ) = q * n := show ((t : ℕ) : ℤ) = q * n, from hn.symm ▸ by simp,
(domain.mul_right_inj hm0).1
  (by rw [mul_assoc xq, ← hm', hn', mul_left_comm, ← hpqt, mul_left_comm, mul_assoc])

[Kenny Lau]

thanks

[Chris Hughes]

What's the fastest way to prove this?

even_sum_four_squares {n a b c d : ℤ}
    (H : a * a + b * b + c * c + d * d = 2 * n) :
    ∃ w x y z, w * w + x * x + y * y + z * z = 2 * n ∧
    w * w + x * x ≡ 0 [ZMOD 2] ∧ y * y + z * z ≡ 0 [ZMOD 2]

[Kenny Lau]

aha

[Chris Hughes]

That was horrible

[Chris Hughes]

I just did a bazillion cases on whether things were odd or even.

[Kevin Buzzard]

A mathematician would say that clearly two of a,b,c have the same parity

[Kevin Buzzard]

so let w and x be those two

[Kevin Buzzard]

I would like to prove it in Lean with some kind of WLOG

[Kevin Buzzard]

"wlog a and b have the same parity"

[Kevin Buzzard]

because I can switch c with either a or b if necessary

[Kevin Buzzard]

So here the symmetry is three-fold.

[Kevin Buzzard]

The question is invariant under any permutation of the set {a,b,c}

[Kevin Buzzard]

and I know two of those elements must be congruent mod 2

[Kevin Buzzard]

so WLOG they're a and b

[Chris Hughes]

Very difficult to say nicely in lean

[Chris Hughes]

This was my proof

have h' : a * a + b * b + c * c + d * d ≡ 0 [ZMOD 2] :=
  modeq_zero_iff.2 (H.symm ▸ dvd_mul_right _ _),
or.cases_on (int.mod_two_eq_zero_or_one (a * a))
  (λ ha, or.cases_on (int.mod_two_eq_zero_or_one (b * b))
    (λ hb, ⟨a, b, c, d, H, even_add_even ha hb,
      modeq_add_cancel_left (show a * a + b * b ≡ 0 [ZMOD 2], from even_add_even ha hb)
      (int.modeq.trans (by simp) h')⟩)
    (λ hb, or.cases_on (int.mod_two_eq_zero_or_one (c * c))
      (λ hc, ⟨a, c, b, d, by simp [H.symm], even_add_even ha hc,
        modeq_add_cancel_left (show a * a + c * c ≡ 0 [ZMOD 2], from even_add_even ha hc)
          (int.modeq.trans (by simp) h')⟩)
      (λ hc, ⟨a, d, b, c, by simp [H.symm],
        modeq_add_cancel_left (show b * b + c * c ≡ 0 [ZMOD 2], from odd_add_odd hb hc)
          (int.modeq.trans (by simp) h'),
        odd_add_odd hb hc⟩)))
  (λ ha, or.cases_on (int.mod_two_eq_zero_or_one (b * b))
    (λ hb, or.cases_on (int.mod_two_eq_zero_or_one (c * c))
      (λ hc, ⟨b, c, a, d, by simp [H.symm], even_add_even hb hc,
        modeq_add_cancel_left (show b * b + c * c ≡ 0 [ZMOD 2], from even_add_even hb hc)
          (int.modeq.trans (by simp) h')⟩)
      (λ hc, ⟨a, c, b, d, by simp [H.symm], odd_add_odd ha hc,
        modeq_add_cancel_left (show a * a + c * c ≡ 0 [ZMOD 2], from odd_add_odd ha hc)
          (int.modeq.trans (by simp) h')⟩))
    (λ hb, ⟨a, b, c, d, by simp [H.symm], odd_add_odd ha hb,
      modeq_add_cancel_left (show a * a + b * b ≡ 0 [ZMOD 2], from odd_add_odd ha hb)
          (int.modeq.trans (by simp) h')⟩))

[Kevin Buzzard]

It looks a bit like a sonnet

[Kevin Buzzard]

My WLOG observation was that, just as we have a 2-variable WLOG which says that if the question is invariant under switching the two variables and we know that some predicate must be satisfied by some arrangement of the variables (e.g. x <= y), then we may assume that the predicate is satisfied by the default arrangement,

[Kevin Buzzard]

there is a 3-variable generalisation which says that if the question is invariant under all permutations of three variables and you can find some predicate which is true for some arrangement (e.g. "two of these three variables get sent to the same element under a map to a type with two elements") then WLOG it's true for the default arrangement

[Kevin Buzzard]

I am very interested in making Lean do things which mathematicians find trivial, painlessly, so I quite like thinking about things such as this.

[Kevin Buzzard]

I regard issues such as the one you brought up as a barrier to getting mathematicians to adopt automated proof checking as part of their routine

[Kevin Buzzard]

If you find yourself needing this kind of WLOG again I'd be interested to hear.

[Kevin Buzzard]

I'd happily spend some time over the summer trying to learn how to write tactics such as this. In this case it feel like it's a generalisation of Simon's WLOG

[Kevin Buzzard]

If you had it then the proof would be Wlog3 a %2 = b % 2, by tactic.ring (showing that permuting the variables doesn't change the assumption)

[Kevin Buzzard]

and then let w be a, x be b etc

[Johan Commelin]

So now we need @Simon Hudon to write an n-variable WLOG tactic... (-;

[Kevin Buzzard]

I think that the 2-variable WLOG is a powerful tool which genuinely does come up in practice

[Kevin Buzzard]

I am less convinced that the 3-variable WLOG shows up so much

[Kevin Buzzard]

however it sounds like a good exercise for the beginner

[Kevin Buzzard]

or possibly an incredibly difficult one

[Kevin Buzzard]

I think the n-variable one should definitely be left to Hudon ;-)

[Simon Hudon]

Interesting! In my previous prover, I had n-variable permutations in wlog but after talking to Assia, I started thinking that it was not the most useful generalization

[Simon Hudon]

n-pairs of swaps seemed more interesting

[Simon Hudon]

If you come up with another example where 3+ variable permutation is useful, I'll implement it

[Kevin Buzzard]

I agree that one should find out what users actually need in practice before leaping into multi-variable WLOG. I can't believe I just said that phrase.

[Kevin Buzzard]

The reason I suggested 3-variable WLOG is that at some point I suspect that it will do my Lean understanding some good if I were to actually write a tactic, and Chris and I will be spending the summer working on Lean together (with 13 other people)

[Simon Hudon]

Are you becoming a ... pragmatist? gasp

[Kevin Buzzard]

no, I just want to learn

[Simon Hudon]

But seriously, it is certainly a fun exercise. Let me know if you have questions