diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2021-09-04 01:16:29 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-09-04 10:48:48 +0900 |
| commit | f292ea0c9594e4c2bd3581cef8b7989a8391d9b3 (patch) | |
| tree | afa0721d0d89d6e1410af65367a39f17c87f3816 | |
| parent | 975418f4c2e1520649196458d3211e6ef9ec531a (diff) | |
fast-expt: Add fast-expt.lisp file.
| -rw-r--r-- | fast-expt.lisp | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/fast-expt.lisp b/fast-expt.lisp new file mode 100644 index 0000000..3318946 --- /dev/null +++ b/fast-expt.lisp @@ -0,0 +1,38 @@ +(defmacro square (x) + `(* ,x ,x)) + +(defun fast-expt (b n) + (cond + ((zp n) 1) + ((evenp n) (square (fast-expt b (/ n 2)))) + (t (* b (fast-expt b (- n 1)))))) + +(defthm add-halves + (implies (and (acl2-numberp n) + (evenp n)) + (equal n (+ (* 1/2 n) (* 1/2 n)))) + :rule-classes nil) + +(defthm expt-add-halves + (implies (and (acl2-numberp n) + (acl2-numberp b) + (evenp n)) + (equal (expt b n) (expt b (+ (* 1/2 n) (* 1/2 n))))) + :hints (("Goal" :do-not-induct t + :use (:instance add-halves (n n)))) + :rule-classes nil) + +(defthm add-expts + (implies (and (natp b) + (natp n) + (natp m)) + (equal (expt b (+ n m)) + (* (expt b n) + (expt b m))))) + +(defthm expt-fast-expt + (implies (and (natp n) + (natp b)) + (equal (fast-expt b n) + (expt b n))) + :hints (("Subgoal *1/4'''" :use (:instance expt-add-halves (n n))))) |