coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]identical functions up to rewriting

From: "Yevgeniy Makarov" <emakarov AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]identical functions up to rewriting
Date: Fri, 16 Feb 2007 11:38:36 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=gA1wL7vYzSGp0kDyJlEV53ZtUwjpIRYCzgmUWICeIGjhymQmHnpGdhmZn0s0QGn2OEloewwFFtRxdlBAkrp3BVI37SLfuIUK34xkkVdixbKsbcyHKuALVMRCg0VvX6TDUUgXEggHXMzaNU0g9QQtrwbskmmBmp8EbgQQ9SkkGt0=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

Coq does not have an extensionality axiom or theorem, though this
axiom is consistent with the Set-predicative Calculus of Inductive
Constructions (see FAQ at
http://coq.inria.fr/V8.1/faq.html#htoc41). You can prove instead that
the results of application of both functions to the same argument are
equal (if it helps).

Yevgeniy

On 16 Feb 2007 01:17:48 +0000,
rcp AT cs.nott.ac.uk

<rcp AT cs.nott.ac.uk>
wrote:

Hello,

How can I prove the following two functions are the same (if at all)?

Lemma id_fin_fun: (fun (n:nat) (i: Fin n) => i) = (fun (n:nat) (i:Fin n) =>
rv n (rv n i).

Where rv (n:nat) : Fin n - Fin n, and reverses the order of Fin n. There is
a proof: forall (n:nat) (i: Fin n), rv n (rv n i) = i. When I use
extensionality I get an error - "unbounded reference in environment".

Thanks,

RP.

[Coq-Club]identical functions up to rewriting, rcp
- Re: [Coq-Club]identical functions up to rewriting, Yevgeniy Makarov
- <Possible follow-ups>
- Re: [Coq-Club]identical functions up to rewriting, rcp