• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
      • Omaps
      • All-by-membership
      • Defset
      • In
      • Primitives
        • Setp
        • Insert
          • Weak-insert-induction
        • Head
        • Tail
        • Sfix
        • Emptyp
      • Subset
      • Mergesort
      • Intersect
      • Union
      • Pick-a-point-subset-strategy
      • Delete
      • Double-containment
      • Difference
      • Cardinality
      • Set
      • Intersectp
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Insert

Weak-insert-induction

Inducting over insert without exposing the set order.

When we want to insert an element into an ordered set, the set order obviously has to be involved so that we can decide where to put the new element. Accordingly, the set order plays a role in the induction scheme that we get from insert's definition. This makes insert somewhat different than other set operations (membership, union, cardinality, etc.) that just use a simple tail-based induction, where the set order is already hidden by tail.

When we are proving theorems about sets, we generally want to avoid thinking about the set order, but we sometimes need to induct over insert. So, here we introduce a new induction scheme that allows us to induct over insert but hides the set order. We disable the ordinary induction scheme that insert uses, and set up an induction hint so that weak-insert-induction will automatically be used instead.

Definitions and Theorems

Theorem: weak-insert-induction-helper-1

(defthm weak-insert-induction-helper-1
  (implies (and (not (in a x))
                (not (equal (head (insert a x)) a)))
           (equal (head (insert a x)) (head x))))

Theorem: weak-insert-induction-helper-2

(defthm weak-insert-induction-helper-2
  (implies (and (not (in a x))
                (not (equal (head (insert a x)) a)))
           (equal (tail (insert a x))
                  (insert a (tail x)))))

Theorem: weak-insert-induction-helper-3

(defthm weak-insert-induction-helper-3
  (implies (and (not (in a x))
                (equal (head (insert a x)) a))
           (equal (tail (insert a x)) (sfix x))))

Function: weak-insert-induction

(defun weak-insert-induction (a x)
  (declare (xargs :guard (setp x)))
  (cond ((emptyp x) nil)
        ((in a x) nil)
        ((equal (head (insert a x)) a) nil)
        (t (list (weak-insert-induction a (tail x))))))

Theorem: use-weak-insert-induction

(defthm use-weak-insert-induction
  t
  :rule-classes ((:induction :pattern (insert a x)
                             :scheme (weak-insert-induction a x))))