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 :=
  -- 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],

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