Zulip Chat Archive

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

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

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

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

#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: Dec 20 2023 at 11:08 UTC