Stream: general

Topic: question about le on sets

Scott Morrison (Jul 28 2020 at 02:40):

import data.set.lattice

-- FAILS:
example {X : Type*} {ι : Type*} (U : ι → set X) {x} {i} (h : x ∈ U i) : x ∈ supr U :=
(le_supr U i) h -- function expected at le_supr U i term has type complete_lattice.le (U i) (supr U)

-- WORKS, but makes me sad:
example {X : Type*} {ι : Type*} (U : ι → set X) {x} {i} (h : x ∈ U i) : x ∈ supr U :=
begin
have := le_supr U i,
exact this h
end


Scott Morrison (Jul 28 2020 at 02:41):

What is one meant to do here to write a term-mode proof?

Yury G. Kudryashov (Jul 28 2020 at 03:04):

(show ..., from ...) h

Sebastien Gouezel (Jul 28 2020 at 06:40):

-- WORKS:
example {X : Type*} {ι : Type*} (U : ι → set X) {x} {i} (h : x ∈ U i) : x ∈ supr U :=
(le_supr U i : _) h


Scott Morrison (Jul 28 2020 at 07:36):

I'd forgotten that trick.

Mario Carneiro (Jul 28 2020 at 08:30):

alternatively

example {X : Type*} {ι : Type*} : ∀ (U : ι → set X) {i x}, x ∈ U i → x ∈ supr U := le_supr


Eric Wieser (Jul 29 2020 at 07:10):

Can you explain what's going on in that trick @Sebastien Gouezel?

Kenny Lau (Jul 29 2020 at 07:11):

Lean elaborates from outside to inside

Kenny Lau (Jul 29 2020 at 07:11):

that trick forces Lean to evaluate the inside first

Gabriel Ebner (Jul 29 2020 at 08:35):

@Eric Wieser During elaboration, Lean keeps track of the "expected type" of a subexpression. For example, if we elaborate (x + y : ℕ), then the expected type of x will be ℕ, no matter how little we know about x.
This works by propagating the expected type to the arguments when elaborating function applications. I believe this is what goes wrong in the first example. The (e : _) pattern is idiomatically used to prevent the expected type propagation.

Eric Wieser (Jul 29 2020 at 08:58):

Is there somewhere sensible to collect tricks like this, along with the trick of by letI := ....; exact for letI in term mode, etc?

Johan Commelin (Jul 29 2020 at 09:00):

I don't think we have anything more organised than Zulip atm...

Johan Commelin (Jul 29 2020 at 09:00):

But feel free to PR them to the "extra" docs

Johan Commelin (Jul 29 2020 at 09:00):

https://github.com/leanprover-community/mathlib/tree/master/docs/extras

Kevin Buzzard (Jul 29 2020 at 09:27):

Eric, if you can list ten tips which newcomers can only find out by running into them and asking, I could write a blog post :-)

Eric Wieser (Jul 29 2020 at 09:35):

@Johan Commelin, I assume you mean https://github.com/leanprover-community/leanprover-community.github.io/tree/newsite/templates/extras?

Probably, yes

I'm getting old

Johan Commelin (Jul 29 2020 at 09:36):

We should burn that other directory with fire (or just leave a README with a pointer to the new location).

Patrick Massot (Jul 29 2020 at 09:40):

I thought the old one already disappeared

Eric Wieser (Jul 29 2020 at 10:25):

A redirect from the old page would be more useful - I think google indexes it above the new one

Chris Wong (Jul 29 2020 at 12:28):

I don't think GitHub Pages supports automatic redirects, sadly. But maybe <link rel="canonical"> can help with the Google issue?