How to make a function that accepts only positive Float?

Stream: general

[Mykhailo Dm]

For example, i would like to write a log function that accepts only positive Float as a base.

[Riccardo Brasca]

You can specify the domain of a function to be any type you want. But note that if f it is defined on positive real numbers and x is a real number that you know to be positive, then f x does not make sense (there are ways to make it work in a certain sense, but it is annoying). The usual solution is to define f x for any x, using a junk value in the non positive case.

[Jireh Loreaux]

import Lean

def Float.log' (x : {x : Float // 0 < x}) : Float := x.1.log

/- Lean complains here that:

unused variable `hx`
note: this linter can be disabled with `set_option linter.unusedVariables false`-/
def Float.log'' (x : Float) (hx : 0 < x) : Float := x.log

[Riccardo Brasca]

It's probably a good idea to read this https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/

[Jireh Loreaux]

But yes, I agree with Riccardo, you probably just want Float.log (espcially because you can't prove anything about Float since it is opaque.

[Mykhailo Dm]

Jireh Loreaux said:

import Lean

def Float.log' (x : {x : Float // 0 < x}) : Float := x.1.log

/- Lean complains here that:

unused variable `hx`
note: this linter can be disabled with `set_option linter.unusedVariables false`-/
def Float.log'' (x : Float) (hx : 0 < x) : Float := x.log

Trying to #eval any of these (#eval Float.log' (10.)) with both positive and negative values gives me an errors. Am I doing something wrong here or i have to call them somehow a bit in a special way?

[Kyle Miller]

These expect a proof that 10 is positive. That is, you need to put something in place of sorry here:

#eval Float.log'' 10.0 (by sorry)

However, like Jireh said, Float is opaque, so this isn't something that can be proved, as far as I know.

[Kyle Miller]

If you are OK with trusting the Lean compiler as part of the trusted code base, you can use native_decide to calculate that it is in bounds:

#eval Float.log'' 10.0 (by native_decide)

[Kyle Miller]

native_decide uses the runtime characteristics of Float rather than any theoretical specification

[Mykhailo Dm]

Kyle Miller said:

If you are OK with trusting the Lean compiler as part of the trusted code base, you can use native_decide to calculate that it is in bounds:

#eval Float.log'' 10.0 (by native_decide)

Yay, it works, thanks!! But this isn't "compile time", right?

[Kyle Miller]

by native_decide is a compile-time check. It only works for compile-time constants. (More specifically, it is "elaboration time" in Lean terminology)

It's possible to do run-time checking too, using a different method (if h : ... then ... else ... syntax)