A database used to extend
Although this table has nothing to do with soundness, the rules it lists are intended to obey the untranslate contract—that is, the replacements listed for each pattern should macro-expand to their targets. If this property is violated, proof output might become very confusing! For example, a rule that displays calls to member as if they were calls to subsetp would make proof output very difficult to understand.
We do nothing to enforce this contract. Hence, a sensible user must ensure that their use of this table is disciplined.
This function is just an inefficient check for if a natural number is even or odd, using a flag-based mutual recursion scheme.
(defun even/odd-p (flg x) (declare (xargs :guard (and (or (eq flg 'even) (eq flg 'odd)) (natp x)))) (if (eq flg 'even) (if (zp x) t (even/odd-p 'odd (1- x))) (if (zp x) nil (even/odd-p 'even (1- x)))))
Something simple you might want to do with this is 'hide' the flag function with macros such as the following:
But of course in proofs you will still see the flag functions. To hide
these flags, you can call the macro
(add-untranslate-pattern (even/odd-p 'even ?x) (even-p ?x)) (add-untranslate-pattern (even/odd-p 'odd ?x) (odd-p ?x))
The effect of these patterns can be seen by submitting the following
commands. We first disable the type prescription of
(in-theory (disable (:definition even/odd-p) (:type-prescription even/odd-p))) (thm (equal (+ (even-p x) (even-p y)) (+ (odd-p y) (odd-p x))))
Some of the proof output generated is now as follows:
Subgoal *1/2 (IMPLIES (AND (NOT (EQ 'ODD 'EVEN)) (NOT (ZP X)) (EQUAL (+ (EVEN-P (+ -1 X)) (EVEN-P Y)) (+ (ODD-P (+ -1 X)) (ODD-P Y)))) (EQUAL (+ (EVEN-P X) (EVEN-P Y)) (+ (ODD-P X) (ODD-P Y)))). Subgoal *1/2' (IMPLIES (AND (NOT (ZP X)) (EQUAL (+ (EVEN-P (+ -1 X)) (EVEN-P Y)) (+ (ODD-P (+ -1 X)) (ODD-P Y)))) (EQUAL (+ (EVEN-P X) (EVEN-P Y)) (+ (ODD-P X) (ODD-P Y)))).
As you can see,
Matt Kaufmann suggested the following challenge problem, inspired by the hand-written untranslation routine for the RTL library. We begin with the following code:
(defun foo$ (n $path) (cons n $path)) (defmacro foo (x) `(foo$ ,x $path)) (add-macro-alias foo foo$) (in-theory (disable foo))
The theorem Matt proposed looking at was the following:
With no support for untranslate, this theorem ends up producing the following goal:
The RTL untranslator can handle this given the following command:
(table rtl-tbl 'sigs-btree (symbol-alist-to-btree (dollar-alist '(foo) nil)))
This yields the following, nice goal:
Matt challenged me to come up with a system that would rewrite only $path. Using the untranslate pattern table, here is the command:
(add-untranslate-pattern (foo$ ?n $path) (foo ?n))
As you can see, it produces exactly the same output:
The syntax for these patterns is as follows:
Any quoted constant matches with a quoted constant. Note that numbers and so forth must be MANUALLY quoted.
Unquoted symbols behave as follows:
So, for example, the pattern
Similarly, the pattern