Advanced extralogical programming of FGL.
While FGL can be used to symbolically simulate logical terms and bitblast theorems, it can also be used as a programming platform for advanced algorithms involving SAT checks and a mix of logical and extralogical code.
Suppose we want to check whether several conditions are satisfiable, summarize the results in an object and pretty-print that summary.
;; Suppose (my-test-condition n x) gives the nth condition to be tested. (defun my-test-condition (n x) ...) ;; Iterate from M-1 down to 0 testing each condition and collect a list of the ;; indices of all those that were invalid. (def-fgl-program test-my-conditions (m x) (if (zp m) nil (let* ((next-m (1- m)) ;; Narrow the equivalence context from UNEQUIV to IFF to ensure ;; that an accurate result is produced for my-test-condition. (testcond (narrow-equiv '(iff) (my-test-condition next-m x))) (validity-check-result (fgl-validity-check (make-fgl-ipasir-config) testcond)) ;; Note: validity-check-result is syntactically T if the validity ;; check was successful. If not, it's some symbolic truth value ;; represented as a g-boolean object. (valid (syntax-interp (eq validity-check-result t)))) (if valid (test-my-conditions next-m x) (cons next-m (test-my-conditions next-m x)))))) ;; Summarize the list of non-valid condition indices. (defun my-print-test-condition-results (indices-list) ...) ;; Run a fake proof in which the conditions are tested. (fgl-thm :hyp t :concl (fgl-prog2 (let ((conds (test-my-conditions 100 x))) (my-print-test-condition-results conds)) t))
Note that the body for
Examining counterexamples: The following example shows how to generate all of the Pythagorean triples of a given size, by checking repeatedly whether there exists another triple that is missing from the list.
(define pythag-triple-p ((x natp) (y natp) (z natp)) (and (< 0 (lnfix x)) (<= (lnfix x) (lnfix y)) (equal (* (lnfix z) (lnfix z)) (+ (* (lnfix x) (lnfix x)) (* (lnfix y) (lnfix y)))))) (def-fgl-program find-all-pythag-triples (x y z found) (b* ((cond (narrow-equiv '(iff) (and (not (member-equal (list x y z) found)) (pythag-triple-p x y z)))) (config (make-fgl-ipasir-config)) (sat-res (fgl-sat-check config cond)) (unsat (syntax-interp (not sat-res))) ((when unsat) found) ((list (list error bindings ?vars) &) (syntax-interp (show-counterexample-bind config interp-st state))) ((when error) (cw "Error: ~x0~%" error)) (xval (cdr (assoc 'x bindings))) (yval (cdr (assoc 'y bindings))) (zval (cdr (assoc 'z bindings))) (list (list xval yval zval)) ((unless (and (pythag-triple-p xval yval zval) (not (member-equal list found)))) (fgl-prog2 (syntax-interp (cw "Bad: result: ~x0 found: ~x1~%" list found)) nil))) (find-all-pythag-triples x y z (cons list found)))) (def-fgl-program add-scratch-pair (key val) (syntax-interp (interp-st-put-user-scratch key val interp-st))) (local (in-theory (disable w))) (fancy-ev-add-primitive interp-st-put-user-scratch t) (def-fancy-ev-primitives mine) (fgl-thm :hyp (and (unsigned-byte-p 7 x) (unsigned-byte-p 7 y) (unsigned-byte-p 7 z)) :concl (fgl-prog2 (b* ((trips (find-all-pythag-triples x y z nil))) ;; Store the generated triples in the user-scratch ;; field of the interp-st. (fgl-prog2 (add-scratch-pair :pythag-triples trips) (cw "trips: ~x0~%" trips))) t)) (make-event ;; Fetch the stored triples from the user-scratch field. (b* ((trips (g-concrete->val (cdr (hons-get :pythag-triples (interp-st->user-scratch interp-st)))))) `(def-fgl-thm 7-bit-pythag-trips :hyp (and (unsigned-byte-p 7 x) (unsigned-byte-p 7 y) (unsigned-byte-p 7 z)) :concl (implies (not (member-equal (list x y z) ',trips)) (not (pythag-triple-p x y z))))))