graphs and deleting edges

Stream: new members

[Christopher Schmidt]

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]

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]

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

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]

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]

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]

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]

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]

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]

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

[Kyle Miller]

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]

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

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]

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]

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

[Kyle Miller]

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]

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

[Kyle Miller]

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]

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]

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]

@Kyle Miller Thanks, that looks better.

[Christopher Schmidt]

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]

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

[Kyle Miller]

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]

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