; Jared Davis
;
; Here is a script demonstrating the use of quantification and mapping
; over sets in order to create some basic concepts from Graph Theory.
(in-package "ACL2")
(include-book "sets/map")
; We will represent a graph as a set of edges. Each edge consists of
;
; - a start vertex, from(e)
; - an end vertex, to(e)
;
; We will allow vertices to be any arbitrary objects.
(defun edgep (e)
(declare (xargs :guard t))
(consp e))
(defun from (e)
(declare (xargs :guard (edgep e)))
(car e))
(defun to (e)
(declare (xargs :guard (edgep e)))
(cdr e))
; We now introduce quantification functions for edgep. This allows us to ask
; if, e.g., every element in a set is an edgep (all).
(SETS::quantify-predicate (edgep x)
:in-package-of edgep)
; I'll go ahead and represent graphs as simple sets of edges.
(defun graphp (g)
(declare (xargs :guard t))
(and (SETS::setp g)
(all g)))
; We can construct a graph's vertex set from its edge set. To do so, we'll
; simply union the mappings of the "from" and "to" functions across the edge
; set.
(SETS::map-function (from edge)
:in-package-of edgep
:set-guard ((all ?set))
:list-guard ((all-list ?list))
:element-guard ((edgep a)))
(SETS::map-function (to edge)
:in-package-of edgep
:set-guard ((all ?set))
:list-guard ((all-list ?list))
:element-guard ((edgep a)))
(defun vertices (g)
(declare (xargs :guard (graphp g)))
(SETS::union (map g)
(map g)))
; Here are some examples, to get a feel for how these functions actually
; look. By the way, all of our quantification is done constructively, so
; we can execute these functions.
(graphp '( (a . b) (b . c) (c . d) )) ; => t
(map '( (a . b) (b . c) (c . d) )) ; => (a b c)
(map '( (a . b) (b . c) (c . d) )) ; => (b c d)
(vertices '( (a . b) (b . c) (c . d) )) ; => (a b c d)
; Now we'll introduce the notion of neighbors. We first introduce two
; predicates, which allow us to tell if (from edge) = vertex or if
; (to edge) = vertex for some vertex, v.
(defun from-matches (edge vertex)
(declare (xargs :guard t))
(and (edgep edge)
(equal (from edge) vertex)))
(defun to-matches (edge vertex)
(declare (xargs :guard t))
(and (edgep edge)
(equal (to edge) vertex)))
; We now quantify over these predicates. This allows us to consider
; the set of all edges which originate from a vertex, or which conclude
; at a vertex.
(SETS::quantify-predicate (from-matches edge vertex)
:in-package-of edgep)
(SETS::quantify-predicate (to-matches edge vertex)
:in-package-of edgep)
; Finally, we're ready to say what the neighbors of a vertex are. I'll
; say that the "forward neighbors" are the vertices that can be directly
; reached from this node. Similarly, the "backwards neighbors" are the
; vertices that can directly reach this node.
(defun neighbors-forward (g vertex)
(declare (xargs :guard (graphp g)))
(map (filter g vertex)))
(defun neighbors-backward (g vertex)
(declare (xargs :guard (graphp g)))
(map (filter g vertex)))
(defun neighbors (g vertex)
(declare (xargs :guard (graphp g)))
(SETS::union (neighbors-forward g vertex)
(neighbors-backward g vertex)))
; Here are a couple of examples.
(neighbors '((a . b) (b . c) (c . d)) 'a) ; => (b)
(neighbors '((a . b) (b . c) (c . d)) 'b) ; => (a c)
; Here's a neat theorem, we want to show that the neighbors are always
; a subset of the vertex set. This doesn't require any human thought,
; and is an excellent, deep proof done automatically for us! The theorem
; prover uses a pick-a-point argument to prove the subset, then uses
; reasoning about the inverses of map-from and map-to finish the proof.
(defthm neighbors-are-vertices
(SETS::subset (neighbors g vertex)
(vertices g)))
(defthm neighbors-forward-are-vertices ; this is just fluff
(SETS::subset (neighbors-forward g vertex)
(vertices g)))
(defthm neighbors-backward-are-vertices ; this is just fluff
(SETS::subset (neighbors-backward g vertex)
(vertices g)))