		Search-engine friendly clone of the ACL2 documentation.

Std/osets

Double-containment

A strategy for proving sets are equal because they are subsets of one another.

Double containment can be a good way to prove that two sets are equal to one another.

Unfortunately, because this rule targets equal it can get quite expensive. You may sometimes wish to disable it to speed up your proofs, as directed by accumulated-persistence. In fact, this rule is disabled when importing [books]/std/osets/top.lisp. To reduce its cost when enabled, this rule has a backchain limit.

On the other hand, there are cases in which this rule works well, and where the backchain limit is detrimental. For this reason, we also provide a version of the rule that has no backchain limit. This version can be enabled as needed.

Definitions and Theorems

Theorem: double-containment

(defthm double-containment
  (implies (and (setp x) (setp y))
           (equal (equal x y)
                  (and (subset x y) (subset y x))))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: double-containment-no-backchain-limit

(defthm double-containment-no-backchain-limit
  (implies (and (setp x) (setp y))
           (equal (equal x y)
                  (and (subset x y) (subset y x)))))