diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-18 02:13:36 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2022-07-18 02:13:36 +0900 |
| commit | 87f47e7a248325933d2aa269de898ef521716650 (patch) | |
| tree | d4cf6fd0fa87032021be9ef5726531b13d8a90d2 | |
| parent | e062d5b7a35866b4043c2b325989e1d5a55b46c3 (diff) | |
lists/perm: Add defcongs.
| -rw-r--r-- | lists/perm.lisp | 23 |
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) |