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

• Std/osets

Pick-a-point-subset-strategy

Automatic pick-a-point proofs of subset.

The rewrite rule pick-a-point-subset-strategy tries to automatically reduce proof goals such as:

(implies hyps
         (subset X Y))

To proofs of:

(implies (and hyps (in a X))
         (in a Y))

The mechanism for doing this is somewhat elaborate: the rewrite rule replaces the (subset X Y) with (subset-trigger X Y). This trigger is recognized by a computed hint, which then suggest proving the theorem via functional instantiation of all-by-membership.

The pick-a-point method is often a good way to prove subset relations. On the other hand, this rule is very heavy-handed, and you may need to disable it if you do not want to use the pick-a-point method to solve your goal.

Definitions and Theorems

Function: subset-trigger

(defun subset-trigger (x y)
       (declare (xargs :guard (and (setp x) (setp y))))
       (subset x y))

Theorem: pick-a-point-subset-strategy

(defthm
 pick-a-point-subset-strategy
 (implies
  (and
      (syntaxp (rewriting-goal-lit mfc state))
      (syntaxp
           (rewriting-conc-lit (cons 'subset (cons x (cons y 'nil)))
                               mfc state)))
  (equal (subset x y)
         (subset-trigger x y))))

Function: pick-a-point-subset-hint

(defun
 pick-a-point-subset-hint
 (id clause world computed-hints::stable)
 (declare (ignore id world))
 (if
  (not computed-hints::stable)
  nil
  (let
   ((computed-hints::triggers
         (computed-hints::harvest-trigger clause 'subset-trigger)))
   (if
    (not computed-hints::triggers)
    nil
    (let*
     ((computed-hints::others
           (set-difference-equal clause computed-hints::triggers))
      (computed-hints::hyps
           (computed-hints::others-to-hyps computed-hints::others))
      (computed-hints::fi-hints
           (computed-hints::build-hints
                computed-hints::triggers
                'all-by-membership
                'all-hyps
                'all-set
                'predicate
                'all
                'subset
                computed-hints::hyps
                '(((predicate ?x ?y) (in ?x ?y)))))
      (computed-hints::hints
           (list :use computed-hints::fi-hints
                 :expand computed-hints::triggers)))
     (prog2$
      (cw
       "~|~%Attempting to discharge subgoal by a ~
                            pick-a-point strategy; disable ~x0 to ~
                            prevent this.~%~%"
       'pick-a-point-subset-strategy)
      computed-hints::hints))))))

Theorem: pick-a-point-subset-constraint-helper

(defthm pick-a-point-subset-constraint-helper
        (implies (syntaxp (equal set-for-all-reduction
                                 'set-for-all-reduction))
                 (equal (subset set-for-all-reduction rhs)
                        (cond ((empty set-for-all-reduction) t)
                              ((in (head set-for-all-reduction) rhs)
                               (subset (tail set-for-all-reduction)
                                       rhs))
                              (t nil)))))