Rational expressions and real semimodules

Stream: new members

[Christopher Hoskin]

Given a semimodule M over the reals, I'd like to form an expression like (1/2)m+(1/2)n. After a bit of puzzling, I've come up with the following approach. Is this the "right" way of going about this?

import data.real.basic

noncomputable theory

universes v

variables (M : Type v) [add_comm_group M] [semimodule ℝ M]

variables (r s : ℝ) (m n : M)

instance has_scalar_rat : has_scalar ℚ (M) :=
⟨λ q m,(q : ℝ)•m⟩

#check ((1:ℚ)/2)•m + (1/2:ℚ)•n

#check r•m + s•n

Should I be surprised that mathlib doesn't automagically know that a semimodule over ℝ is also a semimodule over ℚ ?

(For a bit more context, what I'm actually doing is trying to show

instance : has_inf (α →ᵇ ℝ) := ⟨λf g, (1/2:ℚ)•(f+g) - (1/2:ℚ)•|f-g|

)

Thanks,

Christopher

[Johan Commelin]

Is there a reason that you don't want to use 1/2 as real number?

[Christopher Hoskin]

I got a bit scared when I wrote:

#eval (1/2:ℝ)

And got the error

code generation failed, VM does not have code for 'classical.choice'

But perhaps that's nothing to worry about?

[Alex J. Best]

Add noncomputable theory to the top of your file

[Christopher Hoskin]

@Alex J. Best I already have that:

import data.real.basic

noncomputable theory

#eval (1/2:ℝ)

Gives the error code generation failed, VM does not have code for 'classical.choice'

[Alex J. Best]

What would you like that #eval to return? Real numbers are infinite cauchy sequences after all!

[Alex J. Best]

If you want to know that type of something / check it is written correctly, you can use #check when you write #eval you are asking lean to try and apply the definition of division in the real numbers to evaluate that expression.

[Christopher Hoskin]

@Alex J. Best Fair point, but shouldn't

#eval 2*(1/2:ℝ)

return 1?

[Bryan Gin-ge Chen]

mathlib's real numbers aren't computable, so there's no code Lean can #eval. There's an open issue about computable reals here #1038.

[Alex J. Best]

There are several different ideas of computation, lean can prove that 2 * (1/2) = 1 using tactics like tactic#norm_num but when you ask it to #eval you are asking it to really evaluate that expression using the mathematical definition of what 2, *, 1, / mean in the reals

[Christopher Hoskin]

Okay. (1/2:ℝ)•m + (1/2:ℝ)•n isn't producing any error messages, so I'm happy to go with that. I was just trying to check that (1/2:ℝ) wasn't zero, or something unintended like that.

[Alex J. Best]

This definition reduces down to something like docs#cau_seq.completion.Cauchy.has_inv, which splits into cases on whether the Cauchy sequence converges to 0 or not, this is not something lean can check in finite time! So the axiom of choice is used to make this definition.

[Alex J. Best]

Yeah it can be harder to sanity check things involving reals because of this, you can use norm_num to check some things though like:

example : (1/2:ℝ) ≠ 0 := by norm_num

[Christopher Hoskin]

Also I was thinking Lean might be able to automatically coerce a rational to a real in this context.

[Alex J. Best]

In a way thats what the norm_num version is doing, but you wouldn't want to define the mathemtical notion of division by saying "x /y in the reals is := if x and y are integers then take the rational x / y otherwise do the cauchy sequence thing", that would be a nightmare to prove properties of.
#eval will always try and evaluate the actual definition of things, which is not always the best way to calculate it.

[Christopher Hoskin]

I meant, I thought Lean might be able to automatically coerce a rational to a real in the context of semimodule scalar multiplication. But not to worry. thanks for your help.

[Kevin Buzzard]

Sure there's an automatic coercion from rationals to reals, in any context where the reals are imported

[Eric Wieser]

What is →ᵇ in the example above?