; File: unbounded-case.lisp
; Author: Julien Schmaltz
; September 12th, 2001
; University of Texas at Austin, Texas, USA
; visitor of University Joseph Fourier, Grenoble, France

; content: 
; listp code for the unbounded case of the  algorithm presented in the talk

(in-package "ACL2")

; Please adapt the ../../ to point to the right directory
(include-book "../../../books/Arithmetic-4/bind-free/top")
(set-non-linearp t)
(include-book "../../../books/Arithmetic-4/floor-mod/floor-mod")


(defun n-clockwise (from n)
  (mod (+ from 1) n))

(defun n-counter-clockwise (from n)
  (mod (- from 1) n))

(defun n-across (from n)
  (mod (+ from (/ n 2)) n))

;Subgoal 3
;(IMPLIES (AND (NOT (OR (NOT (INTEGERP DEST))
;                       (< DEST 0)
;                       (< (+ -1 N) DEST)
;                       (NOT (INTEGERP FROM))
;                       (< FROM 0)
;                       (< (+ -1 N) FROM)
;                       (NOT (INTEGERP N))
;                       (<= N 0)
;                       (NOT (EQUAL (MOD N 4) 0))))
;              (NOT (EQUAL (+ DEST (- FROM)) 0))
;              (< 0 (MOD (+ DEST (- FROM)) N))
;              (<= (MOD (+ DEST (- FROM)) N)
;                  (* N 1/4)))
;         (E0-ORD-< (MIN (NFIX (MOD (+ DEST (- (MOD (+ FROM 1) N))) N))
;                        (NFIX (MOD (+ (MOD (+ FROM 1) N) (- DEST))
;                                   N)))
;                   (MIN (NFIX (MOD (+ DEST (- FROM)) N))
;                        (NFIX (MOD (+ FROM (- DEST)) N)))))


(defthm mod-x-=-x
  (implies (and (rationalp x)
                (integerp n)
                (<= 0 x)
                (< 0 n)
                (< x n))
           (equal (mod x n) x)))


(defthm mod-x-=-x-+-n
  (implies (and (rationalp x) 
                (< x 0)
                (< (- x) n)
                (integerp n)
                (< 0 n))
           (equal (mod x n)
                  (+ x n)))
  :hints (("GOAL" :in-theory (enable mod))))

(defthm force-case-split
  (implies (and (integerp dest)
                (integerp from)
                (<= 0 dest)
                (<= 0 from))
            (iff (not (equal dest from))
                  (or (< (+ dest (- from)) 0)
                      (< 0 (+ dest (- from))))))
  :rule-classes nil)

(defthm <=-=-<-or-=
  (implies (and (acl2-numberp a)
                (acl2-numberp b)
                )
           (equal (<= a b)
                  (or (< a b)
                      (= a b))))
  :rule-classes nil)

(defthm Subgoal-3.4
  (IMPLIES (AND (INTEGERP DEST)
                (<= 0 DEST)
                (<= DEST (+ -1 N))
                (INTEGERP FROM)
                (<= 0 FROM)
                (<= FROM (+ -1 N)) 
              	(INTEGERP N)
                (< 0 N)
                (INTEGERP (* N 1/4))
                (NOT (EQUAL DEST FROM))
                (NOT (INTEGERP (* (+ DEST (- FROM)) (/ N))))
                (NOT (INTEGERP (+ (* DEST (/ N)) (- (* FROM (/ N))))))
                (< (MOD (+ -1 DEST (- FROM)) N)
                   (MOD (+ 1 (- DEST) FROM) N))
                (< (MOD (+ DEST (- FROM)) N)
                   (MOD (+ (- DEST) FROM) N)))
            (< (MOD (+ -1 DEST (- FROM)) N)
               (MOD (+ DEST (- FROM)) n)))
  :hints (("GOAL" :use ((:instance force-case-split)
                        (:instance <=-=-<-or-= (a dest) (b (+ -1 n)))
                        (:instance <=-=-<-or-= (a from) (b (+ -1 n)))))))

(defthm subgoal-3.3
  (IMPLIES (AND (INTEGERP DEST)
                (<= 0 DEST)
                (<= DEST (+ -1 N))
                (INTEGERP FROM)
                (<= 0 FROM)
                (<= FROM (+ -1 N))
                (INTEGERP N)
                (INTEGERP (* 1/4 N))
                (NOT (EQUAL DEST FROM))
                (NOT (INTEGERP (+ (* DEST (/ N)) (- (* FROM (/ N))))))
                (<= (MOD (+ DEST (- FROM)) N) (* 1/4 N))
                (< (MOD (+ -1 DEST (- FROM)) N)
                   (MOD (+ 1 (- DEST) FROM) N))
                (<= (MOD (+ (- DEST) FROM) N)
                    (MOD (+ DEST (- FROM)) N)))
           (< (MOD (+ -1 DEST (- FROM)) N)
              (MOD (+ (- DEST) FROM) N)))
  :hints (("GOAL" :use ((:instance force-case-split)
                        (:instance <=-=-<-or-= (a dest) (b (+ -1 n)))
                        (:instance <=-=-<-or-= (a from) (b (+ -1 n)))))))

(defthm subgoal-3.2
  (IMPLIES (AND (INTEGERP DEST)
              (<= 0 DEST)
              (<= DEST (+ -1 N))
              (INTEGERP FROM)
              (<= 0 FROM)
              (<= FROM (+ -1 N))
              (INTEGERP N)
              (INTEGERP (* 1/4 N))
              (NOT (EQUAL DEST FROM))
              (NOT (INTEGERP (+ (* DEST (/ N)) (- (* FROM (/ N))))))
              (<= (MOD (+ DEST (- FROM)) N) (* 1/4 N))
              (<= (MOD (+ 1 (- DEST) FROM) N)
                  (MOD (+ -1 DEST (- FROM)) N))
              (< (MOD (+ DEST (- FROM)) N)
                 (MOD (+ (- DEST) FROM) N)))
         (< (MOD (+ 1 (- DEST) FROM) N)
            (MOD (+ DEST (- FROM)) N)))
  :hints (("GOAL" :use ((:instance force-case-split)
                        (:instance <=-=-<-or-= (a dest) (b (+ -1 n)))
                        (:instance <=-=-<-or-= (a from) (b (+ -1 n)))))))

(defthm subgoal-3.1
  (IMPLIES (AND (INTEGERP DEST)
              (<= 0 DEST)
              (<= DEST (+ -1 N))
              (INTEGERP FROM)
              (<= 0 FROM)
              (<= FROM (+ -1 N))
              (INTEGERP N)
              (INTEGERP (* 1/4 N))
              (NOT (EQUAL DEST FROM))
              (NOT (INTEGERP (+ (* DEST (/ N)) (- (* FROM (/ N))))))
              (<= (MOD (+ DEST (- FROM)) N) (* 1/4 N))
              (<= (MOD (+ 1 (- DEST) FROM) N)
                  (MOD (+ -1 DEST (- FROM)) N))
              (<= (MOD (+ (- DEST) FROM) N)
                  (MOD (+ DEST (- FROM)) N)))
         (< (MOD (+ 1 (- DEST) FROM) N)
            (MOD (+ (- DEST) FROM) N)))
  :hints (("GOAL" :use ((:instance force-case-split)
                        (:instance <=-=-<-or-= (a dest) (b (+ -1 n)))
                        (:instance <=-=-<-or-= (a from) (b (+ -1 n)))))))


;Subgoal 2
;(IMPLIES (AND (NOT (OR (NOT (INTEGERP DEST))
;                       (< DEST 0)
;                       (< (+ -1 N) DEST)
;                       (NOT (INTEGERP FROM))
;                       (< FROM 0)
;                       (< (+ -1 N) FROM)
;                       (NOT (INTEGERP N))
;                       (<= N 0)
;                       (NOT (EQUAL (MOD N 4) 0))))
;              (NOT (EQUAL (+ DEST (- FROM)) 0))
;              (NOT (AND (< 0 (MOD (+ DEST (- FROM)) N))
;                        (<= (MOD (+ DEST (- FROM)) N)
;                            (* N 1/4))))
;              (<= (+ N (- (* N 1/4)))
;                  (MOD (+ DEST (- FROM)) N))
;              (< (MOD (+ DEST (- FROM)) N) N))
;         (E0-ORD-< (MIN (NFIX (MOD (+ DEST (- (MOD (+ -1 FROM) N)))
;                                   N))
;                        (NFIX (MOD (+ (MOD (+ -1 FROM) N) (- DEST))
;                                   N)))
;                   (MIN (NFIX (MOD (+ DEST (- FROM)) N))
;                        (NFIX (MOD (+ FROM (- DEST)) N)))))

(defthm subgoal-2.4
  (IMPLIES (AND (INTEGERP DEST)
              (<= 0 DEST)
              (<= DEST (+ -1 N))
              (INTEGERP FROM)
              (<= 0 FROM)
              (<= FROM (+ -1 N))
              (INTEGERP N)
              (INTEGERP (* 1/4 N))
              (NOT (EQUAL DEST FROM))
              (< (* 1/4 N) (MOD (+ DEST (- FROM)) N))
              (<= (* 3/4 N) (MOD (+ DEST (- FROM)) N))
              (< (MOD (+ DEST (- FROM)) N) N)
              (< (MOD (+ 1 DEST (- FROM)) N)
                 (MOD (+ -1 (- DEST) FROM) N))
              (< (MOD (+ DEST (- FROM)) N)
                 (MOD (+ (- DEST) FROM) N)))
         (< (MOD (+ 1 DEST (- FROM)) N)
            (MOD (+ DEST (- FROM)) N)))
  :hints (("GOAL" :use ((:instance force-case-split)
                        (:instance <=-=-<-or-= (a dest) (b (+ -1 n)))
                        (:instance <=-=-<-or-= (a from) (b (+ -1 n)))))))

(defthm subgoal-2.3
  (IMPLIES (AND (INTEGERP DEST)
              (<= 0 DEST)
              (<= DEST (+ -1 N))
              (INTEGERP FROM)
              (<= 0 FROM)
              (<= FROM (+ -1 N))
              (INTEGERP N)
              (< 0 N)
              (INTEGERP (* 1/4 N))
              (NOT (EQUAL DEST FROM))
              (< (* 1/4 N) (MOD (+ DEST (- FROM)) N))
              (<= (* 3/4 N) (MOD (+ DEST (- FROM)) N))
              (< (MOD (+ DEST (- FROM)) N) N)
              (<= (MOD (+ -1 (- DEST) FROM) N)
                  (MOD (+ 1 DEST (- FROM)) N))
              (< (MOD (+ DEST (- FROM)) N)
                 (MOD (+ (- DEST) FROM) N)))
         (< (MOD (+ -1 (- DEST) FROM) N)
            (MOD (+ DEST (- FROM)) N)))
   :hints (("GOAL" :use ((:instance force-case-split)
                         (:instance <=-=-<-or-= (a dest) (b (+ -1 n)))
                         (:instance <=-=-<-or-= (a from) (b (+ -1 n)))))))

(defthm subgoal-2.1
  (IMPLIES (AND (INTEGERP DEST)
              (<= 0 DEST)
              (<= DEST (+ -1 N))
              (INTEGERP FROM)
              (<= 0 FROM)
              (<= FROM (+ -1 N))
              (INTEGERP N)
              (< 0 N)
              (INTEGERP (* 1/4 N))
              (NOT (EQUAL DEST FROM))
              (< (* 1/4 N) (MOD (+ DEST (- FROM)) N))
              (<= (* 3/4 N) (MOD (+ DEST (- FROM)) N))
              (< (MOD (+ DEST (- FROM)) N) N)
              (<= (MOD (+ -1 (- DEST) FROM) N)
                  (MOD (+ 1 DEST (- FROM)) N))
              (<= (MOD (+ (- DEST) FROM) N)
                  (MOD (+ DEST (- FROM)) N)))
         (< (MOD (+ -1 (- DEST) FROM) N)
            (MOD (+ (- DEST) FROM) N)))
  :hints (("GOAL" :use ((:instance force-case-split)
                        (:instance <=-=-<-or-= (a dest) (b (+ -1 n)))
                        (:instance <=-=-<-or-= (a from) (b (+ -1 n)))))))

(defthm abs-<-1-imp-not-int
  (implies (and (< (abs x) 1)
                (not (equal x 0)))
           (not (integerp x))))

(defthm subgoal-2.2
  (IMPLIES (AND (INTEGERP DEST)
                (<= 0 DEST)
                (<= DEST (+ -1 N))
                (INTEGERP FROM)
                (<= 0 FROM)
                (<= FROM (+ -1 N))
                (INTEGERP N)
                (< 0 N)
                (INTEGERP (* 1/4 N))
                (NOT (EQUAL DEST FROM))
                (< (* 1/4 N) (MOD (+ DEST (- FROM)) N))
                (<= (* 3/4 N) (MOD (+ DEST (- FROM)) N))
                (< (MOD (+ DEST (- FROM)) N) N)
                (< (MOD (+ 1 DEST (- FROM)) N)
                   (MOD (+ -1 (- DEST) FROM) N))
                (<= (MOD (+ (- DEST) FROM) N)
                    (MOD (+ DEST (- FROM)) N)))
           (< (MOD (+ 1 DEST (- FROM)) N)
              (MOD (+ (- DEST) FROM) N)))
  :hints (("GOAL" :use ((:instance force-case-split)
                        (:instance <=-=-<-or-= (a dest) (b (+ -1 n)))
                        (:instance <=-=-<-or-= (a from) (b (+ -1 n)))))))

;Subgoal 1
;(IMPLIES (AND (NOT (OR (NOT (INTEGERP DEST))
;                       (< DEST 0)
;                       (< (+ -1 N) DEST)
;                       (NOT (INTEGERP FROM))
;                       (< FROM 0)
;                       (< (+ -1 N) FROM)
;                       (NOT (INTEGERP N))
;                       (<= N 0)
;                       (NOT (EQUAL (MOD N 4) 0))))
;              (NOT (EQUAL (+ DEST (- FROM)) 0))
;              (NOT (AND (< 0 (MOD (+ DEST (- FROM)) N))
;                        (<= (MOD (+ DEST (- FROM)) N)
;                            (* N 1/4))))
;              (NOT (AND (<= (+ N (- (* N 1/4)))
;                            (MOD (+ DEST (- FROM)) N))
;                        (< (MOD (+ DEST (- FROM)) N) N))))
;         (E0-ORD-< (MIN (NFIX (MOD (+ DEST (- (N-ACROSS FROM N))) N))
;                        (NFIX (MOD (+ (N-ACROSS FROM N) (- DEST)) N)))
;                   (MIN (NFIX (MOD (+ DEST (- FROM)) N))
;                        (NFIX (MOD (+ FROM (- DEST)) N)))))

(defthm mod-x-=-minusx-pos
  (implies (and (rationalp x)
                (integerp n)
                (< 0 n)
                (<= n x)
                (< x (* 2 n)))
           (equal (mod x n)
                  (- x n))))

(defthm mod-+-n/2-pos
  (implies (and (< x n)
                (rationalp x)
                (integerp n)
                (<= (* 1/2 n) x)
                (< 2 n)
                )
           (< (mod (+ x (* 1/2 n)) n)
              (mod x n))))

(defthm mod-+-n/2-neg
  (implies (and (< x 0)
                (< (- x) n)
                (rationalp x)
                (<= (- x) (* 1/2 n))
                (integerp n)
                (< 0 n))
           (<  (mod (+ x (* 1/2 n)) n)
               (mod x n))))

(defthm subgoal-1.18
  (IMPLIES (AND (INTEGERP DEST)
              (<= 0 DEST)
              (<= DEST (+ -1 N))
              (INTEGERP FROM)
              (<= 0 FROM)
              (<= FROM (+ -1 N))
              (INTEGERP N)
              (< 0 N)
              (INTEGERP (* 1/4 N))
              (NOT (EQUAL DEST FROM))
              (< (* 1/4 N) (MOD (+ DEST (- FROM)) N))
              (< (MOD (+ DEST (- FROM)) N) (* 3/4 N))
              (INTEGERP (MOD (+ DEST (- FROM) (* -1/2 N)) N))
              (INTEGERP (MOD (+ (- DEST) FROM (* 1/2 N)) N))
              (< (MOD (+ DEST (- FROM) (* -1/2 N)) N)
                 (MOD (+ (- DEST) FROM (* 1/2 N)) N))
              (<= (MOD (+ (- DEST) FROM) N)
                  (MOD (+ DEST (- FROM)) N)))
         (< (MOD (+ DEST (- FROM) (* -1/2 N)) N)
            (MOD (+ (- DEST) FROM) N)))
   :hints (("GOAL" :use ((:instance mod-+-n/2-pos (x (+ (- dest) from)))
                         (:instance mod-+-n/2-neg (x (+ (- dest) from))))
                   :in-theory (disable mod-+-n/2-pos mod-+-n/2-neg))))



(defthm subgoal-1.16
  (IMPLIES (AND (INTEGERP DEST)
              (<= 0 DEST)
              (<= DEST (+ -1 N))
              (INTEGERP FROM)
              (<= 0 FROM)
              (<= FROM (+ -1 N))
              (INTEGERP N)
              (< 0 N)
              (INTEGERP (* 1/4 N))
              (NOT (EQUAL DEST FROM))
              (< (* 1/4 N) (MOD (+ DEST (- FROM)) N)); these 2 hyps hust tell
                                                     ; that dest is in the
                                                     ; other half circle
              (< (MOD (+ DEST (- FROM)) N) (* 3/4 N));
              (INTEGERP (MOD (+ DEST (- FROM) (* -1/2 N)) N))
              (INTEGERP (MOD (+ (- DEST) FROM (* 1/2 N)) N))
              (<= (MOD (+ (- DEST) FROM (* 1/2 N)) N) ; h1
                  (MOD (+ DEST (- FROM) (* -1/2 N)) N))
              (<= (MOD (+ (- DEST) FROM) N) ; h1 and h2 => 0 < dest-from <= n/2
                                            ; or -n < dest-from <= -n/2
                  (MOD (+ DEST (- FROM)) N)))
         (< (MOD (+ (- DEST) FROM (* 1/2 N)) N)
            (MOD (+ (- DEST) FROM) N)))
  :hints (("GOAL" :use ((:instance mod-+-n/2-pos (x (+ (- dest) from)))
                        (:instance mod-+-n/2-neg (x (+ (- dest) from))))
                  :in-theory (disable mod-+-n/2-pos mod-+-n/2-neg))))

(defthm mod-+-1/2-=-mod-minus-1/2
  (implies (and (integerp n)
                (< 0 n)
                (rationalp x)
                (< (abs x) n))
           (equal (mod (+ x (* -1/2 n)) n)
                  (mod (+ x (* 1/2 n)) n)))
  :hints (("GOAL" :in-theory (enable mod))))

(defthm mod-n/2-pos
  (implies (and (< 0 x)
                (< x n)
                (rationalp x)
                (integerp n)
                (<= (* 1/2 n) x)
                (< 0 n)
                )
           (< (mod (+ x (* -1/2 n)) n)
              (mod x n))))

(defthm mod-n/2-neg
  (implies (and (< x 0)
                (< (- x) n)
                (rationalp x)
                (<= (- x) (* 1/2 n))
                (integerp n)
                (< 0 n))
           (<  (mod (+ x (* -1/2 n)) n)
               (mod x n))))

(defthm subgoal-1.15
  (IMPLIES (AND (INTEGERP DEST)
              (<= 0 DEST)
              (<= DEST (+ -1 N))
              (INTEGERP FROM)
              (<= 0 FROM)
              (<= FROM (+ -1 N))
              (INTEGERP N)
              (< 0 N)
              (INTEGERP (* 1/4 N))
              (NOT (EQUAL DEST FROM))
              (< (* 1/4 N) (MOD (+ DEST (- FROM)) N))
              (< (MOD (+ DEST (- FROM)) N) (* 3/4 N))
              (INTEGERP (MOD (+ DEST (- FROM) (* -1/2 N)) N))
              (INTEGERP (MOD (+ (- DEST) FROM (* 1/2 N)) N))
              (<= (MOD (+ (- DEST) FROM (* 1/2 N)) N)
                  (MOD (+ DEST (- FROM) (* -1/2 N)) N))
              (< (MOD (+ DEST (- FROM)) N)
                 (MOD (+ (- DEST) FROM) N)))
         (< (MOD (+ (- DEST) FROM (* 1/2 N)) N)
            (MOD (+ DEST (- FROM)) N)))
    :hints (("GOAL" :use ((:instance mod-n/2-pos (x (+ dest (- from))))
                          (:instance mod-n/2-neg (x (+ dest (- from)))))
                    :in-theory (disable mod-n/2-pos mod-n/2-neg))))



(defthm subgoal-1.17
  (IMPLIES (AND (INTEGERP DEST)
              (<= 0 DEST)
              (<= DEST (+ -1 N))
              (INTEGERP FROM)
              (<= 0 FROM)
              (<= FROM (+ -1 N))
              (INTEGERP N)
              (INTEGERP (* 1/4 N))
              (NOT (EQUAL DEST FROM))
              (< (* 1/4 N) (MOD (+ DEST (- FROM)) N))
              (< (MOD (+ DEST (- FROM)) N) (* 3/4 N))
              (INTEGERP (MOD (+ DEST (- FROM) (* -1/2 N)) N))
              (INTEGERP (MOD (+ (- DEST) FROM (* 1/2 N)) N))
              (< (MOD (+ DEST (- FROM) (* -1/2 N)) N)
                 (MOD (+ (- DEST) FROM (* 1/2 N)) N))
              (< (MOD (+ DEST (- FROM)) N)
                 (MOD (+ (- DEST) FROM) N)))
         (< (MOD (+ DEST (- FROM) (* -1/2 N)) N)
            (MOD (+ DEST (- FROM)) N)))
  :hints (("GOAL" :use ((:instance mod-n/2-pos (x (+ dest (- from))))
                        (:instance mod-n/2-neg (x (+ dest (- from)))))
                  :in-theory (disable mod-n/2-pos mod-n/2-neg))))

(defun n-go-to-node (dest from n)
  (declare (xargs :measure (min (nfix (mod (- dest from) n))
                                (nfix (mod (- from dest) n)))))
  (cond ((or (not (integerp dest)) 
            (< dest 0) 
            (< (- n 1) dest) 
            (not (integerp from)) 
            (< from 0) 
            (< (- n 1) from) 
            (not (integerp n)) 
            (<= n 0) 
            (not (equal (mod n 4) 0))) 
        nil) 
        ((equal (- dest from) 0) nil)
        ((and (< 0 (mod (- dest from) n))
              (<= (mod (- dest from) n) (/ n 4))) 
         (cons from 
               (n-go-to-node dest (n-clockwise from n) n)))
        ((and (<= (- n (/ n 4)) (mod (- dest from) n))
              (< (mod (- dest from) n) n))
         (cons from 
	       (n-go-to-node dest (n-counter-clockwise from n) n)))
        (t
         (cons from 
               (n-go-to-node dest (n-across from n) n)))))