Recursion and Induction Problems 50, 51, and 55
Sandip Ray
[ I am CCing J in this message, since this pertains to the Recursion
and Induction notes, in case he finds these helpful. ]
As requested by the class, at the bottom of the email are three
proofs, of problems 50, 51, and 55, from Moore's "Recursion and
Induction" notes. Since I'm short on time, I did the proofs in a
hurry so there might be some mistakes, in which case please point them
out to me. But they should give you an idea of how the proofs go, and
hopefully, some sense of how to proceed with such proofs.
I have some comments in the proofs, which correspond to sentences that
start with ";;". Those are only for your help, in order to suggest
why I did what I did. They are not part of the derivation and can be
ignored if you understand the proofs. But maybe they'll be helpful if
you want to know the intuition behind some steps. The problems 50 and
51 are pretty standard. Problem 55, I decided to do a very different
proof from what you might have thought, since I wanted to make a
point; hopefully this will suggest the need and importance of
high-level strategies when pursuing a proof project.
Thanks. I hope these are useful. Let me know if you have questions.
-- Sandip
=====================================================================
;; Here are solutions to problems 50, 51, and 55 in Moore's "Recursion
;; and Induction" notes, done at the request of the CS389R class to
;; show how a sample "hand derivation" looks like. Note that your
;; solutions might be different from mine. There is no "best"
;; solution to a proof. Any solution that is correct according to the
;; axioms and rules of inference will be acceptable.
Problem 50:
(sub (app a a) a)
;; This problem cannot be done with induction. If you try, you'll
;; soon hit a brick wall. So we generalize the problem, and prove the
;; problem by instantiation. The generalization that comes to mind
;; is, generalize (app a a) to (app a b), and think of the appropriate
;; lemma. The lemma that I came up with is Lemma 1.
(sub (app a a) a)
= {Lemma 1}
(and (sub a a) (sub a a))
= {Definition of and}
(sub a a)
= {Lemma 2}
T
------------------------------------------------------------------------
;; Lemma 1 is a typical regulation proof. I will prove this by
;; induction.
Lemma 1:
(equal (sub (app a b) c)
(and (sub a c) (sub b c)))
We prove by induction.
Base Case:
(implies (not (consp a))
(equal (sub (app a b) c)
(and (sub a c) (sub b c))))
By deduction law, we simplify the conclusion taking the hypothesis as
given.
LHS = (sub (app a b) c)
= {Definition app, given}
(sub b c)
RHS = (and (sub a c) (sub b c))
= {Definition sub, given}
(and t (sub b c))
= {Definition and}
(sub b c)
= LHS
Induction step:
(implies (and (consp a)
(equal (sub (app (cdr a) b) c)
(and (sub (cdr a) c)
(sub b c))))
(equal (sub (app a b) c)
(and (sub a c)
(sub b c))))
By deduction law, we simplify the conclusion taking the hypothesis as
given.
LHS = (sub (app a b) c)
= {Definition app, given}
(sub (cons (car a) (app (cdr a) b)) c)
= {Definition sub, axiom car-cons, cdr-cons}
(if (mem (car a) c)
(sub (app (cdr a) b) c)
nil)
= {Given}
(if (mem (car a) c)
(and (sub (cdr a) c)
(sub b c))
nil)
We break into cases (mem (car a) c), and (not (mem (car a) c))
Case (mem (car a) c):
LHS = (and (sub (cdr a) c)
(sub b c))
RHS = (and (sub a c)
(sub b c))
= {Definition sub}
(and (if (mem (car a) c)
(sub (cdr a) c)
nil)
(sub b c))
= {Given from case}
(and (sub (cdr a) c)
(sub b c))
= LHS
Case (not (mem (car a) c)):
LHS = nil
RHS = (and (sub a c)
(sub b c))
= {Definition sub, given from case}
(and nil (sub b c))
= {Definition and}
nil
= LHS
--------------------------------------------------------------------
;; Lemma 2 is a bit more tricky. The problem is that we need to
;; generalize carefully. My generalization is lemma 3,
Lemma 2:
(equal (sub x x) t)
;; Looks like you already did this exercise in Problem 48. But I'm
;; doing this for completeness.
We prove by induction.
Base case:
(implies (not (consp x))
(equal (sub x x) t))
By deduction law, it is sufficient to prove
Given (not (consp x))
Prove (equal (sub x x) t)
We proceed by simplification
(sub x x)
= {Definition of sub, given}
T
Induction step:
(implies (and (consp x)
(equal (sub (cdr x) (cdr x)) t))
(equal (sub x x) t))
By deduction law, it is sufficient to prove
Given (and (consp x)
(equal (sub (cdr x) (cdr x)) t))
Prove (equal (sub x x) t)
We proceed by simplification
(sub x x)
= {Definition of sub, given}
(if (mem (car x) x) (sub (cdr x) x) nil)
= {Definition mem, given}
(if t (sub (cdr x) x) nil)
= {axiom of if}
(sub (cdr x) x)
= {Lemma 3}
T
------------------------------------------------------------------
Lemma 3
(implies (sub p (cdr q)) (equal (sub p q) t))
We prove this by induction.
Base case:
(implies (not (consp p))
(implies (sub p (cdr q)) (equal (sub p q) t)))
Induction step:
(implies (and (consp p)
(implies (sub (cdr p) (cdr q))
(equal (sub (cdr p) q) t)))
(implies (sub p (cdr q))
(equal (sub p q) t)))
= {Simplification, Definition sub}
(implies (and (consp p)
(sub p (cdr q))
(mem (car p) (cdr q))
(sub (cdr p) (cdr q))
(equal (sub (cdr p) q) t))
(equal (sub p q) t)))
By deduction law and simplification, it is sufficient to prove the following:
Given: (and (consp p)
(sub (cdr p) (cdr q))
(mem (car p) (cdr q))
(sub p (cdr q)))
Prove (equal (sub p q) t)
(sub p q)
= {Definition sub, given}
(if (mem (car p) q) (sub (cdr p) q) nil)
= {Axiom about if, Lemma 2.3}
(sub (cdr p) q)
= {Given}
T
================================================================================
;; This proof is a very standard proof. I went following the method
;; more or less. More comments below.
Problem 51:
(implies (and (nil-listp a)
(nil-listp b))
(equal (mapnil1 a b)
(mapnil1 b a)))
Where I define nil-listp as follows:
(defun nil-listp (x)
(if (consp x)
(and (equal (car x) nil)
(nil-listp (cdr x)))
(equal x nil)))
Proof:
We proceed by induction.
Base Case:
(implies (not (consp a))
(implies (and (nil-listp a)
(nil-listp b))
(equal (mapnil1 a b)
(mapnil1 b a))))
= {Simplification, definition nil-listp}
(implies (and (not (consp a))
(nil-listp a)
(equal a nil)
(nil-listp b))
(equal (mapnil1 a b)
(mapnil1 b a)))
By deduction law, it is sufficient to prove the conclusion by
taking the hypothesis as given. Thus we will prove:
Given: (and (nil-listp b)
(nil-listp b)
(equal a nil)
(not (consp a)))
Prove: (equal (mapnil1 a b)
(mapnil1 b a))
LHS
= [Definition of mapnil1]
b
RHS
= {Lemma 1, given}
(app b nil)
= {Lemma 2}
b
= RHS
------------------------------------------------------------------
;; This lemma is the only key insight that I need in this. The lemma
;; says that if we're dealing with a list of nils then mapnil1 is the
;; same as app.
Lemma 1:
(implies (nil-listp a)
(equal (mapnil1 a b)
(app a b)))
We proceed by induction on a:
Base case:
(implies (and (not (consp a))
(implies (nil-listp a)
(equal (mapnil1 a b)
(app a b)))
Again, we prove the conclusion by taking the hypothesis as given.
Thus, we want to prove:
Given: (and (not (consp a))
(nil-listp a))
Prove: (equal (mapnil1 a b)
(app a b))
LHS = (mapnil1 a b)
= {Definition mapnil1, given}
b
RHS = (app a b)
= {Definition app, given}
b
= LHS
Induction step:
(implies
(and (consp a)
(implies (nil-listp (cdr a))
(equal (mapnil1 (cdr a) b)
(app (cdr a) b)
(implies (nil-listp a)
(equal (mapnil1 a b)
(app a b))))
= {Simplification + definition of nil-listp}
(implies (and (consp a)
(equal (car a) nil)
(nil-listp a)
(equal (mapnil1 (cdr a) b)
(app (cdr a) b)))
(equal (mapnil1 a b)
(app a b)))
We take the antecedents as given and we simplify the conclusion
(using deduction law).
;; The only complexity of the proof comes in moving cons around. I
;; defer the proof that cons can be moved as lemma 3, and go on to
;; finish this. We consider lemma 3 later.
RHS = (app a b)
= {Definition app}
(cons (car a) (app (cdr a) b))
= {given}
(cons nil (mapnil1 (cdr a) b))
= {Lemma 3}
(mapnil1 (cdr a) (cons nil b))
= {Definition mapnil1}
(mapnil1 a b)
--------------------------------------------------------------------
;; This lemma is a standard induction. I should probably have left
;; this as an exercise.
Lemma 2:
(implies (nil-listp b)
(equal (app b nil) b))
Proof:
Use induction.
Base case
(implies (not (consp b))
(implies (nil-listp b)
(equal (app b nil) b)))
= {Simplification}
(implies (and (not (consp b))
(nil-listp b))
(equal (app b nil) b))
= {Definition nil-listp, simplification}
(implies (and (not (consp b))
(equal b nil))
(equal (app b nil) b))
By deduction law, we prove by taking the hypothesis as given and
simplifying the conclusion.
LHS = (app b nil)
= {Definition app, given}
b
= RHS
Induction Step:
(implies (not (consp b))
(implies (nil-listp (cdr b))
(equal (app (cdr b) nil) (cdr b)))
(implies (nil-listp b)
(equal (app b nil) b)))
= {Simplification, Definition nil-listp}
(implies (and (not (consp b))
(equal (car b) nil)
(nil-listp (cdr b))
(equal (app (cdr b) nil) (cdr b))
(nil-listp b))
(equal (app b nil) b))
By deduction law, we prove by taking the hypothesis as given and
simplifying the conclusion.
LHS = (app b nil)
= {Definition app}
(cons (car b) (app (cdr b) nil))
= {given}
(cons (car b) (cdr b))
= {Axiom}
b
= RHS
---------------------------------------------------------------------
Lemma 3:
(implies (nil-listp p)
(equal (mapnil1 p (cons nil a))
(cons nil (mapnil1 p a))))
Use induction:
Base case
(implies (not (consp p))
(implies (nil-listp p)
(equal (mapnil1 p (cons nil a))
(cons nil (mapnil1 p a)))))
= {Simplification, definition nil-listp}
(implies (and (not (consp p))
(nil-listp p)
(equal p nil))
(equal (mapnil1 p (cons nil a))
(cons nil (mapnil1 p a))))
We take the antecedents as given and we simplify the conclusion
(using deduction law).
LHS = (mapnil1 p (cons nil a))
= {Definition mapnil1, given}
(cons nil a)
RHS = (cons nil (mapnil1 p a))
= {Definition mapnil1, given}
(cons nil a)
= LHS
Induction step:
(implies (and (consp p)
(implies (nil-listp (cdr p))
(equal (mapnil1 (cdr p)
(cons nil (cons nil a)))
(cons nil (mapni1 (cdr p) (cons nil a))))))
(implies (nil-listp p)
(equal (mapnil1 p (cons nil a))
(cons nil (mapnil1 p a)))))
= {Simplification, definition nil-listp}
(implies (and (consp p)
(equal (car p) nil)
(nil-listp (cdr p))
(nil-listp p)
(equal (mapnil1 (cdr p)
(cons nil (cons nil a)))
(cons nil (mapnil1 (cdr p) (cons nil a)))))
(equal (mapnil1 p (cons nil a))
(cons nil (mapnil1 p a))))
We prove this by taking the hypothesis of the implication as given
and proving the conclusion.
LHS = (mapnil1 (cdr p) (cons nil (cons nil a)))
= {Given}
(cons nil (mapnil1 (cdr p) (cons nil a)))
= {Definition mapnil1}
(mapnil1 p a)
=======================================================================
Problem 55.
(implies (and (perm x y)
(perm y z))
(perm x z))
;; One way to reason about perm of course is to wade through the
;; induction and do it. If you stare at it, you might see some lemmas to
;; prove. For example,
;; (implies (and (mem e y)
;; (perm x (del e y)))
;; (perm (cons e x) y))
;; But here I show a very different approach, which suggests a different
;; high-level strategy. This approach might at first seem too much work,
;; but it makes proofs a whole lot easier as you go. For example, you
;; can use the same approach to prove Problems 53, 54 with little
;; change. (Just change the last theorem.)
;; The general idea is to sit back and think why we believe in the
;; theorem. For perm the intuition is that (perm x y) holds if and only
;; if for each element e, the occurrence of e in x is the same as that in
;; y. If we think that way, then we can define a function as follows.
(defun how-many (e x)
(if (consp x)
(+ (if (equal e (car x)) 1 0)
(how-many e (cdr x)))
0))
;; The function simply counts the number of occurrences of e in x. The
;; idea is that if (perm x y) holds if and only if for all e (how-many e
;; x) = (how-many e y).
;; So the first thing we do is make the above statement formal. One
;; direction is easy. That is given by the following lemma.
Lemma 1:
(implies (perm x y)
(equal (how-many e x) (how-many e y)))
We proceed by induction.
Base case:
(implies (not (consp x))
(implies (perm x y)
(equal (how-many e x) (how-many e y))))
= {Simplification, Definition perm}
(implies (and (not (consp x))
(perm x y)
(not (consp y)))
(equal (how-many e x) (how-many e y)))
By deduction law, we take the hypothesis as given and simplify the
conclusion.
LHS = (how-many e x)
= {Definition how-many, given}
0
RHS = (how-many e y)
= {Definition how-many}
0
= LHS
Induction step:
(implies (and (consp x)
(implies (perm (cdr x) (del (car x) y))
(equal (how-many e (cdr x))
(how-many e (del (car x) y)))))
(implies (perm x y)
(equal (how-many e x) (how-many e y))))
= {Simplification, Definition perm}
(implies (and (consp x)
(mem (car x) y)
(perm x y)
(perm (cdr x) (del (car x) y))
(equal (how-many e (cdr x))
(how-many e (del (car x) y))))
(equal (how-many e x) (how-many e y)))
By deduction law, we take the hypothesis as given and simplify the
conclusion.
LHS = (how-many e x)
= {Definition how-many}
(+ (if (equal e (car x)) 1 0)
(how-many e (cdr x)))
= {Given}
(+ (if (equal e (car x)) 1 0)
(how-many e (del (car x) y)))
= {Lemma 1.1, simplification}
(+ (if (equal e (car x)) 1 0)
(if (equal e (car x))
(- (how-many e y) 1)
(how-many e y)))
We break this into cases and do each case. The cases are:
1. (not (equal e (car x)))
2. (equal e (car x))
Case 2:
LHS
= {Axiom on if}
(+ 1 (- (how-many e y) 1))
= {Arithmetic, Lemma 3}
(how-many e y)
= RHS
Case 1:
LHS
= {Axiom of if}
(+ 0 (how-many e y))
= {Arithmetic}
(how-many e y)
-----------------------------------------------------------------------
;; Now the other direction. We want to say that if for all e (how-many e
;; x) = (how-many e y) then (perm x y) holds. But how do we make that
;; statement? The following is a simple trick. You have already seen
;; this trick used in the BDD examples. The idea is to think
;; contrapositive of the above statement. That statement is, if (perm x
;; y) does not hold then then there exists some object whose count is
;; different in x than y. Instead of stating that existential statement,
;; we define a function to pick this element out. Let's call this
;; function (perm-witness x y). The following is the simple definition
;; of that function.
(defun perm-witness (x y)
(if (endp x)
(if (endp y) nil
(car y))
(if (not (equal (how-many (car x) x)
(how-many (car x) y)))
(car x)
(perm-witness (rest x) (del (car x) y)))))
;; Clearly, this function picks out an element whose count is different
;; in x and y if (perm x y) does not hold. The following lemma makes
;; this precise. If you are having trouble seeing that this lemma says
;; so, again think about the contrapositive of the lemma.
Lemma 2:
(implies (equal (how-many (perm-witness x y) x)
(how-many (perm-witness x y) y))
(perm x y))
We proceed by induction
Base case:
(implies (not (consp x))
(implies (equal (how-many (perm-witness x y) x)
(how-many (perm-witness x y) y))
(perm x y)))
= {Simplification, definition perm, perm-witness}
(implies (and (not (consp x))
(equal (how-many (if (endp y) nil (car y)) x)
(how-many (if (endp y) nil (car y) y))))
(not (consp y)))
= {Simplification, definition how-many}
(implies (and (not (consp x))
(equal 0 (how-many (if (endp y) nil (car y) y))))
(not (consp y)))
= {Simplification, contrapositive}
(implies (and (not (consp x))
(consp y))
(not (equal 0 (how-many (if (endp y) nil (car y)) y))))
By deduction law, we take hypothesis as given, and simplify the
conclusion.
(not (equal 0 (how-many (if (endp y) nil (car y)) y)))
= {Simplification, given (consp y)}
(not (equal 0 (how-many (car y) y)))
= {Definition how-many}
(not (equal 0 (+ 1 (how-many (car y) (cdr y)))))
= {Arithmetic, Lemma 3}
T
----------------------------------------------------------------------
Lemma 3:
(natp (how-many e x))
Proof:
Use induction.
Base case:
(implies (not (consp x))
(natp (how-many e x)))
By deduction law, we take hypothesis as given and simplify the
conclusion.
(natp (how-many e x))
= {definition how-many}
(natp 0)
= {Arithmetic}
T
Induction step:
(implies (and (consp x)
(natp (how-many e (cdr x))))
(natp (how-many e x)))
By deduction law, we take hypothesis as given and simplify the
conclusion.
(natp (how-many e x))
= {Definition how-many}
(natp (+ (if (equal e (car x)) 1 0)
(how-many e (cdr x))))
Now easy completion by cases (equal e (car x)), (not (equal e (car
x)))
;; Now we make use of the above lemmas to lift the theorems from perm
;; to how-many.
Problem 55:
(implies (and (perm x y)
(perm y z))
(perm x z))
We take the hypothesis as given and prove the conclusion. Thus we
want to prove:
Given (and (perm x y)
(perm y z))
Prove: (perm x z)
By lemma 2, it is sufficient to prove:
(how-many (perm-witness x z) x) = (how-many (perm-witness x z) z)
From given, we have by instantiation of Lemma 1:
(and (equal (how-many (perm-witness x z) x)
(how-many (perm-witness x z) y))
(equal (how-many (perm-witness x z) y)
(how-many (perm-witness x z) z)
By Equality
(equal (how-many (perm-witness x z) x)
(how-many (perm-witness x z) z))
Q.E.D.
;; You can do the same trick for proving 53 and 54. So you see, we have
;; gotten off with reasoning about how-many, by first reducing perm
;; questions to how-many questions. This suggests that it's sometimes
;; easier to think about high-level strategies before diving on a proof.
------------------------------------------------------------------------
jdiamond
In your proof of Problem 50, Lemma 3, you seem to assume
(mem (car p) q). This is exactly where I ran into trouble -
the case part of the proof if you don't assume this to be true.
Can you explain why you don't need to consider the case
where (not (mem (car p) q) ?
Thanks,
- jeff
jdiamond
It seems impossible to solve this without something extremely out of
the box like your lemma equating mapnil1 with append. How did you
come up with such an idea, and perhaps even more importantly, how did
you decide in which places to replace mapnil1 with append? (You could
have just replaced it everywhere, resulting in the proof (app a b) =
(app b a), but you didn't...)
jdiamond
(implies (equal (how-many (perm-witness x y) x)
(how-many (perm-witness x y) y))
(perm x y))
the same number of times in x than in y. To simplify discussion,
let's assume that x and y are sets, so perm-witness returns the first
element that is in x but not in y, or 'nil.
Then how-many is used in a somewhat degenerate way. By definition of
perm-witness, if such an element exists, then the first how-many will
return 1 and the second will return 0. (Or in the general (non set)
case, n and n-1). So they won't be equal - the second term will be
one less. But if x and y are perms, then witness returns 'NIL.
Here's the part that seems tricky to me. how-many gets a 'nil as its
first argument. It will then count all the nil elements (cars) of y.
So they will be equal only if lists x and y have the same number of
elements 'nil. (As the car of each cons.) Which they will if they are
perms. So what the witness does is reduce a general how-many for each
item on the list to a how-many for 'nils in the list.
When I used a similar approach to a different problem, I didn't use
the contrapositive with a witness function. Instead I used a function
to iterate across... i.e.
(defun many-match (x y) ; ignore base case for illustration
(if (equal (how-many (car x) x) (how-many (car x) y)) 'T
(many-match (rm-all (car x) x) (rm-all (car x) y))
)
This seems similar to your first case (the non contrapositive) but it
seems sufficient to show the second direction... It's even easier if
you restrict yourself to sets - then rm-all becomes rm, etc.
Or am I missing something?
- jeff
Sandip Ray
Presumably you're talking about the following step:
(implies (and (consp p)
(implies (sub (cdr p) (cdr q))
(equal (sub (cdr p) q) t)))
(implies (sub p (cdr q))
(equal (sub p q) t)))
= {Simplification, Definition sub}
(implies (and (consp p)
(sub p (cdr q))
(mem (car p) (cdr q))
(sub (cdr p) (cdr q))
(equal (sub (cdr p) q) t))
(equal (sub p q) t)))
If you expand sub you'll notice that (sub p (cdr q)) will be equal to
nil in the case (not (mem (car p) (cdr q))). Since the term (sub p
(cdr q)) is an antecedent (first argument) of "implies", this case
immediately reduces to t (since (implies nil ...) = t) so we are left
with the other case.
-- Sandip
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=googlegroups.com; s=beta;
h=domainkey-signature:received:received:x-sender:x-apparently-to
:mime-version:content-type:received:date:in-reply-to:x-ip:references
:user-agent:x-http-useragent:message-id:subject:from:to:reply-to
:sender:precedence:x-google-loop:mailing-list:list-id:list-post
:list-help:list-unsubscribe:x-beenthere-env:x-beenthere;
bh=JzmlbwPVpj6THE3CYCVo2LWu4e5qi+V7hR+FXJ2AA4U=;
b=UfsAWlYZuzi8NYSPbaNlZakrVv0GUZ6No0ue0Ww9rzgWtQrvER7B0EApN7ov9YIMUp
0qx8/5US0bEdensK6kcIF4Cj4HwoZ0dOaliYj9VJN7G2HeDTCOM/1+iUISrwBrGkaO72
o34Vo1ZGT3m9yEWkrVBMeGRjkFP17Sxyzblao=
DomainKey-Signature: a=rsa-sha1; c=nofws;
d=googlegroups.com; s=beta;
h=x-sender:x-apparently-to:mime-version:content-type:date:in-reply-to
:x-ip:references:user-agent:x-http-useragent:message-id:subject:from
:to:reply-to:sender:precedence:x-google-loop:mailing-list:list-id
:list-post:list-help:list-unsubscribe:x-beenthere-env:x-beenthere;
b=2asVRARojUFeFc3R10BkLj3wg58NlR7MhcVlSAG6mp4Y2nSfGp4IvgTALIQI3tYEdH
VdLpLbX+alKxMJ2NPlnDB4fZ+Oy3yi9IxYYlxLCSYIh0C3DCId4KvOolj4iffr/bjmDn
RFRPjGC0Kyiu8/FWfn0gfVYjCF2avBxNrfg1s=
X-Sender: jeffrey...@gmail.com
X-Apparently-To: utexas-cs38...@googlegroups.com
Date: Wed, 5 Nov 2008 13:23:01 -0800 (PST)
X-IP: 24.227.245.177
X-HTTP-UserAgent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.0.3) Gecko/2008092414 Firefox/3.0.3,gzip(gfe),gzip(gfe)
From: jdiamond <jeffrey...@gmail.com>
Reply-To: utexas-cs38...@googlegroups.com
Sender: utexas-cs38...@googlegroups.com
X-Google-Loop: groups
Mailing-List: list utexas-cs38...@googlegroups.com;
contact utexas-cs389r-...@googlegroups.com
X-BeenThere-Env: utexas-cs38...@googlegroups.com
X-SpamAssassin-Status: No, hits=0.6 required=5.0
X-UTCS-Spam-Status: No, hits=-130 required=165
jdiamond
more general problem I have in this class, and so I would be very
grateful if Sandip or *anyone* else in the class could kindly answer
this.
As with many other problems, Sandip says:
(implies (and (perm x y)
(perm y z))
(perm x z))
;; One way to reason about perm of course is to wade through the
;; induction and do it. If you stare at it, you might see some lemmas
to
;; prove. For example,
;; (implies (and (mem e y)
;; (perm x (del e y)))
;; (perm (cons e x) y))
see ANYTHING that would lead me to see that lemma to prove.
It would help me a GREAT DEAL if someone would kindly:
(1) Show the induction hypothesis for this problem,
(2) Show how you derive something that suggests proving the lemma
above.
Much appreciated,
- Jeff
Sandip Ray
the idea of using app? I wouldn't quite know, and I don't think
there's an algorithm for that. That's really the creative component
of a proof. I realized that the whole reason why all this works is
because if a and b are lists of nils the function (mapnil1 a b) acts
like appending the two lists. That's just an insight I got studying
the function --- and the entire proof was based on finsing a way to
make use of that intuition. Now I did not want to use it in every
place, just where it seemed to help me. That's standard in any
mathematical proof: you have the intuition and you make use of the
intuition in the right place.
But maybe I'm not understanding your question.
-- Sandip
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=googlegroups.com; s=beta;
h=domainkey-signature:received:received:x-sender:x-apparently-to
:mime-version:content-type:received:date:in-reply-to:x-ip:references
:user-agent:x-http-useragent:message-id:subject:from:to:reply-to
:sender:precedence:x-google-loop:mailing-list:list-id:list-post
:list-help:list-unsubscribe:x-beenthere-env:x-beenthere;
bh=bXdoAh1de7Oqoy8XU6YlgEiDWKCcgiv1q+T8+y7opTk=;
b=HglZikmFYKDyV+Bt4ryuud5MSe0gSLRHZ/L5vE9qvKjNzsf0ldqIRMW07r3/DRHX9l
n8uZHDYnfcATOyOOuv/KudAPY1q6T6IJ/ZVpU+Re2KeIQPcpUbV8e/E96fyh8BOsR31j
M9Ff1qHXh6wI6WKzWL03/sinegyp1uehKqAPE=
DomainKey-Signature: a=rsa-sha1; c=nofws;
d=googlegroups.com; s=beta;
h=x-sender:x-apparently-to:mime-version:content-type:date:in-reply-to
:x-ip:references:user-agent:x-http-useragent:message-id:subject:from
:to:reply-to:sender:precedence:x-google-loop:mailing-list:list-id
:list-post:list-help:list-unsubscribe:x-beenthere-env:x-beenthere;
b=EUzxInwG79e6Pr1oSkujD0AdSki7NVbZLbrGEJVV372OdiGrkj9+TJaEsUqzTcY37k
YINA9DoGy/wV1KGgApcG3y+cBz7aRjua6NoAyeEatWfK6RbiJlMztVD0VnmH94a1qEOh
isADzXbbKxSOfefS4xHazQdw4ITy8XLgmVnlo=
X-Sender: jeffrey...@gmail.com
X-Apparently-To: utexas-cs38...@googlegroups.com
Date: Wed, 5 Nov 2008 14:28:45 -0800 (PST)
X-IP: 24.227.245.177
X-HTTP-UserAgent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.0.3) Gecko/2008092414 Firefox/3.0.3,gzip(gfe),gzip(gfe)
From: jdiamond <jeffrey...@gmail.com>
Reply-To: utexas-cs38...@googlegroups.com
Sender: utexas-cs38...@googlegroups.com
X-Google-Loop: groups
Mailing-List: list utexas-cs38...@googlegroups.com;
contact utexas-cs389r-...@googlegroups.com
X-BeenThere-Env: utexas-cs38...@googlegroups.com
X-SpamAssassin-Status: No, hits=0.6 required=5.0
X-UTCS-Spam-Status: No, hits=-130 required=165
Sandip Ray
If I were trying to use induction directly, here's probably the
induction I would use:
x <- (cdr x)
y <- (del (car x) y)
z <- (del (car x) z)
under (consp x).
If you try this induction, and then go through simplification, you'll
probably see the lemmas. I've not done this directly for a while, and
I don't have time right now, but is this the induction you tried? If
so, where did you get stuck? (BTW, do you see why I tried this
induction rather than anything else?)
But the reason why I did not do it this way is because I wanted to
emphasize that this approach is indeed a somewhat low-level term
manipulation, and does not correspond to my intuition about perm. So
I wanted to do a proof that does capture that intuition. But this
approach will probably succeed. (The induction above feels right.)
-- Sandip
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=googlegroups.com; s=beta;
h=domainkey-signature:received:received:x-sender:x-apparently-to
:mime-version:content-type:received:date:in-reply-to:x-ip:references
:user-agent:x-http-useragent:message-id:subject:from:to:reply-to
:sender:precedence:x-google-loop:mailing-list:list-id:list-post
:list-help:list-unsubscribe:x-beenthere-env:x-beenthere;
bh=Lnmyp41Kv7DMVMSA+FYTvnEEaY2fQpyRPSCzKzgJCcY=;
b=Eu0XR2zN+krFZx+Of/zB+O/MSEWkqocenPwUXdCNj4gIzeyWSwNy70hd3haI7oAxlP
pAKxa2qvt8Fj9+k33pGzQPColhlPaA+IHZuuUummrrYwKpgzYbRmwl0uCmOBrbjigYA6
u7dH55gnnmw8b2xOyMX88kPuhdyUtz9rdGqYM=
DomainKey-Signature: a=rsa-sha1; c=nofws;
d=googlegroups.com; s=beta;
h=x-sender:x-apparently-to:mime-version:content-type:date:in-reply-to
:x-ip:references:user-agent:x-http-useragent:message-id:subject:from
:to:reply-to:sender:precedence:x-google-loop:mailing-list:list-id
:list-post:list-help:list-unsubscribe:x-beenthere-env:x-beenthere;
b=tzAxFMWHFbTgPAtJb3uwmmkEL/CUNSu0FFzIBJ2njB2rmYgKWVeM0ThAMPIxwmzVX9
gFiidIbHiXYtO/T/9+BbzZN8t9dIKK2tgSSVmEuzOnhh9PVO03op3vIvZcR5/vOupkzd
4g239Z7uVIqb3ccUTDDC6LQTpxF9V8mqRJCEM=
X-Sender: jeffrey...@gmail.com
X-Apparently-To: utexas-cs38...@googlegroups.com
Date: Wed, 5 Nov 2008 17:36:28 -0800 (PST)
X-IP: 98.97.0.230
X-HTTP-UserAgent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.0.3) Gecko/2008092414 Firefox/3.0.3,gzip(gfe),gzip(gfe)
From: jdiamond <jeffrey...@gmail.com>
Reply-To: utexas-cs38...@googlegroups.com
Sender: utexas-cs38...@googlegroups.com
X-Google-Loop: groups
Mailing-List: list utexas-cs38...@googlegroups.com;
contact utexas-cs389r-...@googlegroups.com
X-BeenThere-Env: utexas-cs38...@googlegroups.com
X-SpamAssassin-Status: No, hits=0.6 required=5.0
X-UTCS-Spam-Status: No, hits=-130 required=165