Walks as Graphs

Stream: new members

[Christopher Schmidt]

Hello everyone,
once again I have an issue with my directed graphs. I am trying to transfer directed walks to directed (sub)graphs :

import tactic

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)

@[ext]
structure directed_subgraph {V : Type u} (G : directed_simple_graph V)
extends directed_simple_graph V :=
(verts : set V)
(adj_sub : ∀ {v w : V}, adj v w → G.adj v w)
(edge_vert : ∀ {v w : V}, adj v w → v ∈ verts ∧ w ∈ verts)

@[simps]
protected def singleton_directed_subgraph (G : directed_simple_graph V) (v : V) :
G.directed_subgraph :=
{ verts := {v},
  adj := ⊥,
  adj_sub := by simp [-set.bot_eq_empty],
  edge_vert := by simp [-set.bot_eq_empty] }

@[simps]
def directed_subgraph_of_adj (G : directed_simple_graph V) {v w : V} (hvw : G.adj v w) :
G.directed_subgraph :=
{ verts := {v, w},
  adj := λ a b, (v, w) = (a, b),
  adj_sub := λ a b h, by
  { simp only [prod.mk.inj_iff] at h,
    rw [←h.1, ← h.2],
    exact hvw, },
  edge_vert := λ a b h, by
  { simp only [set.mem_insert_iff, set.mem_singleton_iff],
    simp only [prod.mk.inj_iff] at h,
    split,
    { left, exact eq.symm h.1},
    { right, exact eq.symm h.2}, }}

@[derive decidable_eq]
inductive directed_walk : V → V → Type u
| nil {u : V} : directed_walk u u
| cons {u v w: V} (h : G.adj u v) (p : directed_walk v w) : directed_walk u w

namespace directed_walk

@[simp] protected def to_directed_subgraph : Π {u v : V}, G.directed_walk u v → G.directed_subgraph
| u _ nil := G.singleton_directed_subgraph u
| _ _ (cons h p) := G.directed_subgraph_of_adj h ⊔ p.to_directed_subgraph

@[simp] protected def to_directed_graph {u v : V} (p : G.directed_walk u v) :
directed_simple_graph V :=
p.to_directed_subgraph.to_directed_simple_graph

end directed_walk

end directed_simple_graph

Any help is appreciated.

[Kyle Miller]

What is your issue?

[Christopher Schmidt]

@Kyle Miller oh, the code (i.e. "to_directed_subgraph" and "to_directed_graph") does not compile

there seems to be a problem with " ⊔" and "p.to_directed_subgraph.to_directed_simple_graph"

[Kyle Miller]

⊔ comes from defining a has_sup instance. This is implied by the lattice instance for subgraph (the sup field): https://github.com/leanprover-community/mathlib/blob/9003f28797c0664a49e4179487267c494477d853/src/combinatorics/simple_graph/subgraph.lean#L266

[Christopher Schmidt]

Kyle Miller schrieb:

⊔ comes from defining a has_sup instance. This is implied by the lattice instance for subgraph (the sup field): https://github.com/leanprover-community/mathlib/blob/9003f28797c0664a49e4179487267c494477d853/src/combinatorics/simple_graph/subgraph.lean#L266

Thanks. I managed to fix my problem.