# Zulip Chat Archive

## Stream: new members

### Topic: actually computing a thing

#### Torey Hilbert (Mar 14 2022 at 03:02):

Is there any way to actually compute a thing in Lean? I was trying to write a quick example of a measure to make sure my definitions made sense, and I first wasn't able to figure out how to specify that I was describing a measure over the borel space over the reals, and then I realized I couldn't even figure out how to tell it to compute the Lebesgue measure of an interval.

How would I get Lean to tell me what the Lebesgue measure of the interval [0, 7] is? Also, less serious, but how do I say "α is this specific measurable space" instead of hypothesizing "α is some measurable space"? Thank you!

#### Torey Hilbert (Mar 14 2022 at 03:03):

I guess in general my question is how do I deal with specific objects instead of variable

#### Heather Macbeth (Mar 14 2022 at 03:52):

```
import measure_theory.measure.lebesgue
open measure_theory.measure set
example : volume (Icc (0:ℝ) 7) = 7 := by norm_num
```

#### Kyle Miller (Mar 14 2022 at 04:03):

Let me plug a new mathlib command, which lets us avoid writing `example`

and the expected answer:

```
#norm_num volume (Icc (0:ℝ) 7)
-- ennreal.of_real 7
```

#### Heather Macbeth (Mar 14 2022 at 04:08):

Nice! So why doesn't it take the final step from `ennreal.of_real 7`

to 7, and could it be made to?

#### Mario Carneiro (Mar 14 2022 at 04:21):

We would need theorems about `ennreal.of_real (bit0 n) = bit0 (ennreal.of_real n)`

and so on

#### Mario Carneiro (Mar 14 2022 at 04:21):

norm_num doesn't know anything about `ennreal`

#### Mario Carneiro (Mar 14 2022 at 04:21):

in fact I don't think it's doing anything at all in this example except possibly a subtraction

#### Mario Carneiro (Mar 14 2022 at 04:21):

this is all `simp`

#### Kyle Miller (Mar 14 2022 at 04:22):

It seems like `norm_num`

is helping `simp`

add in non-negativity hypotheses?

```
example : volume (Icc (0:ℝ) 7) = 7 :=
begin
simp,
-- ennreal.of_real 7 = 7
have : 0 ≤ (3 : ℝ), by norm_num,
simp only [this, ennreal.of_real_bit1, zero_le_one, ennreal.of_real_one],
end
```

#### Kyle Miller (Mar 14 2022 at 04:23):

I'd basing that on the fact that `norm_num`

calls `simp`

with itself as the discharger.

#### Torey Hilbert (Mar 14 2022 at 05:14):

This has been very helpful - Thank you!

#### Kyle Miller (Mar 14 2022 at 08:24):

@Heather Macbeth I was finding this to be very puzzling, and I've realized that there were a number of ways I'd implemented `#norm_num`

incorrectly. What `norm_num`

is supposed to do is repeatedly do `norm_num1`

and `simp`

with `norm_num1`

as the discharger, but instead it just did `simp`

and then `norm_num1`

. #12667 is an attempt to fix it, and it evaluates `volume (Icc (0:ℝ) 7)`

all the way to `7`

.

Last updated: Dec 20 2023 at 11:08 UTC