; File: single-event.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 proof as a single event (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") ; I include all the lemmas that were proved during the talk (include-book "lemmas") (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)) (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) (defun n-go-to-node (dest from n) (declare (xargs :measure (min (nfix (mod (- dest from) n)) (nfix (mod (- from dest) n))) :hints (("GOAL" :use ((:instance force-case-split) (:instance <=-=-<-or-= (a dest) (b (+ -1 n))) (:instance <=-=-<-or-= (a from) (b (+ -1 n))) (:instance mod-+-n/2-pos (x (+ (- dest) from))) ) :in-theory (disable PREFER-POSITIVE-ADDENDS-< mod-+-n/2-pos )) ("Subgoal 808.4" :cases ((<= 0 (+ -1 from)) (< (+ -1 from) 0)))) )) (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)))))