; Jared Davis <jared@cs.utexas.edu>
;
; 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<edgep>).

(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<edgep> 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<edgep> ?set))
  :list-guard ((all-list<edgep> ?list))
  :element-guard ((edgep a)))     

(SETS::map-function (to edge)
  :in-package-of edgep
  :set-guard ((all<edgep> ?set))
  :list-guard ((all-list<edgep> ?list))
  :element-guard ((edgep a)))


(defun vertices (g)
  (declare (xargs :guard (graphp g)))
  (SETS::union (map<from> g)
	       (map<to> 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<from> '( (a . b) (b . c) (c . d) )) ; => (a b c)
(map<to>   '( (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<to> (filter<from-matches> g vertex)))

(defun neighbors-backward (g vertex)
  (declare (xargs :guard (graphp g)))
  (map<from> (filter<to-matches> 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)))