#|

In this lab we will focus on proving termination using measure
functions. The exercises bring up many interesting issues, so make
sure you know how to prove the functions below terminate.

Your goal is to come up with paper-and-pencil proofs, not ACL2s
proofs. We provide ACL2s definitions so that you can explore the
functions, e.g., you can trace definitions as per the Piazza post on
debugging & understanding code.

Prove that the following functions are terminating by coming up with
an appropriate measure function and proving that it is a measure
function.

|#

(definec app?-t2 (x :tl y :tl acc :tl) :tl
  (if (endp x)
      (if (endp y)
          acc
        (app?-t2 x (rest y) (cons (first y) acc)))
    (app?-t2 (rest x) y (cons (first x) acc))))

(definec app?-t3 (x :tl y :tl acc :tl) :tl
  (cond ((and (endp x) (endp y)) acc)
        ((endp x) (app?-t3 x (rest y) (cons (first y) acc)))
        ((endp y) (app?-t3 (rest x) y (cons (first x) acc)))
        (t (app?-t3 x nil (app?-t3 nil y acc)))))

(definec app?-t4 (x :tl y :tl acc :tl) :tl
  (cond ((and (endp x) (endp y)) acc)
        ((endp x) (app?-t4 x (rest y) (cons (first y) acc)))
        ((endp y) (app?-t4 y x acc))
        (t (app?-t4 x nil (app?-t4 acc nil y)))))

; Here is a function that you may find useful when constructing a
; measure function for magnitude. It is non-recursive, so you don't
; have to prove termination.

(defunc ceil (x)
  :input-contract (and (rationalp x) (>= x 0))
  :output-contract (natp (ceil x))
  (ceiling x 1))

; Here are some tests showing how ceil works.

(check= (ceil 11) 11)
(check= (ceil 10/3) 4)
(check= (ceil 10/101) 1)

:program
; ACL2s needs help to prove termination of the following definitions.

(defunc magnitude (x)
  :input-contract (and (rationalp x) (>= x 0))
  :output-contract (integerp (magnitude x))
  (cond ((equal x 0) 0)
        ((>= x 10) (+ 1 (magnitude (/ x 10))))
        ((< x 1) (* -1 (magnitude (/ 1 x))))
        (t 1)))

; To come up with a measure, you have to understand how magnitude
; works, so one way to do that is to trace it and try running it on
; examples.

(trace$ magnitude)

(magnitude 20)
(magnitude 200000)
(magnitude 200000000000)
(magnitude 1/20)
(magnitude 1/200000)
(magnitude 1/200000000000)

; Now, come up with a measure function and prove it correct.