coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Assistance with simple bounded number proof?

From: frank maltman <frank.maltman AT googlemail.com>
To: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Assistance with simple bounded number proof?
Date: Fri, 13 May 2011 06:35:24 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=date:from:to:cc:subject:message-id:in-reply-to:references:x-mailer :mime-version:content-type:content-transfer-encoding; b=qCWDmouqnPjs7O8diTfjAknitsI1XPvT+OgxmDuJPLXsmqLkYolOkIUxkax+Z5Sa+6 LTCk8aYbnOm9bphxONEL8m8h7agJEolSR6XkP2eU0S61nicoYVU8MP2HG4DitFIoqr0y +XsleTAFWVQELWdMeTheNU7NTGm3dfP6sMaNI=

On Fri, 13 May 2011 07:24:10 +0200
Guillaume Melquiond
<guillaume.melquiond AT inria.fr>
wrote:

> Le vendredi 13 mai 2011 à 02:51 +0000, frank maltman a écrit :
>
> >   IHf : fin_nat f < fin_bound f
> >   ============================
> >    S
> >      ((fix fin_nat (b0 : nat) (f0 : fin b0) {struct f0} : nat :=
> >          match f0 with
> >          | FZ _ => 0
> >          | FS b1 f' => S (fin_nat b1 f')
> >          end) b f) < S b
> >
> > I'm left scratching my head, unfortunately. I'm not sure what I need
> > to be able to solve this.
>
> If not for the leading S constructors in both sides, your goal would be
> convertible to the induction hypothesis (since fin_bound f is b). So
> just remove them with lemma lt_n_S and then apply the hypothesis.

Thank you!

It seems blindingly obvious now that I look at it.

[Coq-Club] Assistance with simple bounded number proof?, frank maltman
- Re: [Coq-Club] Assistance with simple bounded number proof?, Guillaume Melquiond
  - Re: [Coq-Club] Assistance with simple bounded number proof?, frank maltman
- Re: [Coq-Club] Assistance with simple bounded number proof?, Adam Chlipala