embedding looples graphs as graphs

Stream: new members

[Christopher Schmidt]

Hello everyone,
Is it possible to embed directed loopless graphs in directed graphs such that I can use Def only made for directed graphs for the loopless ones as well? For directed graphs I already got a bunch of stuff..

universe u

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

@[ext]
structure directed_loopless_simple_graph (V : Type u) :=
(adj : V → V → Prop) (loopless : irreflexive adj . obviously)

Any help is appreciated.

[Sky Wilshaw]

You can construct the function from directed_loopless_simple_graph V to directed_simple_graph V, and show it is injective. It could be useful to mark it as a coercion, so you can use directed simple graph definitions for directed loopless simple graphs.

[Kyle Miller]

You can get that function easily by using the extends keyword:

universe u

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

@[ext]
structure directed_loopless_simple_graph (V : Type u) extends directed_simple_graph V :=
(loopless : irreflexive adj . obviously)

This defines directed_loopless_simple_graph.to_directed_simple_graph. Furthermore, if you have G : directed_loopless_simple_graph V and write G.adj it will automatically insert this function for you.

[Christopher Schmidt]

Thank you!

[Kyle Miller]

Lean 3 supports "generalized field notation", which means this works:

universe u

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

@[ext]
structure directed_loopless_simple_graph (V : Type u) extends directed_simple_graph V :=
(loopless : irreflexive adj . obviously)

def directed_simple_graph.edge_set {V : Type u} (G : directed_simple_graph V) : set (V × V) :=
{p | G.adj p.1 p.2}

lemma directed_loopless_simple_graph.diag_not_mem {V : Type u}
  (G : directed_loopless_simple_graph V) (v : V) :
  ¬ (v, v) ∈ G.edge_set :=
begin
  -- ⊢ (v, v) ∉ G.to_directed_simple_graph.edge_set
  exact G.loopless v,
end

[Kyle Miller]

the only real limitation is that you have to look at terms like G.to_directed_simple_graph.edge_set in the goal view.

[Kyle Miller]

The way it works is that when you write G.edge_set, it first looks at the namespace associated to the type for G, then it looks at its parent, and its parent, and so on until it finds something called edge_set in that namespace.

[Kyle Miller]

Then it inserts G (or a projection to a parent structure) as the first argument of the correct type.

[Christopher Schmidt]

Ah I see, thats useful to understand. I am just getting started :smile:

[Icaro Costa]

What @[ext] does?

[Kyle Miller]

attr#ext on a structure automatically creates an "ext" lemma for you. With the above example, try #print directed_simple_graph.ext after the structure to see what it made.

[Sky Wilshaw]

To add a bit more, "ext" is short for "extensionality". In lean's type theory, objects are considered equal if they were made from the same components. So to prove that two directed simple graphs are the same, it suffices to prove that their adjacency matrices coincide - this proof would use the ext lemma. You can invoke this reasoning in proofs by using the ext tactic,