When does ↑ work?

Stream: new members

[Marcus Rossel]

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]

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

works.

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Eric Wieser]

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

[Marcus Rossel]

Eric Wieser said:

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

Why is that?

[Eric Wieser]

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]

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]

@Marcus Rossel what does "same" mean?

[Johan Commelin]

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

[Marcus Rossel]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

The simp normal form in this case is ↑i.

[Kevin Buzzard]

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

[Marcus Rossel]

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]

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]

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

[Bryan Gin-ge Chen]

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.