Library ATBR.Force

Require Import List.
Require Import Arith.

Section force.
  Variable T: Type.
  Variable f: nat -> T.

  Fixpoint force_rec acc i :=
    match i with
      | O => acc
      | S i => force_rec (f i :: acc) i
      end.

  Fixpoint nth i l :=
    match l,i with
      | nil, _ => f O
      | a::_, O => a
      |_::q, S i => nth i q
    end.
End force.

Definition print T n f := @force_rec T f nil n.

Definition id T n f :=
    let l := @print T n f in
      fun i => nth f i l.

Section correction.
  Variable T: Type.

  Lemma force_rec_rec: forall (f: nat -> T) i a, force_rec f a (S i) = f 0 :: force_rec (fun k => f (S k)) a i.

  Lemma nth_force_rec: forall n (f g: nat -> T) i a, i<n -> nth g i (force_rec f a n) = f i.

  Lemma nth_force_rec': forall n (f g: nat -> T) i, n<=i -> nth g i (force_rec f nil n) = g O.

  Lemma id_id: forall n (f: nat -> T) i, i<n -> id n f i = f i.

  Lemma id_notid: forall n (f: nat -> T) i, n<=i -> id n f i = f O.

End correction.

Section force2.
  Variable T: Type.
  Variables n m: nat.
  Variable f: nat -> nat -> T.

  Definition id2 := id n (fun i => id m (f i)).
  Definition print2 := print n (fun i => print m (f i)).

  Lemma id2_id: forall i j, i<n -> j<m -> id2 i j = f i j.
End force2.