# Zulip Chat Archive

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

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

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