#|
Question 4:

It would be really silly to have our compiler pass accidentally leave
some NOTs or some ANDs or some ORs in the code. See if you can prove
the contract for compile. As before, you don't get to assume the
contract holds for be, but the induction principle will let you assume
it holds for pieces of be.

Formalize in ACL2s the following statements, perform contact checking
and completion and provide proofs.

4a: Suppose  (booleanp be).
Prove that   (cexp (compile be)).

FORMALIZATION:

(implies (booleanp be)
         (cexp (compile be)))

CONTRACT CHECKING AND COMPLETION:

(implies (and (booleanp be)
              (bexp be))
         (cexp (compile be)))

PROOF:

C1. (booleanp be)
C2. (bexp be)

(cexp (compile be))
  = { Def compile, C1 }
(cexp be)
  = { Def cexp, C1 }
t


4b: Suppose (varp be).
Prove that  (cexp (compile be)).

FORMALIZATION:

(implies (varp be)
         (cexp (compile be)))

CONTRACT CHECKING AND COMPLETION:

(implies (and (varp be)
              (bexp be))
         (cexp (compile be)))

PROOF:

C1. (varp be)
C2. (bexp be)

(cexp (compile be))
  = { Def compile, C1 }
(cexp be)
  = { Def cexp, C1 }
t

4c: Suppose (bex-notp be) and
            (cexp (compile (second be))).
Prove that  (cexp (compile be)).

FORMALIZATION:

(implies (and (bex-notp be)
              (cexp (compile (second be))))
         (cexp (compile be)))

CONTRACT CHECKING AND COMPLETION:

(implies (and (bex-notp be)
              (cexp (compile (second be)))
              (bexp be))
         (cexp (compile be)))

PROOF:

C1. (bex-notp be)
C2. (cexp (compile (second be)))
C3. (bexp be)

(cexp (compile be))
  = { Def compile, C1 }
(cexp (list 'nand
            (compile (second be))
            (compile (second be))))
  = { Def cexp, C2 }
(cexp (list 'nand
            cex
            cex)
  = { Def cexp }
t

4d: Suppose (bex-andp be) and
            (cexp (compile (second be)))
            (cexp (compile (third be))).
Prove that  (cexp (compile be)).

FORMALIZATION:

(implies (and (bex-andp be)
              (cexp (compile (second be))))
              (cexp (compile (third be)))
         (cexp (compile be)))

CONTRACT CHECKING AND COMPLETION:

(implies (and (bex-andp be)
              (cexp (compile (second be)))
              (cexp (compile (third be)))
              (listp be)
              (bexp be))
         (cexp (compile be)))

PROOF:

C1. (bex-andp be)
C2. (cexp (compile (second be)))
C3. (cexp (compile (third be)))
C4. (bexp be)
(cexp (compile be))
  = { Def compile, C1 }
(cexp  (list 'nand
               (list 'nand
                     (compile (second be))
                     (compile (third be)))
               (list 'nand
                     (compile (second be))
                     (compile (third be)))))
  = { Def cexp, C2 C3 }
(cexp (list 'nand
            (list 'nand
                  cex
                  cex)
            (list 'nand
                  cex
                  cex)))
  = { Def cexp }
(cexp (list 'nand
             cex
             cex))
  = { Def cexp }
t

4e: Suppose (bex-orp be) and
            (cexp (compile (second be)))
            (cexp (compile (third be))).
Prove that  (cexp (compile be)).

FORMALIZATION:

(implies (and (bex-orp be)
              (cexp (compile (second be))))
              (cexp (compile (third be)))
         (cexp (compile be)))

CONTRACT CHECKING AND COMPLETION:

(implies (and (bex-orp be)
              (cexp (compile (second be)))
              (cexp (compile (third be)))
              (listp be)
              (bexp be))
         (cexp (compile be)))

PROOF:

C1. (bex-orp be)
C2. (cexp (compile (second be)))
C3. (cexp (compile (third be)))
C4. (bexp be)
(cexp (compile be))
  = { Def compile, C1 }
(cexp  (list 'nand
               (list 'nand
                     (compile (second be))
                     (compile (second be)))
               (list 'nand
                     (compile (third be))
                     (compile (third be)))))
  = { Def cexp, C2 C3 }
(cexp (list 'nand
            (list 'nand
                  cex
                  cex)
            (list 'nand
                  cex
                  cex)))
  = { Def cexp }
(cexp (list 'nand
             cex
             cex))
  = { Def cexp }
t