Real.cos -1

Stream: mathlib4

[Kevin Buzzard]

I was lean4ifying the docs for my UG course and in them I talk about Real.sqrt(-1) when explaining junk values. As far as I'm concerned it's rather unfortunate that this syntax is not even valid any more in Lean 4, so following the principle I tell the students ("brackets not necessary") I tried Real.sqrt -1 and got a very surprising answer. Just to emphasize that this is no longer about junk values, can anyone guess the value of Real.cos -1?

[Ruben Van de Velde]

Is it

fun x => cos x - 1?

[Utensil Song]

Seems that #check Real.cos (-1 : ℝ) is needed to get expected.

[Jireh Loreaux]

Is the type ascription necessary?

[Utensil Song]

Now I'm puzzled by this:

import Mathlib

example : (Real.sqrt 2)^2 = (2 : ℝ) := by
  norm_num
  done -- works

example : Real.sqrt 2 = 2 ^ (1 / 2) → false := by
  norm_num
  done -- works

example : Real.sqrt 2 = 2 ^ (1 / 2 : ℝ) := by
  norm_num
  done -- fails

[Ruben Van de Velde]

Does norm_num try to support real powers at all?

[Ruben Van de Velde]

The code was commented out during the port (Mathlib/Analysis/SpecialFunctions/Pow/Real.lean), and hasn't been restored yet

[Ruben Van de Velde]

Though it seems like even in mathlib3 it only supported integer exponents

[Kevin Buzzard]

The 1/2 in the middle example is a Nat.

[Utensil Song]

Yes, the example is there to demonstrate that norm_num seems to be able to penetrate Real.sqrt to an extent to know that's false.

[Utensil Song]

Ah, the limitation is on the power side (for reals).

[Kevin Buzzard]

example : Real.sqrt 2 = 1 → False := by
  simp

[Kevin Buzzard]

(and norm_num tries simp)

[Mario Carneiro]

Kevin Buzzard said:

I tried Real.sqrt -1 and got a very surprising answer. Just to emphasize that this is no longer about junk values, can anyone guess the value of Real.cos -1?

I do find this a bit funny, like a "last laugh" against the people who argued that type theory was going to solve the problem of "junk theorems" in ZFC. They said 1 ∈ 2 was ludicrous but now through a system of coercions and overloading we are seeing the same kind of junk values showing up in a strongly typed system. (Of course it's not actually a ludicrous answer, it's just an answer which is domain specific and being observed out of its domain - which is much the same as what you could say about 1 ∈ 2.)

[Eric Rodriguez]

I feel like this is just a bad priority for the negation operator, no?

[Eric Rodriguez]

I think -x and - x should mean different things, but that's probably horrifying behaviour

[Kevin Buzzard]

In Lean 3, \-1 had precendence 1034 > 1024 (at least at some point) to make sure that f x\-1 parsed as f (x\-1).

[Mario Carneiro]

This isn't \-1 though, it's just a literal x-1

[Mario Carneiro]

I assume you would not expect x - 1 to be interpreted as x (-1)

[Mario Carneiro]

maybe we could make the spaces factor in here but currently they make no difference

[Mario Carneiro]

certainly x -1 is misleading spacing

[Mario Carneiro]

I think that the no space form x-1 shows up enough that we can't ban it, so really it's just a matter of x -1 or x- 1 which look like linter warnings to me

[Kevin Buzzard]

Yes I know \-1 isn't -1, I was trying to imply that we could make unary neg have binding power greater than function application -- but maybe that wouldn't solve the problem?

[Mario Carneiro]

the problem is that high-precedence unary negation is genuinely ambiguous with binary subtraction

[Mario Carneiro]

because we do not want x - 1 to mean x (- 1)