From 80ff85f0f558e31a5aff784b2d38547c870f9d95 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Fri, 6 Aug 2021 01:16:56 +0900 Subject: peano: Add nat* function and theorems. --- peano.lisp | 59 +++++++++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 55 insertions(+), 4 deletions(-) (limited to 'peano.lisp') diff --git a/peano.lisp b/peano.lisp index 8c7f7d3..5028a13 100644 --- a/peano.lisp +++ b/peano.lisp @@ -55,10 +55,12 @@ (equal (nat+ x y) (nat+ y x)))) -(defthm nat+-zero - (implies (nat? x) - (equal (nat+ nil x) - x))) +(defthm nat+-left-zero + (implies (and (nat? x) + (z? x) + (nat? y)) + (equal (nat+ x y) + y))) (defthm nat+-right-cancellative (equal (equal (nat+ x k) (nat+ y k)) @@ -81,3 +83,52 @@ (defthm associativity-of-nat+ (equal (nat+ x (nat+ y z)) (nat+ (nat+ x y) z))) + +(defun nat* (x y) + (if (z? y) + nil + (nat+ x (nat* x (pred y))))) + +(defthm nat*-left-one + (equal (nat* x (succ nil)) + x)) + +(defthm nat*-right-one + (equal (nat* x (succ nil)) + x)) + +(defthm nat*-commutative + (implies (and (nat? x) + (nat? y)) + (equal (nat* x y) + (nat* y x)))) + +(defthm nat?-nat* + (implies (and (nat? x) + (nat? y)) + (nat? (nat* x y)))) + +(defthm nat*-left-zero + (implies (and (z? x) + (nat? x)) + (equal (nat* x y) + nil))) + +(defthm distributivity-of-nat* + (implies (and (nat? x) + (nat? y) + (nat? z)) + (equal (nat* x (nat+ y z)) + (nat+ (nat* x y) + (nat* x z))))) + +(defthm associativity-of-nat* + (implies (and (nat? x) + (nat? y) + (nat? z)) + (equal (nat* x (nat* y z)) + (nat* (nat* x y) z))) + :hints (("Goal" :in-theory (disable nat*-commutative) + :use ((:instance nat*-commutative + (x (cdr z)) + (y (nat* x y))))))) -- cgit v1.2.3