|
|
|---|
|
|
|
|---|
Create an induction scheme that adds a duplicate variable to the substitution.
Certain types of proofs require inductions that are rather simple modifications of existing induction schemes. For example, to prove a congruence on some recursive function, typically you want to induct almost on that function, but with the simple modification that for each substitution in the induction scheme, you want to basically copy the substitution of an existing variable into a new variable.
For example, consider our attempt to prove that sum-pairs-list is nat-list congruent:
(defun nat-list-equiv (x y) (if (atom x) (atom y) (and (consp y) (equal (nfix (car x)) (nfix (car y))) (nat-list-equiv (cdr x) (cdr y))))) (defun sum-pairs-list (x) (if (atom x) nil (if (atom (cdr x)) (list (nfix (car x))) (cons (+ (nfix (car x)) (nfix (cadr x))) (sum-pairs-list (cddr x)))))) (defequiv nat-list-equiv) (defthm sum-pairs-list-nat-list-equiv-congruence (implies (nat-list-equiv x y) (equal (sum-pairs-list x) (sum-pairs-list y))) :rule-classes :congruence)
The proof of the congruence rule fails with no hint, and neither of the following induction hints don't help either:
:hints (("goal" :induct (nat-list-equiv x y))))
:hints (("goal" :induct (list (sum-pairs-list x)
(sum-pairs-list y))))
What we really want is an induction scheme that inducts as sum-pairs-list on (say) x, but does a similar substitution on y, e.g.,
(defun sum-pairs-list-double-manual (x y) (declare (ignorable y)) (if (atom x) nil (if (atom (cdr x)) (list (nfix (car x))) (cons (+ (nfix (car x)) (nfix (cadr x))) (sum-pairs-list-double-manual (cddr x) (cddr y)))))) (defthm sum-pairs-list-nat-list-equiv-congruence ;; sum-pairs-list-double-manual works (implies (nat-list-equiv x y) (equal (sum-pairs-list x) (sum-pairs-list y))) :hints (("goal" :induct (sum-pairs-list-double-manual x y))) :rule-classes :congruence)
Def-doublevar-ind automatically generates a function like this, e.g.:
(def-doublevar-induction sum-pairs-list-double :orig-fn sum-pairs-list :old-var x :new-var y) (defthm sum-pairs-list-nat-list-equiv-congruence ;; sum-pairs-list-double works (implies (nat-list-equiv x y) (equal (sum-pairs-list x) (sum-pairs-list y))) :hints (("goal" :induct (sum-pairs-list-double x y))) :rule-classes :congruence)
This can be used with flag functions and their defthm macros (see make-flag): use def-doublevar-ind to define a new induction scheme based on the flag function, and give a hint to the flag defthm macro to use that induction scheme. For example,
(flag::make-flag foo-flag foo-mutualrec ...) (flag::def-doublevar-ind foo-doublevar-ind :orig-fn foo-flag :old-var x :new-var y) (defthm-foo-flag (defthm foo1-thm ...) (defthm foo2-thm ...) :hints (("goal" :induct (foo-doublevar-ind flag x a b y))))