Library CoqApprox.basic_rec

This file is part of the CoqApprox formalization of rigorous polynomial approximation in Coq: http://tamadi.gforge.inria.fr/CoqApprox/
Copyright (c) 2010-2013, ENS de Lyon and Inria.
This library is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the library under the terms of the CeCILL-C license as circulated by CEA, CNRS and Inria at the following URL: http://www.cecill.info/
As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the library's author, the holder of the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details.

Require Import ZArith.
Require Import NaryFunctions.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple.
Require Import seq_compl nary_tuple.


Set Implicit Arguments.

Ltac flatten := repeat
  first[rewrite<-pred_of_minus in *| rewrite<-plusE in *|rewrite<-minusE in *].
Ltac iomega := intros; flatten; (omega || apply/leP; omega).
Ltac iomega_le := (repeat move/leP=>?); iomega.

Section Defix1.

Variable T : Type.

Variable F : T -> nat -> T.
to be instantiated by a function satisfying u(n) = F(u(n-1), n).

Fixpoint loop1 (n p : nat) (a : T) (s : seq T) {struct n} : seq T :=
  match n with
    | 0 => s
    | m.+1 => let c := F a p in loop1 m p.+1 c (c :: s)
  end.

Variable a0 : T.

Definition rec1down n := loop1 n 1 a0 [:: a0].

Definition rec1up n := rev (rec1down n).

Lemma loop1SE :
  forall n p a s,
  (loop1 n.+1 p a s) = let c := F a p in loop1 n p.+1 c (c :: s).

Lemma loop1E : forall p a s, (loop1 0 p a s) = s.

Lemma size_loop1 : forall n p a s, size (loop1 n p a s) = n + size s.

Lemma size_rec1down : forall n, size (rec1down n) = n.+1.

Lemma size_rec1up n : size (rec1up n) = n.+1.

Variable d : T.

Lemma head_loop1 :
  forall n s a p, head d s = a ->
  head d (loop1 n.+1 p a s) = F (head d (loop1 n p a s)) (n+p).

Lemma head_rec1down n :
  head d (rec1down n.+1) = F (head d (rec1down n)) n.+1.


Lemma rec1up_nth_last k : nth d (rec1up k) k = last d (rec1up k).

Lemma rec1down_correct k :
  nth d (rec1down k.+1) 0 = F (nth d (rec1down k) 0) k.+1.

Lemma rec1up_correct k :
  nth d (rec1up k.+1) k.+1 = F (nth d (rec1up k) k) k.+1.

Lemma nth_defaults d1 d2 (s : seq T) n :
    n < size s -> nth d1 s n = nth d2 s n.

Lemma loop1S_ex :
  forall n p a s, exists c,
  loop1 n.+1 p a s = c :: (loop1 n p a s).

Lemma behead_rec1down n: behead (rec1down n.+1) = rec1down n.

Lemma nth_rec1down d1 p q n:
  nth d1 (rec1down (p+q+n)) (p+q) = nth d1 (rec1down (p+n)) p.

Lemma nth_rec1down_dflt2 d1 d2 p q n:
  nth d1 (rec1down (p+q+n)) (p+q) = nth d2 (rec1down (p+n)) p.

Lemma rec1down_nth_indep d1 d2 m1 m2 n:
  n <= m1 -> n <= m2 ->
  nth d1 (rec1down m1) (m1 - n) = nth d2 (rec1down m2) (m2 - n).

Lemma rec1up_nth_indep d1 d2 m1 m2 n :
  n <= m1 -> n <= m2 ->
  nth d1 (rec1up m1) n = nth d2 (rec1up m2) n.

For the base case

Lemma rec1down_co0 n: nth d (rec1down n) n = a0.

Lemma rec1down_co0' n: last d (rec1down n) = a0.

Lemma rec1up_co0 n : nth d (rec1up n) 0 = a0.

Lemma rec1up_co0' n : head d (rec1up n) = a0.

End Defix1.

Section Test1.

Let n_rec (a0 : nat) (n : nat) := n.
Eval compute in rec1up n_rec 17 5.

Let fact_rec a n := (a * n)%N.
Let fact n := rec1up fact_rec 1%N n.
Eval compute in fact 8.

Let factz_rec a n := (a * (Z_of_nat n))%Z.
Definition factz n := rec1up factz_rec 1%Z n.
Eval compute in factz 100.

End Test1.

Section Defix2.

Variable T : Type.

Variable F : T -> T -> nat -> T.
to be instantiated by a function satisfying u(n) = F(u(n-2), u(n-1), n).

Fixpoint loop2 (n p : nat) (a b : T) (s : seq T) {struct n} : seq T :=
  match n with
    | 0 => s
    | m.+1 => let c := F a b p in loop2 m p.+1 b c (c :: s)
  end.

Variables a0 a1 : T.

Definition rec2down n :=
  if n is n'.+1 then (loop2 n' 2 a0 a1 [:: a1; a0]) else [:: a0].

Definition rec2up n := (rev (rec2down n)).

Lemma loop2E :
  forall n p a b s,
    (loop2 n.+1 p a b s) = let c := F a b p in loop2 n p.+1 b c (c :: s).

Lemma size_loop2 : forall n p a b s, size (loop2 n p a b s) = n + size s.

Lemma size_rec2down : forall n, size (rec2down n) = n.+1.

Lemma size_rec2up n : size (rec2up n) = n.+1.

Variable d : T.

Lemma head_loop2 :
  forall n s a b p, hb d s = a -> head d s = b ->
    let s' := (loop2 n p a b s) in
      head d (loop2 n.+1 p a b s) = F (hb d s') (head d s') (n+p).

Lemma head_rec2down :
  forall n, head d (rec2down n.+2) =
    F (hb d (rec2down n.+1)) (head d (rec2down n.+1)) n.+2.

Lemma behead_loop2 :
  forall n s a b p, behead (loop2 n.+1 p a b s) = loop2 n p a b s.

Lemma behead_rec2down :
  forall n, behead (rec2down n.+1) = rec2down n.


Lemma rec2up_nth_last : forall k, nth d (rec2up k) k = last d (rec2up k).

Lemma rec2down_correct k :
  nth d (rec2down k.+2) 0 =
  F (nth d (rec2down k.+1) 1) (nth d (rec2down k.+1) 0) k.+2.

Lemma rec2down_correct' k :
  nth d (rec2down k.+2) 0 =
  F (nth d (rec2down k) 0) (nth d (rec2down k.+1) 0) k.+2.

Relying on rec2down_correct
Lemma rec2up_correct k :
    nth d (rec2up k.+2) k.+2 =
    F (nth d (rec2up k.+1) k) (nth d (rec2up k.+1) k.+1) k.+2.

Relying on rec2down_correct'
Lemma rec2up_correct' k :
    nth d (rec2up k.+2) k.+2 =
    F (nth d (rec2up k) k) (nth d (rec2up k.+1) k.+1) k.+2.

Lemma loop2S_ex :
  forall n p a b s, exists c,
  loop2 n.+1 p a b s = c :: (loop2 n p a b s).

Lemma behead_rec2down_again :
  forall n,
  behead (rec2down n.+1) = rec2down n.

Lemma nth_rec2down d1 p q n :
  nth d1 (rec2down (p+q+n)) (p+q) = nth d1 (rec2down (p+n)) p.

Lemma nth_rec2down_dflt2 d1 d2 p q n :
  nth d1 (rec2down (p+q+n)) (p+q) = nth d2 (rec2down (p+n)) p.

Lemma nth_rec2down_indep d1 d2 m1 m2 n : n <= m1 -> n <= m2 ->
  nth d1 (rec2down m1) (m1 - n) = nth d2 (rec2down m2) (m2 - n).

Lemma nth_rec2up_indep d1 d2 m1 m2 n : n <= m1 -> n <= m2 ->
  nth d1 (rec2up m1) n = nth d2 (rec2up m2) n.

For the base case

Lemma rec2down_co0 : forall n, nth d (rec2down n) n = a0.

Lemma rec2up_co0 n : nth d (rec2up n) 0 = a0.

Lemma rec2down_co1 : forall n, nth d (rec2down n.+1) n = a1.

Lemma rec2up_co1 n : nth d (rec2up n.+1) 1 = a1.

End Defix2.

Section Test2.

Let foo2_rec (a b : Z*nat) (n : nat) := (a.1 + b.1, n)%Z.
Let foo2 n := rec2up foo2_rec (Z0,O) (1%Z,1%N) n.
Eval compute in foo2 5.

Let fibz_rec (a b : Z) (_ : nat) := (a + b)%Z.
Definition fibz n := rec2up fibz_rec 0%Z 1%Z n.
Eval compute in fibz 5.

End Test2.

Define some "aliases" for the purposes of partial-evaluation.
Definition snd' := Eval unfold snd in snd.

Fixpoint catrev' T (s1 s2 : seq T) {struct s1} : seq T :=
  match s1 with
  | [::] => s2
  | x :: s1' => catrev' s1' (x :: s2)
  end.
Definition rev' {T} (s : seq T) := nosimpl (catrev' s [::]).

Lemma rev'E T : @rev' T =1 @rev T.

Definition hide_let (A B : Type) (a : A) (v : A -> B) := let x := a in v x.

Define a function to make a Tuple slide, popping the left-most component.
Fixpoint slideN_aux (T : Type) (c : T) (n0 : nat) : T ^ n0 -> T ^ S n0 :=
  match n0 return (T ^ n0 -> T ^ S n0) with
    | 0 => fun _ : T ^ 0 => (c, tt)
    | S n1 => fun b0 : T ^ S n1 =>
        let (a, b') := b0 in cons_Tuple a (@slideN_aux T c n1 b')
  end.

Definition slideN (T : Type) (n : nat) (b : T ^ n) (c : T) : T ^ n :=
  snd' (@slideN_aux T c n b).

Section DefixN.

Variable T : Type.

Variable N : nat.

Variable init : T ^ N.

Variable F : T ^^ N --> (nat -> T).
Let F1 := nuncurry F.
The variable F can be instantiated by a function representing the sequence u(n) = F(u(n-N),..., u(n-1), n).

Fixpoint loopN (n : nat) (p : nat) : (T ^^ N --> (seq T -> seq T)) :=
  match n with
    | O => napply_discard T (fun x : seq T => x) N
    | S n' =>
      ncurry
      (fun (t : T ^ N) (l : seq T) =>
        hide_let (F1 t p) (fun v1 =>
          nuncurry (loopN n' p.+1) (slideN t v1) (v1 :: l)))
  end.

Definition recNdown n :=
  if (n.+1-N) is n'.+1
    then (nuncurry (loopN n'.+1 N) init (rev' (Ttoseq init)))
    else rev (take n.+1 (Ttoseq init)).

Lemma recNdownE (n : nat) :
  recNdown n =
  if n>=N
    then (nuncurry (loopN (n-N).+1 N) init (rev (Ttoseq init)))
    else rev (take n.+1 (Ttoseq init)).

Definition recNup n := rev (recNdown n).

Lemma nuncurry_const (B : Type) (b : B) (n : nat) (d : T ^ n) :
  (nuncurry (napply_discard T b n) d) = b.

Lemma nuncurry_ncurry (A B : Type) (n : nat) (f : A ^ n -> B) (x : A ^ n) :
  nuncurry (ncurry f) x = f x.

Lemma loopNE (n p : nat) t s :
  nuncurry (loopN n.+1 p) t s = let c := F1 t p in
  nuncurry (loopN n p.+1) (slideN t c) (c :: s).

Lemma size_loopN (n p : nat) t s :
  size (nuncurry (loopN n p) t s) = n + size s.

Lemma size_recNdown : forall n, size (recNdown n) = n.+1.

Lemma size_recNup : forall n, size (recNup n) = n.+1.

End DefixN.

Theorem recNdown_init_correct (T : Type) (N : nat)
  (init : T ^ N) (F : T ^^ N --> (nat -> T)) (F1 := nuncurry F) (n : nat) :
  n < N ->
  recNdown init F n = rev (take n.+1 (Ttoseq init)).

Theorem recNup_init_correct (T : Type) (N : nat)
  (init : T ^ N) (F : T ^^ N --> (nat -> T)) (F1 := nuncurry F) (n : nat) :
  n < N ->
  recNup init F n = take n.+1 (Ttoseq init).

Lemma Ttoseq_slideN_aux (m : nat) (T : Type) (t : T ^ m) (c : T) :
  Ttoseq (slideN_aux c t) = rcons (Ttoseq t) c.

Lemma Ttoseq_slideN (m : nat) (T : Type) (t : T ^ m) (c : T) :
  Ttoseq (slideN t c) = behead (rcons (Ttoseq t) c).

Lemma loopNS_ex (T : Type) (m : nat)
  (F : T ^^ m --> (nat -> T)) (F1 := nuncurry F)
  (n p : nat) (t : T ^ m) (s : seq T) :
  exists c, nuncurry (loopN F n.+1 p) t s = c :: (nuncurry (loopN F n p) t s).

Lemma behead_rcons (T : Type) (s : seq T) (x : T) :
  s <> [::] -> behead (rcons s x) = rcons (behead s) x.

Lemma behead_rev_take (T : Type) (s : seq T) (n : nat) :
  n <= size s -> behead (rev (take n s)) = rev (take n.-1 s).


Lemma behead_recNdown (T : Type) (m : nat)
  (init : T ^ m) (F : T ^^ m --> (nat -> T)) (F1 := nuncurry F) (n : nat) :
  behead (recNdown init F n.+1) = recNdown init F n.

Lemma nth_recNdown (T : Type) (m : nat)
  (init : T ^ m) (F : T ^^ m --> (nat -> T))
  (d1 : T) (p q n : nat) :
  nth d1 (recNdown init F (p+q+n)) (p+q) = nth d1 (recNdown init F (p+n)) p.

Lemma nth_recNdown_dflt2 (T : Type) (m : nat)
  (init : T ^ m) (F : T ^^ m --> (nat -> T))
  (d1 d2 : T) (p q n : nat) :
  nth d1 (recNdown init F (p+q+n)) (p+q) = nth d2 (recNdown init F (p+n)) p.

Section ProofN.

Variables (T : Type) (N : nat)
  (init : T ^ N) (F : T ^^ N --> (nat -> T)).

Theorem nth_recNdown_indep (d1 d2 : T) (m1 m2 n : nat) :
  n <= m1 -> n <= m2 ->
  nth d1 (recNdown init F m1) (m1 - n) = nth d2 (recNdown init F m2) (m2 - n).

Theorem nth_recNup_indep (d1 d2 : T) (m1 m2 n : nat) :
  n <= m1 -> n <= m2 ->
  nth d1 (recNup init F m1) n = nth d2 (recNup init F m2) n.

Lemma slideN_lastN (d : T) (t : T ^ N) (c : T) :
  slideN t c = lastN d N (rev (c :: rev (Ttoseq t))).

Lemma head_loopN (d : T) (n p : nat) (s : seq T) :
  init = lastN d N (rev s) ->
  size s >= N ->
  head d (nuncurry (loopN F n.+1 p) init s) =
  nuncurry F
    (lastN d N
      (rev (nuncurry (loopN F n p) init s)))
    (p+n).

End ProofN.

Section ProofN'.

Theorem recNdown_correct T (N : nat) (init : T ^ N) (F : T ^^ N --> (nat -> T))
  (d : T) (n : nat) :
  N <= n ->
  head d (recNdown init F n) =
  nuncurry F (lastN d N (rev (recNdown init F n.-1))) n.

Theorem recNup_correct T (N : nat) (init : T ^ N) (F : T ^^ N --> (nat -> T))
  (d : T) (n : nat) :
  N <= n ->
  last d (recNup init F n) =
  nuncurry F (lastN d N (recNup init F n.-1)) n.

End ProofN'.


A tactic to partially evaluate recNdown/recNup. See below for an example.

Ltac exactN f := let g :=
  eval lazy zeta beta iota
            delta[nuncurry ncurry Ttoseq nprod_to_list napply_discard
                  slideN slideN_aux cons_Tuple snd' rev' catrev'
                  loopN recNdown recNup Tofseq nprod_of_list f]
  in f in let h :=
  eval lazy beta delta[hide_let] in g
  in exact h.

Section TestN.

Let F (a b : Z) (_ : nat) := (a + b)%Z.
Let Fib2 n := rec2up F 0%Z 1%Z n.

Let FibN := recNup 2 [Tuple 0%Z; 1%Z] F.
Let FibNc := ncurry (recNup 2) 0%Z 1%Z F.
Let FibNs := recNup 2 [Tuple of [:: 0%Z; 1%Z]] F.

Let FibN' : nat -> seq Z.
Let FibNc' : nat -> seq Z.
Let FibNs' : nat -> seq Z.

End TestN.