Lab 9 Problem Set.

In this lab we will first revisit termination and measure functions.
This will be essential for the upcoming HW09 and also for Exam 2 (not yet
upcoming...).

Instead of more drill exercises, we will do a fun and educational trick problem.

We will then review the idea of induction, both from a mathematical
perspective, and from that of ACL2s, to the (limited) extent we will have
covered this topic in class by then.

===========================================================================
======= Termination and Measure Functions
===========================================================================

Let's play with a function that operates on natural numbers _modulo n_ :
this means we only consider natural numbers i in the range 0 <= i < n (note
that n is excluded); there are exactly n such numbers. Arithmetic
operations such as addition "wrap around", as we will see.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Here is a predicate nat-mod-n-p(a,n) that returns true exactly if
; argument a is of datatype nat-mod-n. This is like a recognizer,
; except that the function takes not only a, but also the "parameter" n as input:

(defunc nat-mod-n-p (a n)
  :input-contract t
  :output-contract (booleanp (nat-mod-n-p a n))
  (if (and (natp a) (natp n))
    (< a n)
    nil))

; For example, suppose we define the concrete type of numbers 0,1,2,3:

(defdata mod-4 (range integer (0 <= _ < 4)))

; then the following theorem holds (and ACL2s should be able to prove it):

(thm (equal (mod-4p a) (nat-mod-n-p a 4)))

; What does the theorem state?

; Now consider the function

(defunc plus-mod-n (a b n)
  :input-contract (and (nat-mod-n-p a n) (nat-mod-n-p b n))
  :output-contract (nat-mod-n-p (plus-mod-n a b n) n)
  (let ((sum (+ a b)))
    (if (< sum n)
      sum
      (- sum n))))

(check= (plus-mod-n 2 3 10) 5)
(check= (plus-mod-n 2 3  5) 0)
(check= (plus-mod-n 2 3  4) 1)

; Observe that (plus-mod-n a b n) returns the sum of a and b modulo n. That
; is, it returns the sum a+b, unless that sum equals or exceeds n, in which
; case the result "wraps around": the result is the remainder of a+b when
; divided by n.

; Now define an analogous function minus-mod-n such that (minus-mod-n a b n)
; returns a-b modulo n. See tests below, and define 3 more.

; Think about what happens when a-b is negative: the output MUST be non-negative.

(defunc minus-mod-n (a b n)
  :input-contract (and (nat-mod-n-p a n) (nat-mod-n-p b n))
  :output-contract (nat-mod-n-p (minus-mod-n a b n) n)
...

(check= (minus-mod-n 5 3 10) 2)
(check= (minus-mod-n 3 5 10) 8)
(check= (minus-mod-n 3 5  6) 4)

; We are now switching into program mode, as we are about to define a
; function that ACL2s has difficulties proving terminating (for good reasons):

(acl2s-defaults :set testing-enabled nil)
(set-defunc-termination-strictp nil)
(set-defunc-function-contract-strictp nil)
(set-defunc-body-contracts-strictp nil)

; Consider

(defunc inc-dec (a b n)
  :input-contract (and (nat-mod-n-p a n) (nat-mod-n-p b n))
  :output-contract (booleanp (inc-dec a b n))
  (if (equal a b)
    t
    (inc-dec (plus-mod-n a 1 n) (minus-mod-n b 1 n) n)))

; Function inc-dec(a,b,n) implements the following loop:

; while a and b are not equal:
;   increment a by 1 modulo n
;   decrement b by 1 modulo n
; end of loop

; Run the following tests at the ACL2s prompt, IN THIS ORDER:

; (inc-dec 2 3 7)
; (inc-dec 3 4 7)
; (inc-dec 2 4 8)
; (inc-dec 3 4 6)

; What happens in these function calls? do they (seem to) terminate?

; Now turn on function call tracing for inc-dec:

(acl2::trace! inc-dec)

; and run the *terminating* ones of the above test cases again at the ACL2s prompt.

; Come up with a conjecture for restrictions on the inputs (a b n) such
; that the function terminates.

; I'm just asking for a conjecture -- no proofs (which is not easy at all).

...

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Now let's look at the special case n=3:

(defunc inc-dec-3 (a b)
  :input-contract (and (nat-mod-n-p a 3) (nat-mod-n-p b 3))
  :output-contract (booleanp (inc-dec-3 a b))
  (if (equal a b)
    t
    (inc-dec-3 (plus-mod-n a 1 3) (minus-mod-n b 1 3))))

In this case, possible values for a and b in the above functions are 0,1,2.
That means there are only finitely many possible inputs to inc-dec-3! How many?

1. Prove that inc-dec-3 terminates, by writing down the call sequence for
EACH possible input. The call sequence must end with an input that
satisfies a=b (since only then inc-dec-3 terminates)!

Hint: there are more than a handful cases, but the above task requires very
little writing. Be smart!

...

2. Suppose your instructor is stubborn and says: "I only accept termination
proofs via measure functions, not silly enumerations as you did above."

Hmm. Can we comply and provide a measure function for inc-dec-3 ?

Also see if ACL2s can prove termination (without help) even for this simple
special case!

...

===========================================================================
======= Induction: Basics and Review
===========================================================================

Consider the following claim:

(C) For every natural number n,      1 + 3 + 5 + 7 + ... + 2n+1 = (n+1)^2

1. Prove (C) using classical mathematical induction.

...

2. Define an ACL2s function sum-odd that takes n as argument and computes
   the sum on the left of (C). The definition must satisfy:

   (check= (sum-odd 1) 4)

...

3. Formalize (C) as an ACL2s conjecture. Can ACL2s prove it automatically?
   If not, you have not formalized it correctly in ACL2s.

...

4. Extract the induction scheme of sum-odd and apply it to (C). How do the
   resulting proof obligations relate to what you did in 1. ?

...

5. (optional) Prove (C) ACL2s-style, i.e. discharge the proof obligations
   identified in 4, using Equational Reasoning.