## Stream: maths

### Topic: Proof depending on n mod 2

#### Johan Commelin (Jul 16 2018 at 11:16):

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 (Jul 16 2018 at 11:33):

what is it that you want to prove?

#### Kenny Lau (Jul 16 2018 at 11:33):

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

#### Chris Hughes (Jul 16 2018 at 11:35):

nat.mod_two_eq_zero_or_one I believe

#### Kenny Lau (Jul 16 2018 at 11:35):

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

#### Johan Commelin (Jul 16 2018 at 11:45):

Ok, I'll try that.

#### Johan Commelin (Jul 16 2018 at 11:45):

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 (Jul 16 2018 at 11:46):

could you include the types of v and a?

#### Johan Commelin (Jul 16 2018 at 11:46):

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

#### Johan Commelin (Jul 16 2018 at 11:46):

v and a live in some comm ring.

#### Kenny Lau (Jul 16 2018 at 11:49):

ring can't prove this:

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


#### Johan Commelin (Jul 16 2018 at 11:51):

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

#### Kenny Lau (Jul 16 2018 at 11:51):

I don't know what ring knows

#### Johan Commelin (Jul 16 2018 at 11:53):

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

#### Mario Carneiro (Jul 16 2018 at 11:57):

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)

fair enough

#### Johan Commelin (Jul 16 2018 at 12:01):

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

#### Mario Carneiro (Jul 16 2018 at 12:02):

ring deals with commutative rings and commutative semirings

#### Mario Carneiro (Jul 16 2018 at 12:02):

Negatives are supported

#### Johan Commelin (Jul 16 2018 at 12:36):

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 (Jul 16 2018 at 12:38):

that could probably go in group_power.lean

#### Patrick Massot (Jul 16 2018 at 12:38):

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

#### Mario Carneiro (Jul 16 2018 at 12:38):

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

#### Johan Commelin (Jul 16 2018 at 12:39):

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 (Jul 16 2018 at 12:43):

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 (Jul 16 2018 at 12:43):

that's 7 minutes :P

#### Kenny Lau (Jul 16 2018 at 12:46):

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 (Jul 16 2018 at 12:47):

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


You win (-;

#### Mario Carneiro (Jul 16 2018 at 12:48):

Now you are just showing off :P

#### Mario Carneiro (Jul 16 2018 at 12:48):

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

#### Kenny Lau (Jul 16 2018 at 12:49):

not much difference, I think

#### Mario Carneiro (Jul 16 2018 at 12:52):

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

I see

#### Kenny Lau (Jul 16 2018 at 12:53):

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;