Zulip Chat Archive

Stream: new members

Topic: Frustration with simple `nat` lemmas


view this post on Zulip Eric Wieser (Nov 07 2020 at 12:27):

Am I missing a trick here? I can't find a lemma to close my goal, and I seem to have had to do way too much work to prove something so "obvious":

example (R : Type*) [comm_ring R] (n : ) : (-1 : R) ^ ((n + 1) * (n + 1 + 1)) = (-1) ^ (n * (n + 1)) :=
begin
  conv_rhs { rw neg_one_pow_eq_pow_mod_two },
  conv_lhs { rw neg_one_pow_eq_pow_mod_two },
  congr' 1,
  simp [mul_add, add_mul],
  conv_rhs { rw add_zero (n*n + n) },
  rw add_assoc (n*n + n) n,
  apply nat.add_mod_eq_add_mod_left (n*n + n),
  rw [add_assoc, add_assoc, add_assoc (n + n)],
  rw nat.add_mod_right (n + n) 2,
  rw nat.zero_mod,
  sorry, -- (n + n) % 2 = 0
end

view this post on Zulip Kevin Buzzard (Nov 07 2020 at 12:42):

example (n : ) : (n + n) % 2 = 0 :=
begin
  rw  mul_two,
  simp
end

view this post on Zulip Kevin Buzzard (Nov 07 2020 at 12:43):

Your example doesn't compile for me, even with adding random imports I can't make sense of (-1 : R). The way I'd prove it would to prove (1) (-1)^even=1, (2) forall t, t*(t+1) is even.

view this post on Zulip Eric Wieser (Nov 07 2020 at 12:46):

Oh, I guess I meant comm_ring R

view this post on Zulip Eric Wieser (Nov 07 2020 at 12:47):

forall t, t*(t+1) is even seems like something I've run into often enough that it would be nice if it were in mathlib

view this post on Zulip Eric Wieser (Nov 09 2020 at 11:13):

Ah, it's mostly there already:

example {a : } : even (a * (a + 1)) := by simp [decidable.em] with parity_simps

Is this still worth an explicit simp lemma?

@[simp]
lemma nat.even_mul_succ {a : } : even (a * (a + 1)) :=
nat.even_mul.mpr $ if h : even a then or.inl h else or.inr (nat.even_succ.mpr h)

Can we eliminate the need for writing decidable.em? Is even n ∨ ¬(even n) a good parity simp lemma?


Last updated: May 11 2021 at 22:14 UTC