Creating an edge from vertices

Stream: graph theory

[Gabriel Moise]

Hello!
I was trying some proofs and lemmas about the incidence matrix of a graph, and I would find it useful if I could have a definition of an edge from the 2 given vertices, knowing the fact that they are adjacent in the graph. I tried something like this

import linear_algebra.matrix
import combinatorics.simple_graph.basic

open_locale big_operators matrix
open finset matrix simple_graph

universes u v
variables {V : Type u} [fintype V]

namespace simple_graph

variables (G : simple_graph V) [decidable_rel G.adj] [decidable_eq V]

def edge_from_vertices (i j : V) (H_adj : G.adj i j) : G.edge_set := ⟦(i,j)⟧

end simple_graph

However, there is a problem because Lean can't coerce the ⟦(i,j)⟧ into a member of the G.edge_set. Has anyone encountered this and has a solution? I would like to have something like, the edge_from_vertices i j H_adj would be
e such that e.val = ⟦(i,j)⟧, but I don't know how to define that.

[Eric Rodriguez]

I'm confused what you mean; isn't G.adj i j evidence that i j is an edge? Can you post a #mwe explaining what you need it for?

[Alena Gusakov]

I'm pretty sure there's a lemma stating that there exists an edge iff adjacent, you might be able to use that?

[Gabriel Moise]

I wasn't talking about the evidence that (i,j) represents an edge, I was talking about having the edge as an object and using it for calculations, for instance:

lemma filter_edge_card_one {i j : V} (H_adj : G.adj i j) :
  filter (λ (x : (G.edge_set)), ↑x = ⟦(i, j)⟧) univ = {G.edge_from_vertices i j H_adj} :=
begin
  sorry
end

[Alena Gusakov]

I think you can use the existence lemma to create the edge but I'm not currently able to test it (it's like 6 am where I am sorry lol)

[Alena Gusakov]

I think I get what you're saying though - G.edge_set isn't a type, so you can't say def etc : G.edge_set := ...

[Eric Wieser]

Sure you can, because docs#set.has_coe_to_sort exists? (although you probably shouldn't!)

[Alena Gusakov]

You can do def etc : sym2 V := ... because that's the type of edges

[Eric Wieser]

filter (λ (x : (G.edge_set)), ↑x = ⟦(i, j)⟧) univ should be the same as filter (λ (x : sym2 V), x = ⟦(i, j)⟧) G.edge_set, and the latter will be easier to work with

[Gabriel Moise]

Well, I am sure that there is a possibility, but I am not very accustomed to working with coercions, although I stumble upon them a lot, so I wanted to see an example so that I can understand more.

[Eric Wieser]

At a guess you're looking for

def edge_from_vertices (i j : V) (H_adj : G.adj i j) : G.edge_set := ⟨⟦(i,j)⟧, H_adj⟩

[Eric Wieser]

Or another way to write it, without exploiting that docs#sym2.from_rel_prop is true by rfl:

def edge_from_vertices (i j : V) (H_adj : G.adj i j) : G.edge_set :=
⟨_, sym2.from_rel_prop.mpr H_adj⟩

[Gabriel Moise]

Can you explain a little how does the construction work (⟨⟦(i,j)⟧, H_adj⟩) ?

[Eric Wieser]

↥G.edge_set is short for {x // x ∈ G.edge_set} aka subtype (∈ G.edge_set). subtype x is just a pair of x and p x (docs#subtype)

[Eric Wieser]

Conveniently, it turns out the statements ⟦(i,j)⟧ ∈ G.edge_set and G.adj i j are defeq, so as long as lean already knows what type it's looking for, you can supply a proof of the latter (H_adj) where the former is expected.

[Gabriel Moise]

Oh, I think I see what you mean. Thank you very much! I am currently working on proving more lemmas and I might have more questions, I will use this topic for that, if that's ok :smile: