Help with explicit sets

Stream: new members

[Robert Spencer]

I've been battling a while now with sets, finsets, fintypes and such forth for a while now. I have many questions, but as way of a first one I have this.

Given the following definition of a quiver:

variables {α β : Type}

structure quiver :=
  (vertices : set α)
  (edges : set β)
  (s : edges → vertices)
  (t : edges → vertices)

I would like to define a small "toy" example so I can prove some theorems with it. Something like

variables (A B : α ) (a : β )  [decidable_eq α] [decidable_eq β]

def test_quiver : @quiver α β :=
  {
    vertices := {A, B},
    edges := {a},
    s := λ e, A,
    t := λ e, B,
  }

A lot about this screams sub-optimal to me: for example the s and t functions I'd prefer to define by some mapping from a to values (so that defining more complicated quivers is simple). I presume there is some way to do this with inductive functions, but that is secondary.

The first problem is that the above doesn't compile.

/home/rob...ry/src/quiver.lean:40:9: error: type mismatch at field 's'
  λ (e : ↥{a}), A
has type
  ↥{a} → α
but is expected to have type
  ↥{a} → ↥{A, B}

I understand the error, and I understand the problem (A is of type α and a priori has nothing to do with the set {A, B}). My question is how to fix this? Since I can't even find where the {...} notation is defined, I don't know what type {A,B} even is, so don't know what is missing.

[Reid Barton]

You've defined "a quiver whose vertices are a subset of α and whose edges are a subset of β". Unless you really meant to do this for some reason, it would probably make things a lot easier to define

structure quiver :=
  (vertices : Type)
  (edges : Type)
  (s : edges → vertices)
  (t : edges → vertices)

[Robert Spencer]

Ok, sure: I suppose that makes a little more sense (and coercion will convert any subsets of type α to a type when I need to define a quiver on a subset of α?)

[Robert Spencer]

The question then changes to "how do I make a Type with exactly three named elements in it"

[Reid Barton]

https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#enumerated-types

[Reid Barton]

To answer your original question, ↥{A, B} is the type subtype {A, B}. To give a value of this type you need to give a value of the underlying type α together with a proof that the value belongs to the subset {A, B}--I assume by simp will do it for you.

[Robert Spencer]

Ahhhh. Sigh. Obvious now. Thank you for your time!