Zulip Chat Archive

Stream: general

Topic: strange elaboration


view this post on Zulip Kenny Lau (Jun 10 2020 at 07:31):

import analysis.normed_space.basic

open_locale big_operators

variables {α : Type} [normed_group α] {t : finset α} {f : α  α}

-- ∀ (ε : ℝ), ε > 0 → ∥t.sum f∥ < ε
example : ε > 0,  t.sum f  < ε := by skip

-- ∀ (ε : ℕ), ε > 0 → ∥∑ (i : α) in t, f i∥ < ↑ε
example : ε > 0,  ( i in t, f i)  < ε := by skip

view this post on Zulip Kenny Lau (Jun 10 2020 at 07:31):

the epsilon in the second example is (wrongly) interpreted as a natural number

view this post on Zulip Kenny Lau (Jun 10 2020 at 07:32):

the notation is irrelevant:

-- ∀ (ε : ℕ), ε > 0 → ∥∑ (i : α) in t, f i∥ < ↑ε
example : ε > 0,  t.sum (λ i, f i)  < ε := by skip

view this post on Zulip Kenny Lau (Jun 10 2020 at 07:34):

strangely enough the type is correct again if > 0 is removed:

import analysis.normed_space.basic

variables {α : Type} [normed_group α] {t : finset α} {f : α  α}

-- ∀ (ε : ℝ), ε > 0 → ∥t.sum f∥ < ε
example : ε > 0,  t.sum f  < ε := by skip

-- ∀ (ε : ℝ), ∥t.sum (λ (i : α), f i)∥ < ε
example : ε,  t.sum (λ i, f i)  < ε := by skip

-- INCORRECT
-- ∀ (ε : ℕ), ε > 0 → ∥t.sum (λ (i : α), f i)∥ < ↑ε
example : ε > 0,  t.sum (λ i, f i)  < ε := by skip

view this post on Zulip Mario Carneiro (Jun 10 2020 at 08:03):

In what sense is it incorrect? It looks like lean was able to type it either way

view this post on Zulip Mario Carneiro (Jun 10 2020 at 08:03):

The 0 is the source of the nat defaulting

view this post on Zulip Kenny Lau (Jun 10 2020 at 08:10):

@Mario Carneiro then why does it get elaborated as \R in the first example?

view this post on Zulip Kenny Lau (Jun 10 2020 at 08:10):

maybe not "incorrect" but rather "inconsistent"

view this post on Zulip Mario Carneiro (Jun 10 2020 at 08:11):

nat defaulting has always been a little weird, since it is somewhat outside the usual elaboration process. It happens "late" but it still has to trigger before type inference is complete

view this post on Zulip Kenny Lau (Jun 10 2020 at 08:11):

so should I change it to the longer form \forall \e : \R, \e > 0 \to?

view this post on Zulip Kenny Lau (Jun 10 2020 at 08:11):

https://github.com/leanprover-community/mathlib/runs/756776916

view this post on Zulip Mario Carneiro (Jun 10 2020 at 08:11):

I've never really been convinced it is a good idea, but the original point was so that people could just write #eval 1 + 1 and get something sensible

view this post on Zulip Kenny Lau (Jun 10 2020 at 08:11):

https://github.com/leanprover-community/mathlib/pull/3014

view this post on Zulip Yury G. Kudryashov (Jun 10 2020 at 08:12):

AFAIR you can use ε > (0 : real).

view this post on Zulip Mario Carneiro (Jun 10 2020 at 08:13):

You can also .. ninja'd

view this post on Zulip Kenny Lau (Jun 10 2020 at 08:13):

oh

view this post on Zulip Mario Carneiro (Jun 10 2020 at 08:13):

we should make ∀(ε : ℝ) > 0, work

view this post on Zulip Mario Carneiro (Jun 10 2020 at 08:14):

it's a bit silly that you can't put a type ascription there

view this post on Zulip Kenny Lau (Jun 10 2020 at 08:15):

#lean4 ?

view this post on Zulip Mario Carneiro (Jun 10 2020 at 08:18):

3.x should be able to handle it without too much work

view this post on Zulip Mario Carneiro (Jun 10 2020 at 08:18):

although I'm not in a position to hack on lean ATM


Last updated: May 16 2021 at 21:11 UTC