How to tell Lean to interpret all numbers as `Real`s?

Stream: new members

[Ilmārs Cīrulis]

Is it possible to tell Lean (with some command) that I want all numbers to be interpreted as ℝ?

[Ilmārs Cīrulis]

With exceptions marked with specific type, if necessary.

[Ilmārs Cīrulis]

Ok, I looked at all commands here and found nothing like that.

So, probably answer is no. At least if no metaprogramming (?) is used.

[Notification Bot]

Lessness has marked this topic as resolved.

[Kyle Miller]

You can add an OfNat default instance for reals, but this cannot be scoped to a particular module — it will affect all modules that import your module too.

[Ilmārs Cīrulis]

Kyle Miller said:

You can add an OfNat default instance for reals, but this cannot be scoped to a particular module — it will affect all modules that import your module too.

Maybe completely noob question, but how I do that? :sweat_smile:

[Notification Bot]

Lessness has marked this topic as unresolved.

[Ilmārs Cīrulis]

And, is there something similar for interpreting all numbers with decimal points (1.23 etc.) as Real?

[Ilmārs Cīrulis]

Thanks, discorders. This works for all natural numbers equal to at least 2.

import Mathlib

@[default_instance]
instance NatToReal (n : Nat) [n.AtLeastTwo]: OfNat Real n := ⟨↑n⟩

[Daniel Weber]

Lessness said:

And, is there something similar for interpreting all numbers with decimal points (1.23 etc.) as Real?

I think you can do the same for docs#OfScientific

[Ilmārs Cīrulis]

Yes, thank you! It seems that my try was successful. :partying_face:
(I kinda cheated a bit, but now everything works.)

import Mathlib

@[default_instance]
instance NatToReal (n: Nat) [n.AtLeastTwo]: OfNat Real n := ⟨↑n⟩

@[default_instance]
noncomputable instance ScientificToReal: OfScientific Real where
  ofScientific m s e := ↑(Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e))

def ex: - 37 / 2 = - 18.5 := by
  norm_num

[Eric Wieser]

Should mathlib override the default meaning of 0.5 to be Rat/NNRat instead of Float?

[Daniel Weber]

I think that's a good idea for mathlib itself, but this might hurt dependencies

[Ilmārs Cīrulis]

Just in case, if someone wants to know how to do instances for 0 and 1 too:

import Mathlib

@[default_instance]
instance NatToReal (n: Nat) [n.AtLeastTwo]: OfNat Real n := ⟨↑n⟩

@[default_instance]
instance ZeroToReal: Zero Real where
  zero := @OfNat.ofNat ℝ 0 Zero.toOfNat0

@[default_instance]
instance OneToReal: One Real where
  one := @OfNat.ofNat ℝ 1 One.toOfNat1

@[default_instance]
noncomputable local instance ScientificToReal: OfScientific Real where
  ofScientific m s e := ↑(Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e))

[Notification Bot]

Lessness has marked this topic as resolved.

[Notification Bot]

Lessness has marked this topic as unresolved.

[Ilmārs Cīrulis]

Yeah, no. I'm still dumb. :| The 0 and 1 doesn't work if without neighboring Real numbers that force them to be Real.

import Mathlib

@[default_instance]
instance NatToReal (n: Nat) [n.AtLeastTwo]: OfNat Real n := ⟨↑n⟩

@[default_instance]
instance ZeroToReal: Zero Real where
  zero := @OfNat.ofNat ℝ 0 Zero.toOfNat0

@[default_instance]
instance OneToReal: One Real where
  one := @OfNat.ofNat ℝ 1 One.toOfNat1

@[default_instance]
noncomputable instance ScientificToReal: OfScientific Real where
  ofScientific m s e := ↑(Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e))

def p1: Prop := (- 1.0) ^ (- 0.0) = 1.0

def p2: Prop := (- 1) ^ (- 0) = 1
-- causes error

[Kyle Miller]

Maybe you could give a HomogeneousPow Real instance?

[Ilmārs Cīrulis]

Yes, it seems that ^ is the reason. Now trying to make such instance, hopefully, it will be success.

[Ilmārs Cīrulis]

@[default_instance]
noncomputable instance RealPow: HPow Real Real Real where
  hPow := Real.rpow

Success!

[Ilmārs Cīrulis]

For now everything seems to be working correctly, yay :partying_face: