; Arithmetic can be surprisingly tough to reason about, but let's
; give it a try:
(defun sum-up-to (n)
(if (zp n)
0
(+ n (sum-up-to (1- n)))))
(sum-up-to 4)
(defthm sum-up-to-property ; fails
(implies (natp n)
(equal (sum-up-to n)
(/ (* n (+ 1 n))
2))))
(include-book "arithmetic/top" :dir :system)
(defthm sum-up-to-property
(implies (natp n)
(equal (sum-up-to n)
(/ (* n (+ 1 n))
2))))
; Better yet:
:ubt! :x-1 ; undo defthm and include-book
(encapsulate
()
(local (include-book "arithmetic/top" :dir :system))
(defthm sum-up-to-property
(implies (natp n)
(equal (sum-up-to n)
(/ (* n (+ 1 n))
2)))))