paths using arrays

Stream: lean4

[Dean Young]

What is the easiest way to require something like

 (L.get (i)).snd= (L.get (i+1)).fst

for each i in the appropriate index, and where L is a list of "pairs".

I'm trying to define paths in a graph. It's specifically important that these paths
be stored as arrays with extra information. I also want a path of length 0 to be stored as an empty array. All this is because I want Lean to be able to run an equality check on two different paths without much effort later on.

-- a graph consists of:
structure graph where
    V : Type    -- a type of vertices
    E : Type    -- a type of edges, such that
    d₀ : E → V  -- each edge has a head
    d₁ : E → V  -- each edge has a tail



structure edge (G : graph) where
    e : G.E
    v₀ : G.V
    v₁ : G.V
    p₀ : G.d₀ e = v₀
    p₁ : G.d₁ e = v₁

open List

def matches (G : graph) (edges : List (edge G)) (i : Fin (edges.length)) (p : i < edges.length - 1) : Prop := sorry

/-
I need n < m ↔ succ n < succ m
-/

structure path (G : graph) where
    edges : List (edge G)
    beginning : (edges.length = 0) → G.V -- marks the starting vertex for paths of length 0
--  sequential : ??? some condition must ensure that the path is sequential

/-
here, some condition must ensure that the path is
in fact a path, but I'd like some help figuring out the
best way to index the list (I'm completely new to them)
-/

def pointpath {G : graph} (v : G.V) : path G := {edges := [], beginning := λ (_: [].length = 0) => v}

def domain {G : graph} (p : path G) (q : p.edges.length ≠ 0) : G.V := sorry

def codomain {G : graph} (p : path G) (q : p.edges.length ≠ 0) : G.V := sorry

def concatenate {G : graph} (p₀ : path G) (p₁ : path G) : (path G) := sorry

[Jeremy Salwen]

Not an expert, but my understanding would be that there would be many different ways to represent the condition, each of which might be appropriate if you use that style of proposition in your proofs.

For example, you could encode it using indices to say [i] and [i+1] are connected: forall i, edges[i].v1 = edges[i+1].v0
You could also use isInfix with a list of size two: forall e1 e2, [e1, e2] <:+: edges -> e1.v1 = e2.v0
You could also do a recursive definition: sequential := l.head.v1 = l.tail.head.v1 ∧ sequential l.tail

etc, etc

You could also represent a path as a list of vertices, with the attached proof showing that it only passes through valid edges.

I think the key thing is that you can prove the equivalence of these different statements, and transform it to the form you need for a specific proof. So a good starting point is thinking about which form would be easiest to use as a hypothesis to use in your proofs, and start there.

[Eric Wieser]

Are you aware of docs#simple_graph.walk?

[Dean Young]

oh thanks, that's great