Zulip Chat Archive

Stream: new members

Topic: graphs and deleting edges


Christopher Schmidt (Jan 12 2023 at 10:56):

Hello everyone,
I am working with my directed simple graphs:

universes u

@[ext]
structure directed_simple_graph (V : Type u) := (adj : V  V  Prop)

namespace directed_simple_graph
variables {V : Type u}
variables (G : directed_simple_graph V)

and I am trying to implement the deleting edges definiton from simple graphs, which have symmetric edges :

def delete_edges (s : set (sym2 V)) : simple_graph V :=
{ adj := G.adj \ sym2.to_rel s,
  symm := λ a b, by simp [adj_comm, sym2.eq_swap] }

Of course, I only need adjacency not symmetry. However, I did not see a way to translate s to a relation. Therefore I tried to explicitly define what adj is supposed to do when s is deleted :

def delete_edges (s : set (V × V)) : directed_simple_graph V :=
{ adj := λ v1 v2, if (v1,v2)  s then G.adj v1 v2 else false}

That does work but I am not 100% sure whether it is doing what it is supposed to do. Is there a more convenient way, such that one can prove

@[simp] lemma delete_edges_adj (s : set (V × V)) (v w : V) :
  (G.delete_edges s).adj v w  G.adj v w  ¬ (v, w)  s := sorry

by rfl ? As in:

@[simp] lemma delete_edges_adj (s : set (sym2 V)) (v w : V) :
  (G.delete_edges s).adj v w  G.adj v w  ¬ (v, w)  s := iff.rfl

Any help is appreciated.

Alistair Tucker (Jan 12 2023 at 12:43):

Why not just write s as a relation? Then

def delete_edges (s : V  V  Prop) : directed_simple_graph V :=
{ adj := G.adj \ s }

@[simp] lemma delete_edges_adj (s : V  V  Prop) (v w : V) :
  (G.delete_edges s).adj v w  G.adj v w  ¬ s v w := iff.rfl

Christopher Schmidt (Jan 12 2023 at 14:03):

@Alistair Tucker I would like s to be the set of the edges one wants to remove from the directed graph..

As s, for directed graphs, has no symmetry, one obviously can not use

sym2.to rel s

but is there a way to obtain a relation from s?

Kyle Miller (Jan 12 2023 at 14:23):

You can write it as λ v w, (v, w) ∈ s. There might be some definition(s) in mathlib for going between a set of pairs and a relation, but nothing comes to mind.

Kyle Miller (Jan 12 2023 at 14:26):

sym2.to_rel exists mainly because it's an inverse to sym2.from_rel and there are a few lemmas about it. It's also not too bad to write λ v w, ⟦(v, w)⟧ ∈ s for it instead.

Alistair Tucker (Jan 12 2023 at 14:50):

Internally set (V × V) is just V × V → Prop anyway. But perhaps you want to draw some subtle distinction here that I don't understand...

Kyle Miller (Jan 12 2023 at 14:53):

Yes, the set "API" expects that you always respect the proper syntax of a set. Sure a set is a predicate, but you ought to always use the membership syntax for things like simp to work properly.

Kyle Miller (Jan 12 2023 at 14:54):

Also, my functions have type V → V → Prop (not V × V → Prop).

If docs#function.uncurry allowed Sort* rather than Type* I might have written function.uncurry (∈ s)

Kyle Miller (Jan 12 2023 at 14:55):

This (∈ s) notation is how you're expected to turn a set back into a predicate. It's the inverse of docs#set_of

Alistair Tucker (Jan 12 2023 at 15:14):

Sorry I should have made it clear that I was addressing @Christopher Schmidt

Kyle Miller (Jan 12 2023 at 15:16):

I guess you could take what I wrote as addressing why you might want a set (V × V) argument rather than a raw relation.

Kyle Miller (Jan 12 2023 at 15:17):

@Christopher Schmidt Another design, instead of defining delete_edges, is to make a function to create a directed_simple_graph from an edge set, then define the difference of two graphs

Kyle Miller (Jan 12 2023 at 15:18):

For simple graphs we don't do that because there's the annoyance that you have to delete the diagonal from the set, since simple graphs are loopless.

Christopher Schmidt (Jan 12 2023 at 16:11):

Thanks for your help and ideas. What I have accomplished through that:

variables {s : set (V \times V)}

def set_to_rel: directed_simple_graph V  set (V × V)  (V  V  Prop) :=
λ G s v1 v2, (v1,v2)  s

/-- `from_edge_set` constructs a `directed_simple_graph` from a set of edges. -/
def from_edge_set : directed_simple_graph V := { adj := (G.set_to_rel s) }

/-- Given a set of vertex pairs, remove all of the corresponding edges from the
graph's edge set, if present. -/
def delete_edges (s : set (V × V)) : directed_simple_graph V :=
{ adj := G.adj \ (G.set_to_rel s) }

/-- The difference of two graphs `x \ y` has the edges of `x` with the edges of `y` removed. -/
instance : has_sdiff (directed_simple_graph V) := λ x y, { adj := x.adj \ y.adj,}⟩

@[simp] lemma delete_edges_adj (s : set (V × V)) (v w : V) :
  (G.delete_edges s).adj v w  G.adj v w  ¬ (v,w)  s := iff.rfl

Does that look alright ?

Kyle Miller (Jan 12 2023 at 16:26):

You likely don't want G to be an argument to set_to_rel since it's not used.

Kyle Miller (Jan 12 2023 at 16:26):

I'd suggest this:

universes u

@[ext]
structure directed_simple_graph (V : Type u) :=
(adj : V  V  Prop)

namespace directed_simple_graph
variables {V : Type u} (G : directed_simple_graph V)

/-- `from_edge_set` constructs a `directed_simple_graph` from a set of edges. -/
def from_edge_set (s : set (V × V)) : directed_simple_graph V :=
{ adj := λ v w, (v, w)  s }

/-- The difference of two graphs `x \ y` has the edges of `x` with the edges of `y` removed. -/
instance : has_sdiff (directed_simple_graph V) := λ x y, { adj := x.adj \ y.adj }⟩

/-- Given a set of vertex pairs, remove all of the corresponding edges from the
graph's edge set, if present. -/
def delete_edges (s : set (V × V)) : directed_simple_graph V := G \ from_edge_set s

@[simp] lemma delete_edges_adj (s : set (V × V)) (v w : V) :
  (G.delete_edges s).adj v w  G.adj v w  ¬ (v,w)  s := iff.rfl

end directed_simple_graph

Kyle Miller (Jan 12 2023 at 16:27):

and I probably wouldn't have delete_edges since you can write G \ from_edge_set s

Kyle Miller (Jan 12 2023 at 16:30):

I'd also add the @[simps] attribute to from_edge_set (which automatically makes a from_edge_set_adj lemma) and add

@[simp] lemma adj_sdiff (G G' : directed_simple_graph V) (v w : V) :
  (G \ G').adj v w  G.adj v w  ¬ G'.adj v w := iff.rfl

Kyle Miller (Jan 12 2023 at 16:32):

These together should prove the analogue of delete_edges_adj, but I seem to be missing an import that makes simp handle it automatically...

lemma delete_edges_adj (s : set (V × V)) (v w : V) :
  (G \ from_edge_set s).adj v w  G.adj v w  ¬ (v,w)  s := begin simp, /- missing import? -/ end

Kyle Miller (Jan 12 2023 at 16:35):

Ah, I had @[simps] on the instance in my own file, which gave the "wrong" simp lemma for this. Here:

universes u

@[ext]
structure directed_simple_graph (V : Type u) :=
(adj : V  V  Prop)

namespace directed_simple_graph
variables {V : Type u} (G : directed_simple_graph V)

/-- `from_edge_set` constructs a `directed_simple_graph` from a set of edges. -/
@[simps]
def from_edge_set (s : set (V × V)) : directed_simple_graph V :=
{ adj := λ v w, (v, w)  s }

/-- The difference of two graphs `x \ y` has the edges of `x` with the edges of `y` removed. -/
instance : has_sdiff (directed_simple_graph V) := λ x y, { adj := x.adj \ y.adj }⟩

@[simp] lemma adj_sdiff (G G' : directed_simple_graph V) (v w : V) :
  (G \ G').adj v w  G.adj v w  ¬ G'.adj v w := iff.rfl

-- Then this particular lemma is unnecessary:
example (s : set (V × V)) (v w : V) :
  (G \ from_edge_set s).adj v w  G.adj v w  ¬ (v,w)  s := by simp

end directed_simple_graph

Christopher Schmidt (Jan 12 2023 at 16:51):

@Kyle Miller Thanks, that looks better.

Christopher Schmidt (Jan 12 2023 at 16:57):

If one includes the delete_edges Def, why does

@[simp] lemma delete_edges_univ_eq : G.delete_edges set.univ =  :=
by { ext, simp }

give an error? (wanted to have it analogous to mathlib)

Kyle Miller (Jan 12 2023 at 17:00):

That depends on what you defined bot to be. I'm guessing you don't have an adjacency simp lemma for it?

Kyle Miller (Jan 12 2023 at 17:03):

This works:

instance : has_bot (directed_simple_graph V) := ⟨{ adj :=  }⟩

@[simp]
lemma not_adj_bot (v w : V) : ¬ ( : directed_simple_graph V).adj v w := false.elim

@[simp] lemma delete_edges_univ_eq :
  G \ from_edge_set set.univ =  :=
by { ext, simp, }

Christopher Schmidt (Jan 12 2023 at 18:36):

Oh, I tough that this symbol is predefined as an always false, as G.delete edges set.univ obviously is an "always false relation".
Anyways.. thank you :smile: .


Last updated: Dec 20 2023 at 11:08 UTC