x ^ 2 defeq

Stream: mathlib4

[Timo Carlin-Burns]

If x : ℝ, x ^ 2 = x * (x * 1) by rfl, not x * x. This could be changed by redefining npowRec

def npowRec [One M] [Mul M] : ℕ → M → M
  | 0, _ => 1
  | 1, a => a
  | n + 1, a => (npowRec n a) * a

Would this change be a good idea?

There's a comment above npowRec explaining the current rationale

-- use `x * npowRec n x` and not `npowRec n x * x` in the definition to make sure that
-- definitional unfolding of `npowRec` is blocked, to avoid deep recursion issues.
def npowRec [One M] [Mul M] : ℕ → M → M
  | 0, _ => 1
  | n + 1, a => a * npowRec n a

I don't really understand what this comment is saying. What "definitional unfolding" is the current solution blocking?

[Ruben Van de Velde]

What would the purpose of the change be?

[Eric Wieser]

Note that x ^ n is often not defeq to npowRec n x anyway

[Timo Carlin-Burns]

Eric Wieser said:

Note that x ^ n is often not defeq to npowRec n x anyway

It is for all real numbers x

example (x : ℝ) (n : ℕ) : x ^ n = npowRec n x := rfl

[Timo Carlin-Burns]

Ruben Van de Velde said:

What would the purpose of the change be?

Well the current defeq can always be worked around with simp [pow_two] (or pow_succ for greater n), but I was just surprised when I tried to prove

theorem normSq_mk (x y : ℝ) : Complex.normSq ⟨x, y⟩ = x ^ 2 + y ^ 2 :=
  rfl

and it failed.

[Damiano Testa]

I think that you should be surprised when you can prove something by rfl, not when you cannot! :upside_down:

[Damiano Testa]

If in informal maths you say "this is true by definition", then in formal maths you say "there is a lemma asserting this". Relying on defeq is too strong, but propeq is closer to what "by definition" means informally.

[Damiano Testa]

Maybe, renaming DefEq to CompSciEq would have confused fewer people...

[Eric Wieser]

Arguably we should really implement npowRec with binary recursion for a performance boost on things like x ^ 16!

[Reid Barton]

Timo Carlin-Burns said:

theorem normSq_mk (x y : ℝ) : Complex.normSq ⟨x, y⟩ = x ^ 2 + y ^ 2 :=
  rfl

and it failed.

Surely the real definition of Complex.normSq ⟨x, y⟩ is x ^ 2 + y ^ 2 + 0? :upside_down:

[Kevin Buzzard]

There's nothing wrong with

import Mathlib.Data.Complex.Basic

theorem normSq_mk (x y : ℝ) : Complex.normSq ⟨x, y⟩ = x ^ 2 + y ^ 2 := by
  simp [Complex.normSq]
  ring

Defeq is over-rated. It's not even a mathematical concept really. It's specific to dependent type theory I guess?

[Jireh Loreaux]

I would argue that defeq is a mathematical concept, but that the defeq required by dependent type theory isn't. For instance, we certainly have a notion in mathematics of "this is true by definition". I think the key feature of the mathematical version is: upon creating a definition, you're allowed to provide multiple definitions as long as you show they are propositionally equal / equivalent.

[Kevin Buzzard]

Right -- several things can be "true by definition" because we're allowed to switch definition! But that's not what we're talking about here I guess.

[Eric Rodriguez]

Doesn't Isabell have a notion of defeq like that?

[Kevin Buzzard]

Right -- maybe I should have said "Lean's defeq is not even a mathematical concept really" (in agreement with Jireh)