Zulip Chat Archive

Stream: new members

Topic: When does ↑ work?


view this post on Zulip Marcus Rossel (Dec 28 2020 at 14:47):

I'm confused about when the (\u) operator works - especially related to subtypes. When I try it in small examples, it always works:

example (x : { n :  // n > 10 }) :  := x -- doesn't even need the ↑
example (α : Type*) (p : α  Prop) (x : { a // p a }) (y : α) : Prop := x = y -- needs the ↑

But when I try to use it in my own projects I always have to resort to using x.val.
For example (sorry for the size of this example):

import data.finset

class digraph.edge (ε ι : Type*) [decidable_eq ι] :=
  (src : ε  ι)
  (dst : ε  ι)

variables (ι δ : Type*) (ε : Π is : finset ι, ({ i // i  is }  δ)  Type*)
variables [decidable_eq ι] [ i d, digraph.edge (ε i d) ι]

structure digraph :=
  (ids : finset ι)
  (data : { i // i  ids }  δ)
  (edges : finset (ε ids data))

def in_degree_of (g : digraph ι δ ε) (i : { x // x  g.ids}) :  :=
  (g.edges.filter (λ e, edge.dst e = i.val)).card -- `↑i` doesn't work

In the last line, replacing i.val with ↑i is not possible. It produces the error:

don't know how to synthesize placeholder
context:
ι : Type u_1,
δ : Type u_2,
ε : Π (is : finset ι), ({i // i  is}  δ)  Type u_3,
_inst_1 : decidable_eq ι,
_inst_2 : Π (i : finset ι) (d : {i_1 // i_1  i}  δ), digraph.edge (ε i d) ι,
g : digraph ι δ ε,
i : {x // x  g.ids},
e : ε g.ids g.data
 Type ?

Which placeholder can't Lean synthesize?

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 14:52):

    (g.edges.filter (λ e, edge.dst e = (i : ι))).card

works.

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 14:53):

I think what's going on is that after the lambda, Lean doesn't know the type of e when it comes to figuring out where it should be coercing i.

view this post on Zulip Marcus Rossel (Dec 28 2020 at 14:54):

Kevin Buzzard said:

I think what's going on is that after the lambda, Lean doesn't know the type of e when it comes to figuring out where it should be coercing i.

Isn't the type of e constrained by the type of g.edges.filter though?

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 14:55):

I have no idea in what order everything happens -- I have never looked at the elaborator code (I can't read C++). This works too:

    (g.edges.filter (λ e, (edge.dst e : ι) = i)).card

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 14:56):

I just go by the general rule of thumb that if Lean can't figure out what you mean and it looks like it's an issue with working out types, then add some type ascriptions.

view this post on Zulip Marcus Rossel (Dec 28 2020 at 14:58):

My fuss is really about writing ↑i instead of i.val only for looks anyway :D So I guess i.val is still a perfectly fine solution.

view this post on Zulip Eric Wieser (Dec 28 2020 at 15:08):

Sometimes it's still better to use the arrow + a type ascription instead of .val

view this post on Zulip Eric Wieser (Dec 28 2020 at 15:08):

Eg all the lemmas about fin are written in terms of the arrow

view this post on Zulip Marcus Rossel (Dec 28 2020 at 15:09):

Eric Wieser said:

Sometimes it's still better to use the arrow + a type ascription instead of .val

Why is that?

view this post on Zulip Eric Wieser (Dec 28 2020 at 15:09):

So if you define things using .val, you can't apply any lemmas to the definition until you rewrite all the .val's into arrows

view this post on Zulip Marcus Rossel (Dec 28 2020 at 15:11):

Eric Wieser said:

So if you define things using .val, you can't apply any lemmas to the definition until you rewrite all the .val's into arrows

I don't understand. Say we have x : { n : ℕ // n > 10 }, then doesn't ↑x and x.val produce the same thing, since:

instance coe_subtype {a : Sort u} {p : a  Prop} : has_coe {x // p x} a := subtype.val

view this post on Zulip Johan Commelin (Dec 28 2020 at 15:11):

@Marcus Rossel what does "same" mean?

view this post on Zulip Johan Commelin (Dec 28 2020 at 15:11):

They will be equal in the sense of provably equal, and even definitionally equal. But they are clearly not syntactically equal.

view this post on Zulip Marcus Rossel (Dec 28 2020 at 15:12):

Johan Commelin said:

They will be equal in the sense of provably equal, and even definitionally equal. But they are clearly not syntactically equal.

By "same" I mean definitionally equal.

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 15:12):

Different tactics use different levels of equality. For example rw uses syntactic equality.

view this post on Zulip Johan Commelin (Dec 28 2020 at 15:12):

Some automation relies on syntactic equality. So if you want simp or rw to help you...

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 15:14):

There is a concept of "simp normal form" in Lean, which is the preferred way to express something. For example you can't just have some lemmas about a nonempty set XX with XX\not=\emptyset being used as the definition, some as X.nonempty and some with x,xX\exists x, x \in X -- even though they might all be definitionally equal, rw and simp would prefer that just one of these is used (otherwise you have to state lemmas in 3 ways). Did you know that there are essentially no occurrences of > in mathlib? Because it was decided that a < b was the simp normal form for b > a.

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 15:15):

The simp normal form in this case is ↑i.

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 15:16):

In some sense this concept should be called the "mathlib normal form".

view this post on Zulip Marcus Rossel (Dec 28 2020 at 15:18):

Kevin Buzzard said:

There is a concept of "simp normal form" in Lean, which is the preferred way to express something. For example you can't just have some lemmas about a nonempty set XX with XX\not=\emptyset being used as the definition, some as X.nonempty and some with x,xX\exists x, x \in X -- even though they might all be definitionally equal, rw and simp would prefer that just one of these is used (otherwise you have to state lemmas in 3 ways). Did you know that there are essentially no occurrences of > in mathlib? Because it was decided that a < b was the simp normal form for b > a.

Awesome, thanks! This explains a lot :)

view this post on Zulip Bryan Gin-ge Chen (Dec 28 2020 at 16:37):

I've been thinking lately that it might be nice to have some documentation explicitly stating what the simp normal form is for various expressions. Not sure where the best place to put such notes would be; maybe in doc strings of definitions?

view this post on Zulip Rob Lewis (Dec 28 2020 at 16:47):

There and/or in module docs under implementation notes. This is very important information to have!

view this post on Zulip Bryan Gin-ge Chen (Dec 28 2020 at 17:10):

I created #5518 for this since I didn't want to forget. There are still some details I'm not sure about, so suggestions are welcome.


Last updated: May 08 2021 at 19:11 UTC