coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mixing induction and coinduction

From: Taral <taralx AT gmail.com>
To: muad <muad.dib.space AT gmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Mixing induction and coinduction
Date: Thu, 27 Aug 2009 13:38:00 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=Sg2YygWm7ni7/ilptTthhMDRG5tYzF78aFK0SfpWhT3KZbSLvU3UtCedChBlHPlWsd BBwsQDNnxM3knF7e5nE38hrdLJbVccRYD+RsbU0jTXjgfUDav1RzVq88vB5aCmaAfNoJ 4+yIlmtOwaA77YAWDlDoKBd+6v1vLyR8EOUp4=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Thu, Aug 27, 2009 at 12:56 PM,
muad<muad.dib.space AT gmail.com>
wrote:
> My proof of this Fin injectivity is the culmination of about 500 line script
> using pigeonhole principle, I assume you have something similar?

I haven't actually written it, but that's basically how it goes.

If n < m, build an element of Fin m that is not in Fin n, rewrite the
type, then deconstruct and use inversion after n unrolls.

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown

[Coq-Club] Mixing induction and coinduction, Edsko de Vries
- Re: [Coq-Club] Mixing induction and coinduction, Ekaterina Komendantskaya
  - Re: [Coq-Club] Mixing induction and coinduction, Nils Anders Danielsson
- Re: [Coq-Club] Mixing induction and coinduction, Celia Picard
  - Re: [Coq-Club] Mixing induction and coinduction, Taral
    - Re: [Coq-Club] Mixing induction and coinduction, muad
      - Re: [Coq-Club] Mixing induction and coinduction, Taral