Library Coq.Lists.StreamMemo


Require Import Eqdep_dec.
Require Import Streams.

Memoization

Successive outputs of a given function f are stored in a stream in order to avoid duplicated computations.

Section MemoFunction.

Variable A: Type.
Variable f: nat -> A.

CoFixpoint memo_make (n:nat) : Stream A := Cons (f n) (memo_make (S n)).

Definition memo_list := memo_make 0.

Fixpoint memo_get (n:nat) (l:Stream A) : A :=
  match n with
    | O => hd l
    | S n1 => memo_get n1 (tl l)
  end.

Theorem memo_get_correct: forall n, memo_get n memo_list = f n.

Building with possible sharing using a iterator g : We now suppose in addition that f n is in fact the n-th iterate of a function g.

Variable g: A -> A.

Hypothesis Hg_correct: forall n, f (S n) = g (f n).

CoFixpoint imemo_make (fn:A) : Stream A :=
  let fn1 := g fn in
  Cons fn1 (imemo_make fn1).

Definition imemo_list := let f0 := f 0 in
  Cons f0 (imemo_make f0).

Theorem imemo_get_correct: forall n, memo_get n imemo_list = f n.

End MemoFunction.

For a dependent function, the previous solution is reused thanks to a temporary hiding of the dependency in a "container" memo_val.

#[universes(template)]
Inductive memo_val {A : nat -> Type} : Type :=
  memo_mval: forall n, A n -> memo_val.
Arguments memo_val : clear implicits.

Section DependentMemoFunction.

Variable A: nat -> Type.
Variable f: forall n, A n.

Notation memo_val := (memo_val A).

Fixpoint is_eq (n m : nat) : {n = m} + {True} :=
  match n, m return {n = m} + {True} with
  | 0, 0 =>left True (eq_refl 0)
  | 0, S m1 => right (0 = S m1) I
  | S n1, 0 => right (S n1 = 0) I
  | S n1, S m1 =>
     match is_eq n1 m1 with
     | left H => left True (f_equal S H)
     | right _ => right (S n1 = S m1) I
     end
  end.

Definition memo_get_val n (v: memo_val): A n :=
match v with
| memo_mval m x =>
    match is_eq n m with
    | left H =>
       match H in (eq _ y) return (A y -> A n) with
        | eq_refl => fun v1 : A n => v1
       end
    | right _ => fun _ : A m => f n
    end x
end.

Let mf n := memo_mval n (f n).

Definition dmemo_list := memo_list _ mf.

Definition dmemo_get n l := memo_get_val n (memo_get _ n l).

Theorem dmemo_get_correct: forall n, dmemo_get n dmemo_list = f n.

Finally, a version with both dependency and iterator

Variable g: forall n, A n -> A (S n).

Hypothesis Hg_correct: forall n, f (S n) = g n (f n).

Let mg v := match v with
             memo_mval n1 v1 => memo_mval (S n1) (g n1 v1) end.

Definition dimemo_list := imemo_list _ mf mg.

Theorem dimemo_get_correct: forall n, dmemo_get n dimemo_list = f n.

End DependentMemoFunction.

An example with the memo function on factorial