Automatic pick-a-point proofs of subset.
The rewrite rule
(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
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.
(defun subset-trigger (x y) (declare (xargs :guard (and (setp x) (setp y)))) (subset x y))
(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))))
(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))))))
(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)))))