## Stream: new members

### Topic: embedding looples graphs as graphs

#### Christopher Schmidt (Jan 10 2023 at 15:18):

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 (Jan 10 2023 at 15:20):

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 (Jan 10 2023 at 15:23):

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.

Thank you!

#### Kyle Miller (Jan 10 2023 at 15:29):

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

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 (Jan 10 2023 at 15:30):

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 (Jan 10 2023 at 15:31):

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 (Jan 10 2023 at 15:32):

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

#### Christopher Schmidt (Jan 10 2023 at 15:39):

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

#### Icaro Costa (Jan 11 2023 at 17:12):

What @[ext] does?

#### Kyle Miller (Jan 11 2023 at 17:38):

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 (Jan 12 2023 at 01:35):

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,

Last updated: Dec 20 2023 at 11:08 UTC