Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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.A:Type
f:nat -> A
forall n : nat, memo_get n memo_list = f n
Proof.A:Type
f:nat -> A
forall n : nat, memo_get n memo_list = f n
assert (F1: forall n m, memo_get n (memo_make m) = f (n + m)).A:Type
f:nat -> A
forall n m : nat, memo_get n (memo_make m) = f (n + m)
A:Type
f:nat -> A
F1:forall n m : nat,
memo_get n (memo_make m) = f (n + m)
forall n : nat, memo_get n memo_list = f n
{A:Type
f:nat -> A
forall n m : nat, memo_get n (memo_make m) = f (n + m) induction n as [| n Hrec]; try (intros m; reflexivity).A:Type
f:nat -> A
n:nat
Hrec:forall m : nat,
memo_get n (memo_make m) = f (n + m)
forall m : nat,
memo_get (S n) (memo_make m) = f (S n + m)
  intros m; simpl; rewrite Hrec.A:Type
f:nat -> A
n:nat
Hrec:forall m0 : nat,
memo_get n (memo_make m0) = f (n + m0)
m:nat
f (n + S m) = f (S (n + m))
  rewrite plus_n_Sm; auto. }A:Type
f:nat -> A
F1:forall n m : nat,
memo_get n (memo_make m) = f (n + m)
forall n : nat, memo_get n memo_list = f n
intros n; transitivity (f (n + 0)); try exact (F1 n 0).A:Type
f:nat -> A
F1:forall n0 m : nat,
memo_get n0 (memo_make m) = f (n0 + m)
n:nat
f (n + 0) = f n
rewrite <- plus_n_O; auto.
Qed.

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.A:Type
f:nat -> A
g:A -> A
Hg_correct:forall n : nat, f (S n) = g (f n)
forall n : nat, memo_get n imemo_list = f n
Proof.A:Type
f:nat -> A
g:A -> A
Hg_correct:forall n : nat, f (S n) = g (f n)
forall n : nat, memo_get n imemo_list = f n
assert (F1: forall n m, memo_get n (imemo_make (f m)) = f (S (n + m))).A:Type
f:nat -> A
g:A -> A
Hg_correct:forall n : nat, f (S n) = g (f n)
forall n m : nat,
memo_get n (imemo_make (f m)) = f (S (n + m))
A:Type
f:nat -> A
g:A -> A
Hg_correct:forall n : nat, f (S n) = g (f n)
F1:forall n m : nat,
memo_get n (imemo_make (f m)) = f (S (n + m))
forall n : nat, memo_get n imemo_list = f n
{A:Type
f:nat -> A
g:A -> A
Hg_correct:forall n : nat, f (S n) = g (f n)
forall n m : nat,
memo_get n (imemo_make (f m)) = f (S (n + m)) induction n as [| n Hrec]; try (intros m; exact (eq_sym (Hg_correct m))).A:Type
f:nat -> A
g:A -> A
Hg_correct:forall n0 : nat, f (S n0) = g (f n0)
n:nat
Hrec:forall m : nat,
memo_get n (imemo_make (f m)) = f (S (n + m))
forall m : nat,
memo_get (S n) (imemo_make (f m)) = f (S (S n + m))
  simpl; intros m; rewrite <- Hg_correct, Hrec, <- plus_n_Sm; auto. }A:Type
f:nat -> A
g:A -> A
Hg_correct:forall n : nat, f (S n) = g (f n)
F1:forall n m : nat,
memo_get n (imemo_make (f m)) = f (S (n + m))
forall n : nat, memo_get n imemo_list = f n
destruct n as [| n]; try reflexivity.A:Type
f:nat -> A
g:A -> A
Hg_correct:forall n0 : nat, f (S n0) = g (f n0)
F1:forall n0 m : nat,
memo_get n0 (imemo_make (f m)) = f (S (n0 + m))
n:nat
memo_get (S n) imemo_list = f (S n)
unfold imemo_list; simpl; rewrite F1.A:Type
f:nat -> A
g:A -> A
Hg_correct:forall n0 : nat, f (S n0) = g (f n0)
F1:forall n0 m : nat,
memo_get n0 (imemo_make (f m)) = f (S (n0 + m))
n:nat
f (S (n + 0)) = f (S n)
rewrite <- plus_n_O; auto.
Qed.

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.A:nat -> Type
f:forall n : nat, A n
mf:=fun n : nat => memo_mval n (f n):nat -> memo_val
forall n : nat, dmemo_get n dmemo_list = f n
Proof.A:nat -> Type
f:forall n : nat, A n
mf:=fun n : nat => memo_mval n (f n):nat -> memo_val
forall n : nat, dmemo_get n dmemo_list = f n
intros n; unfold dmemo_get, dmemo_list.A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
memo_get_val n
  (memo_get memo_val n (memo_list memo_val mf)) = 
f n
rewrite (memo_get_correct memo_val mf n); simpl.A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
match is_eq n n with
| left H =>
    match H in (_ = y) return (A y -> A n) with
    | eq_refl => fun v1 : A n => v1
    end
| right _ => fun _ : A n => f n
end (f n) = f n
case (is_eq n n); simpl; auto; intros e.A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
match e in (_ = y) return (A y -> A n) with
| eq_refl => fun v1 : A n => v1
end (f n) = f n
assert (e = eq_refl n).A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
e = eq_refl
A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
H:e = eq_refl
match e in (_ = y) return (A y -> A n) with
| eq_refl => fun v1 : A n => v1
end (f n) = f n
-A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
e = eq_refl apply eq_proofs_unicity.A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
forall x y : nat, x = y \/ x <> y
  induction x as [| x Hx]; destruct y as [| y].A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
0 = 0 \/ 0 <> 0
A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
y:nat
0 = S y \/ 0 <> S y
A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y : nat, x = y \/ x <> y
S x = 0 \/ S x <> 0
A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
S x = S y \/ S x <> S y
  +A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
0 = 0 \/ 0 <> 0 left; auto.
  +A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
y:nat
0 = S y \/ 0 <> S y right; intros HH; discriminate HH.
  +A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y : nat, x = y \/ x <> y
S x = 0 \/ S x <> 0 right; intros HH; discriminate HH.
  +A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
S x = S y \/ S x <> S y case (Hx y).A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
x = y -> S x = S y \/ S x <> S y
A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
x <> y -> S x = S y \/ S x <> S y
    *A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
x = y -> S x = S y \/ S x <> S y intros HH; left; case HH; auto.
    *A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
x <> y -> S x = S y \/ S x <> S y intros HH; right; intros HH1; case HH.A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
HH:x <> y
HH1:S x = S y
x = y
      injection HH1; auto.
-A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
n:nat
e:n = n
H:e = eq_refl
match e in (_ = y) return (A y -> A n) with
| eq_refl => fun v1 : A n => v1
end (f n) = f n rewrite H; auto.
Qed.

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.A:nat -> Type
f:forall n : nat, A n
mf:=fun n : nat => memo_mval n (f n):nat -> memo_val
g:forall n : nat, A n -> A (S n)
Hg_correct:forall n : nat, f (S n) = g n (f n)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
forall n : nat, dmemo_get n dimemo_list = f n
Proof.A:nat -> Type
f:forall n : nat, A n
mf:=fun n : nat => memo_mval n (f n):nat -> memo_val
g:forall n : nat, A n -> A (S n)
Hg_correct:forall n : nat, f (S n) = g n (f n)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
forall n : nat, dmemo_get n dimemo_list = f n
intros n; unfold dmemo_get, dimemo_list.A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
memo_get_val n
  (memo_get memo_val n (imemo_list memo_val mf mg)) =
f n
rewrite (imemo_get_correct memo_val mf mg); simpl.A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
match is_eq n n with
| left H =>
    match H in (_ = y) return (A y -> A n) with
    | eq_refl => fun v1 : A n => v1
    end
| right _ => fun _ : A n => f n
end (f n) = f n
A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
forall n0 : nat,
mf (S n0) = memo_mval (S n0) (g n0 (f n0))
-A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
match is_eq n n with
| left H =>
    match H in (_ = y) return (A y -> A n) with
    | eq_refl => fun v1 : A n => v1
    end
| right _ => fun _ : A n => f n
end (f n) = f n case (is_eq n n); simpl; auto; intros e.A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
match e in (_ = y) return (A y -> A n) with
| eq_refl => fun v1 : A n => v1
end (f n) = f n
  assert (e = eq_refl n).A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
e = eq_refl
A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
H:e = eq_refl
match e in (_ = y) return (A y -> A n) with
| eq_refl => fun v1 : A n => v1
end (f n) = f n
  +A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
e = eq_refl apply eq_proofs_unicity.A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
forall x y : nat, x = y \/ x <> y
    induction x as [| x Hx]; destruct y as [| y].A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
0 = 0 \/ 0 <> 0
A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
y:nat
0 = S y \/ 0 <> S y
A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y : nat, x = y \/ x <> y
S x = 0 \/ S x <> 0
A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
S x = S y \/ S x <> S y
    *A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
0 = 0 \/ 0 <> 0 left; auto.
    *A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
y:nat
0 = S y \/ 0 <> S y right; intros HH; discriminate HH.
    *A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y : nat, x = y \/ x <> y
S x = 0 \/ S x <> 0 right; intros HH; discriminate HH.
    *A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
S x = S y \/ S x <> S y case (Hx y).A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
x = y -> S x = S y \/ S x <> S y
A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
x <> y -> S x = S y \/ S x <> S y
      --A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
x = y -> S x = S y \/ S x <> S y intros HH; left; case HH; auto.
      --A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
x <> y -> S x = S y \/ S x <> S y intros HH; right; intros HH1; case HH.A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
x:nat
Hx:forall y0 : nat, x = y0 \/ x <> y0
y:nat
HH:x <> y
HH1:S x = S y
x = y
         injection HH1; auto.
  +A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
e:n = n
H:e = eq_refl
match e in (_ = y) return (A y -> A n) with
| eq_refl => fun v1 : A n => v1
end (f n) = f n rewrite H; auto.
-A:nat -> Type
f:forall n0 : nat, A n0
mf:=fun n0 : nat => memo_mval n0 (f n0):nat -> memo_val
g:forall n0 : nat, A n0 -> A (S n0)
Hg_correct:forall n0 : nat, f (S n0) = g n0 (f n0)
mg:=fun v : memo_val =>
match v with
| memo_mval n1 v1 => memo_mval (S n1) (g n1 v1)
end:memo_val -> memo_val
n:nat
forall n0 : nat,
mf (S n0) = memo_mval (S n0) (g n0 (f n0)) intros n1; unfold mf; rewrite Hg_correct; auto.
Qed.

End DependentMemoFunction.

An example with the memo function on factorial

(*
Require Import ZArith.
Open Scope Z_scope.

Fixpoint tfact (n: nat) :=
  match n with
   | O => 1
   | S n1 => Z.of_nat n * tfact n1
  end.

Definition lfact_list :=
  dimemo_list _ tfact (fun n z => (Z.of_nat (S  n) * z)).

Definition lfact n := dmemo_get _ tfact n lfact_list.

Theorem lfact_correct n: lfact n = tfact n.
Proof.
intros n; unfold lfact, lfact_list.
rewrite dimemo_get_correct; auto.
Qed.

Fixpoint nop p :=
  match p with
   | xH => 0
   | xI p1 => nop p1
   | xO p1 => nop p1
  end.

Fixpoint test z :=
  match z with
   | Z0 => 0
   | Zpos p1 => nop p1
   | Zneg p1 => nop p1
  end.

Time Eval vm_compute in test (lfact 2000).
Time Eval vm_compute in test (lfact 2000).
Time Eval vm_compute in test (lfact 1500).
Time Eval vm_compute in (lfact 1500).
*)