## Stream: new members

### Topic: Rational expressions and real semimodules

#### Christopher Hoskin (Jan 22 2021 at 21:25):

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 (Jan 22 2021 at 21:29):

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

#### Christopher Hoskin (Jan 22 2021 at 21:31):

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 (Jan 22 2021 at 21:31):

Add noncomputable theory to the top of your file

#### Christopher Hoskin (Jan 22 2021 at 21:33):

@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 (Jan 22 2021 at 21:33):

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

#### Alex J. Best (Jan 22 2021 at 21:34):

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 (Jan 22 2021 at 21:35):

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

#eval 2*(1/2:ℝ)


return 1?

#### Bryan Gin-ge Chen (Jan 22 2021 at 21:36):

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 (Jan 22 2021 at 21:37):

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 (Jan 22 2021 at 21:40):

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 (Jan 22 2021 at 21:42):

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 (Jan 22 2021 at 21:43):

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 (Jan 22 2021 at 21:51):

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

#### Alex J. Best (Jan 22 2021 at 21:55):

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 (Jan 22 2021 at 22:03):

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 (Jan 23 2021 at 05:58):

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

#### Eric Wieser (Jan 23 2021 at 15:07):

What is →ᵇ in the example above?

Last updated: May 18 2021 at 16:25 UTC