a defproperty that runs in Dracula, but won't admit

racket-bug-submit commented 12 years ago

Originally submitted on: Wed Oct 29 18:56:01 -0400 2008

Property definitions usually admit under the ACL2 mode in Dracula, but there seems to be at least one case where a runnable property fails to admit

Steps to Reproduce:

(include-book "doublecheck" :dir :teachpacks)
(defun is-prefix (ps xs)
  (or (endp ps)
      (and (not (endp xs))
           (equal (car ps) (car xs))
           (is-prefix (cdr ps) (cdr xs)))))
(defun pattern-in (ps xs)
  (if (endp xs)
      (endp ps)
      (or (is-prefix ps xs)
          (pattern-in ps (cdr xs)))))

;(match-prefix ps xs) = (qs rs ys)
;   where qs = longest sequence prefixing is both ps and xs
;         (append qs rs) = ps  --ie, rs is what's left of ps
;     and (append qs ys) = xs  --ie, ys is what's left of xs
(defun match-prefix (ps xs)
  (if (or (endp ps) (endp xs)
          (not (equal (car ps) (car xs))))
      (list nil ps xs)
      (let* ((pspsxs (match-prefix (cdr ps) (cdr xs))))
        (list (cons (car ps) (car pspsxs))
              (cadr pspsxs)
              (caddr pspsxs)))))

; (break-at-prefix ps xs) = (before after)
;   where (append before ps after) = xs if ps occurs in xs
;     and before = xs, after=nil otherwise
(defun break-at-pattern (ps xs)
  (if (endp xs)
      (list nil nil)
      (let* ((pspsxs (match-prefix ps xs)))
        (if (null (cadr pspsxs))
            (list nil (caddr pspsxs))
            (let* ((xsxs (break-at-pattern ps (cdr xs))))
              (list (cons (car xs) (car xsxs))
                    (cadr xsxs)))))))

(defproperty bap-when-pattern-present-tst
  (ps :value (random-list-of (random-integer))
   xs :value (random-list-of (random-integer)))
  (implies (and (true-listp ps)
                (true-listp xs)
                (pattern-in ps xs))
           (equal (append (car (break-at-pattern ps xs))
                          ps
                          (cadr (break-at-pattern ps xs)))
                  xs)))

Release:

4.1

Environment:

windows "Windows NT 5.1 (Build 2600) Service Pack 3" (win32\i386\3m) (get-display-depth) = 32 Human Language: english (current-memory-use) 98983816

Collections: (("C:\Documents and Settings\Rex Page\Application Data\PLT Scheme\4.1\collects" non-existent-path) ("C:\Program Files\PLT\collects" "afm" "algol60" "browser" "combinator-parser" "compiler" "config" "defaults" "drscheme" "dynext" "embedded-gui" "eopl" "errortrace" "ffi" "file" "framework" "frtime" "games" "graphics" "gui-debugger" "help" "hierlist" "htdch" "htdp" "html" "icons" "info-domain" "lang" "launcher" "lazy" "macro-debugger" "make" "mred" "mrlib" "mysterx" "mzcom" "mzlib" "mzscheme" "net" "openssl" "parser-tools" "planet" "plot" "preprocessor" "profj" "r5rs" "r6rs" "readline" "redex" "rnrs" "s-exp" "scheme" "scribble" "scribblings" "setup" "sgl" "slatex" "slideshow" "srfi" "stepper" "string-constants" "swindle" "syntax" "syntax-color" "teachpack" "test-box-recovery" "test-engine" "tex2page" "texpict" "trace" "typed-scheme" "version" "web-server" "wxme" "xml")) Computer Language: (("Dracula Languages" "Dracula v4.2") (#("C:\ACL2-3.3\bin\acl2.exe" #f) . #(#t write mixed-fraction-e #f #t debug)))

This bug was converted from Gnats bug 9876.

[anon-submit page AT ou.edu]

racket-bug-submit commented 12 years ago

On Wed, 29 Oct 2008 20:22:56 -0400, cce@plt-scheme.org wrote:

Rex, this is not a bug.  The random testing defproperty performs at
runtime neither guarantees the logical truth of a claim, nor aids
ACL2's proof search.  There are many defproperty terms that run
successfully but nevertheless will not admit.  To find the problem,
you'll have to either find a counterexample by refining the random
distributions or prove the theorem correct by applying normal ACL2
techniques.

--Carl

On Wed, Oct 29, 2008 at 6:56 PM,  <page@ou.edu> wrote:
> A new problem report is waiting at
>  http://bugs.plt-scheme.org/query/?cmd=view&pr=9876
>
> Reported by Rex Page for release: 4.1
>
> *** Description:
> Property definitions usually admit under the ACL2 mode in Dracula, but there seems to be at least one case where a runnable property fails to admit

racket-bug-submit commented 12 years ago

On Wed, 29 Oct 2008 20:24:53 -0400, cce classified this bug as not-a-bug

DoubleCheck's random testing does not guarantee successful theorem proving.

racket-bug-submit commented 12 years ago

samth / test-bugs