How to use `eq_zero_of_zpow_eq_zero`?

Stream: new members

[Thomas Preu]

Over ℝ I'd like to inferre (-1) = 0 from (-1) ^ n = 0 in a proof by contradiction where n : ℕ. It seemed that eq_zero_of_zpow_eq_zero was the right theorem, however I get an error.
So I thought I should do a simple explicit example and tried

#eval eq_zero_of_zpow_eq_zero ((2 : ℝ) ^ (3 : ℤ) = (0 : ℝ) : Prop)

to get:

application type mismatch
  eq_zero_of_zpow_eq_zero (2 ^ 3 = 0)
argument
  2 ^ 3 = 0
has type
  Prop : Type
but is expected to have type
  ?m.46818 ^ ?m.46819 = 0 : Prop

What am I doing wrong?

[Kenny Lau]

@Thomas Preu firstly, use #check instead of #eval

[Kenny Lau]

and then secondly, please inspect the result of #check eq_zero_of_zpow_eq_zero. your error suggests that it's simply due to misaligned arguments (i.e. maybe u mistook the second argument for the first argument, etc.)

[Ruben Van de Velde]

zpow means internet exponent, not natural

[Aaron Liu]

*integer

[Ruben Van de Velde]

Damnit autocorrect

[Ruben Van de Velde]

Does docs#eq_zero_of_pow_eq_zero exist?

[Kenny Lau]

I see, I misread the error

[Ruben Van de Velde]

Nope

[Aaron Liu]

That's a 404

[Aaron Liu]

@loogle _ ^ (_ : Nat) = 0

[loogle]

Failure! Bot is unavailable

[Kenny Lau]

lol

[Aaron Liu]

I think it's just called docs#pow_eq_zero

[Alfredo Moreira-Rosa]

here an example :

import Mathlib

example : ¬ (2 : ℝ) ^ (3 : ℤ) = (0 : ℝ) := by
  by_contra h
  apply eq_zero_of_zpow_eq_zero at h
  simp at h

[Ruben Van de Velde]

I'm going to rename eq_zero_of_zpow_eq_zero to match

[Ruben Van de Velde]

#30443

[Thomas Preu]

Aaron Liu said:

I think it's just called docs#pow_eq_zero

First I tried pow_eq_zero, but VSCode put it in strike-through, told me it's deprecated and better use eq_zero_of_zpow_eq_zero.

[Ruben Van de Velde]

Huh, that's really odd, pow_eq_zero doesn't seem to be deprecated

[Thomas Preu]

ecyrbe said:

here an example :

import Mathlib

example : ¬ (2 : ℝ) ^ (3 : ℤ) = (0 : ℝ) := by
  by_contra h
  apply eq_zero_of_zpow_eq_zero at h
  simp at h

Usually an implication can be applied like a function. Why is the apply tactic necessary here?
And thank you for showing a use case, that's very helpful.

[Kenny Lau]

Thomas Preu said:

Usually an implication can be applied like a function. Why is the apply tactic necessary here?

because you said apply, what do you mean?

[Kenny Lau]

it isn't strictly necessary

[Kenny Lau]

have := eq_zero_of_zpow_eq_zero h would also work

[Kenny Lau]

@Thomas Preu in another thread @Kevin Buzzard pointed out what the real error was, i didn't even notice it, you wrote in a proposition instead of the proof; in Lean the statement and the proof are two distinct things, e.g. h : P means that h is a proof of P, here h is the proof and P is the statement

[Kenny Lau]

Thomas Preu said:

eq_zero_of_zpow_eq_zero ((2 : ℝ) ^ (3 : ℤ) = (0 : ℝ) : Prop)

the function eq_zero_of_zpow_eq_zero eats in a proof of a proposition, so something like:

eq_zero_of_zpow_eq_zero (h : (2 : ℝ) ^ (3 : ℤ) = (0 : ℝ))

[Kenny Lau]

notice how the statement appears to the right of the colon in my correct version and to the left of the colon in your version

[Kevin Buzzard]

(here is my message)

[Kenny Lau]

to make it absolutely clearer what this error means, 37 is a natural number, in Lean we write 37 : Nat, which means "37 is a term of the type Nat". if there's a function Nat.fib : Nat -> Natthat takes in a natural number (i.e a term of type Nat), then it would be nonsense to write:
:cross_mark: Nat.fib (Nat : Type)
The correct thing to write would be:
:check: Nat.fib (37 : Nat).

[Ruben Van de Velde]

Anyway, that's why your explicit example failed, but the zpow lemma was still the wrong one if your n is a natural number

[Thomas Preu]

Ruben Van de Velde said:

Anyway, that's why your explicit example failed, but the zpow lemma was still the wrong one if your n is a natural number

I got to make it work using casts. It looks like this now:

example (h11 : (- (1 : ℝ)) ^ (n : ℕ) = 0): False := by
  have h11a : ((- (1 : ℝ)) ^ (Int.ofNat n) = 0) := by
    apply h11
  have h11b : (- (1 : ℝ) = 0) := eq_zero_of_zpow_eq_zero h11a
  simp at h11b

Is this the way you are supposed to go about these type issues?

[Kenny Lau]

well you don't have to use the zpow lemma

[Ruben Van de Velde]

Right, this is the straightforward solution:

import Mathlib

example (h11 : (- (1 : ℝ)) ^ (n : ℕ) = 0): False := by
  have := pow_eq_zero h11
  simp at this

[Ruben Van de Velde]

But also, if that's not an option and you want to use a result about integers, you generally would use the coercion rather than Int.ofNat, and your apply h11 is hiding that it's relying on the fact that nonnegative integer powers are defined as natural powers, which is somewhat brittle. (This is "definitional equality" versus "propositional equality".) Compare:

import Mathlib

example (h11 : (- (1 : ℝ)) ^ (n : ℕ) = 0): False := by
  have h11a : ((- (1 : ℝ)) ^ (Int.ofNat n) = 0) := by
    rw [Int.ofNat_eq_coe, zpow_natCast, h11]
    -- ^ No longer relying on the specific way integer powers are defined
  have h11b : (- (1 : ℝ) = 0) := eq_zero_of_zpow_eq_zero h11a
  simp at h11b

example (h11 : (- (1 : ℝ)) ^ (n : ℕ) = 0): False := by
  have h11a : ((- (1 : ℝ)) ^ (n : ℤ) = 0) := by
    -- ^ More typical way of writing the embedding of ℕ into ℤ
    rw [zpow_natCast, h11]
  have h11b : (- (1 : ℝ) = 0) := eq_zero_of_zpow_eq_zero h11a
  simp at h11b

example (h11 : (- (1 : ℝ)) ^ (n : ℕ) = 0): False := by
  rw [← zpow_natCast] at h11
  -- ^ Just shorter
  have h11b : (- (1 : ℝ) = 0) := eq_zero_of_zpow_eq_zero h11
  simp at h11b

[Thomas Preu]

Thank you, these type casts still confuse me.
So the upshot is that it works, because we coerce naturals to integers and because of the way powers over the integers are defined, right?
If I had some (arbitrary) result over the rationals or reals, say, and would want to specialize to the natural numbers, it wouldn't work this way - or does it?

[Kenny Lau]

@Thomas Preu so, different types are distinct, period. however, sometimes there are standard functions to transport from one type to another. for the sake of confusion, let's call them coe. So for example you have n : Nat, and then you can have coe n : Int.

Note, there is always a function, and it is always called coe, it is never n : Int.

Now lean also does some magic to kinda hide it from you when you see it so that it doesn't clutter your view (lean hides a lot of things because otherwise each goal would be 10 pages long), so when you type n : Int, it does typecheck, and Lean automatically inserts the coe; and to help you out, Lean automatically prints a little uparrow, so you see it as ↑n : Int.

[Kenny Lau]

one code is worth a 1000 words, so:

variable (n : Nat)
#check (n : Int) -- ↑n : Int

[Kenny Lau]

note again that there is always a function that you sometimes don't need to type, but that doesn't mean it's not there; that means that in other contexts it will fail, such as:

variable (h : ∀ n : Int, n = n)
#check (h : ∀ n : Nat, n = n) -- type mismatch

[Kenny Lau]

this makes no sense to Lean because Int and Nat are never the same

[Kenny Lau]

Kenny Lau said:

in other contexts

i.e. when it's in a "binder", i.e. when it's the variable in a forall or exists or etc, those can never be coerced (that's what "coe" stands for)

[Kenny Lau]

Thomas Preu said:

So the upshot is that it works, because we coerce naturals to integers and because of the way powers over the integers are defined, right?

it's because of the way integers are defined, an integer is defined to be either Int.ofNat n for some n : Nat, or Int.negSucc n for some n : Nat, and "these are the only ways you can build an integer"

[Kenny Lau]

because of the promise in the last part, to define a function with domain Int, you can split it into those two cases automatically

[Kenny Lau]

def foo : Int -> Nat
| Int.ofNat n => n * n
| Int.negSucc n => n + n

#reduce foo 3
#reduce foo (-3)

[Kenny Lau]

this is a specific property of Int that happens to be true because of how we've set things up; in other words, it's an "implementation detail", and not an inherently true mathematical property

[Kenny Lau]

that's why we've said that it's bad to rely on this implementation detail

[Kenny Lau]

the standard way to interact with an object is with theorems, and not with the underlying definition

[Kenny Lau]

in the example above, the theorems you should use are:

def foo : Int -> Nat
| Int.ofNat n => n * n
| Int.negSucc n => n + n

@[simp] theorem foo_natCast (n : Nat) : foo (n : Int) = n * n := rfl

@[simp] theorem foo_neg_natCast (n : Nat) : foo (-n : Int) = (n-1) + (n-1) :=
  match n with
  | 0 => rfl
  | (n+1) => by rw [Int.natCast_add, Int.natCast_one,
      ← Int.negSucc_eq]; rfl

[Kenny Lau]

this is a more "mathematical" way to interact with integers

[Kenny Lau]

the fact that negSucc exists is mathematically messy because it doesn't start at 0, so all our standard lemmas should use the standard forms instead, which are n and -n (that's how we mathematically think about natural numbers)

[Thomas Preu]

Do I understand correctly that the theorems (usually) work via the coe functions?
I guess the rationals extend the naturals in a way, that includes the naturals just as an isomorphic (wrt. certain relevant structures) copy, but that does not literally contain the naturals in the same way as you explained above in the case of integers containing the natural numbers. Do I understand correctly that this is why theorems using coe would be needed to apply a result for rationals to natural numbers?

[Aaron Liu]

Thomas Preu said:

but that does not literally contain the naturals in the same way as you explained above in the case of integers containing the natural numbers.

Now I'm worried you might have a misunderstanding about how the integers contain the naturals

[Kenny Lau]

that's partially correct, it's more accurate to say that we have certain "standard forms" of terms of given types; for Int the standard forms are n and -n, but for other types the standard forms can be different; for Rat the standard form would be n / d with n : Int and d : Nat; for Real there's no standard form (for set theory reasons) but you can have things like Real.sqrt 2 etc.

[Kenny Lau]

for polynomials the standard form would be sums of C r * X ^ n, no coe anywhere

[Kenny Lau]

@Thomas Preu in other words, certain types have standard constructors, i.e. IKEA instruction manuals to build terms of that type

[Kenny Lau]

for the simplest type Nat, you are given two tools, Nat.zero gives you a natural number that you call zero, and if you have a natural number already, you can keep apply Nat.succ to get a higher and higher natural number

[Kenny Lau]

without these tools you have no way to interact with every natural number

[Darij Grinberg]

Can't you just square it?

[Darij Grinberg]

squaring works in any nontrivial ring, while eq_zero_of_zpow_eq_zero generalizes to reduced rings at best

[Darij Grinberg]

or units