The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I even tend to be a little more "extreme" when I write fixpoints:

when I write a fixpoint, I almost always try to have the indices of the inductive as arguments only (that is almost the minimal set of arguments which do not change between recursive calls).

I almost always determine which arguments change between calls and make only those required as arguments.

Thus, when I analyze

​​   Definition fold_right A B (f: B → A → A) :
      forall n, A -> list B n -> A :=
    fix go n a L :=
    match L with
    | nil _ => a
    | cons x t => f x (go _ a t)
    end.
​

I even see that the "a" argument does not need to be an argument of the fixpoint, and I tend to rather write:

​​​   Definition fold_right A B (f: B → A → A) (a : A) :
      forall n, list B n -> A :=
    fix go n L :=
    match L with
    | nil _ => a
    | cons x t => f x (go _ t)
    end.
​​

​And for fold_left, I tend to use:​

​​​​   Definition fold_left A B (f: B → A → A) :
      forall n, list B n -> A -> A :=
    fix go n L :=
    match L with
    | nil _ => fun a => a
    | cons x t => fun a => go _ t (f x a)
    end.
​

or

​   Definition fold_left A B (f: B → A → A) :
      forall n, list B n -> A -> A :=
    fix go n L :=

    fun a =>

    match L with
    | nil _ => a
    | cons x t => go _ t (f x a)
    end.

With this way to write things, it is always obvious on which arguments recursion is performed, and minimizes the number of arguments to write in recursive calls.

​

2016-02-01 13:27 GMT+01:00 Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>:

So that's the difference I missed.

 

Thank you very much!

On Mon, Feb 1, 2016 at 1:28 PM, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

On 02/01/2016 12:16 PM, Ilmārs Cīrulis wrote:

Fixpoint fold_right A B n (f: B → A → A) (a: A) (L: list B n): A :=
   match L with
   | nil _ => a
   | cons x t => f x (fold_right f a t)
   end.

You have to write this function in a slightly different way so as to convince Coq that f remains constant during each recursive call:

​​

  Definition fold_right A B (f: B → A → A) :
      forall n, A -> list B n -> A :=
    fix go n a L :=
    match L with
    | nil _ => a
    | cons x t => f x (go _ a t)
    end.

Now f is no longer an argument of the fix.

List.fold_right is written in this way too.