summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2022-07-18 02:13:36 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2022-07-18 02:13:36 +0900
commit87f47e7a248325933d2aa269de898ef521716650 (patch)
treed4cf6fd0fa87032021be9ef5726531b13d8a90d2
parente062d5b7a35866b4043c2b325989e1d5a55b46c3 (diff)
lists/perm: Add defcongs.
-rw-r--r--lists/perm.lisp23
1 files changed, 23 insertions, 0 deletions
diff --git a/lists/perm.lisp b/lists/perm.lisp
index a5b5487..d93a0c5 100644
--- a/lists/perm.lisp
+++ b/lists/perm.lisp
@@ -68,3 +68,26 @@
:rule-classes ((:rewrite :match-free :all)))))
(defequiv perm)
+
+(defcong perm perm (remove1 e x) 2)
+(defcong perm iff (member e x) 2)
+
+
+(local (include-book "std/lists/rev" :dir :system))
+(local (defthm perm-rev
+ (perm (rev x) (double-rewrite x))
+ :hints (("Goal" :induct (perm x x)))))
+
+(defcong perm perm (append x y) 2)
+(defcong perm perm (append x y) 1)
+(defcong perm perm (cons x y) 2)
+(defcong perm perm (revappend x y) 2)
+(defcong perm perm (revappend x y) 1)
+
+(local
+ (defthm member-remove
+ (implies (not (equal x y))
+ (iff (member x (remove y z))
+ (member x (double-rewrite z))))))
+
+(defcong perm perm (remove e x) 2)