actually computing a thing

Stream: new members

[Torey Hilbert]

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]

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

[Heather Macbeth]

import measure_theory.measure.lebesgue

open measure_theory.measure set

example : volume (Icc (0:ℝ) 7) = 7 := by norm_num

[Kyle Miller]

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]

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]

We would need theorems about ennreal.of_real (bit0 n) = bit0 (ennreal.of_real n) and so on

[Mario Carneiro]

norm_num doesn't know anything about ennreal

[Mario Carneiro]

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

[Mario Carneiro]

this is all simp

[Kyle Miller]

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]

I'd basing that on the fact that norm_num calls simp with itself as the discharger.

[Torey Hilbert]

This has been very helpful - Thank you!

[Kyle Miller]

@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.