1
$\begingroup$

I have been trying various things to try to prove that the product of two positive rationals is positive in ACL2, see here for one attempt.

Recently, I entered the following Skolem function via defun-sk and was pleased that that ACL2 accepted it.

(defun-sk numerator-denominator-exist (z)
  (exists x
    (and (integerp (car x))
         (integerp (cadr x))
         (= z (/ (car x) (cdr x))))))

Intuitively, this function shows that the following proposition holds (with the domain of discourse being the ACL2 universe):

$$ [\forall z \in \mathbb{Q}] [\exists x] (\text{fst}(x) \in \mathbb{Z} \land \text{snd}(x) \in \mathbb{Z} \land \text{fst}(x) / \text{snd}(x) = z) $$

However, ACL2 appears not to actually check that the Skolem function witnesses the proposition that it corresponds to.

For example, the Toplevel will happily admit this defun-sk.

(defun-sk non-rejected-skolem-function ()
  (exists z (not (= z z))))

Is there a way to get ACL2 to check whether a Skolem function actually witnesses the truth of the proposition that it corresponds to?

$\endgroup$

2 Answers 2

1
$\begingroup$

defun-sk only defines a proposition. I.e., for your (defun-sk numerator-denominator-exist ...) example, this event will generate a function numerator-denominator-exist which is constrained to return t iff the existential you wrote holds. The defun-sk event itself does not try to prove or disprove the defined proposition. You can try to prove it yourself using a defthm:

(defthm numerator-denominator-exists
  (numerator-denominator-exist z)
  :hints ...)

If you are going to use skolem functions, I'd suggest closely reading :doc defchoose, the underlying mechanism used by the defun-sk macro, to understand how underconstrained functions are generated, and the key axiom introduced. Although I'd suggest avoiding all if this as possible as a beginner. Proofs using skolem functions tend to necessitate giving precise :use hints in a way that would usually be avoided in ACL2. Consider instead of proving for all z there exists some x such that whatever, write a function which takes z and evaluates to the witness x, and then proof that the desired condition holds on any evaluation of the function.

$\endgroup$
1
$\begingroup$

The best advice I can give you with respect to defun-sk is that once you use ACL2 enough you will realize that you can usually get away without it. The reason being that usually if you want to construct something in some environment you just define a function that constructs the object explicitly (ie. my-witness below), and if you want to have an existential in the hypothesis its the same as having it be universally quantified.

Nevertheless here's how you would go about your example:

(defun deconstruct (z x)
  (and (integerp (car x))
       (integerp (cadr x))
       (= z (/ (car x) (cadr x)))))

(defun-sk nd (z)
  (exists (x)
          (deconstruct z x)))

;; this generates the following definition
(DEFUN ND (Z)
   (DECONSTRUCT Z (ND-WITNESS Z)))

;; satisfying the theorem
(DEFTHM ND-SUFF
   (IMPLIES (DECONSTRUCT Z X) (ND Z)))

(defthm nd-imp-rat
    (implies (nd z)
             (rationalp z)))

(defun my-witness (z)
    (list (numerator z) (denominator z)))

(defthm rat-imp-nd
    (implies (rationalp z)
             (nd z))
  :hints 
  (("Goal" :use ((:instance nd-suff
                  (x (my-witness z))))))))
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.