Proof depending on n mod 2

Stream: maths

[Johan Commelin]

I need to prove a fact about (-a)^n, with n : nat. I would like to split into two cases, depending on whether n is odd or even. What is the best way to do this in mathlib?

[Kenny Lau]

what is it that you want to prove?

[Kenny Lau]

you might be able to rewrite n into (n/2)*2 + (n%2) if you use the division algorithm

[Chris Hughes]

nat.mod_two_eq_zero_or_one I believe

[Kenny Lau]

my point is, sometimes you don't need to split into two cases

[Johan Commelin]

Ok, I'll try that.

[Johan Commelin]

So, here is another substep that I currently have:

rw show v * (-a)^n = ((-1)^n * v) * a^n,
    begin
      rw [neg_eq_neg_one_mul, mul_pow], ring,
    end,

[Kenny Lau]

could you include the types of v and a?

[Johan Commelin]

Should ring be able to do those rewrites itself? I think it would make sense to me to teach ring about negatives...

[Johan Commelin]

v and a live in some comm ring.

[Kenny Lau]

it isn't about negatives

[Kenny Lau]

it's about powers

[Kenny Lau]

ring can't prove this:

example : x^n * y^n = (x * y)^n := by ring

[Johan Commelin]

Should ring be able to prove it, by rw mul_pow whenever possible?

[Kenny Lau]

I don't know what ring knows

[Johan Commelin]

My "Should" was a moral should. As in, does it make sense to give ring these extra powers?

[Mario Carneiro]

No. It is not a rewrite system, it is a decision procedure for polynomial equalities. x^n is not a polynomial (of two variables x, n)

[Kenny Lau]

fair enough

[Johan Commelin]

Mario, so would it make sense to rename ring into semiring, and have a ring tactic that is semiring + some other superpowers?

[Mario Carneiro]

ring deals with commutative rings and commutative semirings

[Mario Carneiro]

Negatives are supported

[Johan Commelin]

Ok, so what is the fastest way to prove H : ∀ {n : ℕ}, ((-1 : R)^n = 1) ∨ ((-1 : R)^n = -1), where R is a comm_ring.

[Mario Carneiro]

that could probably go in group_power.lean

[Patrick Massot]

That's the fastest way: have Mario write it in mathlib

[Mario Carneiro]

but you can prove it either by induction or by quotient remainder theorem like kenny suggested

[Johan Commelin]

I'm halfway a proof by induction, but everytime I need a stupid little fact from mathlib it costs me 15 minutes to find it...

[Kenny Lau]

import tactic.ring

universe u
variables (R : Type u) [comm_ring R] (n : nat)

example : ((-1 : R)^n = 1) ∨ ((-1 : R)^n = -1) :=
begin
  induction n with n ih, {simp},
  rw [pow_succ, neg_one_mul, neg_inj', neg_eq_iff_neg_eq, eq_comm, or_comm],
  assumption
end

[Kenny Lau]

that's 7 minutes :P

[Kenny Lau]

import tactic.ring

universe u
variables (R : Type u) [comm_ring R] (n : nat)

example : ((-1 : R)^n = 1) ∨ ((-1 : R)^n = -1) :=
begin
  induction n with n ih, {simp},
  cases ih with ih ih,
  { right, simp [pow_succ, ih] },
  { left, simp [pow_succ, ih] }
end

[Kenny Lau]

import tactic.ring

universe u
variables (R : Type u) [comm_ring R] (n : nat)

example : ((-1 : R)^n = 1) ∨ ((-1 : R)^n = -1) :=
begin
  induction n with n ih, {simp},
  cases ih with ih ih; [right, left];
  simp [pow_succ, ih]
end

[Johan Commelin]

You win (-;

[Mario Carneiro]

Now you are just showing off :P

[Mario Carneiro]

What's it look like using the equation compiler for the induction?

[Kenny Lau]

not much difference, I think

[Mario Carneiro]

I think it's a bit neater

theorem neg_one_pow_eq_or {R} [comm_ring R] : ∀ n : ℕ, ((-1 : R)^n = 1) ∨ ((-1 : R)^n = -1)
| 0     := by simp
| (n+1) := by cases neg_one_pow_eq_or n; simp [pow_succ, h]

also left and right are unnecessary

[Kenny Lau]

I see

[Kenny Lau]

import tactic.ring

universe u
variables (R : Type u) [comm_ring R] (n : nat)

example : ((-1 : R)^n = 1) ∨ ((-1 : R)^n = -1) :=
begin
  cases nat.mod_two_eq_zero_or_one n;
  rw [← nat.mod_add_div n 2, pow_add, pow_mul, h];
  simp [pow_two]
end