A solution to quantifier-tutorial Exercise 2
In quantifier-tutorial exercise 2, it asks if we can prove or disprove the conjecture below.
Exercise 2. If there is an ACL2 object
xwhich satisfies M, then there exists a least ACL2 object ythat satisfies M.
This hypothesis can be disproved. Here is one possible solution, provided by Yan Peng..
(in-package "ACL2") (include-book "misc/total-order" :dir :system) ;; This hypothesis can be disproved. ;; The intuition: find a function M that can be satisfied and does not have a ;; minimal object that satisfies it. ;; For example, if M is evenp, then for any ACL2 object that satisfies M, one ;; can always construct a smaller object by subtracting 2 from it, which also ;; satisfies M. ;; Instead of using defstub, we provide an implementation for M which calls ;; evenp. (defun M (x) (evenp x)) ;; We prove a helper lemma that says if x satisfies M, then (- x 2) also ;; satisfies M and it is a smaller object. (defthm -2-satisfies-M-and-<< (implies (M x) (and (M (- x 2)) (<< (- x 2) x))) :hints (("Goal" :in-theory (enable << lexorder alphorder)))) (in-theory (disable evenp M)) (defun-sk some-M () (exists x (M x))) (in-theory (disable some-M some-M-suff)) ;; We prove M can be satisfied by providing a witness 0. (defthm some-M-lemma (some-M) :hints (("Goal" :use ((:instance some-M-suff (x 0)))))) ;; We negate none-below-2 (defun-sk exists-below (y) (exists r (and (<< r y) (M r)))) (in-theory (disable exists-below exists-below-suff)) ;; We negate min-M2 (defun-sk not-min-M () (forall y (implies (M y) (exists-below y)))) (in-theory (disable not-min-M not-min-M-necc)) ;; We prove that forall y, if y satisfies M, then there exists another smaller ;; object that satisfies M. (defthm not-min-M-lemma (not-min-M) :hints (("Goal" :use (;; The definition of not-min-M provides a witness ;; (not-min-M-witness) that satisfies M but doesn't satisfy ;; exists-below. (:instance (:definition not-min-M)) ;; By instantiating exists-below-suff, we provide a smaller ;; object r:(- (not-min-M-witness) 2) than ;; y:(not-min-M-witness), and satisfies M. This makes ;; (not-min-M-witness) vacuous, allowing us to prove the ;; forall. (:instance exists-below-suff (r (- (not-min-M-witness) 2)) (y (not-min-M-witness))))))) ;; We prove both some-M and not-min-M (defthm |minimal does not exist| (and (some-M) (not-min-M)))