# 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