# Zulip Chat Archive

## 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