Zulip Chat Archive

Stream: general

Topic: question about `le` on sets


view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 28 2020 at 02:41):

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

view this post on Zulip Yury G. Kudryashov (Jul 28 2020 at 03:04):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 28 2020 at 07:36):

I'd forgotten that trick.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jul 29 2020 at 07:10):

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

view this post on Zulip Kenny Lau (Jul 29 2020 at 07:11):

Lean elaborates from outside to inside

view this post on Zulip Kenny Lau (Jul 29 2020 at 07:11):

that trick forces Lean to evaluate the inside first

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 29 2020 at 09:00):

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

view this post on Zulip Johan Commelin (Jul 29 2020 at 09:00):

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

view this post on Zulip Johan Commelin (Jul 29 2020 at 09:00):

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

view this post on Zulip 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 :-)

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 29 2020 at 09:36):

Probably, yes

view this post on Zulip Johan Commelin (Jul 29 2020 at 09:36):

I'm getting old

view this post on Zulip 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).

view this post on Zulip Patrick Massot (Jul 29 2020 at 09:40):

I thought the old one already disappeared

view this post on Zulip 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

view this post on Zulip 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?
https://en.wikipedia.org/wiki/Canonical_link_element

view this post on Zulip Bryan Gin-ge Chen (Jul 29 2020 at 13:46):

Johan Commelin said:

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

I've added some README files in #3623.


Last updated: May 09 2021 at 20:11 UTC