• Top
  • Documentation
    • Xdoc
    • ACL2-doc
    • Recursion-and-induction
      • R-and-i-annotated-bibliography
      • R-and-i-definitions-revisited
      • R-and-i-terms
      • R-and-i-structural-induction
      • R-and-i-relations-between-recursion-and-induction
      • R-and-i-ordinals
      • R-and-i-inadequacies-of-structural-recursion
      • R-and-i-axioms
      • R-and-i-abbreviations-for-terms
      • R-and-i-terms-as-formulas
      • R-and-i-more-problems
      • R-and-i-still-more-problems
      • R-and-i-definitional-principle
      • R-and-i-function-definitions
      • R-and-i-introduction
      • R-and-i-table-of-contents
      • R-and-i-substitutions
      • R-and-i-arithmetic
        • R-and-i-ACL2-arithmetic
        • R-and-i-peano-arithmetic
      • R-and-i-induction-principle
      • R-and-i-data-types
      • R-and-i-more-inadequacies-of-the-definitional-principle
    • Loop$-primer
    • Operational-semantics
    • Pointers
    • Doc
    • Documentation-copyright
    • Publications
    • Course-materials
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• R-and-i-arithmetic

R-and-i-peano-arithmetic

Recursion and Induction: Peano Arithmetic

Recall that the integers are being treated as atomic objects in this document. But we can explore elementary arithmetic by thinking of a list of n  nils as a representation for the natural number n. We will call such a list a “nat.” Thus, (nil nil nil) is a nat, but 3 is a natural number.

Problem 65.
Define (nat x) to recognize nats.

Problem 66.
Define (plus x y) to take two arbitrary lists (even ones that are not nats) and to return the nat representing the sum of their lengths. By defining plus this way we ensure that it always returns a nat and that it is commutative.

Problem 67.
Define (times x y) to take two arbitrary lists and to return the nat representing the product of their lengths.

Problem 68.
Define (power x y) to take two arbitrary lists and to return the nat representing the exponentiation of their lengths, i.e., if x and y are of lengths i  and j, then (power x y) should return the nat representing i^j.

Problem 69.
Define (lesseqp x y) to return t or nil according to whether the length of x is less than or equal to that of y.

Problem 70.
Define (evennat x) to return t or nil according to whether the length of x is even.

Problem 71.
Prove

(implies (nat i) 
         (equal (plus i nil) i)) 

Problem 72.
Prove

(equal (plus (plus i j) k) 
       (plus i (plus j k))) 

Problem 73.
Prove

(equal (plus i j) (plus j i)) 

Problem 74.
Prove

(equal (times (times i j) k) 
       (times i (times j k))) 

Problem 75.
Prove

(equal (times i j) (times j i)) 

Problem 76.
Prove

(equal (power b (plus i j)) 
       (times (power b i) (power b j))) 

Problem 77.
Prove

(equal (power (power b i) j) 
       (power b (times i j))) 

Problem 78.
Prove

(lesseqp i i) 

Problem 79.
Prove

(implies (and (lesseqp i j) 
              (lesseqp j k)) 
         (lesseqp i k)) 

Problem 80.
Prove

(equal (lesseqp (plus i j) (plus i k)) 
       (lesseqp j k)) 

Problem 81.
Prove

(implies (and (evennat i) 
              (evennat j)) 
         (evennat (plus i j))) 

Next: ACL2 Arithmetic (or Table of Contents)