Zulip Chat Archive

Stream: maths

Topic: Proof depending on n mod 2


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jul 16 2018 at 11:33):

what is it that you want to prove?

view this post on Zulip 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

view this post on Zulip Chris Hughes (Jul 16 2018 at 11:35):

nat.mod_two_eq_zero_or_one I believe

view this post on Zulip Kenny Lau (Jul 16 2018 at 11:35):

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

view this post on Zulip Johan Commelin (Jul 16 2018 at 11:45):

Ok, I'll try that.

view this post on Zulip 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,

view this post on Zulip Kenny Lau (Jul 16 2018 at 11:46):

could you include the types of v and a?

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Jul 16 2018 at 11:46):

v and a live in some comm ring.

view this post on Zulip Kenny Lau (Jul 16 2018 at 11:49):

it isn't about negatives

view this post on Zulip Kenny Lau (Jul 16 2018 at 11:49):

it's about powers

view this post on Zulip Kenny Lau (Jul 16 2018 at 11:49):

ring can't prove this:

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

view this post on Zulip Johan Commelin (Jul 16 2018 at 11:51):

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

view this post on Zulip Kenny Lau (Jul 16 2018 at 11:51):

I don't know what ring knows

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jul 16 2018 at 11:57):

fair enough

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 16 2018 at 12:02):

ring deals with commutative rings and commutative semirings

view this post on Zulip Mario Carneiro (Jul 16 2018 at 12:02):

Negatives are supported

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 16 2018 at 12:38):

that could probably go in group_power.lean

view this post on Zulip Patrick Massot (Jul 16 2018 at 12:38):

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

view this post on Zulip Mario Carneiro (Jul 16 2018 at 12:38):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 16 2018 at 12:43):

that's 7 minutes :P

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 16 2018 at 12:47):

You win (-;

view this post on Zulip Mario Carneiro (Jul 16 2018 at 12:48):

Now you are just showing off :P

view this post on Zulip Mario Carneiro (Jul 16 2018 at 12:48):

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

view this post on Zulip Kenny Lau (Jul 16 2018 at 12:49):

not much difference, I think

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 16 2018 at 12:52):

I see

view this post on Zulip 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