Using ∈ for Parameters

Stream: new members

[Marcus Rossel]

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]

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]

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]

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]

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

[Marcus Rossel]

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]

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]

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]

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]

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]

Here's an example to illustrate this:

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

[Adam Topaz]

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]

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]

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]

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

[Adam Topaz]

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

[Adam Topaz]

@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]

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

[Adam Topaz]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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