## Stream: general

### Topic: strange elaboration

#### 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


#### Kenny Lau (Jun 10 2020 at 07:31):

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

#### 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


#### 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


#### 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

#### Mario Carneiro (Jun 10 2020 at 08:03):

The 0 is the source of the nat defaulting

#### Kenny Lau (Jun 10 2020 at 08:10):

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

#### Kenny Lau (Jun 10 2020 at 08:10):

maybe not "incorrect" but rather "inconsistent"

#### 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

#### Kenny Lau (Jun 10 2020 at 08:11):

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

#### Kenny Lau (Jun 10 2020 at 08:11):

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

#### 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

#### Kenny Lau (Jun 10 2020 at 08:11):

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

#### Yury G. Kudryashov (Jun 10 2020 at 08:12):

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

#### Mario Carneiro (Jun 10 2020 at 08:13):

You can also .. ninja'd

oh

#### Mario Carneiro (Jun 10 2020 at 08:13):

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

#### Mario Carneiro (Jun 10 2020 at 08:14):

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

#lean4 ?

#### Mario Carneiro (Jun 10 2020 at 08:18):

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

#### 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