#|

Lab 5 Problem Set.

In line with the next homework, in this lab we will do some logic
exercises. This is very new material, so expect to get stuck here and
there. The purpose of the lab is precisely to help you get unstuck
immediately, rather than having to wait for the next office hour. So try
these at home, and come prepared with questions.

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; A. Substitutions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; The following are somewhat tricky substitution questions. Think about
; them, and ask if you cannot solve them. Their purpose is to sharpen your
; understanding of substitutions, rather than routine practice (the
; homework will help you with the latter).

#|

1. Let sigma1 = ((a b)) and sigma2 = ((b a)). Then, for any formula phi,
(phi|sigma1)|sigma2 = phi. True or false? If true, explain why. If false,
give a counterexample.

...

2. Let sigma = ((a b) (b a)). Then, for any formula phi,
(phi|sigma)|sigma = phi. True or false? If true, explain why.
If false, give a counterexample.

...

3. For any formula phi and any substitution sigma,
(phi|sigma)|sigma = phi|sigma . True or false? If true, explain why.
If false, give a counterexample.

...

4. Give an example of two formulas f and g and a substitution sigma such that
all of the following hold: (i) f and g are *not* logically equivalent,
(ii) f|sigma = g, and (iii) g|sigma = f.

...

5. Give an example of a formula g such that, for any substitution
sigma, the formula g|sigma is *not* valid.

...

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; B. Equational Reasoning
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

For the following conjectures:

- first perform conjecture contract checking. This is required NO MATTER
  whether you think the conjecture is true or false!

- then predict whether the conjecture is true or false.
  If false, you should be able to find a counterexample.
  If true, prove it by equational reasoning.

cons, rest, and arithmetic functions are built in -- all we know about them
is the axioms that define them; see the ACL2s lecture notes.

Here are some other functions' definitions:

(defunc len (l)
  :input-contract (listp l)
  :output-contract (natp (len l))
  (if (endp l)
    0
    (+ 1 (len (rest l)))))

(defunc app (a b)
  :input-contract (and (listp a) (listp b))
  :output-contract (listp (app a b))
  (if (endp a)
    b
    (cons (first a) (app (rest a) b))))

(defunc dup (x)
  :input-contract (listp x)
  :output-contract (listp (dup x))
  (if (endp x)
    nil
    (cons (first x) (cons (first x) (dup (rest x))))))

Warning: some of the below conjectures are "odd" -- they seem to make no
sense. How do we wiggle ourselves out of this situation? Can logic help?

|#

#|

6. (len (cons a l)) = l + 1

7. (len (cons a l)) = (len l) + 1

8. (len (rest l)) = (len l) - 1

9. (len (cons l1 l2)) = (len l1) + (len l2)

10. l = () v (len (cons a l)) >= 2

11. (app (cons x y) z) = (cons x (app y z))

Advanced:

12. (len (dup x)) = 2 * (len x) => (len (dup (cons a x))) = 2 * (len (cons a x))

|#