coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about Extraction

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Question about Extraction
Date: Fri, 4 Sep 2015 23:55:53 +0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ilmars.cirulis AT gmail.com; spf=Pass smtp.mailfrom=ilmars.cirulis AT gmail.com; spf=None smtp.helo=postmaster AT mail-yk0-f172.google.com
Ironport-phdr: 9a23:Wy7rVhA9BcPKkIIJ5ilbUyQJP3N1i/DPJgcQr6AfoPdwSP79ocbcNUDSrc9gkEXOFd2CrakU16yO7eu5BDBIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/ni6bqpdaKPlkArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Ku4zSqUdBzA7OUg04tfqvF/NV0HHsnAbSyAdlgdCKwnD9hDzGJnr5HjUrO14jQieOGbsVvgfWC6/66ZwAEvpjCIOLSV/+2DNl8hxl4pUpRugo1p0xIuCM9LdD+Z3Yq6IJYBSfmFGRMsEDyE=

It happened in the following situation.

Maybe there's some way to work around it...

---

Require Import List.

Definition fin n := { m | m < n }.

Definition inc_fin_limit {n} (f: fin n): fin (S n).

Proof.

destruct f as [x p]. exists x. auto.

Defined.

Definition inc_fin_limit_for_list {n} (L: list (fin n)): list (fin (S n)) :=

map inc_fin_limit L.

Extraction inc_fin_limit_for_list.

let inc_fin_limit_for_list n l =

map (inc_fin_limit n) l

Extraction Inline inc_fin_limit.

Extraction inc_fin_limit_for_list.

let inc_fin_limit_for_list n l =

map (fun f -> f) l

On Thu, Sep 3, 2015 at 2:52 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Is there a way to get simplified result of extraction?

For example, I have function that is extracted to "let F l = map (fun f -> f) l" that can be simplified to "let F l = l".

[Coq-Club] Question about Extraction, Ilmārs Cīrulis, 09/03/2015
- Re: [Coq-Club] Question about Extraction, Ilmārs Cīrulis, 09/04/2015
  - Re: [Coq-Club] Question about Extraction, Gabriel Scherer, 09/07/2015
    - Re: [Coq-Club] Question about Extraction, John Wiegley, 09/07/2015