(set-guard-checking :none)

; ----

(include-book "arithmetic-5/top" :dir :system)

(SET-DEFAULT-HINTS '((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP
                                              HIST PSPV)))

(defun plus (x y)
  (if (zp x)
      (nfix y)
      (+ 1 (plus (- x 1) y))))

(defun times (x y)
  (if (zp x)
      0
      (plus y (times (- x 1) y))))

(defthm times-assoc
  (implies (and (natp i) (natp j) (natp k))
           (equal (times (times i j) k)
                  (times i (times j k)))))

; ----

(set-guard-checking :none)

(DEFUN MOVE-DISKS(N A B C) ; Piyush's problem
  (IF (ZP N)
    NIL
    (IF (EQUAL N 1)
      (LIST (CONS A B))
      (APPEND (MOVE-DISKS (- N 1) A C B)
            (APPEND (LIST (CONS A B)) (MOVE-DISKS (- N 1) C B A))))))

(DEFUN HANOI (N)
  (MOVE-DISKS N 'A 'C 'B))

(hanoi 3)

(len (hanoi 3))
(len (hanoi 4))
(len (hanoi 5))

(defthm len-hanoi
  (implies (natp n)
           (equal (len (hanoi n)) (- (expt 2 n) 1))))

(hanoi 3)
(hanoi 2)

(defthm len-move-disks
  (implies (natp n)
           (equal (len (move-disks n x y z))
                  (- (expt 2 n) 1))))

(defthm len-append
  (equal (len (append a b))
         (+ (len a) (len b))))

(defthm len-move-disks
  (implies (natp n)
           (equal (len (move-disks n x y z))
                  (- (expt 2 n) 1))))

(defthm len-hanoi
  (implies (natp n)
           (equal (len (hanoi n)) (- (expt 2 n) 1))))

(DEFUN IS-SORTED (LST) ; Hyeonseo's problem
  (COND ((ENDP LST) T)
	((ENDP (CDR LST)) T)
	(T (AND (<= (CAR LST) (CADR LST))
		(IS-SORTED (CDR LST))))))

(is-sorted '(1 2 3 4 5))

(DEFUN REMOVE-LTE (X LST)
  (IF (ENDP LST)
      NIL
      (LET ((NEXT (REMOVE-LTE X (CDR LST))))
	(IF (<= (CAR LST) X)
	    NEXT (APPEND (LIST (CAR LST)) NEXT)))))

(remove-lte 3 '(1 2 3 4 5 6))

(DEFUN REMOVE-GT (X LST)
  (IF (ENDP LST)
      NIL
      (LET ((NEXT (REMOVE-GT X (CDR LST))))
	(IF (> (CAR LST) X)
	    NEXT (APPEND (LIST (CAR LST)) NEXT)))))

(remove-gt 3 '(1 2 3 4 5 6))

(DEFUN QUICKSORT (LST)
  (IF (ENDP LST)
      NIL
      (LET ((PIVOT (CAR LST)) (REST (CDR LST)))
	(APPEND (QUICKSORT (REMOVE-GT PIVOT REST))
		(LIST PIVOT)
		(QUICKSORT (REMOVE-LTE PIVOT REST))))))

(quicksort '(5 4 3 2 1 10 9 8 7 6))

(DEFTHM PROVE-QUICKSORT-CORRECTNESS
  (IMPLIES (TRUE-LISTP X)
           (IS-SORTED (QUICKSORT X))))