## 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 :=
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 :=

@[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 :=

/-- The difference of two graphs x \ y has the edges of x with the edges of y removed. -/

@[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. -/

/-- 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) :


#### 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. -/

@[simp] lemma adj_sdiff (G G' : directed_simple_graph V) (v w : V) :

-- 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