The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

The fact that "map id = id" cannot be obtained by computation alone,
so there seems to be little chance for Extraction to optimize it by
itself. Furthermore, in the current case, it is not the case that
(inc_fin_limit_for_list) is (map id) at the Coq level: the
inc_fin_limit change the type of its argument, so it is not an
identity function, and you could not prove that (map inc_fin_limit L =
L) as the two sides of the equalities have different types.


You can work around this by using a different representation of "lists
whose elements are constrained by predicates". A trivial approach is
to pass separately (L: list nat) a boolean or Prop, for example
(List.Forall (below n) L). The inc_fin_limit_for_list function then
has type

  Definition below n := fun m => m < n.
  Definition inc_fin_limit_for_list {n} L:
   (Forall (below n) L) -> Forall (below (S n)) L.

This representation makes it obvious that the list itself is not
mutated, but then the user has to pass the elements and their
properties separately. A compromise would be, for example (apologies
for the naive tactics code):

  Definition below n := fun m => m < n.

  Definition refined_list {A} (p : A -> Prop) :=
    { L : list A | forall x, In x L -> p x }.

  Definition inc_limit_for_list {n} (L : refined_list (below n)) :
refined_list (below (S n)).
    destruct L as [L H]. exists L.
    intros x Hx. assert (below n x); unfold below in *; auto.
  Defined.

  Extraction inc_limit_for_list.
  (* let inc_limit_for_list n l = l *)

This is admittedly less modular than your approach as you have to
define the element properties globally on the list, for the sole
purpose of efficiency.

I think if you want tight control over the generated ML code, the
approach of writing the computational part of your program in ML style
(with little dependent typing) and passing around
properties/invariants separately is probably the most reliable.

On Fri, Sep 4, 2015 at 10:55 PM, Ilmārs Cīrulis
<ilmars.cirulis AT gmail.com>
 wrote:
> 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".
>>
>>
>>
>>
>