~/Dropbox/talks/weak-arithmetic-2019-05/demos$ acl2-8.2
Welcome to Clozure Common Lisp Version 1.12-dev (v1.12-dev.5) DarwinX8664!

 ACL2 Version 8.2 built May 5, 2019  15:14:49.
 Copyright (C) 2019, Regents of the University of Texas
 ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
 are welcome to redistribute it under certain conditions.  For details,
 see the LICENSE file distributed with ACL2.

 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).
 See the documentation topic note-8-2 for recent changes.
 Note: We have modified the prompt in some underlying Lisps to further
 distinguish it from the ACL2 prompt.

ACL2 Version 8.2.  Level 1.  Cbd 
"/Users/kaufmann/Dropbox/talks/weak-arithmetic-2019-05/demos/".
System books directory "/Users/kaufmann/acl2/v8-2/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>(defun sum-to-n (n)
       ; Recursive definition: ACL2 proves n-1 is less than n when
       ; n is a positive integer.
	 (if (posp n) ; n is a positive integer
	     (+ n (sum-to-n (- n 1)))
	   0))

For the admission of SUM-TO-N we will use the relation O< (which is
known to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT N).  The non-trivial part of the measure conjecture is

Goal
(IMPLIES (POSP N)
         (O< (ACL2-COUNT (+ -1 N))
             (ACL2-COUNT N))).
Goal'

Q.E.D.

That completes the proof of the measure theorem for SUM-TO-N.  Thus,
we admit this function under the principle of definition.  We observe
that the type of SUM-TO-N is described by the theorem 
(AND (INTEGERP (SUM-TO-N N)) (<= 0 (SUM-TO-N N))).  We used the :compound-
recognizer rule POSP-COMPOUND-RECOGNIZER and primitive type reasoning.

Summary
Form:  ( DEFUN SUM-TO-N ...)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:DEFINITION NOT)
        (:DEFINITION POSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
Prover steps counted:  24
 SUM-TO-N
ACL2 !>(thm ; sum-to-n(n) = n(n+1)/2
	(implies (natp n)
		 (equal (sum-to-n n)
			(/ (* n (+ n 1))
			   2))))
Goal'
Goal''

([ A key checkpoint:

Goal''
(IMPLIES (AND (INTEGERP N) (<= 0 N))
         (EQUAL (SUM-TO-N N)
                (+ (* 1/2 N) (* N 1/2 N))))

*1 (Goal'') is pushed for proof by induction.

])

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (SUM-TO-N N).  This
suggestion was produced using the :induction rule SUM-TO-N.  If we
let (:P N) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (POSP N)) (:P N))
     (IMPLIES (AND (POSP N) (:P (+ -1 N)))
              (:P N))).
This induction is justified by the same argument used to admit SUM-TO-N.
When applied to the goal at hand the above induction scheme produces
four nontautological subgoals.
Subgoal *1/4
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3''
Subgoal *1/3'''
Subgoal *1/3'4'
Subgoal *1/3'5'
Subgoal *1/3'6'
Subgoal *1/3'7'

([ A key checkpoint while proving *1 (descended from Goal''):

Subgoal *1/3''
(IMPLIES (AND (INTEGERP N)
              (< 0 N)
              (EQUAL (SUM-TO-N (+ -1 N))
                     (+ (* 1/2 N)
                        (* -1/2 N)
                        (* (+ -1 N) 1/2 N)))
              (<= 0 N))
         (EQUAL (+ N (SUM-TO-N (+ -1 N)))
                (+ (* 1/2 N) (* N 1/2 N))))

*1.1 (Subgoal *1/3'7') is pushed for proof by induction.

])
Subgoal *1/2
Subgoal *1/1

So we now return to *1.1, which is

(IMPLIES (AND (RATIONALP S)
              (< 0 S)
              (RATIONALP R)
              (< 0 R)
              (INTEGERP N)
              (< 0 N)
              (<= 0 N))
         (EQUAL (+ N R S (* -1 R) (* -1/2 N))
                (+ R S))).

No induction schemes are suggested by *1.1.  Consequently, the proof
attempt has failed.

Summary
Form:  ( THM ...)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:DEFINITION FIX)
        (:DEFINITION NATP)
        (:DEFINITION NOT)
        (:DEFINITION POSP)
        (:DEFINITION SUM-TO-N)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART BINARY-*)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART INTEGERP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART POSP)
        (:EXECUTABLE-COUNTERPART SUM-TO-N)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUM-TO-N)
        (:REWRITE ASSOCIATIVITY-OF-*)
        (:REWRITE ASSOCIATIVITY-OF-+)
        (:REWRITE COMMUTATIVITY-2-OF-+)
        (:REWRITE COMMUTATIVITY-OF-*)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE DISTRIBUTIVITY)
        (:REWRITE FOLD-CONSTS-IN-+)
        (:REWRITE UNICITY-OF-0))
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1490

---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---

*** Key checkpoint at the top level: ***

Goal''
(IMPLIES (AND (INTEGERP N) (<= 0 N))
         (EQUAL (SUM-TO-N N)
                (+ (* 1/2 N) (* N 1/2 N))))

*** Key checkpoint under a top-level induction: ***

Subgoal *1/3''
(IMPLIES (AND (INTEGERP N)
              (< 0 N)
              (EQUAL (SUM-TO-N (+ -1 N))
                     (+ (* 1/2 N)
                        (* -1/2 N)
                        (* (+ -1 N) 1/2 N)))
              (<= 0 N))
         (EQUAL (+ N (SUM-TO-N (+ -1 N)))
                (+ (* 1/2 N) (* N 1/2 N))))

ACL2 Error in ( THM ...):  See :DOC failure.

******** FAILED ********
ACL2 !>(include-book "arithmetic/top" ; include a "community book"
		     :dir :system)

Summary
Form:  ( INCLUDE-BOOK "arithmetic/top" ...)
Rules: NIL
Time:  0.23 seconds (prove: 0.00, print: 0.00, other: 0.23)
 "/Users/kaufmann/acl2/v8-2/books/arithmetic/top.lisp"
ACL2 !>(thm ; sum-to-n(n) = n(n+1)/2 (succeeds this time)
	(implies (natp n)
		 (equal (sum-to-n n)
			(/ (* n (+ n 1))
			   2))))
Goal'
Goal''

([ A key checkpoint:

Goal''
(IMPLIES (NATP N)
         (EQUAL (SUM-TO-N N)
                (+ (* 1/2 N) (* 1/2 N N))))

*1 (Goal'') is pushed for proof by induction.

])

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (SUM-TO-N N).  This
suggestion was produced using the :induction rule SUM-TO-N.  If we
let (:P N) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (POSP N)) (:P N))
     (IMPLIES (AND (POSP N) (:P (+ -1 N)))
              (:P N))).
This induction is justified by the same argument used to admit SUM-TO-N.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1

*1 is COMPLETED!
Thus key checkpoint Goal'' is COMPLETED!

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:DEFINITION FIX)
        (:DEFINITION NOT)
        (:DEFINITION SUM-TO-N)
        (:EXECUTABLE-COUNTERPART BINARY-*)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NATP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART POSP)
        (:EXECUTABLE-COUNTERPART SUM-TO-N)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART UNARY--)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING NATP-FC-1)
        (:INDUCTION SUM-TO-N)
        (:REWRITE ASSOCIATIVITY-OF-*)
        (:REWRITE ASSOCIATIVITY-OF-+)
        (:REWRITE COMMUTATIVITY-2-OF-*)
        (:REWRITE COMMUTATIVITY-2-OF-+)
        (:REWRITE COMMUTATIVITY-OF-*)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE DISTRIBUTIVITY)
        (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+)
        (:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT)
        (:REWRITE MINUS-CANCELLATION-ON-LEFT)
        (:REWRITE UNICITY-OF-1)
        (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  599

Proof succeeded.
ACL2 !>:pso ; "print saved output"

Output replay for: ( THM ...)

By the simple :rewrite rule ASSOCIATIVITY-OF-* we reduce the conjecture
to

Goal'
(IMPLIES (NATP N)
         (EQUAL (SUM-TO-N N) (* N (+ N 1) 1/2))).

This simplifies, using the :executable-counterpart of BINARY-* and
the :rewrite rules COMMUTATIVITY-2-OF-*, COMMUTATIVITY-OF-*, 
COMMUTATIVITY-OF-+ and DISTRIBUTIVITY, to

Goal''
(IMPLIES (NATP N)
         (EQUAL (SUM-TO-N N)
                (+ (* 1/2 N) (* 1/2 N N)))).

Name the formula above *1.

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (SUM-TO-N N).  This
suggestion was produced using the :induction rule SUM-TO-N.  If we
let (:P N) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (POSP N)) (:P N))
     (IMPLIES (AND (POSP N) (:P (+ -1 N)))
              (:P N))).
This induction is justified by the same argument used to admit SUM-TO-N.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.

Subgoal *1/3
(IMPLIES (AND (NOT (POSP N)) (NATP N))
         (EQUAL (SUM-TO-N N)
                (+ (* 1/2 N) (* 1/2 N N)))).

But simplification reduces this to T, using the :compound-recognizer
rules NATP-COMPOUND-RECOGNIZER and POSP-COMPOUND-RECOGNIZER, the :executable-
counterparts of BINARY-*, BINARY-+, EQUAL, NATP, NOT, POSP and SUM-TO-N,
linear arithmetic, primitive type reasoning, the :forward-chaining
rule NATP-FC-1 and the :type-prescription rule NONNEGATIVE-PRODUCT.

Subgoal *1/2
(IMPLIES (AND (POSP N)
              (EQUAL (SUM-TO-N (+ -1 N))
                     (+ (* 1/2 (+ -1 N))
                        (* 1/2 (+ -1 N) (+ -1 N))))
              (NATP N))
         (EQUAL (SUM-TO-N N)
                (+ (* 1/2 N) (* 1/2 N N)))).

This simplifies, using the :compound-recognizer rules 
NATP-COMPOUND-RECOGNIZER and POSP-COMPOUND-RECOGNIZER, the :definitions
FIX and SUM-TO-N, the :executable-counterparts of BINARY-* and UNARY--,
primitive type reasoning, the :rewrite rules ASSOCIATIVITY-OF-+, 
COMMUTATIVITY-2-OF-+, COMMUTATIVITY-OF-*, DISTRIBUTIVITY, 
DISTRIBUTIVITY-OF-MINUS-OVER-+, FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT,
MINUS-CANCELLATION-ON-LEFT and UNICITY-OF-1 and the :type-prescription
rule NONNEGATIVE-PRODUCT, to

Subgoal *1/2'
(IMPLIES (AND (POSP N)
              (EQUAL (SUM-TO-N (+ -1 N))
                     (+ (- (* 1/2 N)) (* 1/2 N N))))
         (EQUAL (+ N (SUM-TO-N (+ -1 N)))
                (+ (* 1/2 N) (* 1/2 N N)))).

But we reduce the conjecture to T, by the :executable-counterpart of
TAU-SYSTEM.

Subgoal *1/1
(IMPLIES (AND (POSP N)
              (NOT (NATP (+ -1 N)))
              (NATP N))
         (EQUAL (SUM-TO-N N)
                (+ (* 1/2 N) (* 1/2 N N)))).

But we reduce the conjecture to T, by the :compound-recognizer rules
NATP-COMPOUND-RECOGNIZER and POSP-COMPOUND-RECOGNIZER and primitive
type reasoning.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:DEFINITION FIX)
        (:DEFINITION NOT)
        (:DEFINITION SUM-TO-N)
        (:EXECUTABLE-COUNTERPART BINARY-*)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NATP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART POSP)
        (:EXECUTABLE-COUNTERPART SUM-TO-N)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART UNARY--)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING NATP-FC-1)
        (:INDUCTION SUM-TO-N)
        (:REWRITE ASSOCIATIVITY-OF-*)
        (:REWRITE ASSOCIATIVITY-OF-+)
        (:REWRITE COMMUTATIVITY-2-OF-*)
        (:REWRITE COMMUTATIVITY-2-OF-+)
        (:REWRITE COMMUTATIVITY-OF-*)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE DISTRIBUTIVITY)
        (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+)
        (:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT)
        (:REWRITE MINUS-CANCELLATION-ON-LEFT)
        (:REWRITE UNICITY-OF-1)
        (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  599
ACL2 !>(thm ; sum-to-n(2k) = k(2k+1)
	    ; Fails (induction not found; previous thm wasn't stored)
	(implies (natp k)
		 (equal (sum-to-n (* 2 k))
			(* k (+ (* 2 k) 1)))))
Goal'

([ A key checkpoint:

Goal'
(IMPLIES (NATP K)
         (EQUAL (SUM-TO-N (* 2 K))
                (+ K (* 2 K K))))

*1 (Goal') is pushed for proof by induction.

])

No induction schemes are suggested by *1.  Consequently, the proof
attempt has failed.

Summary
Form:  ( THM ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:DEFINITION FIX)
        (:REWRITE COMMUTATIVITY-2-OF-*)
        (:REWRITE COMMUTATIVITY-OF-*)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE DISTRIBUTIVITY)
        (:REWRITE UNICITY-OF-1))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  343

---
The key checkpoint goal, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---

*** Key checkpoint at the top level: ***

Goal'
(IMPLIES (NATP K)
         (EQUAL (SUM-TO-N (* 2 K))
                (+ K (* 2 K K))))

ACL2 Error in ( THM ...):  See :DOC failure.

******** FAILED ********
ACL2 !>(defthm sum-to-n-rewrite ; Prove and store a rewrite rule
				; to replace sum-to-n(n) by n(n+1)/2.
	 (implies (natp n)
		  (equal (sum-to-n n)
			 (/ (* n (+ n 1))
			    2))))
Goal'
Goal''

([ A key checkpoint:

Goal''
(IMPLIES (NATP N)
         (EQUAL (SUM-TO-N N)
                (+ (* 1/2 N) (* 1/2 N N))))

*1 (Goal'') is pushed for proof by induction.

])

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (SUM-TO-N N).  This
suggestion was produced using the :induction rule SUM-TO-N.  If we
let (:P N) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (POSP N)) (:P N))
     (IMPLIES (AND (POSP N) (:P (+ -1 N)))
              (:P N))).
This induction is justified by the same argument used to admit SUM-TO-N.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1

*1 is COMPLETED!
Thus key checkpoint Goal'' is COMPLETED!

Q.E.D.

Summary
Form:  ( DEFTHM SUM-TO-N-REWRITE ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:DEFINITION FIX)
        (:DEFINITION NOT)
        (:DEFINITION SUM-TO-N)
        (:EXECUTABLE-COUNTERPART BINARY-*)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NATP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART POSP)
        (:EXECUTABLE-COUNTERPART SUM-TO-N)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART UNARY--)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING NATP-FC-1)
        (:INDUCTION SUM-TO-N)
        (:REWRITE ASSOCIATIVITY-OF-*)
        (:REWRITE ASSOCIATIVITY-OF-+)
        (:REWRITE COMMUTATIVITY-2-OF-*)
        (:REWRITE COMMUTATIVITY-2-OF-+)
        (:REWRITE COMMUTATIVITY-OF-*)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE DISTRIBUTIVITY)
        (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+)
        (:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT)
        (:REWRITE MINUS-CANCELLATION-ON-LEFT)
        (:REWRITE UNICITY-OF-1)
        (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  599
 SUM-TO-N-REWRITE
ACL2 !>(thm ; proof succeeds immediately
	(implies (natp k)
		 (equal (sum-to-n (* 2 k))
			(* k (+ (* 2 k) 1)))))

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:DEFINITION FIX)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART BINARY-*)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE COMMUTATIVITY-2-OF-*)
        (:REWRITE COMMUTATIVITY-OF-*)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE DISTRIBUTIVITY)
        (:REWRITE FOLD-CONSTS-IN-*)
        (:REWRITE SUM-TO-N-REWRITE)
        (:REWRITE UNICITY-OF-1))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  156

Proof succeeded.
ACL2 !>:pso

Output replay for: ( THM ...)

But simplification reduces this to T, using the :compound-recognizer
rule NATP-COMPOUND-RECOGNIZER, the :definitions FIX and SYNP, the :executable-
counterpart of BINARY-*, primitive type reasoning and the :rewrite
rules COMMUTATIVITY-2-OF-*, COMMUTATIVITY-OF-*, COMMUTATIVITY-OF-+,
DISTRIBUTIVITY, FOLD-CONSTS-IN-*, SUM-TO-N-REWRITE and UNICITY-OF-1.

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:DEFINITION FIX)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART BINARY-*)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE COMMUTATIVITY-2-OF-*)
        (:REWRITE COMMUTATIVITY-OF-*)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE DISTRIBUTIVITY)
        (:REWRITE FOLD-CONSTS-IN-*)
        (:REWRITE SUM-TO-N-REWRITE)
        (:REWRITE UNICITY-OF-1))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  156
ACL2 !>