From 4ada0d21de63a954c17d0b9ee4002be7fb7e22ab Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Sat, 14 Aug 2021 11:39:40 +0900 Subject: pigeonhole: Remove warnings. --- pigeonhole.lisp | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'pigeonhole.lisp') diff --git a/pigeonhole.lisp b/pigeonhole.lisp index bda4cfc..4be756b 100644 --- a/pigeonhole.lisp +++ b/pigeonhole.lisp @@ -54,24 +54,28 @@ (defthm not-no-duplicatesp-list-count (implies (< 1 (list-count e x)) - (not (no-duplicatesp x)))) + (not (no-duplicatesp x))) + :rule-classes ((:rewrite :match-free :all))) (defthm not-no-duplicatesp-remove (implies (not (no-duplicatesp (remove e x))) - (not (no-duplicatesp x)))) + (not (no-duplicatesp x))) + :rule-classes ((:rewrite :match-free :all))) (defthm member-if-over-1-map-list-count-is-duplicated (implies (and (no-duplicatesp s) (subsetp x s) (member-if-over-1 (map-list-count x s))) (not (no-duplicatesp x))) - :hints (("Goal" :induct (map-list-count x s)))) + :hints (("Goal" :induct (map-list-count x s))) + :rule-classes ((:rewrite :match-free :all))) (defthm pigeonhole-for-list (implies (and (no-duplicatesp s) (subsetp x s) (< (len s) (len x))) - (not (no-duplicatesp x)))) + (not (no-duplicatesp x))) + :rule-classes ((:rewrite :match-free :all))) (in-theory (disable pigeonhole-for-list)) (defthm blood-types-are-duplicates @@ -126,11 +130,13 @@ (no-duplicatesp (nats-below n))) (defthm duplicates-nats - (implies (and (posp n) + (implies (and (integerp n) + (<= 0 n) (subsetp x (nats-below n)) (< n m) (<= m (len x))) (not (no-duplicatesp x))) + :rule-classes ((:rewrite :match-free :all)) :hints (("Goal" :use (:instance pigeonhole-for-list (s (nats-below n)) (x x))))) -- cgit v1.2.3