How to express (-1)^n?

Stream: new members

[Alex Gu]

I am trying to express (-1)^n in Lean, but having trouble because it seems not to like -1. What's the right way to express this theorem?

theorem thm (n : ℕ) (h : n ≡ 0 [MOD 2]) :
  (-1)^n ≡ 1 [MOD 2] := by sorry

Error:

failed to synthesize
  Neg ℕ

[Yaël Dillies]

[MOD _] notation is for natural number. If you want to deal with integers, you should be using [ZMOD _] notation :smile:

[Adam Topaz]

This isn't quite related to the question, but you should be aware that we have a docs#SignType

[Adam Topaz]

Depending on what your application is, it may be convenient. But if you're just doing some modular arithmetic, then sticking to integers is probably the way to go.

[Alex Gu]

Thanks both :) Getting a bit stuck with the proof now, any good tips here?

theorem thm (n : ℕ) (h : n ≡ 0 [ZMOD 2]) :
  (-1)^n ≡ 1 [ZMOD 2] := by
  cases Nat.even_or_odd n with
  | inl he =>
    obtain ⟨k, hk⟩ := he
    rw [hk]
    simp [pow_mul]
  | inr ho =>

[Damiano Testa]

aesop can finish from there.

[Alex Gu]

Got it! Is there a way to do it by finding the contradiction instead of proving the theorem? (I saw the aesop proof actually ignores the contradcition and goes ahead to prove it)

[Damiano Testa]

What contradiction?

[Damiano Testa]

Oh, you mean using the redundant hypothesis?

[Alex Gu]

That is n = 0 mod 2, then n cannot be odd

[Damiano Testa]

You could do this

    exfalso
    rw [Int.modEq_iff_dvd, zero_sub, dvd_neg] at h
    norm_cast at h
    apply Nat.not_even_iff_odd.mpr ho
    refine (even_iff_exists_two_nsmul n).mpr h

[Eric Wieser]

You might also just want to work in ZMod 2 rather than using [ZMOD 2]

[Alex Gu]

What's the difference?

[Floris van Doorn]

With ZMod 2 you work in the type that has only two elements, 0 and 1. Working with [ZMOD 2] means working with integers, but considering an equivalence relation on it with two equivalence classes.

[Alex Gu]

I see, what would be the equivalent way to write it in ZMod 2 then?

[Eric Wieser]

theorem thm (n : ZMod 2) (h : n = 0) :
    (-1 : ZMod 2)^n.val = 1 := by
  simp [h]

[Eric Wieser]

Though the .val there makes it slightly debatable whether this is the same theorem.

[Edward van de Meent]

i don't think you even need h here? shouldn't this just be true for all n:Nat?

[Edward van de Meent]

because mod 2, $-1=1=1^n$?

[Edward van de Meent]

or am i missing something?

[Alex Mobius]

I think the lower [MOD 2] is unintended, and the TS is trying to express if even n then 1 else -1

[Edward van de Meent]

ah... in that case, i think that the idiomatic way to express this would be this:

import Mathlib.Analysis.Normed.Field.Lemmas

def foo {n:Nat} (h:Even n) : (-1:Int) ^ n = 1 := Even.neg_one_pow h

[Alex Mobius]

Mathlib: there's a lemma for everything (good luck with looking for it) :)

[Edward van de Meent]

exact? was used in this case