From 87f47e7a248325933d2aa269de898ef521716650 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Mon, 18 Jul 2022 02:13:36 +0900
Subject: lists/perm: Add defcongs.

---
 lists/perm.lisp | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

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)
-- 
cgit v1.2.3