Zulip Chat Archive

Stream: new members

Topic: Using ∈ for Parameters


Marcus Rossel (Dec 27 2020 at 17:50):

How does behave when it is used for function parameters?
E.g. consider:

import data.finset

variables {α : Type*} (vertices : finset α)

def first (a  vertices) : Prop := true

theorem second :  a  vertices, a.first := sorry

Hovering over first's parameter a shows that it is of type α. I found this a bit unexpected, because I thought it would also come with a proof that it is a member of vertices.
Where I run into a problem though is with the term a.first. Hovering over a here again shows a : α, but I get the error:

invalid field notation, type is not of the form (C ...) where C is a constant
  a
has type
  ?m_1

I can kind of understand that Lean is complaining, since first expects a ∈ vertices and not just an a : α. But since second declares a ∈ vertices, I don't get why I can't pass it to first.

Kevin Buzzard (Dec 27 2020 at 17:53):

a ∈ g.vertices is just a proposition and so you can give it a label, e.g. def is_source_node {g : digraph ι α ε} (a ∈ g.vertices) : Prop := ... should probably be def is_source_node {g : digraph ι α ε} (ha : a ∈ g.vertices) : Prop :=

Kevin Buzzard (Dec 27 2020 at 17:54):

if you want help with Lean errors then it's much easier for everyone involved if you post a #mwe by the way. That way experienced users can view the same errors you're seeing in the same context.

Kevin Buzzard (Dec 27 2020 at 17:55):

e.g. I'm assuing you have some variable (a : alpha) somewhere or maybe variable {a : alpha} -- these things all make a difference and you're not showing them in your question right now.

Kevin Buzzard (Dec 27 2020 at 17:56):

a.is_source_node is short for (type of a).is_source_node a

Marcus Rossel (Dec 27 2020 at 18:03):

Kevin Buzzard said:

if you want help with Lean errors then it's much easier for everyone involved if you post a #mwe by the way. That way experienced users can view the same errors you're seeing in the same context.

I've updated the code above to be a MWE.

Kevin Buzzard (Dec 27 2020 at 18:06):

I'm surprised your code compiles! a is not defined. I would have written it like this: def first {a : α} (ha : a ∈ vertices) : Prop := true

Marcus Rossel (Dec 27 2020 at 18:07):

I was hoping that a ∈ vertices would provide a concise way of declaring the variable and the corresponding membership-proof in one term. But I guess {a : α} (ha : a ∈ vertices) will have to do.
Thanks!

Kevin Buzzard (Dec 27 2020 at 18:08):

second does not compile because a.first doesn't make sense.

import data.finset

variables {α : Type*} (vertices : finset α)

def first {a : α} (ha : a  vertices) : Prop := true

theorem second :  (a : α) (h : a  vertices), first _ h := sorry

Adam Topaz (Dec 27 2020 at 19:02):

I think there's some syntax sugar that lets you write a \in S even if a is not defined, and lean automatically replaces it by {a : ??} (ha : a \in S) or something like that...

Adam Topaz (Dec 27 2020 at 19:03):

Here's an example to illustrate this:

example {α : Type*} (S : set α) :  (a  S), true :=
begin
  intros a ha,
end

Adam Topaz (Dec 27 2020 at 19:05):

This probably has something to do with the out_param in the definition of has_mem, but I don't know how it actually works...

Adam Topaz (Dec 27 2020 at 19:20):

Here's a slightly minimized version of Kevin's code:

import data.finset

variables {α : Type*} (vertices : finset α)

def first (a  vertices) : Prop := true

theorem second :  {a} (h : a  vertices), first _ _ h := sorry

theorem second' :  (a  vertices), first _ _ H := sorry

Note that second' isn't good because H is an automatically generated name.

Mario Carneiro (Dec 27 2020 at 19:58):

Yes, whenever (a op b) appears as a binder (anywhere), where op is a binary operator, it is elaborated to (a) (H : a op b). This is why first works (you can see that it has this type if you #print it afterwards). The reason second doesn't work is because the type of a is not known until the typeclass argument in a ∈ vertices is resolved, and dot notation requires typing info before typeclass instance resolution. (Also, a.first doesn't work anyway because first is not in the namespace of the type of a.)

Eric Wieser (Dec 27 2020 at 19:58):

I don't think out_param is relevant here, this works for < too

Adam Topaz (Dec 27 2020 at 20:10):

Yeah, you're right. I have no idea what out_param actually does...

Adam Topaz (Dec 27 2020 at 20:17):

@Eric Wieser actually are you sure that out_param doesn't play a role? E.g.

class foo (α β : Type*) := (foo : α  β  Prop)
notation a `∈'` b       := foo.foo a b
instance bar {α : Type*} : foo α (set α) := λ a S, a  S

example {α : Type*} {S : set α} :  (a ∈' S), true := sorry -- fail

class foo' (α : out_param Type*) (β : Type*) := (foo' : α  β  Prop)
notation a `∈''` b       := foo'.foo' a b
instance bar' {α : Type*} : foo' α (set α) := λ a S, a  S

example {α : Type*} {S : set α} :  (a ∈'' S), true := sorry -- okay

Eric Wieser (Dec 27 2020 at 20:18):

Hmm... Is there an outparam on docs#has_lt after all?

Adam Topaz (Dec 27 2020 at 20:21):

No, but lean can deduce the type of a in a < 3 from the type of 3.

Mario Carneiro (Dec 27 2020 at 20:43):

The purpose of out_param is to allow the typeclass problem has_mem ? (finset A) to be solved, setting ? = A

Mario Carneiro (Dec 27 2020 at 20:43):

without the out_param, it would not perform the typeclass search until both sides are known

Mario Carneiro (Dec 27 2020 at 20:44):

The reason a < 3 infers the type of a is because of unification - lt has the type A -> A -> Prop

Mario Carneiro (Dec 27 2020 at 20:44):

if it had the type A -> B -> Prop then it wouldn't work, even if there was an instance has_lt nat nat

Mario Carneiro (Dec 27 2020 at 20:45):

but if lt had the type out_param A -> B -> Prop then lean would be able to infer a : nat

Mario Carneiro (Dec 27 2020 at 20:48):

the binder thing is orthogonal to that, although it works well with a left outparam as in has_mem. As long as you give the type some other way it still works:

class foo (α β : Type*) := (foo : α  β  Prop)
notation a `∈'` b       := foo.foo a b
instance bar {α : Type*} : foo α (set α) := λ a S, a  S

example {α : Type*} {S : set α} :  (a ∈' S), (a : α) = a := sorry -- ok

Last updated: Dec 20 2023 at 11:08 UTC