Library ListFromRight.foldl_rl_only

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


List traversal from right to left: minimalist version.

Origin: introductory example developed with Dominique Larchey-Wendling for our chapter on the Braga method.
Using a well-suited definition of foldl_ref (the second one below), we can avoid the relational graph of the Braga method and no inversion is needed. In one prefers the first version below, see file foldl.v where small inversions are needed.
We consider 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 reasonable 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 scripts shows that foldl is actually extensionally equal to foldl_ref.
The version presented in this file is based on the following variant of foldl_ref: 
let foldl_ref f b l =
  let rec foldl_rl = function
  | Nilr -> b
  | Consr (u, z) -> f (foldl_rl (l2r u)) z
  in foldl_rl (l2r l)
The amount of proofs is then very small. Too small, actually, to need (small) inversions: it just aims at showing that, in this case study, we can limit ourselve to the first ingredient of the Braga method the inductive domain called 𝔻listz here, defined in rl.v.

Require Import Utf8 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.

Reference program for fold_left

We first define a "phase-shifted" version where l2r l is pre-computed

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

    Definition foldl_ref l d := foldl_rl (l2r l) d.
    Definition foldl_ref_total l := foldl_ref l (𝔻listz_all l).

  End sec_params_foldl.

OCaml fold_left

  Fixpoint foldl f b l : B :=
    match l with
    | [] ⇒ b
    | x :: v ⇒ foldl f (f b x) v
    end.

foldl is compatible with +: in the following sense
  Lemma foldl_consr f b (u: list A) (z: A) :
    foldl f b (u +: z) = f (foldl f b u) z.

  Proof.
    revert b. induction u as [|x u Hu]; intro b; simpl.
    - reflexivity.
    - rewrite Hu. reflexivity.
  Qed.

Partial correctness wrt foldl_ref: whenever foldl_ref terminates, foldl computes the same result

  Theorem foldl_eq_partial :
    ∀ f b l (d: 𝔻listz (l2r l)), foldl f b l = foldl_rl f b (l2r l) d.
  Proof.
    intros.
    induction d as [ | u z d IHd]; cbn.
    - reflexivity.
    - rewrite foldl_consr, <- IHd. reflexivity.
  Qed.

Total correctness wrt foldl_ref follows independently
  Corollary foldl_eq_total :
    ∀ f b l, foldl f b l = foldl_ref_total f b l.
  Proof.
    intros; apply foldl_eq_partial.
  Qed.

End sec_context.

Extraction

Require Import Extraction.
Extract Inductive list ⇒ "list" [ "[]" "( :: )" ].
Extraction Implicit foldl_rl [l].
Extraction foldl_rl.
Extraction Inline foldl_rl.
Recursive Extraction foldl_ref foldl.

type 'a rl =
| Nilr
| Consr of 'a list * 'a

(** val l2r : 'a1 list -> 'a1 rl **)

let rec l2r = function
| [] -> Nilr
| x :: v -> (match l2r v with
           | Nilr -> Consr ([], x)
           | Consr (u, z) -> Consr ((x :: u), z))

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

let foldl_ref f b l =
  let rec foldl_rl = function
  | Nilr -> b
  | Consr (u, z) -> f (foldl_rl (l2r u)) z
  in foldl_rl (l2r l)

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

let rec foldl f b = function
| [] -> b
| x :: v -> foldl f (f b x) v