up casting to fintype

Stream: new members

[Shimon Cohen]

I'm trying to use the degree function of combinatorics.simple_graph but I'm getting the error
"failed to synthesize type class instance for ⊢ fintype ↥(gr.neighbor_set 3)"

The code:

import tactic
import combinatorics.simple_graph.basic

def gr : simple_graph (fin 5) :=
  {adj := λ n m, n ≠ m, symm := λ a b, ne.symm, loopless := λ a ha, ha rfl}

#check gr.degree 3

It worked when I tried to do it explicitly like this:

#check @simple_graph.degree (fin 5) gr 3 (fintype.of_finite ↥(gr.neighbor_set 3))

What I should do to make it happen automaticly?

In addition there is a guide/lectures on how to work with graphs or fintype including tactics?

[Eric Wieser]

Adding instance : decidable_rel gr.adj := by rw [gr]; apply_instance works

[Eric Wieser]

Note that this uses docs#simple_graph.neighbor_set_fintype not fintype.of_finite

[Eric Wieser]

Which has the bonus of letting you write #eval gr.degree 3 and getting 4

[Shimon Cohen]

Can you explain what it do?

I tried to do it for another graph and it didn't worked

import tactic
import combinatorics.simple_graph.basic

def gr : simple_graph (fin 5) :=
  {adj := λ n m, n ≠ m}

instance a : decidable_rel gr.adj := by rw [gr]; apply_instance
#eval gr.degree 4

def gra : simple_graph (ℕ) :=
  {adj := λ n m, n ≠ m ∧ n + m < 100, symm := λ n m ⟨ne, lt⟩, ⟨ne.symm, (by linarith)⟩ }

instance b : decidable_rel gra.adj := by rw [gra]; apply_instance

#eval gra.degree 3

[Eric Wieser]

it doesn't work for that one because Lean doesn't know how to deduce that there are a finite number of nodes

[Eric Wieser]

The first one worked because the underlying carrier was finite

[Kyle Miller]

If you can tell Lean how the neighbor set is a fintype then it'll compute degrees for you:

import tactic
import combinatorics.simple_graph.basic

def gr : simple_graph (fin 5) :=
  {adj := λ n m, n ≠ m}

instance a : decidable_rel gr.adj := by rw [gr]; apply_instance
#eval gr.degree 4

def gra : simple_graph ℕ :=
  {adj := λ n m, n ≠ m ∧ n + m < 100, symm := λ n m ⟨ne, lt⟩, ⟨ne.symm, (by linarith)⟩ }

theorem gra_neighbor_set (n : ℕ) : gra.neighbor_set n = {m | n ≠ m ∧ n + m < 100} :=
by { ext m, refl }

instance (n : ℕ) : fintype (gra.neighbor_set n) :=
fintype.of_finset ((finset.range 100).filter (λ m, n ≠ m ∧ n + m < 100))
begin
  intro x,
  rw [gra_neighbor_set],
  simp,
  intros h hnx,
  linarith,
end

#eval gra.degree 3

[Kyle Miller]

You don't need a decidable_eq instance for this in general -- the docs#simple_graph.neighbor_set_fintype instance works by using the decidable_eq instance to filter the finset of all vertices, assuming your vertex type is finite. As Eric said, that can't work in this case since ℕ is not finite.

[Kyle Miller]

Here's another strategy:

instance : decidable_rel gra.adj := by rw [gra]; apply_instance

instance (n : ℕ) : fintype (gra.neighbor_set n) :=
set.fintype_subset {m | m < 100}
begin
  intro x,
  simp [gra],
  intros,
  linarith,
end