NthCdr

Purpose of exercise

Activities

Terminology

Properties

  1. NthCdr delivers true-lists
  2. (NthCdr n xs) equals nil if n is (len xs) or larger
    Note: As a theorem, this property is most useful when it triggers rewriting an NthCdr invocation to nil. This is possible when the property is stated using "equal" rather than "null". This makes the theorem an equivalence relation, which allows ACL2 to use its properties of reflexivity, symmetry, and transitivity more effectively.
  3. NthCdr reduces the length of a non-empty list.
    Note: Since the conclusion of this theorem states a numeric inequality, it has many algebraic corollaries. ACL2 can often make better use of these corollaries if the statement of the theorem places it in the linear rule-class.
  4. (NthCdr n xs) is exactly n less than the length of xs if xs is long enough.
    Note: Since the conclusion of this theorem states an equality, ACL2 uses it as an equivalence relation, which makes many rewrites possible. In this particular case, those rewrites often turn out to be infinite regresses, so it is best to disable the theorem from the outset (defthmD) and include a use-instance hint in theorems where this one serves as a supportive lemma.
  5. (NthCdr n xs) is nil of n is at least as large as (len xs)
  6. (NthCdr m xs) is empty if (NthCdr n xs) is and m is at least as large as n.
  7. NthCdr is additive: (NthCdr (+ n m) xs) is the same as (NthCdr n (NthCdr m xs))
    Note: This is another equivalence relation that often triggers infinite rewrites. Best to define it as disabled (defthmD) and include a use-instance hint when you need it.
    Note: Certain algebraic identities, such as those found in the arithmetic3/top book, are helpful in proving this theorem.
  8. State a special case of the NthCdr-is-additive theorem, based on the following identity: kn = n + (k-1)n
    Note: This theorem can be proved without induction by applying the NthCdr-is-additive theorem, if ACL2 has access to the usual algebraic identities (such as those found in the arithmetic3/top book). 
  9. (cdr (NthCdr n xs)) is (NthCdr (+ n 1) xs)
    Note: This is yet another equivalence relation that can trigger infinite rewrites. Best to define it as disabled (defthmD) and include a use-instance hint when you need it.
  10. NthCdr delivers a list of length zero if its first argument is at least as large as the length of its second argument.
  11. (Nth k xs) is (car (NthCdr k xs)) 

ACL2 instrinsics and other functions useful in this exercise

Useful books of theorems

Notes

Using NthCdr sometimes complicates termination proofs, which ACL2 must do to admit newly defined functions into the logic. This book can be helpful in that process, and in verifying other properties of software that invokes NthCdr.