Zulip Chat Archive

Stream: new members

Topic: Rational expressions and real semimodules


view this post on Zulip 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 rm + sn

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

view this post on Zulip Johan Commelin (Jan 22 2021 at 21:29):

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

view this post on Zulip 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?

view this post on Zulip Alex J. Best (Jan 22 2021 at 21:31):

Add noncomputable theory to the top of your file

view this post on Zulip 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'

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Christopher Hoskin (Jan 22 2021 at 21:35):

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

#eval 2*(1/2:)

return 1?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 23 2021 at 15:07):

What is →ᵇ in the example above?


Last updated: May 18 2021 at 16:25 UTC