Assuming Hypothesis are true in induction proof...

[jdiamond]

During our class discussion, I got the impression that we were not
supposed to assume our hypothesis true while proving the induction
step (even though that is the classic power of induction proofs.) But
in the Moore notes, they show the inductive case to be true by
utilizing all the hypothesis as if they were axioms in the
simplification.

Since you can't simply say your hypothesis is true as a proof, what
the tree-copy example seems to say is that, assuming Hypothesis #2 and
#3 are true, we can show hypothesis #1 is true. Is this a correct
interpretation of how the proof works? 'Cause it seems like you get
into circular reasoning with multiple simultaneous hypothesis.

- jeff

[Sandip Ray]

Hi,

I don't understand what you mean by "we were not supposed to assume
our hypothesis true". The whole essence of induction (in ACL2 and
everywhere else) is that you assume the induction hypothesis true and
prove your conclusion. ACL2 only provides a more general-purpose
induction mechanism than you have typiclly seen in your standard math
proofs.

I think if you can give an example of a problem where you were not
allowed to assume the inductive hypothesis I can provide a clearer
answer to the confusion.

-- 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:x-ip: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=wskSQl1vJo+CvmqR1Z9I2cPVkNxWXmL4N59IQjZJTIY=;
b=XbP5r8FJVLla5ReRcqa/mpgiLo/FB7Po0Hr4ZDbR2CMMFxyH/r++Ti2t+x3fb6UUQw
GQufPK7c2GZ7GwCd8h+yrTXHHmGQCpKjM5hSMcJS1s2CLnZ1xHYhD2ffzOapviH4dqWt
m6PaJYubIVrZHpkGqgR0qwDQC77IZz3bj6+3w=
DomainKey-Signature: a=rsa-sha1; c=nofws;
d=googlegroups.com; s=beta;
h=x-sender:x-apparently-to:mime-version:content-type:date:x-ip
: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=gqeZy6HSl5PQo/C1kOm/lPAtr4yxJWTwpBUxp12LCbvPhHAHDFsY53bAbKNnqEyNxZ
KMlYkCshwGuHcxRNXtHWNcnMe8BcR6mP5gS9Z1xvGsX5uZcyBolZ1KMy57w7iuCiRc1T
c1XrK2jfXtq/hIQyVSBYkKWM7VURUzd0NQLvY=
X-Sender: jeffrey...@gmail.com
X-Apparently-To: utexas-cs38...@googlegroups.com
Date: Sat, 27 Sep 2008 17:54:16 -0700 (PDT)
X-IP: 69.149.26.213
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=-110 required=165