# Zulip Chat Archive

## 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):

it isn't about negatives

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

it's about powers

#### 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`

)

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

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

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

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

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

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; rw [← nat.mod_add_div n 2, pow_add, pow_mul, h]; simp [pow_two] end

Last updated: May 10 2021 at 07:15 UTC