Stavan Jain

Stream: new members

[Stavan Jain]

Hi everyone, my name is Stavan and I'm just about to start my fourth year as an undergraduate at Duke University. I'm majoring in Math and Computer Science and have recently been interested in the paradigm of formalizing mathematics in Lean.

I was trying to define the sequence $a_n = 3^{-n}$ in Lean as below:
def aₙ : ℕ → ℝ := fun (n : ℕ) => 3 ^ (- n : ℝ)

I get the following error message: "failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.instPow', and it does not have executable code".

As I understand, the exponentiation function rpow : $\R \to \R \to \R$ is not computable in Lean. Is there a way I can work around this apart from marking it as noncomputable? More generally, it would be helpful if someone could redirect me to a resource that would help me understand the limitations of noncomputable definitions.

[Damiano Testa]

For most of the mathematical development, is the computable definitions that are a limitation!

[Stavan Jain]

Damiano Testa said:

For most of the mathematical development, is the computable definitions that are a limitation!

In what sense?

[Luigi Massacci]

You can work with rationals, that should be computable (if you actively want computability)

[Luigi Massacci]

And if you need it real-valued at some point you can cast it at the last second

[Luigi Massacci]

Stavan Jain said:

In what sense?

For starters, the "mathematician's" real numbers (i.e. if for you the real numbers are an uncountable set) are inherently uncomputable, so it's hard to to say much of anything about them from a perspective of computation. More in general, computability is a property that takes a lot of effort to preserve, and is quite limiting in what it allows you to do

[Eric Wieser]

Luigi Massacci said:

And if you need it real-valued at some point you can cast it at the last second

Or you can define your function over an arbitrary Semifield, so that it works for both Real and Rational

[Stavan Jain]

Thank you @Luigi Massacci

[Julian Berman]

I think it's usually Kyle who points this out, but just to be sure, note that whether something is noncomputable affects what Lean will evaluate for you -- but it doesn't mean you can't separately calculate the answer via tactics, or prove some answer is the right one, e.g.:

import Mathlib

noncomputable def aₙ : ℕ → ℝ := fun (n : ℕ) ↦ 3 ^ (- n : ℝ)

-- #eval aₙ 0  -- FAILS

example : aₙ 0 = 1 := by
  dsimp [aₙ]
  simp only [CharP.cast_eq_zero, neg_zero, Real.rpow_zero]

[Stavan Jain]

Ah, that's helpful! I assume this is because we have theory about multiplying/exponentiating by 0 for real numbers. Would trying to prove something like example : aₙ 1 = (1/3) := by sorry be futile?

Julian Berman said:

I think it's usually Kyle who points this out, but just to be sure, note that whether something is noncomputable affects what Lean will evaluate for you -- but it doesn't mean you can't separately calculate the answer via tactics, or prove some answer is the right one, e.g.:

import Mathlib

noncomputable def aₙ : ℕ → ℝ := fun (n : ℕ) ↦ 3 ^ (- n : ℝ)

-- #eval aₙ 0  -- FAILS

example : aₙ 0 = 1 := by
  dsimp [aₙ]
  simp only [CharP.cast_eq_zero, neg_zero, Real.rpow_zero]

[Julian Berman]

You should try it!

[Damiano Testa]

You may find it easier to work with

noncomputable abbrev aₙ : ℕ → ℝ := fun (n : ℕ) ↦ (1 / 3) ^ n

Note that the exponent is now a natural number and def became abbrev, which basically saves you from having to unfold aₙ everywhere.

[Damiano Testa]

The def vs abbrev is a technicality, but the choice of what function you use is very important in formalization and a good choice can save you lots of time down the line, for no mathematical difference.

[Stavan Jain]

Julian Berman said:

You should try it!

Thanks! I got it to work:

example : aₙ 1 = (1/3) :=  by
  dsimp [aₙ]
  rw [Nat.cast_one, one_div, Real.rpow_neg_one]

or even

example : aₙ 3 = (1/27) :=  by
  dsimp [aₙ]
  have rpow_three (x : ℝ) : x ^ (3 : ℝ) = x ^ 3 := by
    rw [← Real.rpow_natCast]
    simp only [Nat.cast_ofNat]
  rw [one_div, Real.rpow_neg, rpow_three, inv_inj]
  · linarith
  linarith

However, the second proof relies on the computability of the power function on natural numbers, correct? The first linarith closes the goal 3 ^ 3 = 27

[Stavan Jain]

Damiano Testa said:

The def vs abbrev is a technicality, but the choice of what function you use is very important in formalization and a good choice can save you lots of time down the line, for no mathematical difference.

Ah okay. Is $(1/3)^ n$ a better choice than $3 ^ {-n}$ because it avoids negative exponents?

[Damiano Testa]

Yes, negative and real.

[Damiano Testa]

You can try proving the other lemmas with the new definition and using simp or norm_num.

[Damiano Testa]

E.g.

import Mathlib

noncomputable abbrev aₙ : ℕ → ℝ := fun (n : ℕ) ↦ (1 / 3) ^ n

example : aₙ 3 = (1/27) :=  by
  norm_num

[Stavan Jain]

Ah, that does indeed make the proofs a lot easier. Thank you @Damiano Testa