11institutetext: TU Wien, Vienna, Austria
11email<EMAIL_ADDRESS>
# Formalizing Graph Trail Properties in Isabelle/HOL

Laura Kovács  Hanna Lachnitt  Stefan Szeider

###### Abstract

We describe a dataset expressing and proving properties of graph trails, using
Isabelle/HOL. We formalize the reasoning about strictly increasing and
decreasing trails, using weights over edges, and prove lower bounds over the
length of trails in weighted graphs. We do so by extending the graph theory
library of Isabelle/HOL with an algorithm computing the length of a longest
strictly decreasing graph trail starting from a vertex for a given weight
distribution, and prove that any decreasing trail is also an increasing one.

###### Keywords:

weighted graph increasing/decreasing trails Isabelle/HOL verified theory
formalization

##  1 Introduction

The problem of finding a longest trail with strictly increasing or strictly
decreasing weights in an edge-weighted graph is an interesting graph theoretic
problem [8, 3, 14, 7], with potential applications to scheduling and cost
distribution in traffic planning and routing [5]. In this paper, we formalize
and automate the reasoning about strictly increasing and strictly decreasing
trail properties by developing an extendable flexible library in the proof
assistant Isabelle/HOL [11].

As a motivating example consider the following (undirected) graph $K_{4}$,
where each edge is annotated with a different integer-valued weight ranging
from $1,\ldots,6$:

$v_{1}$$v_{2}$$v_{3}$$v_{4}$$1$$3$$6$$5$$4$$2$ Figure 1: Example graph $K_{4}$

When considering $K_{4}$, the question we address in this paper is whether
$K_{4}$ has a strictly decreasing trail of length $k\geq 1$. A trail is a
sequence of distinct edges $(e_{1},\ldots,e_{k})$, $e_{i}\in E$ such that
there exists a corresponding sequence of vertices $(v_{0},...,v_{k})$ where
$e_{i}=v_{i-1}v_{i}$. A strictly-ordered trail is a trail where the edge
weights of $(e_{1},\ldots,e_{k})$ are either strictly increasing or strictly
decreasing. Our work provides a formally verified algorithm computing such
strictly-ordered trails. Note that there is a decreasing trail in $K_{4}$
starting at vertex $v_{3}$, with trail length 3; namely
$(v_{3}v_{2};v_{2}v_{4};v_{4}v_{3})$ is such a trail, with each edge in the
trail having a higher weight than its consecutive edge in the trail.
Similarly, $K_{4}$ has decreasing trails of length 3 starting from $v_{1}$,
$v_{2}$, and $v_{4}$ respectively. A natural question to ask, which we address
in this paper, is whether it is possible to construct a graph such that the
constructed graph has 4 vertices and 5 edges, and no vertex is the starting
node of a trail of length 3? We answer this question negatively, in an even
more general setting, not restricted to 4 vertices and 5 edges. Similarly to
the theoretical results of [8], we show that, given a graph $G$ with $n$
vertices and $q$ edges, there is always a strictly decreasing trail of length
at least $2\cdot\lfloor\frac{q}{n}\rfloor$. While such a graph theoretical
result has already been announced [8], in this paper we formalize the results
in Isabelle/HOL and construct a Isabelle/HOL-verified algorithm computing
strictly decreasing trails of length $k$, whenever such trails exist.

Let us note that proving that a graph $G$ with $n$ vertices and $q$ edges
has/does not have decreasing trails is possible for small $n$, using automated
reasoning engines such as Vampire [9] and Z3 [6]. One can restrict the weights
to the integers $1,..,q$ and since $q\leq{n\choose 2}$ there is a finite
number of possibilities for each $n$. Nevertheless, the limit of such an
undertaking is reached soon. On our machine111standard laptop with 1.7 GHz
Dual-Core Intel Core i5 and 8 GB 1600 MHz memory even for $n$ = 7, both
Vampire and Z3 fail proving the existence of strictly decreasing trails, using
a 1 hour time limit. This is due to the fact that every combination of edge
weights and starting nodes is tested to be a solution. Thus, the provers are
not able to contribute to the process of finding an effective proof of the
statement. Even for relatively small numbers $n$, our experiments show that
state-of-the-art automated provers are not able to prove whether weighted
graphs have a strictly decreasing trail of a certain length.

We also note that this limitation goes beyond automated provers. In the
Isabelle proof assistant, proving that a complete graph with 3 vertices, i.e.
$K_{3}$, will always contain a strictly decreasing trail of length 3 is quite
exhaustive, as it requires reasoning about 3! = 6 possibilities for a
distribution of a weight function $w$ and then manually constructing concrete
trails:

_w _$($_ v _1_ _$\mathord{,}$_ v _2_ _$)$_  _$=$_ 2  _$\wedge$_ w _$($_ v _2_
_$\mathord{,}$_ v _3_ _$)$_  _$=$_ 1  _$\wedge$_ w _$($_ v _3_ _$\mathord{,}$_
v _1_ _$)$_  _$=$_ 3_

__$\longrightarrow$_ incTrail K _3_ w  _$[$__$($_ v _3_ _$\mathord{,}$_ v _2_
_$)$__$\mathord{,}$__$($_ v _2_ _$\mathord{,}$_ v _1_
_$)$__$\mathord{,}$__$($_ v _1_ _$\mathord{,}$_ v _3_ _$)$__$]$__

Based on such limitations of automative and interactive provers, in this paper
we aim at formalizing and proving existence of trails of length $n$, where
$n\geq 1$ is a symbolic constant. As such, proving for example that graphs
have trails of length $4$, for a concrete $n$, become instances of our
approach. To this end, we build upon existing works in this area. In
particular, the first to raise the question of the minimum length of strictly
increasing trails of arbitrary graphs were Chvátal and Komlós [4].
Subsequently, Graham and Kletman [8] proved that the lower bound of the length
of increasing trails is given by $2\cdot\lfloor\frac{q}{n}\rfloor$, as also
mentioned above. In our work, we formalize and verify such results in
Isabelle/HOL. Yet, our work is not a straightforward adaptation and
formalization of Graham and Kletman’s proof [8]. Rather, we focus on
decreasing trails instead of increasing trails and give an algorithm computing
longest decreasing trails of a given graph (Algorithm 1). By formalizing
Algorithm 1 in Isabelle/HOL, we also formally verify the correctness of the
trails computed by our approach. Moreover, we prove that any strictly
decreasing trail is also an strictly increasing one, allowing this way to use
our formalization in Isabelle/HOL also to formalize results of Graham and
Kletman [8].

#### Contributions.

This paper brings the following contributions.

(1)

We formalize strictly increasing trails and provide basic lemmas about their
properties. We improve results of [8] by giving a precise bound on the
increase of trail length.

(2)

We formalize strictly decreasing trails, in addition to the increasing trail
setting of [8]. We prove the duality between strictly increasing and strictly
decreasing trails, that is, any such decreasing trail is an increasing one,
and vice versa. Thanks to these extensions, unlike [8], we give a constructive
proof of the existence of strictly ordered trails (Lemma 1).

(3)

We design an algorithm computing longest ordered trails (Algorithm 1), and
formally verify its correctness in Isabelle/HOL. We extract our algorithm to
Haskell program code using Isabelle’s program extraction tool. Thus, we obtain
a fully verified algorithm to compute the length of strictly-ordered trails in
any given graph and weight distribution.

(4)

We verify the lower bound on the minimum length of strictly decreasing trails
of arbitrary graphs, and of complete graphs in particular.

(5)

We build upon the Graph-Theory library by Noschinski [12], that is part of the
Archive of Formal Proofs (AFP) and already includes many results on walks and
general properties of graphs. We introduce the digital dataset v formalizing
properties of graph trails. Our dataset consists of $\sim$2000 lines of
Isabelle code and it took about one month for one person to finish. As far as
we know this is the first formalization of ordered trails in a proof
assistant.

This paper was generated from Isabelle/HOL source code using Isabelle’s
document preparation tool and is therefore fully verified. The source code is
available online at https://github.com/Lachnitt/Ordered˙Trail. The rest of the
paper is organized as follows. Section 2 recalls basic terminology and
properties from graph theory. We prove lower bounds on strictly
increasing/decreasing trails in Section 3. We describe our Isabelle/HOL
formalization in Isabelle/HOL in Section 4. We discuss further directions in
Section 5 and conclude our paper with Section 6.

##  2 Preliminaries

We briefly recapitulate the basic notions of graph theory. A graph $G=(V,E)$
consists of a set $V$ of vertices and a set $E\subseteq V\times V$ of edges. A
graph is undirected if $(v_{1},v_{2})\in E$ implies that also
$(v_{2},v_{1})\in E$. A graph is complete if every pair of vertices is
connected by an edge. A graph is loopfree or simple if there are no edges
$(x,x)\in E$ and finite if the number of vertices $|V|$ is finite. Finally, we
call a graph $G^{\prime}=(V^{\prime},E^{\prime})$ a subgraph of $G=(V,E)$ if
$V^{\prime}\subseteq V$ and $E^{\prime}\subseteq E$.

If a graph is equipped with a weight function $w:E\rightarrow\mathbb{R}$ that
maps edges to real numbers, it is called an edge-weighted graph. In the
following, whenever a graph is mentioned it is implicitly assumed that this
graph comes equipped with a weight function. A vertex labelling is a function
$L:V\rightarrow\mathbb{N}$.

A trail of length k in a graph $G=(V,E)$ is a sequence $(e_{1},\ldots,e_{k})$,
$e_{i}\in E$, of distinct edges such that there exists a corresponding
sequence of vertices $(v_{0},...,v_{k})$ where $e_{i}=v_{i-1}v_{i}$. A
strictly decreasing trail in an edge-weighted graph $G=(V,E)$ with weight
function $w$ is a trail such that $w(e_{i})>w(e_{i+1})$. Likewise, a strictly
increasing trail is a trail such that $w(e_{i})<w(e_{i+1})$. A trail is
strictly-ordered if it is strictly increasing or strictly decreasing.

We will denote the length of a longest strictly increasing trail with
$P_{i}(w,G)$. Likewise we will denote the length of a longest strictly
decreasing trail with $P_{d}(w,G)$. In any undirected graph, it holds that
$P_{i}(w,G)=P_{d}(w,G)$, a result that we will formally verify in Section 4.2.

Let $f_{i}(n)=\min_{n}P_{i}(w,K_{n})$ denote the minimum length of an strictly
increasing trail that must exist in the complete graph with $n$ vertices.
Likewise, $f_{d}(n)=\min_{n}P_{d}(w,K_{n})$ in the case that we consider
strictly decreasing trails.

##  3 Lower Bounds on Increasing and Decreasing Trails in Weighted Graphs

The proof introduced in the following is based on similar ideas as in [8].
However, we diverge from [8] in several aspects. Firstly, we consider strictly
decreasing instead of strictly increasing trails, reducing the complexity of
the automated proof (see Section 4). Moreover, we add tighter bounds than
necessary to give a fully constructive proof in terms of an algorithm for
computing the length of these trails (see Section 4.3). We discuss this
further at the end of the section.

We start by introducing the notion of a weighted subgraph and then we built on
that by specifying a family of labelling functions:

######  Definition 1 (Weighted Subgraph)

Let $G=(V,E)$ be a graph with weight function $w:E\rightarrow\\{1,\ldots,q\\}$
where $|E|=q$. For each $i\in\\{0,...,q\\}$ define a weighted subgraph
$G^{i}=(V,E^{i})$ such that $e\in E^{i}$ iff $w(e)\in\\{1,...,i\\}$. That is,
$G^{i}$ contains only edges labelled with weights $\leq i$.

######  Definition 2 (Labelling Function)

For each $G^{i}=(V,E^{i})$, $n=|V|$ we define
$L^{i}:V\\{1,\ldots,\frac{n(n-1)}{2}\\}$ a labelling function such that
$L^{i}(v)$ is the length of a longest strictly decreasing trail starting at
vertex v using only edges in $E^{i}$.

In Figure 2 the example graph from Figure 1 is revisited to illustrate these
definitions. We need to prove the following property.

$v_{1}$$v_{2}$$v_{3}$$v_{4}$$1$$3$$4$$5$$2$

Decreasing trails from $v_{3}$ are:

$v_{3}-v_{4}$,

$v_{3}-v_{1}-v_{2}$,

$v_{3}-v_{2}-v_{1}$,

$v_{3}-v_{2}-v_{4}-v3$

Therefore, $L^{5}(v_{3})=3$.

Decreasing trails from $v_{1}$ are:

$v_{1}-v_{2}$

$v_{1}-v_{3}-v_{4}$

Therefore, $L^{5}(v_{1})=2$.

Figure 2: Graph $G^{5}$ with labelling function $L^{5}$

###### Lemma 1

If $i<q$, then $\sum_{v\in V}L^{i+1}(v)\geq\sum_{v\in V}L^{i}(v)+2$.

###### Proof

Let $e$ be the edge labelled with $i+1$ and denote its endpoints with $u_{1}$
and $u_{2}$. It holds that $E^{i}\cup\\{e\\}=E^{i+1}$, therefore the graph
$G^{i+1}$ is $G^{i}$ with the additional edge $e$. As $w(e^{\prime})<w(e)$,
for all $e^{\prime}\in E^{i}$ we have $L^{i+1}(v)=L^{i}(v)$ for all $v\in V$
with $u_{1}\neq v,u_{2}\neq v$. It also holds that
$L^{i+1}(u_{1})=\max(L^{i}(u_{2})+1,L^{i}(u_{1}))$ because either that longest
trail from $u_{1}$ can be prolonged with edge $e$ ($i+1$ will be greater than
the weight of the first edge in this trail by construction of $L^{i+1}$) or
there is already a longer trail starting from $u_{1}$ not using e. We derive
$L^{i+1}(u_{2})=\max(L^{i}(u_{1})+1,L^{i}(u_{2}))$ based on a similar
reasoning. See Figure 3 for an illustration.

Note that $L^{i+1}(v)=L^{i}(v)$ for $v\in V\setminus\\{u_{1},u_{2}\\}$,
because no edge incident to these vertices was added and a trail starting from
them cannot be prolonged since the new edge has bigger weight than any edge in
such a trail.

If $L(u_{1})=L(u_{2})$, then $L^{i+1}(u_{1})=L^{i}(u_{1})+1$ and
$L^{i+1}(u_{2})=L^{i}(u_{2})+1$ and thus the sum increases exactly by 2. If
$L(u_{1})>L(u_{2})$ then $L^{i+1}(u_{2})=L^{i}(u_{1})+1\geq L^{i}(u_{2})+2$,
otherwise $L^{i+1}(u_{1})=L^{i}(u_{2})+1\geq L^{i}(u_{1})+2$. Thus,

$\displaystyle\sum_{v\in V}L^{i+1}(v)$ $\displaystyle~{}=~{}$
$\displaystyle\sum_{v\in(V-\\{u_{1},u_{2}\\})}L^{i+1}(v)+L^{i+1}(u_{1})+L^{i+1}(u_{2})$
$\displaystyle~{}\geq~{}$
$\displaystyle\sum_{v\in(V-\\{u_{1},u_{2}\\})}L^{i+1}(v)+L^{i}(u_{1})+L^{i}(u_{2})+2$
$\displaystyle~{}=~{}$ $\displaystyle\sum_{v\in V}L^{i}(v)+2.$

∎

Situation before adding edge $e$: $L^{i}(u_{1})$$L^{i}(u_{2})$Case 1:
$L^{i}(u_{1})=L^{i}(u_{2})$: $L^{i+1}(u_{1})+1$$L^{i+1}(u_{2})+1$$i+1$Case 2:
$L^{i}(u_{1})>L^{i}(u_{2})$: $L^{i+1}(u_{2})+1$$L^{i+1}(u_{2})$$i+1$Case 3:
$L^{i}(u_{1})<L^{i}(u_{2})$:$L^{i+1}(u_{1})$$L^{i+1}(u_{1})+1$$i+1$ Figure 3:
Case distinction when adding edge $e$ in Lemma 1

Note that the proof of Lemma 1 is constructive, yielding the Algorithm 1 for
computing longest strictly decreasing trails. Function $findEndpoints$
searches for an edge in a graph $G$ by its weight $i$ and returns both
endpoints. Function $findMax$ returns the maximum value of the array $L$.

for  _$v\in V$_ do

$L(v):=0$

end for

for  _$i=1;i <|E|;i++$_ do

$(u,v)=findEndpoints(G,i)$;

$temp=L(u)$;

$L(u)=\max(L(v)+1,L(u))$ ;

$L(v)=\max(temp+1,L(v))$ ;

end for

return findMax(L);

Algorithm 1 Find Longest Strictly Decreasing Trail

###### Lemma 2

$\sum_{v\in V}L^{q}(v)\geq 2q$.

###### Proof

We proceed by induction, using the property $\sum_{v\in
V}L^{i+1}(v)\geq\sum_{v\in V}L^{i}(v)+2$ from Lemma 1. For the induction base
note that $\sum_{v\in V}L^{0}(v)=0$ because $G^{0}$ does not contain any edges
and thus no vertex has a strictly decreasing trail of length greater than 0. ∎

We next prove the lower bound on the length of longest strictly decreasing
trails.

###### Theorem 3.1

Let $G=(V,E)$ be an undirected edge-weighted graph such that $|V|=n$ and
$|E|=q$. Let $w:E\rightarrow\\{1,\ldots,q\\}$ be a weight function assuming
different weights are mapped to to different edges. Then, $P_{d}(w,G)\geq
2\cdot\lfloor\frac{q}{n}\rfloor$ i.e., there exists a strictly decreasing
trail of length $2\cdot\lfloor\frac{q}{n}\rfloor$.

###### Proof

Assume that no vertex is a starting point of a trail of length at least
$2\cdot\lfloor\frac{q}{n}\rfloor$, that is
$L^{q}(v)<2\cdot\lfloor\frac{q}{n}\rfloor,$ for all $v\in V$. Then,
$\sum_{v\in V}L^{q}(v)<2\cdot\lfloor\frac{q}{n}\rfloor n\leq 2\cdot q$. But
this is a contradiction to Lemma 2 that postulates that the sum of the length
of all longest strictly decreasing trails $\sum_{v\in V}L^{q}(v)$ is greater
than $2\cdot q$. Hence, there has to be at least one vertex with a strictly
decreasing trail that is longer than $2\cdot\lfloor\frac{q}{n}\rfloor$ in
$G^{q}$. This trail contains a subtrail of length
$2\cdot\lfloor\frac{q}{n}\rfloor$. Since $E^{q}=E$ it follows that $G^{q}=G$,
which concludes the proof. ∎

Based on Theorem 3.1, we get the following results.

###### Corollary 1

It holds that $P_{i}(w,G)\geq 2\cdot\lfloor\frac{q}{n}\rfloor$ since when
reversing a strictly decreasing trail one obtains a strictly increasing one.
In this case, define $L^{i}(v)$ as the length of a longest strictly increasing
trail ending at $v$ in $G^{i}$.∎

###### Corollary 2

Let G be as in Theorem 3.1 and additionally assume that G is complete. Then,
there exists a trail of length at least $n-1$, i.e., $f_{i}(n)=f_{d}(n)\geq
n-1$.∎

In [8] the authors present a non-constructive proof. As in Lemma 1 they argue
that the sum of the lengths of all increasing trails is at least 2. Thus, they
overestimate the increase. We however, use the exact increase therefore making
the proof constructive and obtaining Algorithm 1.

##  4 Formalization of Trail Properties in Isabelle/HOL

###  4.1 Graph Theory in the Archive of Formal Proofs

To increase the reusability of our library we build upon the _Graph -Theory_
library by Noschinski [12]. Graphs are represented as records consisting of
vertices and edges that can be accessed using the selectors _pverts_ and
_parcs_. We recall the definition of the type _pair -pre-digraph_:

* record  _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a pair-pre-digraph  _$=$_ pverts  _$\mathord{:}$__$\mathord{:}$_  _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a set parcs  _$\mathord{:}$__$\mathord{:}$_  _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a rel

Now restrictions upon the two sets and new features can be introduced using
locales. Locales are Isabelle’s way to deal with parameterized theories [1].
Consider for example _pair -wf-digraph_. The endpoints of an edge can be
accessed using the functions _fst_ and _snd_. Therefore, conditions _arc -fst-
in-verts_ and _arc -snd-in-verts_ assert that both endpoints of an edge are
vertices. Using so-called sublocales a variety of other graphs are defined.

* locale pair-wf-digraph  _$=$_ pair-pre-digraph  _$+$_

assumes arc-fst-in-verts _$\mathord{:}$_  _$\bigwedge$_ e _$\mathord{.}$_ e
_$\in$_ parcs G  _$\Longrightarrow$_ fst e  _$\in$_ pverts G

assumes arc-snd-in-verts _$\mathord{:}$_  _$\bigwedge$_ e _$\mathord{.}$_ e
_$\in$_ parcs G  _$\Longrightarrow$_ snd e  _$\in$_ pverts G

An object of type __$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ b awalk_ is
defined in _Graph -Theory _$\mathord{.}$_ Arc-Walk_ as a list of edges.
Additionally, the definition _awalk_ imposes that both endpoints of a walk are
vertices of the graph, all elements of the walk are edges and two subsequent
edges share a common vertex.

_type -synonym  _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ b awalk  _$=$_
_$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ b list_

* definition awalk  _$\mathord{:}$__$\mathord{:}$_  _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a  _$\Rightarrow$_  _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ b awalk  _$\Rightarrow$_  _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a  _$\Rightarrow$_ bool

awalk u p v  _$\equiv$_ u  _$\in$_ verts G  _$\wedge$_ set p  _$\subseteq$_
arcs G  _$\wedge$_ cas u p v

We also reuse the type synonym _weight -fun_ introduced in _Weighted -Graph_.

_type -synonym  _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ b weight-fun  _$=$_
_$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ b  _$\Rightarrow$_ real_

Finally, there is an useful definition capturing the notion of a complete
graph, namely _complete -digraph_.

###  4.2 Increasing and Decreasing Trails in Weighted Graphs

In our work we extend the graph theory framework from Section 4.1 with new
features enabling reasoning about ordered trails. To this end, a trail is
defined as a list of edges. We will only consider strictly increasing trails
on graphs without parallel edges. For this we require the graph to be of type
_pair -pre-digraph_, as introduced in Section 4.1.

Two different definitions are given in our formalization. Function _incTrail_
can be used without specifying the first and last vertex of the trail whereas
_incTrail2_ uses more of _Graph -Theory _$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ s_ predefined features. Moreover, making use
of monotonicity _incTrail_ only requires to check if one edge’s weight is
smaller than its successors’ while _incTrail2_ checks if the weight is smaller
than the one of all subsequent edges in the sequence, i.e. if the list is
sorted. The equivalence between the two notions is shown in the following.

_fun_ incTrail  _$\mathord{:}$__$\mathord{:}$_  _$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a pair-pre-digraph  _$\Rightarrow$_
_$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a  _$\times$__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$)$_ weight-fun  _$\Rightarrow$_
_$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a  _$\times$__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$)$_ list  _$\Rightarrow$_ bool  _where_

incTrail g w  _$[$__$]$_  _$=$_ True  _$\mid$_

incTrail g w  _$[$_ e _1_ _$]$_  _$=$_  _$($_ e _1_  _$\in$_ parcs g _$)$_
_$\mid$_

incTrail g w  _$($_ e _1_ _$\\#$_ e _2_ _$\\#$_ es _$)$_  _$=$_  _$($_ if w e
_1_  _$ <$_ w e _2_  _$\wedge$_ e _1_  _$\in$_ parcs g  _$\wedge$_ snd e _1_
_$=$_ fst e _2_

then incTrail g w  _$($_ e _2_ _$\\#$_ es _$)$_ else False _$)$_

_definition_ _$($__in_ pair-pre-digraph _$)$_ incTrail2  _where_

incTrail2 w es u v  _$\equiv$_ sorted-wrt  _$($__$\lambda$_ e _1_ e _2_
_$\mathord{.}$_ w e _1_  _$ <$_ w e _2_ _$)$_ es  _$\wedge$_  _$($_ es  _$=$_
_$[$__$]$_  _$\vee$_ awalk u es v _$)$_

_fun_ decTrail  _$\mathord{:}$__$\mathord{:}$_  _$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a pair-pre-digraph  _$\Rightarrow$_
_$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a  _$\times$__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$)$_ weight-fun  _$\Rightarrow$_
_$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a  _$\times$__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$)$_ list  _$\Rightarrow$_ bool  _where_

decTrail g w  _$[$__$]$_  _$=$_ True  _$\mid$_

decTrail g w  _$[$_ e _1_ _$]$_  _$=$_  _$($_ e _1_  _$\in$_ parcs g _$)$_
_$\mid$_

decTrail g w  _$($_ e _1_ _$\\#$_ e _2_ _$\\#$_ es _$)$_  _$=$_  _$($_ if w e
_1_  _$ >$_ w e _2_  _$\wedge$_ e _1_  _$\in$_ parcs g  _$\wedge$_ snd e _1_
_$=$_ fst e _2_

then decTrail g w  _$($_ e _2_ _$\\#$_ es _$)$_ else False _$)$_

_definition_ _$($__in_ pair-pre-digraph _$)$_ decTrail2  _where_

decTrail2 w es u v  _$\equiv$_ sorted-wrt  _$($__$\lambda$_ e _1_ e _2_
_$\mathord{.}$_ w e _1_  _$ >$_ w e _2_ _$)$_ es  _$\wedge$_  _$($_ es  _$=$_
_$[$__$]$_  _$\vee$_ awalk u es v _$)$_

Defining trails as lists in Isabelle has many advantages including using
predefined list operators, e.g., drop. Thus, we can show one result that will
be constantly needed in the following, that is, that any subtrail of an
ordered trail is an ordered trail itself.

_lemma_ incTrail-subtrail _$\mathord{:}$_

 _assumes_ incTrail g w es

 _shows_ incTrail g w  _$($_ drop k es _$)$_

_lemma_ decTrail-subtrail _$\mathord{:}$_

 _assumes_ decTrail g w es

 _shows_ decTrail g w  _$($_ drop k es _$)$_

In Isabelle we then show the equivalence between the two definitions
_decTrail_ and _decTrail2_ of strictly decreasing trails. Similarly, we also
show the equivalence between the definition _incTrail_ and _incTrail2_ of
strictly increasing trails.

_lemma_ _$($__in_ pair-wf-digraph _$)$_ decTrail-is-dec-walk _$\mathord{:}$_

 _shows_ decTrail G w es  _$\longleftrightarrow$_ decTrail2 w es  _$($_ fst
_$($_ hd es _$)$__$)$_  _$($_ snd  _$($_ last es _$)$__$)$_

_lemma_ _$($__in_ pair-wf-digraph _$)$_ incTrail-is-inc-walk _$\mathord{:}$_

 _shows_ incTrail G w es  _$\longleftrightarrow$_ incTrail2 w es  _$($_ fst
_$($_ hd es _$)$__$)$_  _$($_ snd  _$($_ last es _$)$__$)$_

Any strictly decreasing trail $(e_{1},\ldots,e_{n})$ can also be seen as a
strictly increasing trail $(e_{n},...,e_{1})$ if the graph considered is
undirected. To this end, we make use of the locale _pair -sym-digraph_ that
captures the idea of symmetric arcs. However, it is also necessary to assume
that the weight function assigns the same weight to edge $(v_{i},v_{j})$ as to
$(v_{j},v_{i})$. This assumption is therefore added to _decTrail -eq-rev-
incTrail_ and _incTrail -eq-rev-decTrail_.

_lemma_ _$($__in_ pair-sym-digraph _$)$_ decTrail-eq-rev-incTrail
_$\mathord{:}$_

 _assumes_  _$\forall\,$_ v _1_ v _2_ _$\mathord{.}$_ w  _$($_ v _1_
_$\mathord{,}$_ v _2_ _$)$_  _$=$_ w _$($_ v _2_ _$\mathord{,}$_ v _1_ _$)$_

 _shows_ decTrail G w es  _$\longleftrightarrow$_ incTrail G w  _$($_ rev
_$($_ map  _$($__$\lambda$__$($_ v _1_ _$\mathord{,}$_ v _2_
_$)$__$\mathord{.}$_  _$($_ v _2_ _$\mathord{,}$_ v _1_ _$)$__$)$_ es
_$)$__$)$_

_lemma_ _$($__in_ pair-sym-digraph _$)$_ incTrail-eq-rev-decTrail
_$\mathord{:}$_

 _assumes_  _$\forall\,$_ v _1_ v _2_ _$\mathord{.}$_ w  _$($_ v _1_
_$\mathord{,}$_ v _2_ _$)$_  _$=$_ w _$($_ v _2_ _$\mathord{,}$_ v _1_ _$)$_

 _shows_ incTrail G w es  _$\longleftrightarrow$_ decTrail G w  _$($_ rev
_$($_ map  _$($__$\lambda$__$($_ v _1_ _$\mathord{,}$_ v _2_
_$)$__$\mathord{.}$_  _$($_ v _2_ _$\mathord{,}$_ v _1_ _$)$__$)$_ es
_$)$__$)$_

###  4.3 Weighted Graphs

We add the locale _weighted -pair-graph_ on top of the locale _pair -graph_
introduced in _Graph -Theory_. A _pair -graph_ is a finite, loop free and
symmetric graph. We do not restrict the types of vertices and edges but impose
the condition that they have to be a linear order.

Furthermore, all weights have to be integers between 0 and
$\lfloor\frac{q}{2}\rfloor$ where 0 is used as a special value to indicate
that there is no edge at that position. Since the range of the weight function
is in the reals, the set of natural numbers __$\\{$_ 1
_$\mathord{,}$__$\mathord{.}$__$\mathord{.}$__$\mathord{,}$_ card  _$($_ parcs
G _$)$_ div 2 _$\\}$__ has to be casted into a set of reals. This is realized
by taking the image of the function _real_ that casts a natural number to a
real.

_locale_ weighted-pair-graph  _$=$_ pair-graph  _$($_ G
_$\mathord{:}$__$\mathord{:}$_  _$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_
a _$\mathord{:}$__$\mathord{:}$_ linorder _$)$_ pair-pre-digraph _$)$_  _for_
G  _$+$_

 _fixes_ w  _$\mathord{:}$__$\mathord{:}$_  _$($__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$\times$__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$)$_ weight-fun

 _assumes_ dom _$\mathord{:}$_ e  _$\in$_ parcs G  _$\longrightarrow$_ w e
_$\in$_ real ‘  _$\\{$_ 1 _$\mathord{.}$__$\mathord{.}$_ card  _$($_ parcs G
_$)$_ div 2 _$\\}$_

 _and_ vert-ge _$\mathord{:}$_ card  _$($_ pverts G _$)$_  _$\geq$_ 1

We introduce some useful abbreviations, according to the ones in Section 2

_abbreviation_ _$($__in_ weighted-pair-graph _$)$_ q  _$\equiv$_ card  _$($_
parcs G _$)$_

_abbreviation_ _$($__in_ weighted-pair-graph _$)$_ n  _$\equiv$_ card  _$($_
pverts G _$)$_

_abbreviation_ _$($__in_ weighted-pair-graph _$)$_ W  _$\equiv$_  _$\\{$_ 1
_$\mathord{.}$__$\mathord{.}$_ q div 2 _$\\}$_

Note an important difference between Section 3 and our formalization. Although
a _weighted -pair-graph_ is symmetric, the edge set contains both “directions”
of an edge, i.e., $(v_{1},v_{2})$ and $(v_{2},v_{1})$ are both in _parcs G_.
Thus, the maximum number of edges (in the case that the graph is complete) is
$n\cdot(n-1)$ and not $\frac{n\cdot(n-1)}{2}$. Another consequence is that the
number $q$ of edges is always even.

_lemma_  _$($__in_ weighted-pair-graph _$)$_ max-arcs _$\mathord{:}$_

 _shows_ card  _$($_ parcs G _$)$_  _$\leq$_ n _$*$__$($_ n _$-$_ 1 _$)$_

_lemma_  _$($__in_ weighted-pair-graph _$)$_ even-arcs _$\mathord{:}$_

 _shows_ even q

The below sublocale _distinct -weighted-pair-graph_ refines _weighted -pair-
graph_. The condition _zero_ fixes the meaning of 0. The weight function is
defined on the set of all vertices but since self loops are not allowed; we
use 0 as a special value to indicate the unavailability of the edge. The
second condition _distinct_ enforces that no two edges can have the same
weight. There are some exceptions however captured in the statement __$($_ v
_1_  _$=$_ u _2_  _$\wedge$_ v _2_  _$=$_ u _1_ _$)$_  _$\vee$_  _$($_ v _1_
_$=$_ u _1_  _$\wedge$_ v _2_  _$=$_ u _2_ _$)$__. Firstly, $(v_{1},v_{2})$
should have the same weight as $(v_{2},v_{1})$. Secondly, $w(v_{1},v_{2})$ has
the same value as $w(v_{1},v_{2})$. Note that both edges being self loops
resulting in them both having weight 0 is prohibited by condition _zero_. Our
decision to separate these two conditions from the ones in _weighted -pair-
graph_ instead of making one locale of its own is two-fold: On the one hand,
there are scenarios where distinctiveness is not wished for. On the other
hand, 0 might not be available as a special value.

_locale_ distinct-weighted-pair-graph  _$=$_ weighted-pair-graph  _$+$_

 _assumes_ zero _$\mathord{:}$_  _$\forall\,$_ v _1_ v _2_ _$\mathord{.}$_
_$($_ v _1_ _$\mathord{,}$_ v _2_ _$)$_  _$\notin$_ parcs G
_$\longleftrightarrow$_ w  _$($_ v _1_ _$\mathord{,}$_ v _2_ _$)$_  _$=$_ 0

 _and_ distinct _$\mathord{:}$_  _$\forall\,$_  _$($_ v _1_ _$\mathord{,}$_ v
_2_ _$)$_  _$\in$_ parcs G _$\mathord{.}$_  _$\forall\,$_  _$($_ u _1_
_$\mathord{,}$_ u _2_ _$)$_  _$\in$_ parcs G _$\mathord{.}$_

 _$($__$($_ v _1_  _$=$_ u _2_  _$\wedge$_ v _2_  _$=$_ u _1_ _$)$_  _$\vee$_
_$($_ v _1_  _$=$_ u _1_  _$\wedge$_ v _2_  _$=$_ u _2_ _$)$__$)$_
_$\longleftrightarrow$_ w  _$($_ v _1_ _$\mathord{,}$_ v _2_ _$)$_  _$=$_ w
_$($_ u _1_ _$\mathord{,}$_ u _2_ _$)$_

One important step in our formalization is to show that the weight function is
surjective. However, having two elements of the domain (edges) being mapped to
the same element of the codomain (weight) makes the proof complicated. We
therefore first prove that the weight function is surjective on a restricted
set of edges. Here we use the fact that there is a linear order on vertices by
only considering edges were the first endpoint is bigger than the second.

Then, the surjectivity of $w$ is relatively simple to show. Note that we could
also have assumed surjectivity in _distinct -weighted-pair-graph_ and shown
that distinctiveness follows from it. However, distinctiveness is the more
natural assumption that is more likely to appear in any application of ordered
trails.

_lemma_ _$($__in_ distinct-weighted-pair-graph _$)$_ restricted-weight-fun-
surjective _$\mathord{:}$_

 _$\forall\,$_ k  _$\in$_ W _$\mathord{.}$_  _$\exists\,$__$($_ v _1_
_$\mathord{,}$_ v _2_ _$)$_  _$\in$_  _$\\{$__$($_ p1 _$\mathord{,}$_ p2
_$)$__$\mathord{.}$_  _$($_ p1 _$\mathord{,}$_ p2 _$)$_  _$\in$_ parcs G
_$\wedge$_ p2  _$ <$_ p1 _$\\}$__$\mathord{.}$_ w  _$($_ v _1_ _$\mathord{,}$_
v _2_ _$)$_  _$=$_ k

_lemma_ _$($__in_ distinct-weighted-pair-graph _$)$_ weight-fun-surjective
_$\mathord{:}$_

 _shows_  _$\forall\,$_ k  _$\in$_ W _$\mathord{.}$_  _$\exists\,$__$($_ v _1_
_$\mathord{,}$_ v _2_ _$)$_  _$\in$_ parcs G _$\mathord{.}$_ w  _$($_ v _1_
_$\mathord{,}$_ v _2_ _$)$_  _$=$_ k

###  4.4 Computing a Longest Ordered Trail

We next formally verify Algorithm 1 and compute longest ordered trails. To
this end, we introduce the function _findEdge_ to find an edge in a list of
edges by its weight.

_fun_ findEdge  _$\mathord{:}$__$\mathord{:}$_  _$($__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$\times$__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$)$_ weight-fun  _$\Rightarrow$_
_$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$\times$__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$)$_ list  _$\Rightarrow$_ real
_$\Rightarrow$_  _$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a
_$\times$__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$)$_  _where_

findEdge f  _$[$__$]$_ k  _$=$_ undefined  _$\mid$_

findEdge f  _$($_ e _$\\#$_ es _$)$_ k  _$=$_  _$($_ if f e  _$=$_ k then e
else findEdge f es k _$)$_

Function _findEdge_ will correctly return the edge whose weight is $k$. We do
not care in which order the endpoints are found, i.e. whether $(v_{1},v_{2})$
or $(v_{2},v_{1})$ is returned.

_lemma_ _$($__in_ distinct-weighted-pair-graph _$)$_ findEdge-success
_$\mathord{:}$_

 _assumes_ k  _$\in$_ W  _and_ w  _$($_ v _1_ _$\mathord{,}$_ v _2_ _$)$_
_$=$_ k  _and_  _$($_ parcs G _$)$_  _$\not=$_  _$\\{$__$\\}$_

 _shows_  _$($_ findEdge w  _$($_ set-to-list  _$($_ parcs G _$)$__$)$_ k
_$)$_  _$=$_  _$($_ v _1_ _$\mathord{,}$_ v _2_ _$)$_

 _$\vee$_  _$($_ findEdge w  _$($_ set-to-list  _$($_ parcs G _$)$__$)$_ k
_$)$_  _$=$_  _$($_ v _2_ _$\mathord{,}$_ v _1_ _$)$_

We translate the notion of a labelling function $L^{i}(v)$ (see Definition 2)
into Isabelle. Function _getL G w_ , in short for get label, returns the
length of the longest strictly decreasing path starting at vertex $v$. In
contrast to Definition 2 subgraphs are treated here implicitly. Intuitively,
this can be seen as adding edges to an empty graph in order of their weight.

_fun_ getL  _$\mathord{:}$__$\mathord{:}$_  _$($__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$\mathord{:}$__$\mathord{:}$_ linorder
_$)$_ pair-pre-digraph  _$\Rightarrow$_  _$($__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$\times$__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$)$_ weight-fun

 _$\Rightarrow$_ nat  _$\Rightarrow$_  _$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ a  _$\Rightarrow$_ nat  _where_

getL g w 0 v  _$=$_ 0  _$\mid$_

getL g w  _$($_ Suc i _$)$_ v  _$=$_  _$($_ let  _$($_ v _1_ _$\mathord{,}$_ v
_2_ _$)$_  _$=$_  _$($_ findEdge w  _$($_ set-to-list  _$($_ arcs g _$)$__$)$_
_$($_ Suc i _$)$__$)$_ in

 _$($_ if v  _$=$_ v _1_ then max  _$($__$($_ getL g w i v _2_ _$)$__$+$_ 1
_$)$_  _$($_ getL g w i v _$)$_ else

 _$($_ if v  _$=$_ v _2_ then max  _$($__$($_ getL g w i v _1_ _$)$__$+$_ 1
_$)$_  _$($_ getL g w i v _$)$_ else getL g w i v _$)$__$)$__$)$_

To add all edges to the graph, set $i=|E|$. Recall that _card _$($_ parcs g
_$)$__ $=2*|E|$, as every edge appears twice. Then, iterate over all vertices
and give back the maximum length which is found by using _getL G w_. Since
_getL G w_ can also be used to get a longest strictly increasing trail ending
at vertex $v$ the algorithm is not restricted to strictly decreasing trails.

_definition_ getLongestTrail  _$\mathord{:}$__$\mathord{:}$_

_$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a
_$\mathord{:}$__$\mathord{:}$_ linorder _$)$_ pair-pre-digraph
_$\Rightarrow$_  _$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a
_$\times$__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ a _$)$_ weight-fun
_$\Rightarrow$_ nat  _where_

getLongestTrail g w  _$=$_

Max  _$($_ set  _$[$__$($_ getL g w  _$($_ card  _$($_ parcs g _$)$_ div 2
_$)$_ v _$)$_  _$\mathord{.}$_ v  _$ <$__$-$_ sorted-list-of-set  _$($_ pverts
g _$)$__$]$__$)$_

Exporting the algorithm into Haskell code results in a fully verified program
to find a longest strictly decreasing or strictly increasing trail.

_export -code_ getLongestTrail  _in_ Haskell  _module -name_ LongestTrail

Using an induction proof and extensive case distinction, the correctness of
Algorithm 1 is then shown in our formalization, by proving the following
theorem:

_theorem_ _$($__in_ distinct-weighted-pair-graph _$)$_ correctness
_$\mathord{:}$_

 _assumes_  _$\exists\,$_ v  _$\in$_  _$($_ pverts G _$)$__$\mathord{.}$_ getL
G w  _$($_ q div 2 _$)$_ v  _$=$_ k

 _shows_  _$\exists\,$_ xs _$\mathord{.}$_ decTrail G w xs  _$\wedge$_ length
xs  _$=$_ k

###  4.5 Minimum Length of Ordered Trails

The algorithm introduced in Section 4.4 is already useful on its own.
Additionally, it can be used to verify the lower bound on the minimum length
of a strictly decreasing trail $P_{d}(w,G)\geq
2\cdot\lfloor\frac{q}{n}\rfloor$.

To this end, Lemma 1 from Section 3 is translated into Isabelle as the lemma
_minimal -increase-one-step_. The proof is similar to its counterpart, also
using a case distinction. Lemma 2 is subsequently proved, here named _minimal
-increase-total_.

_lemma_ _$($__in_ distinct-weighted-pair-graph _$)$_ minimal-increase-one-step
_$\mathord{:}$_

 _assumes_ k  _$+$_ 1  _$\in$_ W

 _shows_

 _$($__$\sum\,$_ v  _$\in$_ pverts G _$\mathord{.}$_ getL G w  _$($_ k _$+$_ 1
_$)$_ v _$)$_  _$\geq$_  _$($__$\sum\,$_ v  _$\in$_ pverts G _$\mathord{.}$_
getL G w k v _$)$_  _$+$_ 2

_lemma_ _$($__in_ distinct-weighted-pair-graph _$)$_ minimal-increase-total
_$\mathord{:}$_

 _shows_  _$($__$\sum\,$_ v  _$\in$_ pverts G _$\mathord{.}$_ getL G w  _$($_
q div 2 _$)$_ v _$)$_  _$\geq$_ q

From _minimal -increase-total_ we have that that the sum of all labels after
$q$ div $2$ steps is greater than $q$. Now assume that all labels are smaller
than $q$ div $n$. Because we have $n$ vertices, this leads to a contradiction,
which proves _algo -result-min_.

_lemma_ _$($__in_ distinct-weighted-pair-graph _$)$_ algo-result-min
_$\mathord{:}$_

 _shows_  _$($__$\exists\,$_ v  _$\in$_ pverts G _$\mathord{.}$_ getL G w
_$($_ q div 2 _$)$_ v  _$\geq$_ q div n _$)$_

Finally, using lemma _algo -result-min_ together with the _correctness_
theorem of section 4.4, we prove the lower bound of
$2\cdot\lfloor\frac{q}{n}\rfloor$ over the length of a longest strictly
decreasing trail. This general approach could also be used to extend our
formalization and prove existence of other trails. For example, assume that
some restrictions on the graph give raise to the existence of a trail of
length $m\geq 2\cdot\lfloor\frac{q}{n}\rfloor$. Then, it is only necessary to
show that our algorithm can find this trail.

_theorem_ _$($__in_ distinct-weighted-pair-graph _$)$_ dec-trail-exists
_$\mathord{:}$_

 _shows_  _$\exists\,$_ es _$\mathord{.}$_ decTrail G w es  _$\wedge$_ length
es  _$=$_ q div n

_theorem_ _$($__in_ distinct-weighted-pair-graph _$)$_ inc-trail-exists
_$\mathord{:}$_

 _shows_  _$\exists\,$_ es _$\mathord{.}$_ incTrail G w es  _$\wedge$_ length
es  _$=$_ q div n

Corollary 1 is translated into _dec -trail-exists-complete_. The proof first
argues that the number of edges is $n\cdot(n-1)$ by restricting its domain as
done already in Section 4.3.

_lemma_ _$($__in_ distinct-weighted-pair-graph _$)$_ dec-trail-exists-complete
_$\mathord{:}$_

 _assumes_ complete-digraph n G

 _shows_  _$\exists\,$_ es _$\mathord{.}$_ decTrail G w es  _$\wedge$_ length
es  _$=$_ n _$-$_ 1

###  4.6 Example Graph $K_{4}$

We return to the example graph from Figure 1 and show that our results from
Sections 4.2-4.5 can be used to prove existence of trails of length $k$, in
particular $k=3$ in $K_{4}$. Defining the graph and the weight function
separately, we use natural numbers as vertices.

_abbreviation_ ExampleGraph _$\mathord{:}$__$\mathord{:}$_ nat pair-pre-
digraph  _where_

ExampleGraph  _$\equiv$_  _$($__$\mid$_

pverts  _$=$_  _$\\{$_ 1 _$\mathord{,}$_ 2 _$\mathord{,}$_ 3
_$\mathord{,}$__$($_ 4 _$\mathord{:}$__$\mathord{:}$_ nat
_$)$__$\\}$__$\mathord{,}$_

parcs  _$=$_  _$\\{$__$($_ v _1_ _$\mathord{,}$_ v _2_ _$)$__$\mathord{.}$_ v
_1_  _$\in$_  _$\\{$_ 1 _$\mathord{,}$_ 2 _$\mathord{,}$_ 3
_$\mathord{,}$__$($_ 4 _$\mathord{:}$__$\mathord{:}$_ nat _$)$__$\\}$_
_$\wedge$_ v _2_  _$\in$_  _$\\{$_ 1 _$\mathord{,}$_ 2 _$\mathord{,}$_ 3
_$\mathord{,}$__$($_ 4 _$\mathord{:}$__$\mathord{:}$_ nat _$)$__$\\}$_
_$\wedge$_ v _1_  _$\not=$_ v _2_ _$\\}$_

_$\mid$__$)$_

_abbreviation_ ExampleGraphWeightFunction  _$\mathord{:}$__$\mathord{:}$_
_$($_ nat _$\times$_ nat _$)$_ weight-fun  _where_

ExampleGraphWeightFunction  _$\equiv$_  _$($__$\lambda$__$($_ v _1_
_$\mathord{,}$_ v _2_ _$)$__$\mathord{.}$_

 _$($_ if  _$($_ v _1_  _$=$_ 1  _$\wedge$_ v _2_  _$=$_ 2 _$)$_  _$\vee$_
_$($_ v _1_  _$=$_ 2  _$\wedge$_ v _2_  _$=$_ 1 _$)$_ then 1 else

 _$($_ if  _$($_ v _1_  _$=$_ 1  _$\wedge$_ v _2_  _$=$_ 3 _$)$_  _$\vee$_
_$($_ v _1_  _$=$_ 3  _$\wedge$_ v _2_  _$=$_ 1 _$)$_ then 3 else

 _$($_ if  _$($_ v _1_  _$=$_ 1  _$\wedge$_ v _2_  _$=$_ 4 _$)$_  _$\vee$_
_$($_ v _1_  _$=$_ 4  _$\wedge$_ v _2_  _$=$_ 1 _$)$_ then 6 else

 _$($_ if  _$($_ v _1_  _$=$_ 2  _$\wedge$_ v _2_  _$=$_ 3 _$)$_  _$\vee$_
_$($_ v _1_  _$=$_ 3  _$\wedge$_ v _2_  _$=$_ 2 _$)$_ then 5 else

 _$($_ if  _$($_ v _1_  _$=$_ 2  _$\wedge$_ v _2_  _$=$_ 4 _$)$_  _$\vee$_
_$($_ v _1_  _$=$_ 4  _$\wedge$_ v _2_  _$=$_ 2 _$)$_ then 4 else

 _$($_ if  _$($_ v _1_  _$=$_ 3  _$\wedge$_ v _2_  _$=$_ 4 _$)$_  _$\vee$_
_$($_ v _1_  _$=$_ 4  _$\wedge$_ v _2_  _$=$_ 3 _$)$_ then 2 else 0
_$)$__$)$__$)$__$)$__$)$__$)$__$)$_

We show that the graph $K_{4}$ of Figure 1 satisfies the conditions that were
imposed in _distinct -weighted-pair-graph_ and its parent locale, including
for example no self loops and distinctiveness. Of course there is still some
effort required for this. However, it is necessary to manually construct
trails or list all possible weight distributions. Additionally, instead of
$q!$ statements there are at most $\frac{3q}{2}$ statements needed.

_interpretation_ example _$\mathord{:}$_

distinct-weighted-pair-graph ExampleGraph ExampleGraphWeightFunction

Now it is an easy task to prove that there is a trail of length 3. We only add
the fact that _ExampleGraph_ is a _distinct -weighted-pair-graph_ and lemma
_dec -trail-exists_.

_lemma_ ExampleGraph-decTrail _$\mathord{:}$_

 _$\exists\,$_ xs _$\mathord{.}$_ decTrail ExampleGraph
ExampleGraphWeightFunction xs  _$\wedge$_ length xs  _$=$_ 3

##  5 Discussion and Related Work

Our theory _Ordered -Trail_ builds on top of the _Graph -Theory_ library
presented in [12]. However, this library does not formalize strictly ordered
trails, nor the special weighted graphs we introduced in the locale _distinct
_$-$_ weighted _$-$_ pair _$-$_ graph_. Furthermore, our formalization extends
[12] with definitions on strictly decreasing and increasing trails and
provides many basic lemmas on them. Some of the main challenges in this
context were the reasoning on the surjectivity of the weight function as well
the correctness proof of the algorithm.

Our formalization can be easily extended and could therefore serve as a basis
for further work in this field. The definitions _incTrail_ and _decTrail_ and
the respective properties that are proven in Section 4.2 are the key to many
other variants of trail properties.

Graham et al. [8] also showed upper bounds for trails in complete graphs by
decomposing them into either into cycles or 1-factors. We are currently
working on formalizing and certifying the result that

$f_{d}(n)=f_{i}(n)=\begin{cases}n&\text{if }n\in\\{3,5\\},\\\
n-1&\text{otherwise},\\\ \end{cases}$

that is, for complete graphs with $n=3$ or $n=5$ vertices there always has to
be a trail of length at least $n$ whereas for any other number $n$ of vertices
there only has to be a trail of length $n-1$. Therefore, the lower bound that
we showed in this paper is equal to the exact length with exception of two
special cases. We believe that formalizing this result would be a valuable
extension to the theory _Ordered -Trail_.

Another direction for further investigation are monotone paths. Graham et al.
[8] show that in a complete graph with $n$ vertices there has to be an
increasing path of length at least $\frac{1}{2}(\sqrt{4n-3}-1)$ and at most
$\frac{3n}{4}$. The upper bound was afterwards improved by Calderbank, Chung
and Sturtevant [3], Milans [10] and Bucić et al. [2].

Recently, other classes of graphs have been considered, e.g., trees and planar
graphs [13], on random edge-ordering [14] or on hypercubes [7].

##  6 Conclusion

In this work we formalized strictly increasing and strictly decreasing trails
in the proof assistant Isabelle/HOL. Furthermore, we showed correctness of an
algorithm to find such trails. We provided a verified algorithm and program to
compute monotone trails. We used this algorithm to prove the result that every
graph with $n$ vertices and $q$ edges has a strictly decreasing trail of
length at least $2\cdot\lfloor\frac{q}{n}\rfloor$. For further work we plan to
show that this is a tight bound for every $n$ except for $n=3$ and $5$.

Our results are built on the already existing Isabelle _Graph -theory_ from
the Archive of Formal Proofs. Thus, our results can be used by any theory
using graphs that are specified as in this library. Therefore, our theory is
highly reusable and might be the basis for further work in this field.

Acknowledgements. We thank Prof. Byron Cook (AWS) for interesting discussions
on reasoning challenges with ordered trails. This work was funded by the ERC
Starting Grant 2014 SYMCAR 639270, the ERC Proof of Concept Grant 2018 SYMELS
842066, the Wallenberg Academy Fellowship 2014 TheProSE, the Austrian FWF
research project W1255-N23 and P32441, the Vienna Science and Technology Fund
ICT19-065 and the Austrian-Hungarian collaborative project 101öu8.

## References

  * [1] Ballarin, C.: Tutorial to locales and locale interpretation. In: Contribuciones científicas en honor de Mirian Andrés Gómez. pp. 123–140. Universidad de La Rioja (2010)
  * [2] Bucic, M., Kwan, M., Pokrovskiy, A., Sudakov, B., Tran, T., Wagner, A.Z.: Nearly-linear monotone paths in edge-ordered graphs. arXiv preprint arXiv:1809.01468 (2018)
  * [3] Calderbank, A.R., Chung, F.R., Sturtevant, D.G.: Increasing sequences with nonzero block sums and increasing paths in edge-ordered graphs. Discrete Mathematics 50, 15–28 (1984)
  * [4] Chavtal, V., Komlos, J.: Some combinatorial theorems on monocity. In: Notices of the American Mathematical Society. vol. 17, p. 943. Amer Mathematical Soc 201 Charles St, Providence, RI 02940-2213 (1970)
  * [5] Cook, B., Kovács, L., Lachnitt, H.: Personal Communications on Automated Reasoning at AWS (2019)
  * [6] De Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–340. Springer (2008)
  * [7] De Silva, J., Molla, T., Pfender, F., Retter, T., Tait, M.: Increasing paths in edge-ordered graphs: the hypercube and random graphs. arXiv preprint arXiv:1502.03146 (2015)
  * [8] Graham, R., Kleitman, D.: Increasing paths in edge ordered graphs. Periodica Mathematica Hungarica 3(1-2), 141–148 (1973)
  * [9] Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Proc. of CAV. pp. 1–35 (2013)
  * [10] Milans, K.G.: Monotone paths in dense edge-ordered graphs (2015)
  * [11] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic, vol. 2283. Springer Science & Business Media (2002)
  * [12] Noschinski, L.: Graph theory. Archive of Formal Proofs (Apr 2013), http://isa-afp.org/entries/Graph_Theory.html, Formal proof development
  * [13] Roditty, Y., Shoham, B., Yuster, R.: Monotone paths in edge-ordered sparse graphs. Discrete Mathematics 226(1-3), 411–417 (2001)
  * [14] Yuster, R.: Large monotone paths in graphs with bounded degree. Graphs and Combinatorics 17(3), 579–587 (2001)