; 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)))))