The Coq mailing list

[AUGER Cédric <cirdec.auger AT laposte.net>]

I found out some behaviour of the extraction that surprised me.
No doubt the extraction did something correct, but I expected a
slightly different output.

-------------------

Require Import Utf8.
Require Import List.


Definition fold_left_dep {A : Type} {P : list A → Type}
                         (f : ∀ x l, P (x :: l) → P l)
                         : ∀ l, P l → P nil
:= fix fld l := match l with
                | nil => fun s => s
                | x :: l => fun s => fld l (f x l s)
                end.

Check @fold_left_dep.
Recursive Extraction fold_left_dep.
(*
(*  *)

type 'a list =
| Nil
| Cons of 'a * 'a list

(** val fold_left_dep : ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list ->
'a2 -> 'a2 **)

let rec fold_left_dep f l s =
  match l with
  | Nil -> s
  | Cons (x, l0) -> fold_left_dep f l0 (f x l0 s)
*)

--------------------

I did some closure in my definition of fold_left_dep (the 'f' argument
is not passed during the recursive calls), but the extraction has
removed this closure.

I expected to have:
let fold_left_dep f =
  let rec fld l s =
  match l with
  | Nil -> s
  | Cons (x, l0) -> fld l0 (f x l0 s)
  in fld

Any idea why ?

By deactivating the optimizations, I find this behaviour back (and s
abstraction is kept inside the "match with").
I do not know well enough Ocaml to tell if removing closures offers
better performance or not (I guess the compiler is smart enough to
produce the same code for both), but I tend to add closures to make
the code shorter and less error prone.

On a side note, I knew that fold_right was the function behind the
natural induction "∀ P, (∀ x l, P l → P x l) → P [] → ∀ l, P l"
and that fold_left was for some awful induction:
"∀ P, (∀ x m, P (rev m) → P (rev (x::m))) → ∀ m, P (rev m) → ∀ l, P
(rev_append m l)" and with m = [], we get
"∀ P, (∀ x m, P (rev m) → P (rev (x::m))) → P [] → ∀ l, P l"
(If I well remember, there is such a lemma in the List library).
But I did not know that fold_left was the natural reduction:
"∀ P, (∀ x l, P (x::l) → P l) → ∀ l, P l → P []".
I did not find an interesting, short but non trivial case of use for
this lemma, so I cannot tell if it should be in the standard library,
but it is definetely a good generalization of fold_left with dependant
types.