Zulip Chat Archive

Stream: graph theory

Topic: Creating an edge from vertices


Gabriel Moise (Apr 02 2021 at 08:52):

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 (Apr 02 2021 at 09:44):

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 (Apr 02 2021 at 09:57):

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 (Apr 02 2021 at 09:57):

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 (Apr 02 2021 at 10:00):

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 (Apr 02 2021 at 10:02):

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 (Apr 02 2021 at 10:02):

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

Alena Gusakov (Apr 02 2021 at 10:02):

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

Eric Wieser (Apr 02 2021 at 10:03):

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 (Apr 02 2021 at 10:04):

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 (Apr 02 2021 at 10:05):

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 (Apr 02 2021 at 10:08):

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 (Apr 02 2021 at 10:09):

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

Eric Wieser (Apr 02 2021 at 10:10):

↥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 (Apr 02 2021 at 10:11):

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 (Apr 02 2021 at 10:13):

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:


Last updated: Dec 20 2023 at 11:08 UTC