# 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 suggests 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 ((emptyp set-for-all-reduction) t)
((in (head set-for-all-reduction) rhs)
(subset (tail set-for-all-reduction)
rhs))
(t nil)))))