Library ListFromRight.foldl_issue

Author: Jean-François Monin, Verimag, Université Grenoble Alpes

List traversal from right to left: a first attempt.

Origin: introductory example developed with Dominique Larchey-Wendling for our chapter on the Braga method.

Here is a reference definition of OCaml List.fold_left, which follows the same structural pattern as List.fold_right, but where lists are traversed from right to left.

let rec foldl_ref f b l = fakematch l with
  | [] → b
  | u +: z → f (foldl_ref f b u) z

This can be actually programmed by reflecting this decomposition of lists from the right using l2r.

let rec foldl_ref f b l = match l2r l with
  | Nilr → b
  | Consr (u, z) → f (foldl_ref f b u) z

This definition corresponds to the usual informal drawings explaining the expected result. It is of course quite inefficient, however and it can be seen as a specification of OCaml fold_left, named foldl here.

let rec fold_left f b l = match l with
   | [] → b
   | x :: l → fold_left f (f b x) l

This Coq script plays with a first direct attempt to define foldl_ref in Coq and to prove a simple property on it, in order to illustrate a simple situation where Coq standard inversion fails whereas the small inversion mechanism presented at TYPES'22 succeeds.

However the definition used here for fold_ref raises other issues which are solved with another "phase shifted" definition, see the sibling foldl.v file.

Basic definitions (in particular for small inversions) are in rl.v.

From Stdlib Require Import Utf8.

From Stdlib Require Import List.
Import ListNotations.

Require Import rl.

Section sec_context.

  Context {A B: Type}.
  Implicit Type l u v : list A.
  Implicit Type x y z : A.
  Implicit Type b : B.

  Section sec_params_foldl.
    Variable f: B → A → B.
    Variable b : B.

A convenient helper

Lemma rew {u z} (d : 𝔻 listz (l2r (u +:z))) : 𝔻 listz (Consr u z).
Proof. case l2r_consr; exact d. Defined.

A reference definition for fold_left

    Fixpoint foldl_ref l (d: 𝔻 listz (l2r l)): B :=
      match l2r l in rl l return 𝔻 listz (l2r l) → B with
      | Nilr ⇒ λ d, b
      | Consr u z ⇒ λ d, f (foldl_ref u (π _𝔻 listz_Consr (rew d))) z
      end d.

A lemma where small inversion suceeds, in contrast with Coq inversion.

    Lemma foldl_ref_nil d : foldl_ref [] d = b.
    Proof.
      cbn in d.
      inversion d .
      Fail dependent inversion d.
      destruct (𝔻 listz_inv d) .
      cbn.
      reflexivity.
    Qed.

Unfortunately, a similar statement for the Consr case would need a preliminary step which is not accepted.

    Lemma foldl_ref_cons u z d : foldl_ref (u +: z) d = b.
    Proof.
      Fail rewrite l2r_consr in d.
      revert d.
      Fail rewrite l2r_consr.
    Abort.

A solution is presented in foldl.v

End sec_params_foldl.
End sec_context.