## Stream: new members

### Topic: When does ↑ work?

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

#### Kevin Buzzard (Dec 28 2020 at 14:52):

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


works.

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

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

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


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

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

#### Eric Wieser (Dec 28 2020 at 15:08):

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

#### Eric Wieser (Dec 28 2020 at 15:08):

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

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

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

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


#### Johan Commelin (Dec 28 2020 at 15:11):

@Marcus Rossel what does "same" mean?

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

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

#### Kevin Buzzard (Dec 28 2020 at 15:12):

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

#### Johan Commelin (Dec 28 2020 at 15:12):

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

#### 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 $X$ with $X\not=\emptyset$ being used as the definition, some as X.nonempty and some with $\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.

#### Kevin Buzzard (Dec 28 2020 at 15:15):

The simp normal form in this case is ↑i.

#### Kevin Buzzard (Dec 28 2020 at 15:16):

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

#### 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 $X$ with $X\not=\emptyset$ being used as the definition, some as X.nonempty and some with $\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 :)

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

#### Rob Lewis (Dec 28 2020 at 16:47):

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

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