; **************** BEGIN INITIALIZATION FOR ACL2s B MODE ****************** ;
; (Nothing to see here!  Your actual file is after this initialization code);

#|
Pete Manolios
Fri Jan 27 09:39:00 EST 2012
----------------------------

Made changes for spring 2012.


Pete Manolios
Thu Jan 27 18:53:33 EST 2011
----------------------------

The Beginner level is the next level after Bare Bones level.

|#

; Put CCG book first in order, since it seems this results in faster loading of this mode.
#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading the CCG book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "ccg/ccg" :uncertified-okp nil :dir :acl2s-modes :ttags ((:ccg)) :load-compiled-file nil);v4.0 change

;Common base theory for all modes.
#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s base theory book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "base-theory" :dir :acl2s-modes)

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s customizations book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "custom" :dir :acl2s-modes :uncertified-okp nil :ttags :all)

;Settings common to all ACL2s modes
(acl2s-common-settings)

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading trace-star and evalable-ld-printing books.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "trace-star" :uncertified-okp nil :dir :acl2s-modes :ttags ((:acl2s-interaction)) :load-compiled-file nil)
(include-book "hacking/evalable-ld-printing" :uncertified-okp nil :dir :system :ttags ((:evalable-ld-printing)) :load-compiled-file nil)

;theory for beginner mode
#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s beginner theory book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "beginner-theory" :dir :acl2s-modes :ttags :all)


#+acl2s-startup (er-progn (assign fmt-error-msg "Problem setting up ACL2s Beginner mode.") (value :invisible))
;Settings specific to ACL2s Beginner mode.
(acl2s-beginner-settings)

; why why why why 
(acl2::xdoc acl2s::defunc) ; almost 3 seconds

(cw "~@0Beginner mode loaded.~%~@1"
    #+acl2s-startup "${NoMoReSnIp}$~%" #-acl2s-startup ""
    #+acl2s-startup "${SnIpMeHeRe}$~%" #-acl2s-startup "")


(acl2::in-package "ACL2S B")

; ***************** END INITIALIZATION FOR ACL2s B MODE ******************* ;
;$ACL2s-SMode$;Beginner
#|
CS 2800 Homework 11 - Fall 2017


This homework is to be done in a group of 2-3 students. 

If your group does not already exist:

 * One group member will create a group in BlackBoard
 
 * Other group members then join the group
 
 Submitting:
 
 * Homework is submitted by one group member. Therefore make sure the person
   submitting actually does so. In previous terms when everyone needed
   to submit we regularly had one person forget but the other submissions
   meant the team did not get a zero. Now if you forget, your team gets 0.
   - It wouldn't be a bad idea for group members to send confirmation 
     emails to each other to reduce anxiety.

 * Submit the homework file (this file) on Blackboard. Do not rename 
   this file. There will be a 10 point penalty for this.

 * You must list the names of ALL group members below, using the given
   format. This way we can confirm group membership with the BB groups.
   If you fail to follow these instructions, it costs us time and
   it will cost you points, so please read carefully.


Names of ALL group members: FirstName1 LastName1, FirstName2 LastName2, ...

Note: There will be a 10 pt penalty if your names do not follow 
this format.
|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|
 Inductive Proofs:
 - For all proofs below, solutions must be in the format described in class and
   in the notes. This includes:
     * Explicitly identifying an induction scheme and the function that gives
       rise to it.
     * Labeling general context (C1, C2....) and derived context.
     * Providing justifications for each piece of derived context.
     * Explicitly identifying axioms and theorems used
     * The if axioms and theorem substitutions are not required. You can use
       any other shortcuts previously identified.
     * PL can be given as justification for any propositional logic rules with the
      exceptions of Modus Ponens (MP) and Modus Tollens (MT)
     * Hocus Pocus (HP) is not permissible justification.
     * All arithmetic rules can be justified by writing "Arithmetic".
     
Previous homeworks (such as HW05) identify these requirements in more detail.

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|
For this homework you may want to use ACL2s to help you.

Technical instructions:

- open this file in ACL2s as hw11.lisp

- make sure you are in BEGINNER mode. This is essential! Note that you can
  only change the mode when the session is not running, so set the correct
  mode before starting the session.

- insert your solutions into this file where indicated (usually as "...")

- only add to the file. Do not remove or comment out anything pre-existing
  unless asked to.

- make sure the entire file is accepted by ACL2s. In particular, there must
  be no "..." left in the code. If you don't finish all problems, comment
  the unfinished ones out. Comments should also be used for any English
  text that you may add. This file already contains many comments, so you
  can see what the syntax is.

- when done, save your file and submit it as hw11.lisp

- avoid submitting the session file (which shows your interaction with the
  theorem prover). This is not part of your solution. Only submit the lisp
  file!

|#


#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1.  Let's revisit a problem from the sample exam.  You've been given functions 
how-many-t and how-many* such that how-many = how-many*
|#
(defunc how-many (e l)
  :input-contract (listp l)
  :output-contract (natp (how-many e l))
  (if (endp l)
    0
    (+ (if (equal e (first l)) 1 0)
       (how-many e (rest l)))))

;; how-many-t: All x List x Nat -> Nat
;; The tail recursive helper function for how-many*
;; where acc keeps a tally of the number of instances of
;; found so far in the list l.
(defunc how-many-t (e l acc)
  :input-contract (and (listp l) (natp acc))
  :output-contract (natp (how-many-t e l acc))
  (if (endp l)
    acc
    (how-many-t e (rest l) (+ (if (equal e (first l)) 1 0) acc))))

;; how-many*: All x List -> Nat
(defunc how-many* (e l)
  :input-contract (listp l)
  :output-contract (natp (how-many* e l))
  (how-many-t e l 0))

#|
The goal is to prove the following conjecture:

phi : (listp l) => (how-many* e l) = (how-many e l)

That is, we want to show that the two functions compute the same result on
all inputs. We will prove this in several steps.

(a) Formulate a lemma that relates how-many-t to how-many, by filling in the ... below:

phi_1 : (listp l) /\ (natp acc) => (how-many-t e l acc) =  ... (how-many e l) ...
;;=================================SOLUTION
phi_1 : (listp l) /\ (natp acc) => (how-many-t e l acc) = acc + (how-many e l)

(b) Prove phi_1. Use the induction scheme how-many-t gives rise to. Note
that how-many-t has an if nested inside other functions. You can rewrite
it, using cond, before extracting an induction scheme if you want to use
the I.S. generating pattern from the the notes (it may help).
;;=================================SOLUTION START
We rewrite how-many-t as follows:

(defunc how-many-t (e l acc)
  :input-contract (and (listp l) (natp acc))
  :output-contract (natp (how-many-t e l acc))
  (cond ((endp l)            acc)
        ((equal e (first l)) (how-many-t e (rest l) (+ acc 1)))
        (t                   (how-many-t e (rest l) acc))))

We prove phi_1 following this IS:

- (not ic) => phi_1: trivial

- (listp l) /\ (natp acc) /\ (endp l) => phi_1: easy!

- (listp l) /\ (natp acc) /\ (not (endp l) /\ (equal e (first l)) /\ phi_1|((l (rest l)) (acc (+ acc 1))) => phi_1

- (listp l) /\ (natp acc) /\ (not (endp l) /\ (not (equal e (first l))) /\ phi_1|((l (rest l))) => phi_1

PROOFS:
First recursive case:
- (listp l) /\ (natp acc) /\ (not (endp l) /\ (equal e (first l)) /\ phi_1|((l (rest l)) (acc (+ acc 1))) => phi_1
C1. (listp l)
C2. (natp acc)
C3. (not (endp l))
C4. (equal e (first l))
C5. (listp (rest l)) /\ (natp (+ acc 1)) => (how-many-t e (rest l) (+ acc 1)) = acc + 1 + (how-many e (rest l))
- - -
C6. (listp (rest l)) { C1, C3 }
C7. (natp (+ acc 1)) { C2, arithmetic }
C8. (how-many-t e (rest l) (+ acc 1)) = acc + 1 + (how-many e (rest l)) {C6, C7, C5, MP}

  (how-many-t e l acc)

= { def. how-many-t, C3, C4 }

  (how-many-t e (rest l) (+ acc 1))

= { C8 }

  acc + 1 + (how-many e (rest l))

= { def. how-many, C3, C4 }

  acc + (how-many e l)

Second recursive case:
- (listp l) /\ (natp acc) /\ (not (endp l) /\ (not (equal e (first l))) /\ phi_1|((l (rest l))) => phi_1 :

C1. (listp l)
C2. (natp acc)
C3. (not (endp l))
C4. (not (equal e (first l)))
C5. (and (listp (rest l)) (natp acc)) => (how-many-t e (rest l) acc) = acc + (how-many e (rest l))
- - -
C6. (listp (rest l)) { C1, C3 }
C7. (how-many-t e (rest l) acc) = acc + (how-many e (rest l)) { C5, C6, C2, MP }

  (how-many-t e l acc)

= { def. how-many-t, C3, C4 }

  (how-many-t e (rest l) acc)

= { C7 }

  acc + (how-many e (rest l))

= { def. how-many, C3, C4 }

  acc + (how-many e l)

(c) Using only equational reasoning (no induction!), prove the main
conjecture phi from above. Using phi_1 (which you just proved) this should
be very simple.
phi : (listp l) => (how-many* e l) = (how-many e l)

PROOF:
C1. (listp l)

(how-many* e l)
={Def. how-many*, C1}
(how-many-t e l 0))
={C1, (natp 0), phi_1|(( e e) (l l) (acc 0))}
0 + (how-many e l)
={Arithmetic}
(how-many e l)

;;=================================SOLUTION END
|#


#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2. Filtering Data
Consider the following defdata and the function get-integers that uses it:
We're going to selectively filter out all elements in a list that aren't integers
|#
(defdata integerlist (listof integer))

(defunc get-integers (l)
  :input-contract (listp l)
  :output-contract (integerlistp (get-integers l))
  (cond ((endp l)         nil)
        ((integerp (first l)) (cons (first l) (get-integers (rest l))))
        (t                (get-integers (rest l)))))

(check= (get-integers '(b "23" lk ())) ())
(check= (get-integers '(h "ter" -1 aw 9)) '(-1 9))
(check= (get-integers '("qw" "brc" aw (1 2 3) 89 rt -1)) '(89 -1))

;(a) Write the function get-integers-t, which is a tail-recursive version of
;get-integers with an accumulator:

;; get-integers-t: listp x integerlist -> integerlist
;; get-integers-t takes a list and removes all elements
;; in the list that are not integers (this includes sub-lists of integers)
;; acc is an accumulator that collects integers to return.
(defunc get-integers-t (l acc)
  ;;......................) ;;Obviously write your own tests too
  ;;=============================SOLUTION START
  :input-contract (and (listp l) (integerlistp acc))
  :output-contract (integerlistp (get-integers-t l acc))
  (cond ((endp l)         acc)
        ((integerp (first l)) (get-integers-t (rest l)(cons (first l) acc)))
        (t                (get-integers-t (rest l) acc))))

;; Obv
(check= (get-integers-t '(q "ab" lk ()) '(2 3)) '(2 3))
(check= (get-integers-t '(a "abc" 1 aw 9) ()) '(9 1))
(check= (get-integers-t '("hj" "abc" aw (1 2 3) 89 lk 1) '(10 11)) '(1 89 10 11))
;;===========================SOLUTION END

;; Here is get-integers*, a non-recursive function that calls
;; get-integers-t and suitably initializes l and acc :
(defunc get-integers* (l)
  :input-contract (listp l)
  :output-contract (integerlistp (get-integers* l))
  (rev (get-integers-t l ())))

#|
(c) Identify a lemma that relates get-integers-t to get-integers. Remember
that this is a generalization step, i.e., all arguments to get-integers-t
are variables (no constants). The RHS should include acc.
....................
;; ===========================SOLUTION
(listp l) /\ (integerlistp acc) => (get-integers-t l acc) = (app (rev (get-integers l)) acc)

(d) Assuming that lemma in (c) is true and using ONLY equational reasoning,
prove the main theorem:

  (listp l) => (get-integers* l) = (get-integers l)

If you need any "lemmas", note them down as "debt", to be proved later. This should
include any theorems that we've already proven (you won't need to prove these but you
still need to list them)
....................
;; ===========================SOLUTION START
Context
C1. (listp l)

(get-integers* l)
={C1, Def. get-integers*}
(rev (get-integers-t l ()))
={C1, assuming Lemma in (c) with substitution ((acc ()))}
(rev (app (rev (get-integers l)) ()))
={Lemma L1 below, empty substitution}
(rev (rev (get-integers l)))
={Lemma L2 below with subsitution ((l (get-integers l)))}
(get-integers l)
;; ===========================SOLUTION END

(e) Prove the lemma in (c). Use the induction scheme of get-integers-t. In
doing so, you can use the following lemma for free (i.e., you don't need to
prove it).

L3: (integerp e) /\ (integerlistp l) => (integerlistp (cons e l))

Again, if you need another lemma, note it as "dept"

....................
;; ===========================SOLUTION START
phi:((listp l) /\ (integerlistp acc)) => ((get-integers-t l acc) = (app (rev (get-integers l)) acc))

We prove the claim by induction, using the induction scheme of get-integers-t
Here are the proof obligations:

1. ~((listp l) /\ (integerlistp acc)) => phi
2. (listp l) /\ (integerlistp acc) /\ (endp l) => phi
3. (listp l) /\ (integerlistp acc) /\ (not (endp l)) /\ (integerp (first l)) /\ phi|((l (rest l)) (acc (cons (first l) acc))) => phi
4. (listp l) /\ (integerlistp acc) /\ (not (endp l)) /\ (not (integerp (first l))) /\ phi|((l (rest l)) (acc acc)) => phi

1. Trivial....but here it is anyways
C1. (listp l)
C2. ~(listp l)
--------
C3. nil
Thus the conjecture is true in this context.

2. (listp l) /\ (integerlistp acc) /\ (endp l) => phi
Context
C1. (listp l)
C2. (integerlistp acc)
C3. (endp l)
-------------
C4. (l = nil) { C3, def endp}

LHS
(get-integers-t l acc)
={C1, C2, C3 def get-integer-t}
acc
={Def. app, def endp}
(app nil acc)
={C4, Def. rev, C3}
(app (rev l) acc)
={C3, Def. get-integers}
(app (rev (get-integers l)) acc)


3. (listp l) /\ (integerlistp acc) /\ (not (endp l)) /\ (integerp (first l)) 
     /\ phi|((l (rest l)) (acc (cons (first l) acc))) => phi
Context
C1. (listp l)
C2. (integerlistp acc)
C3. (not (endp l))
C4. (integerp (first l))
C5. ((listp (rest l)) /\ (integerlistp (cons (first l) acc))) =>
        ((get-integers-t (rest l) (cons (first l) acc)) 
            = (app (rev (get-integers (rest l))) (cons (first l) acc)))
------------------
C6. (listp (rest l)) {C1, C3, Def. listp, Def endp}
C7. (integerlistp (cons (first l) acc)) 
    {C4, C2, instantiating L3 with ((e (first l)) (l acc))}
C8. (get-integers-t (rest l) (cons (first l) acc)) 
      = (app (rev (get-integers (rest l))) (cons (first l) acc)) 
    {C6, C7, C5, MP}

RHS
(app (rev (get-integers l)) acc)
= {def get-integers, C3, C4}
(app (rev (cons (first l) (get-integers (rest l)))) acc)
= {def rev, first-rest axioms, consp axiom, def endp....those last 2 we will be flexible about}
(app (app (rev (get-integers (rest l))) (list (first l))) acc)
= {Associativity of app (to add lemma)}
(app (rev (get-integers (rest l))) (app (list (first l)) acc))
= {Def list, def listp, def app (twice), consp axiom, def endp}
(app (rev (get-integers (rest l))) (cons (first l) acc))
= {C8}
(get-integers-t (rest l)(cons (first l) acc))
= {Def get-integers-t, C3, C4}
(get-integers-t l acc)

4. (listp l) /\ (integerlistp acc) /\ (not (endp l)) /\ 
      (not (integerp (first l))) /\ phi|((l (rest l)) (acc acc)) => phi
Context
C1. (listp l)
C2. (integerlistp acc)
C3. (not (endp l))
C4  (not (integerp (first l)))
C5. ((listp (rest l)) /\ (integerlistp acc)) => (get-integers-t (rest l) acc) = (app (rev (get-integers (rest l))) acc)
----------------
C6. (listp (rest l)) {C1, C3, Def. listp}
C7. (get-integers-t (rest l) acc) = (app (rev (get-integers (rest l))) acc) {C6, C2, C5, MP}

LHS
(get-integers-t l acc)
={C1, C2, C3, C4, Def. get-integers-t}
(get-integers-t (rest l) acc)
={C7}
(app (rev (get-integers (rest l))) acc)
={Def get-integers, C1, C3, C4}
(app (rev (get-integers l)) acc)

All proof obligations were valid
QED
;; ===========================SOLUTION END

(f) List here any lemmas that you used in parts c and d. If any of them are "new", you need
to prove them. (Hint: all lemmas in my solution have appeared in class/notes
before but your proof my differ)
============================SOLUTION START                                                                                                                                                                                
L1: (listp l) => (app l nil) = l
L2: (listp l) => (rev (rev l)) = l
L4: Associativity of app 
(listp x)/\(listp y)/\(listp z) => ((app (app x y) z) = (app x (app y z)))
============================SOLUTION END
|#

#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3.
Consider the following functions, the purpose of which is to compute the
sum-of-digits of a decimal number.  We will do this in 3 parts:
1) Write the tail recursive functions add-digits-t and add-digits*
2) Prove add-digits* = add-digits
3) Write rem-t and rem* and prove rem*=rem

|#

(defthm zero-int-neg (implies (and (natp x) (posp y) 
                                   (not (integerp (/ x y))))
                              (> x 0)))

(defunc rem (x y)
  :input-contract (and (natp x) (posp y))
  :output-contract (natp (rem x y))
  ;; ignore this line
  :body-contracts-hints (("Goal" :use zero-int-neg))
  (if (integerp (/ x y))
    0
    (+ 1 (rem (- x 1) y))))

(defthm phi_rem_shrink (implies (and (natp x)(posp y)(>= x y)) 
                                (< (rem x y) x)))
(defthm phi_rem_nat (implies (and (natp x)(posp y)(>= x y)) 
                                (natp (- x (rem x y)))))
(defthm phi_rem_div (implies (and (natp x)(posp y)(>= x y)) 
                                (natp (/ (- x (rem x y)) y))))
(defthm phi_rem_dec (implies (and (natp x)(posp y)(>= x y))
                             (< (/ (- x (rem x y)) 10) x)))



;; Don't ask why the add-digits needed program
;; mode. The above theorems should have made it work.
:program
(defunc add-digits (x)
  :input-contract (natp x)
  :output-contract (natp (add-digits x))
  (if (< x 10)
    x
    (let ((rem10 (rem x 10)))
      (+ rem10 (add-digits (/ (- x rem10) 10))))))
:logic
;;=========================SOLUTION START
(defunc rem-t (x y acc)
  :input-contract (and (natp x) (posp y)(natp acc))
  :output-contract (natp (rem-t x y acc))
  (if (integerp (/ x y))
    acc
    (rem-t (- x 1) y (+ 1 acc))))

(defunc rem* (x y)
  :input-contract (and (natp x)(posp y))
  :output-contract (natp (rem* x y))
  (rem-t x y 0))
(test? (implies (and (natp x)(posp y)) 
                (equal (rem* x y)(rem x y))))
;;=========================SOLUTION END


;; a)
;; DEFINE add-digits-t and add-digits* (with tests) such that
;; add-digits* calculates the same value for the same
;; inputs as add-digits.
;; For example, we have: (check= (add-digits 12345) 15)
;; (check= (add-digits* 12345) 15) should also pass.
:program
;..............
;;===============================SOLUTION START
(defunc add-digits-t (x acc)
  :input-contract (and (natp x) (natp acc))
  :output-contract (natp (add-digits-t x acc))
  (if (< x 10)
    (+ x acc)
    (let ((rem10 (rem* x 10)))
      (add-digits-t (/ (- x rem10) 10) (+ rem10 acc)))))

(defunc add-digits* (x)
  :input-contract (natp x)
  :output-contract (natp (add-digits* x))
  (add-digits-t x 0))

(test? (implies (natp x)(equal (add-digits* x)(add-digits x))))
(check= (add-digits 12345) 15)
(check= (add-digits* 12345) 15)
(check= (add-digits-t 12345 0) 15)
(check= (add-digits-t 1234 5) 15)#|ACL2s-ToDo-Line|#

;;===============================SOLUTION END
#|


(b) Consider this conjecture:

  (natp x) /\ (natp acc) => (add-digits-t x acc) = (add-digits x) + acc

Using the induction scheme add-digits-t gives rise to, prove this conjecture.
Notice that we don't have to worry about order.  Why is that?

You may use rem10 as an abbreviation for (rem x 10), as done in the
function definition. You can use any lemmas or theorems from
the lectures/homework/notes or from basic arithmetic that you may be using,
but clearly identify them. You may also use the following fact without
proof:

  div-rem :: (natp x) /\ (posp d) => (natp (/ (- x (rem x d)) d))
  
=====================================SOLUTION START
Using the induction scheme for add-digits-t we get the following proof obligations
1) ~((natp x)/\(natp acc)) => phi
2) (natp x)/\(natp acc) /\ (< x 10) => phi
3) (natp x)/\(natp acc) /\~(< x 10) /\ phi|((x (rem x 10))(acc (+ (rem x 10) acc))) => phi

Obligation 1:
C1. ~((natp x)/\(natp acc))
C2. ((natp x)/\(natp acc))
------------
C3. nil


Obligation 2:

C1. (natp x)
C2. (natp acc)
C3. (x < 10)

  (add-digits-t x acc)

= { def. add-digits-t, C3 }

  x + acc

= { def. add-digits, C3 }

  (add-digits x) + acc

Obligation 3:

C1. (natp x)
C2. (natp acc)
C3. (not (x < 10))
C4. (natp (/ (- x rem10) 10)) /\ (natp (+ rem10 acc))
      => (add-digits-t (/ (- x rem10) 10) (+ rem10 acc))
        = (add-digits (/ (- x rem10) 10)) + rem10 + acc
-------------
C5. (natp rem10)              { contract axiom rem }
C6. (natp (/ (- x rem10) 10)) { div-rem: ((d 10)), C1, (posp 10)....or arithmetic }
C7. (natp (+ rem10 acc))      { C5, C2, arithmetic }
C8. (add-digits-t (/ (- x rem10) 10) (+ rem10 acc))
      = (add-digits (/ (- x rem10) 10)) + rem10 + acc { C4, C6, C7, MP }

  (add-digits-t x acc)

= { def. add-digits-t, C3 }

  (add-digits-t (/ (- x rem10) 10) (+ rem10 acc))

= { C8 }

  (add-digits (/ (- x rem10) 10)) + rem10 + acc

= { commutativity of addition }

  (+ rem10 (add-digits (/ (- x rem10) 10))) + acc

= { def. add-digits, C3 }

  (add-digits x) + acc
================================SOLUTION END
  
  
(c) Prove:

  (natp x) => (add-digits* x) = (add-digits x)

Use pure equational reasoning. You can use any lemmas or
theorems from the lectures/homework/notes but clearly identify 
them if you use them.
==============================SOLUTION START
C1. (natp x)

  (add-digits* x)

= { def. add-digits* }

  (add-digits-t x 0)

= { (a): ((acc 0)), C1, (natp 0) }

  (add-digits x) + 0

= { arithmetic }

  (add-digits x)
==============================SOLUTION END
|#
#|
d) Wait.  What about rem??  That's not tail recursive and could lead
to problems. Write function rem* and rem-t such that rem* = rem.
Prove the two functions are equivalent.
Feel free to move the definitions of rem-t and rem* to before add-digits-t
and modify add-digits-t to use them (once you prove rem* = rem of course)
|#
;.................
;;==================SOLUTION START
#|
Lemma_rem: (natp x) /\ (posp y) /\ (natp acc) => (rem-t x y acc) = (acc + (rem x y))

C1. (natp x)
C2. (posp y)

(rem* x y)
= {Def rem*}
(rem-t x y 0)
= {Lemma-rem}
(0 + (rem x y))
= {Arithmetic}
(rem x y)

Proving lemma using IS of rem-t
1) ~((natp x) /\ (posp y) /\ (natp acc)) => phi
2) (natp x) /\ (posp y) /\ (natp acc)/\(integerp (/ x y)) => phi
3) (natp x) /\ (posp y) /\ (natp acc) /\~(integerp (/ x y)) 
   /\ phi|((x (- x 1)) (acc (+ 1 acc))) => phi
   
Case 1: 
C1. (natp x) /\ (posp y) /\ (natp acc)
C2. ~((natp x) /\ (posp y) /\ (natp acc))
------------
C3. nil

Case 2:
C1. (natp x)
C2. (posp y)
C3. (natp acc)
C4. (integerp (/ x y))

(rem-t x y acc)
= {C4, def rem-t}
acc
= {Arithmetic}
(acc + 0)
= {Def rem, C4}
(acc + (rem x y))


Case 3:
C1. (natp x)
C2. (posp y)
C3. (natp acc)
C4. ~(integerp (/ x y))
C5. (natp (- x 1))/\(posp y)/\(natp (+ acc 1)) => 
    ((rem-t (- x 1) y (+ 1 acc)) = (+ (+ 1 acc) (rem (- x 1) y)))
---------------
C6. (natp (- x 1)) {C1, arithmetic, C4}
C7. (natp (+ 1 acc)) {C3, arithmetic}
C8. ( ((rem-t (- x 1) y (+ 1 acc)) = (+ (+ 1 acc) (rem (- x 1) y)))
  {C6, C7, C2, C5, MP}
  
(rem-t x y acc)
= {C4, def rem-t}
(rem-t (- x 1) y  (+ 1 acc))
= {C8}
((acc + 1) (rem (- x 1) y))
= {arithmetic}
(acc + (1 + (rem (- x 1) y)))
= { def rem, C4}
(acc + (rem x y)     
============================SOLUTION END
|#

#| EXTRA PRACTICE ???
If you want additional practice problems, try writing tail recursive functions
for the following functions and then prove they are equivalent to the original
   - min-l
   - delete
   - merge
In fact, for many functions that aren't already tail recursive, you can write a tail
recursive version and then prove the equivalence. You can generate your own problems.
   
|#