Library ListFromRight.foldl

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


List traversal from right to left.

Origin: introductory example developed with Dominique Larchey-Wendling for our chapter on the Braga method.
Using a well-suited definition of the reference program foldl_ref we can avoid the relational graph of the Braga method. We can even avoid inversions (see file foldl_rl_only.v), but one may consider that foldl_ref below is more natural. It is recovered here using an ad-hoc sigma type and 2022 small inversions.
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 defined in rl.v. 
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 point is to get a Coq definition of foldl_ref, whereas the recursion is not the usual structural recursion on lists; small inversions will then be used.

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

Defining AND reasoning on a direct definition of foldl_ref, corresponding to the above OCaml program turns out more difficult than expected. Things get smoother with 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 u (l2r u) (π_𝔻listz_Consr d)) z
      end d.

We could then just define foldl_ref l d := foldl_rl l (l2r l) d and show that OCaml fold_left returns the same result, see foldl_rl_only.v
But here we want to stick to the above algorithm for foldl_ref, To this effect we define it according to foldl_rl by construction. Small inversions are needed in the 2 generated proof obligations.
    Definition spec_foldl_ref l d := {b : B | b = foldl_rl l (l2r l) d}.

A convenient helper
    Definition Consr_spec {u z} :
      (∀d, {b : B | b = foldl_rl (u+:z) (Consr u z) d}) →
       ∀d, spec_foldl_ref (u+:z) d.
    Proof. intro S; red. rewrite l2r_consr. exact S. Defined.

Recursive algorithm for foldl_ref
    Arguments exist {_ _}.
    Let Fixpoint foldl_ref_cbc l d : spec_foldl_ref l d.
      refine(
          match l2r l in rl l return ∀ d, spec_foldl_ref l d with
          | Nilr ⇒ λ d, exist b _
          | Consr u z ⇒
              Consr_spec (λ d, let (b, E) := foldl_ref_cbc u (π_𝔻listz_Consr d) in
                               exist (f b z) _)
          end d).
      - destruct (𝔻listz_inv d). cbn. reflexivity.
      - destruct (𝔻listz_inv_π d). cbn. rewrite <- E. reflexivity.
    Defined.
    Definition foldl_ref l (d: 𝔻listz (l2r l)): B := proj1_sig (foldl_ref_cbc l d).

    Lemma foldl_ref_eq l (d: 𝔻listz (l2r l)) : foldl_ref l d = foldl_rl l (l2r l) d.
    Proof. exact (proj2_sig (foldl_ref_cbc l d)). Qed.

Another example using 𝔻listz_inv, for illustration: proof irrelevance of foldl_ref. Here Coq dependent inversion happens to work as well -- yielding a much more complex the proof term.
    Lemma foldl_rl_pirr l (r : rl l) (d d': 𝔻listz r) :
      foldl_rl l r d = foldl_rl l r d'.
    Proof.
      induction d as [ | u z d IHd]; cbn.
      - destruct (𝔻listz_inv d'). cbn. reflexivity.
      - destruct (𝔻listz_inv d') as [d']; cbn. rewrite (IHd d'). reflexivity.
    Qed.

    Corollary foldl_ref_pirr l (d d': 𝔻listz (l2r l)) : foldl_ref l d = foldl_ref l d'.
    Proof. do 2 rewrite foldl_ref_eq. apply foldl_rl_pirr. Qed.

    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_ref f b l d.
  Proof.
    intros. rewrite foldl_ref_eq.
    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 Inline Consr_spec.
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 rec foldl_ref f b l =
  match l2r l with
  | Nilr -> b
  | Consr (u, z) -> f (foldl_ref f b u) z

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

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