dijkstra-shortest-path

(in-package "ACL2")

(defun del
  (x y)
  (if (endp y)
    nil
    (if (equal x (car y))
      (cdr y)
      (cons (car y) (del x (cdr y))))))

(defun memp
  (e x)
  (if (endp x)
    nil
    (or (equal e (car x)) (memp e (cdr x)))))

(defun setp
  (s)
  (cond ((endp s) t)
    ((memp (car s) (cdr s)) nil)
    (t (setp (cdr s)))))

(defun my-union
  (s1 s2)
  (cond ((endp s1) s2)
    ((memp (car s1) s2) (my-union (cdr s1) s2))
    (t (cons (car s1) (my-union (cdr s1) s2)))))

(defun my-subsetp
  (s1 s2)
  (cond ((endp s1) t)
    (t (and (memp (car s1) s2) (my-subsetp (cdr s1) s2)))))

(defun infinitep (x) (null x))

(defun lt
  (x y)
  (cond ((infinitep x) nil) ((infinitep y) t) (t (< x y))))

(defun plus
  (x y)
  (cond ((or (infinitep x) (infinitep y)) nil) (t (+ x y))))

(defun edge-listp
  (lst)
  (cond ((endp lst) (equal lst nil))
    ((and (consp (car lst))
       (rationalp (cdar lst))
       (<= 0 (cdar lst))
       (not (assoc (caar lst) (cdr lst)))) (edge-listp (cdr lst)))
    (t nil)))

(defun graphp
  (g)
  (cond ((endp g) (equal g nil))
    ((and (consp (car g)) (edge-listp (cdar g))) (graphp (cdr g)))
    (t nil)))

(defun cons-set
  (e s)
  (if (memp e s)
    s
    (cons e s)))

(defun all-nodes
  (g)
  (cond ((endp g) nil)
    (t (cons-set (caar g)
        (my-union (strip-cars (cdar g)) (all-nodes (cdr g)))))))

(defun nodep (n g) (memp n (all-nodes g)))

(defun neighbors (n g) (strip-cars (cdr (assoc n g))))

(defun pathp-aux
  (path g)
  (cond ((endp path) nil)
    ((endp (cdr path)) (nodep (car path) g))
    (t (and (memp (cadr path) (neighbors (car path) g))
        (pathp-aux (cdr path) g)))))

(defun pathp
  (path g)
  (and (true-listp path) (pathp-aux path g)))

(defun edge-len (a b g) (cdr (assoc b (cdr (assoc a g)))))

(defun path-len
  (path g)
  (cond ((endp path) nil)
    ((endp (cdr path)) (if (nodep (car path) g)
        0
        nil))
    (t (plus (edge-len (car path) (cadr path) g)
        (path-len (cdr path) g)))))

(defun path (n pt) (cdr (assoc n pt)))

(defun d (n pt g) (path-len (path n pt) g))

(defun choose-next
  (ts pt g)
  (cond ((endp ts) '(non-node))
    ((endp (cdr ts)) (car ts))
    ((lt (d (car ts) pt g) (d (choose-next (cdr ts) pt g) pt g)) (car ts))
    (t (choose-next (cdr ts) pt g))))

(defun reassign
  (u v-lst pt g)
  (cond ((endp v-lst) pt)
    (t (let* ((v (car v-lst)) (w (edge-len u v g)))
        (cond ((lt (plus (d u pt g) w) (d v pt g)) (cons (cons v (append (path u pt) (list v)))
              (reassign u (cdr v-lst) pt g)))
          (t (reassign u (cdr v-lst) pt g)))))))

(defun dsp
  (ts pt g)
  (cond ((endp ts) pt)
    (t (let ((u (choose-next ts pt g)))
        (dsp (del u ts) (reassign u (neighbors u g) pt g) g)))))

(defun dijkstra-shortest-path
  (a b g)
  (let ((p (dsp (all-nodes g) (list (cons a (list a))) g)))
    (path b p)))

(defun pathp-from-to
  (p a b g)
  (and (pathp p g) (equal (car p) a) (equal (car (last p)) b)))

(defthm pathp-from-to-corollary
  (implies (pathp-from-to p a b g)
    (and (pathp p g) (equal (car p) a) (equal (car (last p)) b))))

(defun pt-propertyp
  (a pt g)
  (if (endp pt)
    t
    (and (or (null (cdar pt))
        (pathp-from-to (cdar pt) a (caar pt) g))
      (pt-propertyp a (cdr pt) g))))

(defthm pathp-from-to-path-1
  (implies (and (pt-propertyp a pt g) (path u pt))
    (pathp-from-to (path u pt) a u g))
  :rule-classes :forward-chaining)

(defthm pathp-from-to-path-2
  (implies (and (pt-propertyp a pt g) (path u pt))
    (pathp-from-to (path u pt) a u g)))

(defun lte (n1 n2) (not (lt n2 n1)))

(defun shorterp
  (p1 p2 g)
  (lte (path-len p1 g) (path-len p2 g)))

(defun confinedp
  (p fs)
  (if (endp p)
    t
    (if (endp (cdr p))
      t
      (and (memp (car p) fs) (confinedp (cdr p) fs)))))

(defun-sk shortest-confined-pathp
  (a b p fs g)
  (forall path
    (implies (and (pathp-from-to path a b g) (confinedp path fs))
      (shorterp p path g))))

(defun-sk shortest-pathp
  (a b p g)
  (forall path
    (implies (pathp-from-to path a b g) (shorterp p path g))))

(defun ts-propertyp
  (a ts fs pt g)
  (if (endp ts)
    t
    (and (shortest-confined-pathp a (car ts) (path (car ts) pt) fs g)
      (confinedp (path (car ts) pt) fs)
      (ts-propertyp a (cdr ts) fs pt g))))

(defun fs-propertyp
  (a fs fs0 pt g)
  (if (endp fs)
    t
    (and (shortest-pathp a (car fs) (path (car fs) pt) g)
      (confinedp (path (car fs) pt) fs0)
      (fs-propertyp a (cdr fs) fs0 pt g))))

(defun comp-set
  (ts s)
  (if (endp s)
    nil
    (if (memp (car s) ts)
      (comp-set ts (cdr s))
      (cons (car s) (comp-set ts (cdr s))))))

(defun invp
  (ts pt g a)
  (let ((fs (comp-set ts (all-nodes g))))
    (and (ts-propertyp a ts fs pt g)
      (fs-propertyp a fs fs pt g)
      (pt-propertyp a pt g))))

(defthm prop-path-nil
  (ts-propertyp a s nil (list (cons a (list a))) g))

(defthm comp-set-subset
  (implies (my-subsetp s1 s2) (not (comp-set s2 s1))))

(defthm subsetp-cons
  (implies (my-subsetp x y) (my-subsetp x (cons e y))))

(defthm subsetp-x-x (my-subsetp x x))

(defthm comp-set-id (equal (comp-set s s) nil))

(defthm invp-0
  (implies (nodep a g)
    (invp (all-nodes g) (list (cons a (list a))) g a)))

(defthm subset-union
  (implies (or (my-subsetp s1 s2) (my-subsetp s1 s3))
    (my-subsetp s1 (my-union s2 s3))))

(defthm memp-subset-memp-temp
  (implies (and (memp a s) (my-subsetp s r)) (memp a r)))

(defthm neighbor-implies-nodep
  (implies (memp v (neighbors u g)) (memp v (all-nodes g))))

(defthm paths-table-reassign-lemma2
  (implies (and (pathp p g) (memp v (neighbors (car (last p)) g)))
    (pathp (append p (list v)) g))
  :hints (("Goal" :in-theory (disable neighbors))))

(defthm car-append
  (implies (and (true-listp p) p)
    (equal (car (append p lst)) (car p))))

(defthm last-append
  (equal (car (last (append p (list v)))) v))

(defthm paths-table-reassign-lemma4
  (implies (and (pt-propertyp a pt g)
      (path u pt)
      (graphp g)
      (memp v (neighbors u g)))
    (pathp-from-to (append (path u pt) (list v)) a v g))
  :hints (("Goal" :in-theory (disable neighbors))))

(defthm path-len-implies-not-nil
  (implies (path-len (path u pt) g) (path u pt)))

(defthm edge-len-implies-neighbors
  (implies (edge-len u v g) (memp v (neighbors u g))))

(defthm pt-propertyp-reassign
  (implies (and (pt-propertyp a pt g)
      (graphp g)
      (my-subsetp v-lst (all-nodes g)))
    (pt-propertyp a (reassign u v-lst pt g) g))
  :hints (("Goal" :in-theory (disable path edge-len neighbors))))

(defthm shortest-pathp-corollary
  (implies (and (shortest-pathp a b p g) (pathp-from-to path a b g))
    (shorterp p path g))
  :hints (("Goal" :use shortest-pathp-necc)))

(defthm shortest-implies-unchanged-lemma1
  (equal (path v (cons (cons u path) pt))
    (if (equal v u)
      path
      (path v pt))))

(defthm memp-implies-memp-union-1
  (implies (memp u s1) (memp u (my-union s1 s2))))

(defthm memp-implies-memp-union-2
  (implies (memp u s2) (memp u (my-union s1 s2))))

(defthm not-memp-edge-len-lemma
  (implies (assoc v alst) (memp v (strip-cars alst))))

(defthm not-memp-edge-len
  (implies (not (memp v (all-nodes g)))
    (not (edge-len a v g))))

(defthm path-len-append
  (implies (pathp p g)
    (equal (path-len (append p (list v)) g)
      (plus (path-len p g) (edge-len (car (last p)) v g))))
  :hints (("Goal" :in-theory (disable neighbors edge-len))))

(defthm pathp-implies-true-listp
  (implies (pathp p g) (true-listp p)))

(defthm shortest-implies-unchanged
  (implies (and (shortest-pathp a v (path v pt) g)
      (pt-propertyp a pt g)
      (graphp g)
      (nodep v g))
    (equal (path v (reassign u v-lst pt g)) (path v pt)))
  :hints (("Goal" :in-theory (disable path edge-len neighbors pathp shortest-pathp)) ("Subgoal *1/2" :use ((:instance path-len-implies-not-nil) (:instance pathp-from-to-corollary (p (path u pt)) (b u))
        (:instance shortest-pathp-corollary
          (path (append (path u pt) (list v)))
          (b v)
          (p (path v pt)))))))

(defthm fs-propertyp-memp
  (implies (and (fs-propertyp a fs s pt g) (memp v fs))
    (and (shortest-pathp a v (path v pt) g)
      (confinedp (path v pt) s))))

(defthm fs-propertyp-memp-lemma
  (implies (and (my-subsetp fs (all-nodes g))
      (fs-propertyp a fs s pt g)
      (pt-propertyp a pt g)
      (graphp g)
      (memp v fs))
    (equal (path v (reassign u (neighbors u g) pt g))
      (path v pt)))
  :hints (("Goal" :in-theory (disable neighbors path shortest-pathp))))

(defthm fs-propertyp-choose-next-lemma1
  (implies (and (fs-propertyp a fs s pt g)
      (pt-propertyp a pt g)
      (graphp g)
      (my-subsetp fs (all-nodes g)))
    (fs-propertyp a fs s (reassign u (neighbors u g) pt g) g))
  :hints (("Goal" :in-theory (disable neighbors path shortest-pathp))))

(defthm fs-propertyp-choose-lemma2
  (implies (and (fs-propertyp a fs s pt g)
      (my-subsetp fs (all-nodes g))
      (confinedp (path u pt) s)
      (pt-propertyp a pt g)
      (nodep u g)
      (graphp g)
      (shortest-pathp a u (path u pt) g))
    (fs-propertyp a
      (cons u fs)
      s
      (reassign u (neighbors u g) pt g)
      g))
  :hints (("Goal" :in-theory (disable path neighbors))))

(defthm fs-propertyp-choose-lemma3
  (implies (and (my-subsetp s fs)
      (my-subsetp fs (all-nodes g))
      (pt-propertyp a pt g)
      (fs-propertyp a fs ss pt g))
    (fs-propertyp a s ss pt g))
  :hints (("Goal" :in-theory (disable shortest-pathp path))))

(defthm fs-propertyp-choose-lemma4-lemma
  (implies (and (my-subsetp s ss) (confinedp p s))
    (confinedp p ss)))

(defthm fs-propertyp-choose-lemma4
  (implies (and (my-subsetp s ss) (fs-propertyp a fs s pt g))
    (fs-propertyp a fs ss pt g)))

(defun find-partial-path
  (p s)
  (if (endp p)
    nil
    (if (memp (car p) s)
      (cons (car p) (find-partial-path (cdr p) s))
      (list (car p)))))

(defthm edge-listp-values-positive
  (implies (and (edge-listp a) (cdr (assoc-equal b a)))
    (<= 0 (cdr (assoc-equal b a))))
  :rule-classes :linear)

(defthm graph-weight-nonneg
  (implies (and (graphp g) (edge-len a b g))
    (<= 0 (edge-len a b g)))
  :rule-classes :linear)

(defthm graph-path-weight-nonneg
  (implies (and (graphp g) (path-len p g))
    (<= 0 (path-len p g)))
  :rule-classes :linear :hints (("Goal" :in-theory (disable edge-len))))

(defthm edge-len-implies-nodep
  (implies (edge-len a b g) (memp a (all-nodes g))))

(defthm partial-path-shorterp
  (implies (graphp g) (shorterp (find-partial-path p s) p g))
  :hints (("Goal" :induct (find-partial-path p s)
     :in-theory (disable edge-len))))

(defthm notnodep-necc
  (implies (not (nodep a g)) (not (neighbors a g))))

(defthm pathp-implies-car-nodep
  (implies (pathp p g) (memp (car p) (all-nodes g))))

(defthm pathp-partial-path
  (implies (pathp p g)
    (and (pathp-from-to (find-partial-path p s)
        (car p)
        (car (last (find-partial-path p s)))
        g)
      (confinedp (find-partial-path p s) s))))

(defthm shorterp-trans
  (implies (and (shorterp p1 p2 g) (shorterp p2 p3 g))
    (shorterp p1 p3 g)))

(defthm shorterp-by-partial-trans
  (implies (and (shorterp p (find-partial-path path s) g) (graphp g))
    (shorterp p path g))
  :hints (("Goal" :in-theory (disable shorterp))))

(defthm ts-propertyp-prop-lemma1
  (implies (and (ts-propertyp a ts fs pt g) (memp v ts))
    (and (shortest-confined-pathp a v (path v pt) fs g)
      (confinedp (path v pt) fs)))
  :rule-classes ((:rewrite) (:forward-chaining)))

(defthm ts-propertyp-prop-lemma2
  (implies (and (pathp-from-to path a b g)
      (shortest-confined-pathp a b p fs g)
      (confinedp path fs))
    (shorterp p path g))
  :hints (("Goal" :use shortest-confined-pathp-necc)))

(defthm ts-propertyp-prop
  (implies (and (ts-propertyp a ts fs pt g)
      (confinedp path fs)
      (pathp-from-to path a v g)
      (memp v ts))
    (and (shorterp (path v pt) path g)
      (confinedp (path v pt) fs)))
  :hints (("Goal" :in-theory (disable path shorterp pathp-from-to))))

(defthm shorterp-by-partial-and-choose-next
  (implies (and (shorterp (path u pt) (path v pt) g)
      (memp v ts)
      (ts-propertyp a ts (comp-set ts (all-nodes g)) pt g)
      (pathp-from-to path a v g)
      (confinedp path (comp-set ts (all-nodes g))))
    (shorterp (path u pt) path g))
  :hints (("Goal" :in-theory (disable path shorterp))))

(defthm choose-next-shorterp-other
  (implies (memp v ts)
    (shorterp (path (choose-next ts pt g) pt) (path v pt) g)))

(defthm not-comp-set-id
  (implies (memp v all)
    (iff (memp v (comp-set ts all)) (not (memp v ts)))))

(defthm find-partial-path-last-memp
  (implies (and (memp (car (last p)) ts)
      (pathp p g)
      (my-subsetp ts (all-nodes g)))
    (memp (car (last (find-partial-path p (comp-set ts (all-nodes g)))))
      ts)))

(defthm choose-next-shortest-lemma
  (implies (consp ts) (memp (choose-next ts pt g) ts)))

(defthm choose-next-shortest
  (implies (and (graphp g)
      (consp ts)
      (my-subsetp ts (all-nodes g))
      (invp ts pt g a))
    (shortest-pathp a
      (choose-next ts pt g)
      (path (choose-next ts pt g) pt)
      g))
  :hints (("Goal" :in-theory (disable shorterp path pathp)
     :use ((:instance pathp-partial-path
        (p (shortest-pathp-witness a
            (choose-next ts pt g)
            (path (choose-next ts pt g) pt)
            g))
        (s (comp-set ts (all-nodes g)))) (:instance shorterp-by-partial-and-choose-next
         (u (choose-next ts pt g))
         (path (find-partial-path (shortest-pathp-witness a
               (choose-next ts pt g)
               (path (choose-next ts pt g) pt)
               g)
             (comp-set ts (all-nodes g))))
         (v (car (last (find-partial-path (shortest-pathp-witness a
                   (choose-next ts pt g)
                   (path (choose-next ts pt g) pt)
                   g)
                 (comp-set ts (all-nodes g)))))))))))

(defthm choose-next-confinedp
  (implies (and (invp ts pt g a)
      (consp ts)
      (my-subsetp ts (all-nodes g)))
    (confinedp (path (choose-next ts pt g) pt)
      (comp-set ts (all-nodes g))))
  :hints (("Goal" :in-theory (disable path))))

(defthm subsetp-comp-set-all
  (my-subsetp (comp-set ts all) all))

(defthm subsetp-del (my-subsetp (del u ts) ts))

(defthm cons-subsetp-comp-set-del-lemma
  (my-subsetp (comp-set ts all) (comp-set (del u ts) all)))

(defthm subsetp-comp-set-del-lemma1
  (implies (my-subsetp s1 (cons v s2))
    (my-subsetp s1 (list* v u s2))))

(defthm subsetp-comp-set-del-lemma2
  (implies (and (memp v ts) (not (equal v u)))
    (memp v (del u ts))))

(defthm subsetp-comp-set-del
  (implies (and (setp ts) (setp all))
    (my-subsetp (comp-set (del u ts) all)
      (cons u (comp-set ts all)))))

(defthm edge-listp-prop
  (implies (and (edge-listp lst) (not (assoc u lst)))
    (not (memp u (strip-cars lst)))))

(defthm edge-listp-implies-setp
  (implies (edge-listp lst) (setp (strip-cars lst))))

(defthm not-memp-union
  (implies (and (not (memp u s1)) (not (memp u s2)))
    (not (memp u (my-union s1 s2)))))

(defthm setp-union
  (implies (and (setp s1) (setp s2)) (setp (my-union s1 s2))))

(defthm setp-all-nodes
  (implies (graphp g) (setp (all-nodes g))))

(defthm memp-subset-memp
  (implies (and (my-subsetp s r) (memp a s)) (memp a r)))

(defthm neighbors-subsetp-all-nodes
  (my-subsetp (neighbors u g) (all-nodes g)))

(defthm fs-propertyp-choose
  (implies (and (invp ts pt g a)
      (my-subsetp ts (all-nodes g))
      (graphp g)
      (consp ts)
      (setp ts))
    (let ((u (choose-next ts pt g)))
      (fs-propertyp a
        (comp-set (del u ts) (all-nodes g))
        (comp-set (del u ts) (all-nodes g))
        (reassign u (neighbors u g) pt g)
        g)))
  :hints (("Goal" :in-theory (disable fs-propertyp-choose-lemma3
       fs-propertyp-choose-lemma4
       path
       neighbors
       shortest-pathp
       fs-propertyp)
     :use ((:instance fs-propertyp-choose-lemma4
        (fs (comp-set (del (choose-next ts pt g) ts) (all-nodes g)))
        (s (comp-set ts (all-nodes g)))
        (ss (comp-set (del (choose-next ts pt g) ts) (all-nodes g)))
        (pt (reassign (choose-next ts pt g)
            (neighbors (choose-next ts pt g) g)
            pt
            g))) (:instance fs-propertyp-choose-lemma3
         (s (comp-set (del (choose-next ts pt g) ts) (all-nodes g)))
         (fs (cons (choose-next ts pt g) (comp-set ts (all-nodes g))))
         (ss (comp-set ts (all-nodes g)))
         (pt (reassign (choose-next ts pt g)
             (neighbors (choose-next ts pt g) g)
             pt
             g)))))))

(defthm neighbor-implies-edge-len
  (implies (and (graphp g) (memp v (neighbors u g)))
    (edge-len u v g)))

(defthm pathp-implies-path-len
  (implies (and (graphp g) (pathp p g)) (path-len p g))
  :hints (("Goal" :in-theory (disable neighbors edge-len))))

(defthm path-pt-iff-path-len
  (implies (and (graphp g) (pt-propertyp a pt g))
    (iff (path u pt) (path-len (path u pt) g))))

(defthm reassign-path
  (implies (not (memp v v-lst))
    (equal (path v (reassign u v-lst pt g)) (path v pt))))

(defthm shorterp-reassign-append
  (implies (and (pt-propertyp a pt g)
      (graphp g)
      (path u pt)
      (memp v v-lst))
    (shorterp (path v (reassign u v-lst pt g))
      (append (path u pt) (list v))
      g))
  :hints (("Goal" :in-theory (disable edge-len path pathp-from-to-path-1)) ("Subgoal *1/3" :use ((:instance pathp-from-to-corollary (p (path u pt)) (b u))))))

(defun find-last-next-path
  (p)
  (if (or (endp p) (endp (cdr p)))
    nil
    (cons (car p) (find-last-next-path (cdr p)))))

(defun last-node (p) (car (last (find-last-next-path p))))

(defthm shorterp-reassign-lemma
  (implies (and (path-len (path u pt) g) (pt-propertyp a pt g))
    (and (pathp (path u pt) g)
      (equal (car (path u pt)) a)
      (equal (car (last (path u pt))) u))))

(defthm shorterp-reassign
  (implies (pt-propertyp a pt g)
    (shorterp (path v (reassign u v-lst pt g)) (path v pt) g))
  :hints (("Goal" :in-theory (disable path edge-len neighbors))))

(defthm true-listp-path
  (implies (pt-propertyp a pt g) (true-listp (path u pt))))

(defthm pathp-from-to-append
  (implies (and (pt-propertyp a pt g)
      (path w pt)
      (memp v (neighbors w g)))
    (pathp-from-to (append (path w pt) (list v)) a v g))
  :hints (("Goal" :in-theory (disable neighbors path))))

(defthm confinedp-append
  (implies (and (confinedp p s) (memp (car (last p)) s))
    (confinedp (append p (list v)) s)))

(defthm shorterp-than-append-fs
  (implies (and (shortest-confined-pathp a v (path v pt) s g)
      (fs-propertyp a fs s pt g)
      (my-subsetp fs s)
      (path w pt)
      (pt-propertyp a pt g)
      (memp w fs))
    (shorterp (path v pt) (append (path w pt) (list v)) g))
  :rule-classes nil
  :hints (("Goal" :use ((:instance ts-propertyp-prop-lemma2
        (b v)
        (p (path v pt))
        (fs s)
        (path (append (path w pt) (list v)))))
     :in-theory (disable path shortest-confined-pathp pathp))))

(defthm path-length
  (implies (and (pathp p g) (not (equal (car p) (car (last p)))))
    (<= 2 (len p)))
  :rule-classes :linear)

(defthm pathp-find-last-next
  (implies (and (pathp p g) (<= 2 (len p)))
    (and (pathp (find-last-next-path p) g)
      (memp (car (last p))
        (neighbors (car (last (find-last-next-path p))) g))))
  :hints (("Goal" :in-theory (disable neighbors))))

(defthm find-last-implies-all-in
  (implies (and (find-last-next-path p) (confinedp p fs))
    (memp (car (last (find-last-next-path p))) fs)))

(defthm pathp-from-to-implies-all-path
  (implies (and (pathp-from-to p a v g)
      (not (equal a v))
      (confinedp p fs))
    (and (memp v (neighbors (last-node p) g))
      (pathp-from-to (find-last-next-path p) a (last-node p) g)
      (memp (last-node p) fs)))
  :hints (("Goal" :in-theory (disable pathp neighbors))))

(defthm path-len-implies-pathp
  (implies (and (path-len p g) (true-listp p)) (pathp p g))
  :hints (("Goal" :in-theory (disable edge-len neighbors))))

(defthm shorterp-and-pathp-implies-pathp
  (implies (and (graphp g)
      (shorterp p1 p2 g)
      (true-listp p1)
      (pathp p2 g))
    (pathp p1 g))
  :rule-classes nil
  :hints (("Goal" :in-theory (disable pathp))))

(defthm shorterp-implies-append-shorterp
  (implies (and (shorterp p1 p2 g)
      (graphp g)
      (true-listp p1)
      (equal (car (last p1)) (car (last p2)))
      (pathp p2 g))
    (shorterp (append p1 (list v)) (append p2 (list v)) g))
  :hints (("Goal" :use shorterp-and-pathp-implies-pathp)))

(defthm path-pt-implies-path-last-node
  (implies (and (pt-propertyp a pt g) (pathp (path u pt) g))
    (equal (car (last (path u pt))) u)))

(defthm last-node-lemma1
  (implies (and (graphp g)
      (pt-propertyp a pt g)
      (pathp-from-to p a v g)
      (not (equal a v))
      (shortest-pathp a (last-node p) (path (last-node p) pt) g))
    (shorterp (append (path (last-node p) pt) (list v))
      (append (find-last-next-path p) (list v))
      g))
  :hints (("Goal" :in-theory (disable shortest-pathp shorterp path pathp)
     :use ((:instance shorterp-and-pathp-implies-pathp
        (p1 (path (car (last (find-last-next-path p))) pt))
        (p2 (find-last-next-path p))) (:instance shortest-pathp-corollary
         (b (car (last (find-last-next-path p))))
         (p (path (car (last (find-last-next-path p))) pt))
         (path (find-last-next-path p)))))))

(defthm last-node-lemma2
  (implies (and (equal (car (last p)) v) (pathp p g))
    (equal (append (find-last-next-path p) (list v)) p)))

(defthm last-node-lemma
  (implies (and (graphp g)
      (pt-propertyp a pt g)
      (pathp-from-to p a v g)
      (not (equal a v))
      (shortest-pathp a (last-node p) (path (last-node p) pt) g))
    (shorterp (append (path (last-node p) pt) (list v)) p g))
  :hints (("Goal" :use ((:instance last-node-lemma1) (:instance last-node-lemma2))
     :in-theory (disable shorterp))))

(defthm memp-not-car-implies-memp
  (implies (and (memp v (cons u fs)) (not (equal v u)))
    (memp v fs)))

(defthm fs-propertyp-implies-pathp
  (implies (and (graphp g)
      (fs-propertyp a fs s pt g)
      (memp w fs)
      (pathp-from-to p2 a w g))
    (path w pt))
  :hints (("Goal" :in-theory (disable path
       fs-propertyp-memp
       shortest-pathp
       pathp-from-to)
     :use ((:instance shortest-pathp-corollary
        (b w)
        (p (path w pt))
        (path p2)) (:instance fs-propertyp-memp (v w)))))
  :rule-classes nil)

(defthm ts-propertyp-lemma2-1
  (implies (and (shortest-confined-pathp a v (path v pt) fs g)
      (graphp g)
      (fs-propertyp a fs fs pt g)
      (pathp-from-to p a v g)
      (not (equal a v))
      (path u pt)
      (shortest-pathp a u (path u pt) g)
      (confinedp p (cons u fs))
      (pt-propertyp a pt g))
    (shorterp (path v (reassign u (neighbors u g) pt g)) p g))
  :hints (("Goal" :cases ((equal (last-node p) u))) ("Subgoal 2" :in-theory (disable path
        neighbors
        shortest-confined-pathp
        shorterp
        shortest-pathp
        memp-not-car-implies-memp
        fs-propertyp-memp
        pathp-from-to
        last-node)
      :use ((:instance shorterp-trans
         (p1 (path v (reassign u (neighbors u g) pt g)))
         (p2 (path v pt))
         (p3 (append (path (last-node p) pt) (list v)))) (:instance shorterp-trans
          (p1 (path v (reassign u (neighbors u g) pt g)))
          (p2 (append (path (last-node p) pt) (list v)))
          (p3 p))
        (:instance fs-propertyp-memp (s fs) (v (last-node p)))
        (:instance memp-not-car-implies-memp (v (last-node p)))
        (:instance fs-propertyp-implies-pathp
          (s fs)
          (w (last-node p))
          (p2 (find-last-next-path p)))
        (:instance shorterp-than-append-fs (s fs) (w (last-node p)))))
    ("Subgoal 1" :in-theory (disable path
        neighbors
        shortest-confined-pathp
        last-node
        shorterp
        shortest-pathp
        pathp-from-to)
      :use ((:instance shorterp-trans
         (p1 (path v (reassign u (neighbors u g) pt g)))
         (p2 (append (path u pt) (list v)))
         (p3 p))))))

(defun find-partial-path-to-u
  (p u)
  (cond ((not (memp u p)) nil)
    ((equal (car p) u) (list u))
    (t (cons (car p) (find-partial-path-to-u (cdr p) u)))))

(defthm pathp-implies-path-to-u-pathp
  (implies (and (memp u p) (pathp p g))
    (pathp-from-to (find-partial-path-to-u p u) (car p) u g)))

(defthm not-memp-implies-confinedp
  (implies (and (confinedp p (cons u fs)) (not (memp u p)))
    (confinedp p fs)))

(defthm nil-shorterp-than-nil
  (implies (and (shorterp p1 p2 g) (graphp g) (not p1))
    (not (pathp p2 g))))

(defthm shortest-pathp-nil-implies-lemma
  (implies (and (shortest-pathp a u p1 g)
      (not p1)
      (graphp g)
      (equal (car p2) a)
      (pathp p2 g))
    (not (memp u p2)))
  :hints (("Goal" :in-theory (disable pathp
       shorterp
       shortest-pathp
       pathp-implies-path-to-u-pathp)
     :use ((:instance pathp-implies-path-to-u-pathp (p p2)) (:instance nil-shorterp-than-nil
         (p2 (find-partial-path-to-u p2 u)))))))

(defthm ts-propertyp-lemma2-2
  (implies (and (shortest-confined-pathp a v (path v pt) fs g)
      (graphp g)
      (fs-propertyp a fs fs pt g)
      (pathp-from-to p a v g)
      (not (equal a v))
      (shortest-pathp a u (path u pt) g)
      (confinedp p (cons u fs))
      (pt-propertyp a pt g))
    (shorterp (path v (reassign u (neighbors u g) pt g)) p g))
  :rule-classes nil
  :hints (("Goal" :cases ((path u pt))) ("Subgoal 2" :in-theory (disable neighbors
        path
        pathp
        pathp-from-to
        path-pt-iff-path-len
        shortest-pathp
        shorterp
        shortest-confined-pathp)
      :use ((:instance shorterp-trans
         (p1 (path v (reassign u (neighbors u g) pt g)))
         (p2 (path v pt))
         (p3 p)) (:instance ts-propertyp-prop-lemma2
          (b v)
          (p (path v pt))
          (path p))))
    ("Subgoal 1" :use ts-propertyp-lemma2-1)))

(defthm shortest-pathp-list-a
  (implies (graphp g) (shortest-pathp a a (list a) g)))

(defthm path-a-pt
  (implies (and (pt-propertyp a pt g)
      (graphp g)
      (nodep a g)
      (equal (path a pt) (list a)))
    (equal (path a (reassign u v-lst pt g)) (path a pt)))
  :hints (("Goal" :use ((:instance shortest-implies-unchanged (v a))))))

(defthm ts-propertyp-lemma2-3
  (implies (and (shortest-confined-pathp a v (path v pt) fs g)
      (graphp g)
      (fs-propertyp a fs fs pt g)
      (nodep a g)
      (pathp-from-to p a v g)
      (confinedp p (cons u fs))
      (shortest-pathp a u (path u pt) g)
      (pt-propertyp a pt g)
      (equal (path a pt) (list a)))
    (shorterp (path v (reassign u (neighbors u g) pt g)) p g))
  :rule-classes nil
  :hints (("Goal" :cases ((equal a v))) ("Subgoal 2" :use ts-propertyp-lemma2-2)
    ("Subgoal 1" :in-theory (disable path
        neighbors
        pathp
        shortest-pathp
        shortest-confined-pathp))))

(defthm ts-propertyp-lemma2
  (implies (and (shortest-confined-pathp a v (path v pt) fs g)
      (graphp g)
      (nodep a g)
      (equal (path a pt) (list a))
      (fs-propertyp a fs fs pt g)
      (shortest-pathp a u (path u pt) g)
      (pt-propertyp a pt g))
    (shortest-confined-pathp a
      v
      (path v (reassign u (neighbors u g) pt g))
      (cons u fs)
      g))
  :hints (("Goal" :in-theory (disable reassign
       path
       neighbors
       shortest-pathp
       shortest-confined-pathp)
     :expand ((shortest-confined-pathp a
        v
        (path v (reassign u (neighbors u g) pt g))
        (cons u fs)
        g))
     :use ((:instance ts-propertyp-lemma2-3
        (p (shortest-confined-pathp-witness a
            v
            (path v (reassign u (neighbors u g) pt g))
            (cons u fs)
            g)))))))

(defthm ts-propertyp-lemma3-1
  (implies (confinedp p fs) (confinedp p (cons u fs))))

(defthm ts-propertyp-lemma3-2
  (implies (and (pt-propertyp a pt g) (confinedp (path u pt) fs))
    (confinedp (append (path u pt) (list v)) (cons u fs))))

(defthm ts-propertyp-lemma3-3
  (implies (and (pt-propertyp a pt g)
      (confinedp (path v pt) fs)
      (confinedp (path u pt) fs))
    (confinedp (path v (reassign u v-lst pt g)) (cons u fs)))
  :hints (("Goal" :in-theory (disable path))))

(defthm ts-propertyp-prop-lemma
  (implies (and (ts-propertyp a ts fs pt g) (memp u ts))
    (confinedp (path u pt) fs)))

(defthm ts-propertyp-lemma3
  (implies (and (pt-propertyp a pt g)
      (graphp g)
      (nodep a g)
      (equal (path a pt) (list a))
      (fs-propertyp a fs fs pt g)
      (ts-propertyp a ts fs pt g)
      (memp u ts)
      (shortest-pathp a u (path u pt) g))
    (ts-propertyp a
      (del u ts)
      (cons u fs)
      (reassign u (neighbors u g) pt g)
      g))
  :hints (("Goal" :in-theory (disable path
       neighbors
       nodep
       shortest-pathp
       shortest-confined-pathp)) ("Subgoal *1/2'''" :induct (ts-propertyp a
        ts2
        (cons ts1 fs)
        (reassign ts1 (neighbors ts1 g) pt g)
        g))))

(defthm shortest-confined-pathp-subset
  (implies (and (shortest-confined-pathp a u p fs g) (my-subsetp s fs))
    (shortest-confined-pathp a u p s g))
  :hints (("Goal" :in-theory (disable shortest-confined-pathp shorterp)
     :expand ((shortest-confined-pathp a u p s g))
     :use ((:instance ts-propertyp-prop-lemma2
        (b u)
        (path (shortest-confined-pathp-witness a u p s g)))))))

(defthm ts-propertyp-lemma1
  (implies (and (my-subsetp s fs)
      (my-subsetp fs s)
      (ts-propertyp a ts fs pt g))
    (ts-propertyp a ts s pt g))
  :hints (("Goal" :in-theory (disable shortest-confined-pathp))))

(defthm not-memp-del
  (implies (setp ts) (not (memp u (del u ts)))))

(defthm ts-propertyp-choose-next
  (implies (and (invp ts pt g a)
      (my-subsetp ts (all-nodes g))
      (setp ts)
      (consp ts)
      (graphp g)
      (nodep a g)
      (equal (path a pt) (list a)))
    (let ((u (choose-next ts pt g)))
      (ts-propertyp a
        (del u ts)
        (comp-set (del u ts) (all-nodes g))
        (reassign u (neighbors u g) pt g)
        g)))
  :hints (("Goal" :in-theory (disable neighbors path shortest-pathp)
     :use ((:instance ts-propertyp-lemma1
        (pt (reassign (choose-next ts pt g)
            (neighbors (choose-next ts pt g) g)
            pt
            g))
        (ts (del (choose-next ts pt g) ts))
        (s (comp-set (del (choose-next ts pt g) ts) (all-nodes g)))
        (fs (cons (choose-next ts pt g) (comp-set ts (all-nodes g)))))))))

(defthm invp-choose-next
  (implies (and (invp ts pt g a)
      (my-subsetp ts (all-nodes g))
      (graphp g)
      (consp ts)
      (setp ts)
      (nodep a g)
      (equal (path a pt) (list a)))
    (let ((u (choose-next ts pt g)))
      (invp (del u ts) (reassign u (neighbors u g) pt g) g a)))
  :hints (("Goal" :in-theory (disable neighbors))))

(defthm del-subsetp
  (implies (my-subsetp ts s) (my-subsetp (del u ts) s)))

(defthm del-true-listp
  (implies (true-listp ts) (true-listp (del u ts))))

(defthm del-noduplicates
  (implies (setp ts) (setp (del u ts))))

(defthm path-a-pt-reassign
  (implies (and (pt-propertyp a pt g)
      (graphp g)
      (nodep a g)
      (equal (path a pt) (list a)))
    (equal (path a (reassign u v-lst pt g)) (list a)))
  :hints (("Goal" :in-theory (disable path))))

(defthm invp-last-lemma
  (implies (and (invp ts pt g a)
      (my-subsetp ts (all-nodes g))
      (nodep a g)
      (equal (path a pt) (list a))
      (true-listp ts)
      (graphp g)
      (setp ts))
    (invp nil (dsp ts pt g) g a))
  :hints (("Goal" :in-theory (disable path neighbors))))

(defthm true-listp-union
  (implies (and (true-listp lst1) (true-listp lst2))
    (true-listp (my-union lst1 lst2))))

(defthm true-list-all-nodes (true-listp (all-nodes g)))

(defthm invp-last
  (implies (and (nodep a g) (graphp g))
    (invp nil
      (dsp (all-nodes g) (list (cons a (list a))) g)
      g
      a)))

(defthm main-lemma1
  (implies (and (invp nil pt g a) (nodep b g))
    (shortest-pathp a b (path b pt) g))
  :hints (("Goal" :in-theory (disable path shortest-pathp))))

(defthm main-lemma2
  (implies (and (invp nil pt g a) (nodep b g))
    (or (null (path b pt)) (pathp-from-to (path b pt) a b g)))
  :hints (("Goal" :in-theory (disable path)))
  :rule-classes nil)

(defthm main-lemma3
  (implies (and (nodep a g) (nodep b g) (graphp g))
    (or (null (dijkstra-shortest-path a b g))
      (pathp-from-to (dijkstra-shortest-path a b g) a b g)))
  :hints (("Goal" :use ((:instance main-lemma2
        (pt (dsp (all-nodes g) (list (list a a)) g))))))
  :rule-classes nil)

(defthm main-lemma4
  (implies (and (nodep a g) (nodep b g) (graphp g))
    (shortest-pathp a b (dijkstra-shortest-path a b g) g))
  :hints (("Goal" :in-theory (disable shortest-pathp path))))

(defthm main-theorem
  (implies (and (nodep a g) (nodep b g) (graphp g))
    (let ((rho (dijkstra-shortest-path a b g)))
      (and (or (null rho) (pathp-from-to rho a b g))
        (shortest-pathp a b rho g))))
  :rule-classes nil
  :hints (("Goal" :use (main-lemma3 main-lemma4))))