Require Import Omega.
Require Import Nat.
Require Import ZArith.
Require Import Ring.
Require Import List.
Require Import Ncring.
Require Import Ring_tac.
Require Import FunctionalExtensionality.
From mathcomp Require ssreflect ssrbool ssrfun bigop.
Import ssreflect.SsrSyntax.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.



(** We will follow the development from this paper:
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.43.8188&rep=rep1&type=pdf*)

Open Scope list_scope.
Import ListNotations.

Module LISTTHEOREMS.
  Open Scope nat_scope.

  Lemma seq_peel_begin: forall (n l: nat) (LPOS: l > 0),
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      n :: seq (S n) (l - 1) = seq n l.
  Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
    intros.
(* Goal: forall (n : nat) (_ : gt l O), @eq (list nat) (seq n l) (@app nat (seq n (sub l (S O))) (@cons nat (sub (add n l) (S O)) (@nil nat))) *)
    induction l.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    - inversion LPOS.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    - simpl.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      replace (l - 0) with l.
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r1 bop (@const R nat r2)) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
      reflexivity.
(* Goal: gt (S n) O *)
      omega.
  Qed.

  Lemma cons_append: forall {A: Type} (a: A) (l l': list A),
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
      (cons a l) ++ l' = cons a (l ++ l').
  Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
    intros.
(* Goal: @eq (list A) (@app A (@cons A a l) l') (@cons A a (@app A l l')) *)
    generalize dependent a.
(* Goal: forall a : A, @eq (list A) (@app A (@cons A a l) l') (@cons A a (@app A l l')) *)
    generalize dependent l.
(* Goal: forall (l : list A) (a : A), @eq (list A) (@app A (@cons A a l) l') (@cons A a (@app A l l')) *)
    induction l'.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    - auto.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
    - intros.
(* Goal: @eq (list A) (@app A (@cons A a0 l) (@cons A a l')) (@cons A a0 (@app A l (@cons A a l'))) *)
      replace ((a0 :: a :: l) ++ l') with (a0 :: ((a:: l) ++ l')).
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r1 bop (@const R nat r2)) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
      reflexivity.
(* Goal: @eq (list A) (@cons A a0 (@app A (@cons A a l) l')) (@app A (@cons A a0 (@cons A a l)) l') *)
      apply IHl' with (a := a0) (l := (a::l)).
  Qed.
  
  Lemma seq_peel_end: forall (n l: nat) (L_GT_0: l > 0),
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      seq n l = (seq n (l - 1)) ++ [ n + l - 1].
  Proof.
(* Goal: forall (n l : nat) (_ : gt l O), @eq (list nat) (seq n l) (@app nat (seq n (sub l (S O))) (@cons nat (sub (add n l) (S O)) (@nil nat))) *)
    intros until l.
(* Goal: forall _ : gt l O, @eq (list nat) (seq n l) (@app nat (seq n (sub l (S O))) (@cons nat (sub (add n l) (S O)) (@nil nat))) *)
    generalize dependent n.
(* Goal: forall (n : nat) (_ : gt l O), @eq (list nat) (seq n l) (@app nat (seq n (sub l (S O))) (@cons nat (sub (add n l) (S O)) (@nil nat))) *)
    induction l.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
    - intros. omega.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
    - intros.
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
      assert (LCASES: l = 0 \/ l > 0).
(* Goal: gt (S n) O *)
      omega.

(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
      destruct LCASES as [LEQ0 | LGT0].
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
      + subst.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
        simpl.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        replace (n + 1 - 1) with n; auto; omega.

(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      +  simpl.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
         replace (l - 0) with l.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
         assert (SEQ_S_N: seq (S n) l = seq (S n) (l - 1) ++ [S n + l - 1]).
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
         apply IHl; auto.

(* Goal: @eq (list nat) (@cons nat n (seq (S n) l)) (@app nat (seq n l) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
(* Goal: @eq nat l (sub l O) *)
         rewrite SEQ_S_N.

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
         assert (n :: seq (S n) (l - 1) = seq n l).
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
         apply seq_peel_begin; auto.

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
         replace ( n :: seq (S n) (l - 1) ++ [S n + l - 1]) with
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
             ((n :: seq (S n) (l - 1)) ++ [S n + l - 1]).
(* Goal: @eq (list nat) (@app nat (@cons nat n (seq (S n) (sub l (S O)))) (@cons nat (sub (add (S n) l) (S O)) (@nil nat))) (@app nat (seq n l) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
(* Goal: @eq (list nat) (@app nat (@cons nat n (seq (S n) (sub l (S O)))) (@cons nat (sub (add (S n) l) (S O)) (@nil nat))) (@cons nat n (@app nat (seq (S n) (sub l (S O))) (@cons nat (sub (add (S n) l) (S O)) (@nil nat)))) *)
(* Goal: @eq nat l (sub l O) *)
         rewrite H.
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
         replace (S n + l) with (n + S l).
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r1 bop (@const R nat r2)) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
         reflexivity.
(* Goal: gt (S n) O *)
         omega.
(* Goal: @eq (list nat) (@app nat (@cons nat n (seq (S n) (sub l (S O)))) (@cons nat (sub (add (S n) l) (S O)) (@nil nat))) (@cons nat n (@app nat (seq (S n) (sub l (S O))) (@cons nat (sub (add (S n) l) (S O)) (@nil nat)))) *)
(* Goal: @eq nat l (sub l O) *)
         apply cons_append.
(* Goal: gt (S n) O *)
         omega.
  Qed.
  Close Scope nat_scope.
End LISTTHEOREMS.

(** HintDB of hints for SCEV **)
Global Create HintDb Recurrence.


(** You can build the theory of SCEV over any ring, actually *)
Module Type RECURRENCE.

  Import LISTTHEOREMS.
  Parameter R: Type.
  Parameter (zero one : R).
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
  Parameter (plus mult minus : R -> R-> R).
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
  Parameter (sym : R -> R).

  Parameter rt : ring_theory zero one plus mult minus sym (@eq R).
  Add Ring Rring : rt.

  Notation "0" := zero.  Notation "1" := one.
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
  Notation "x + y" := (plus x y).
  Notation "x * y " := (mult x y).

  (** A class for objects that vary over loop iterations *)
  Class LoopVariant (A R : Type) :=
    {
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      evalAtIx: A -> nat -> R
    }.
  Infix "#" := evalAtIx (at level 10).

  Global Instance loopVariantFn (R: Type):
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    LoopVariant (nat -> R) (R : Type) :=
    {
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      evalAtIx (f: nat -> R) (n: nat) := f n
    }.

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
  Definition scaleLoopVariantFn  (r: R) (f: nat -> R): nat -> R :=
    fun n => r * (f n).


  

  (* Const function *)
  Definition const {A B: Type} (x: A) (y: B) := x.
  
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
  Definition RBinop := R -> R -> R.
  
  Section BR.

    Inductive BR :=
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    | mkBR : R -> (R -> R -> R) -> (nat -> R) -> BR.

    (** I need to define the notation outside again as wel **)
    Notation "'{{' const ',' bop ',' fn  '}}'" :=
      (mkBR const bop fn) (at level 30).


    (** Semantics of evaluating a BR. It's too convenient to be able to
    `Opaque` and `Transparent` this to give it up *)
    Definition evalBR (br: BR) (n: nat): R :=
      match br with
      | mkBR r0 binop f =>
        let
          vals : list R := map f (seq 1 n)
        in
        fold_left binop vals r0
      end.


    (** semantics of evaluating a BR *)
    Global Instance loopVariantBR : LoopVariant BR R :=
      {
        evalAtIx (br: BR) (n: nat) := evalBR br n 
      }.

    Class ToBR A : Type  :=
      {
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        toBR : A -> BR
      }.

    Global Instance liftConstantToBR : ToBR R :=
      {
        toBR (c: R) := mkBR c plus (const zero)
      }.

    Global Instance liftBRToBR: ToBR BR :=
      {
        toBR br := br
      }.


    Lemma liftConstant_eval: forall (n: nat) (r: R),
        evalAtIx (toBR r)  n = r.
    Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      intros.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      simpl.

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) *)
      induction n.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      - auto.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      - rewrite seq_peel_end.
(* Goal: @eq R (@fold_left R R plus (@map nat R (@const R nat zero) (@app nat (seq (S O) (sub (S n) (S O))) (@cons nat (sub (add (S O) (S n)) (S O)) (@nil nat)))) r) r *)
(* Goal: gt (S n) O *)
        rewrite map_app.
(* Goal: @eq R (@fold_left R R plus (@app R (@map nat R (@const R nat zero) (seq (S O) (sub (S n) (S O)))) (@map nat R (@const R nat zero) (@cons nat (sub (add (S O) (S n)) (S O)) (@nil nat)))) r) r *)
(* Goal: gt (S n) O *)
        rewrite fold_left_app.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        replace (S n - 1)%nat with n; try omega.
(* Goal: @eq R (mult (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
        rewrite IHn.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
        simpl.
(* Goal: @eq R (plus r (@const R nat zero (S n))) r *)
(* Goal: gt (S n) O *)
        unfold const; auto; ring.
(* Goal: gt (S n) O *)
        omega.
    Qed.

    Hint Resolve liftConstant_eval : Recurrence.
    Hint Rewrite liftConstant_eval : Recurrence.

    (** Most basic theorem, show how to unfold BR execution *)
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    Lemma evalBR_step: forall `{Ring R} (r0: R) (bop: R -> R -> R) (f: nat -> R) (n : nat),
        ({{r0, bop, f}}) # (S n) = bop ((mkBR r0 bop f) # n)  (f # (S n)).
    Proof.
      Open Scope nat_scope.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (c : R) (f1 f2 : forall _ : nat, R) (bop : forall (_ : R) (_ : R), R) (_ : forall n0 : nat, @eq R (f1 n0) (f2 n0)), @eq R (@evalAtIx BR R loopVariantBR (mkBR c bop f1) n) (@evalAtIx BR R loopVariantBR (mkBR c bop f2) n) *)
      intros until n.
      generalize dependent r0.
      generalize dependent bop.
      generalize dependent f.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      simpl.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) *)
      induction n.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      - auto.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      - intros.

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        assert (STRIP_LAST: seq 2 (S n) = seq 2 (S n - 1) ++ [2 + (S n) - 1]).
(* Goal: gt (S n) O *)
        apply seq_peel_end; omega.

        rewrite STRIP_LAST.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
        simpl.

(* Goal: @eq R (@fold_left R R plus (@map nat R (@const R nat zero) (@app nat (seq (S O) (sub (S n) (S O))) (@cons nat (sub (add (S O) (S n)) (S O)) (@nil nat)))) r) r *)
(* Goal: gt (S n) O *)
        rewrite map_app.
(* Goal: @eq R (@fold_left R R plus (@app R (@map nat R (@const R nat zero) (seq (S O) (sub (S n) (S O)))) (@map nat R (@const R nat zero) (@cons nat (sub (add (S O) (S n)) (S O)) (@nil nat)))) r) r *)
(* Goal: gt (S n) O *)
        rewrite fold_left_app.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
        simpl.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        replace (n - 0) with n.
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r1 bop (@const R nat r2)) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
        reflexivity.
(* Goal: gt (S n) O *)
        omega.
        Close Scope nat_scope.
    Qed.

    
    Hint Resolve evalBR_step : Recurrence.
    Hint Rewrite @evalBR_step : Recurrence.

    (** Functional extentionality style theorems about the
    evaluation of a BR *)
    Section BR_FUNEXT.
      Lemma evalBR_funext_delta:
        forall `{Ring R} (n: nat)
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
          (c: R) (f1 f2: nat -> R)
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
          (bop: R -> R -> R)
          (FUNEXT: forall (n: nat), f1 n = f2 n),
          {{c, bop, f1}} # n = {{c, bop, f2 }} # n.
      Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (c : R) (f1 f2 : forall _ : nat, R) (bop : forall (_ : R) (_ : R), R) (_ : forall n0 : nat, @eq R (f1 n0) (f2 n0)), @eq R (@evalAtIx BR R loopVariantBR (mkBR c bop f1) n) (@evalAtIx BR R loopVariantBR (mkBR c bop f2) n) *)
        intros until n.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) *)
        induction n.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        - (* n = 0 *)
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
          intros; simpl; auto.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        - (* n = S n *)
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          intros.
(* Goal: @eq R (mult (@evalAtIx BR R loopVariantBR (mkBR r1 mult f1) (S n)) (@evalAtIx BR R loopVariantBR (mkBR r2 mult f2) (S n))) (@evalAtIx BR R loopVariantBR (mkBR (mult r1 r2) mult (fun n : nat => mult (f1 n) (f2 n))) (S n)) *)
          repeat rewrite evalBR_step.
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
          erewrite IHn with (f2 := f2); auto.
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
          replace (f1 # (S n)) with (f2 # (S n)); auto.
      Qed.
    End BR_FUNEXT.


    Section BR_CONSTANTS.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      Variable f : nat -> R.
      Variable r0 c: R.

      Definition br := {{ r0, plus, f}}.

      (* Lemma 6 from paper *)
      Lemma add_constant_add_br: forall `{Ring R}  (n: nat),
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
          ((toBR c) # n) +
          {{r0, plus, f}} # n = 
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
          {{(r0 + c), plus, f}} # n.
      Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
        intros.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) *)
        induction n.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        - simpl. ring.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        - rewrite evalBR_step.
(* Goal: @eq R (plus (@evalAtIx BR R loopVariantBR (@toBR R liftConstantToBR c) (S n)) (plus (@evalAtIx BR R loopVariantBR (mkBR r0 plus f) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) f (S n)))) (@evalAtIx BR R loopVariantBR (mkBR (plus r0 c) plus f) (S n)) *)
          ring_simplify in IHn.
(* Goal: @eq R (mult r (mult (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)))) (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) *)
          ring_simplify.

          replace (toBR c # (S n)) with
              (toBR c # n).
(* Goal: @eq R (mult (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
          rewrite IHn.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
          rewrite <- evalBR_step.
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r1 bop (@const R nat r2)) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
          reflexivity.

(* Goal: @eq R (@evalAtIx BR R loopVariantBR (@toBR R liftConstantToBR c) n) (@evalAtIx BR R loopVariantBR (@toBR R liftConstantToBR c) (S n)) *)
          repeat (rewrite liftConstant_eval).
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
          auto.
      Qed.

      Hint Resolve add_constant_add_br : Recurrence.
      Hint Rewrite @add_constant_add_br : Recurrence.

      (* Lemma 7 *)
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      (* Here is where I need a module :( nat -> R forms a module over R *)
      Lemma mul_constant_add_br: forall `{Ring R} (n: nat),
          ((toBR c) # n) * ((mkBR r0 plus f) # n) =
          (mkBR (c * r0) plus (scaleLoopVariantFn c f)) # n.
      Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
        intros.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) *)
        induction n.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        - simpl. ring.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        - rewrite evalBR_step.

          replace (toBR c # (S n)) with
              (toBR c # n).
(* Goal: @eq R (mult r (mult (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)))) (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) *)
          ring_simplify.
(* Goal: @eq R (mult (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
          rewrite IHn.
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r bop (@evalAtIx BR R loopVariantBR (CR_to_BR cr'))) (S n)) (bop (@evalAtIx BR R loopVariantBR (mkBR r bop (@evalAtIx BR R loopVariantBR (CR_to_BR cr'))) n) (evalBR (CR_to_BR cr') (S n))) *)
          rewrite evalBR_step.
          
          replace ((toBR c # n) * (f # (S n))) with
              ((scaleLoopVariantFn c f) # (S n)).
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r1 bop (@const R nat r2)) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
          reflexivity.

(* Goal: @eq R (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (scaleLoopVariantFn c f) (S n)) (mult (@evalAtIx BR R loopVariantBR (@toBR R liftConstantToBR c) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) f (S n))) *)
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (@toBR R liftConstantToBR c) n) (@evalAtIx BR R loopVariantBR (@toBR R liftConstantToBR c) (S n)) *)
          rewrite liftConstant_eval.
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
          auto.

(* Goal: @eq R (@evalAtIx BR R loopVariantBR (@toBR R liftConstantToBR c) n) (@evalAtIx BR R loopVariantBR (@toBR R liftConstantToBR c) (S n)) *)
          repeat (rewrite liftConstant_eval).
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r1 bop (@const R nat r2)) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
          reflexivity.
      Qed.

      
      Hint Resolve mul_constant_add_br : Recurrence.
      Hint Rewrite @mul_constant_add_br : Recurrence.
      (*
    (* Lemma 8 *)
    Lemma pow_constant_add_br: forall `{Ring R} (n: nat),
        pow_N c ((mkBR r0 plus f) # n) =
        (mkBR (pow_N c r0) mult (fun n => pow_N c (f # n))) # n.
       *)

      Lemma mul_constant_mul_br: forall `{Ring R} (n:  nat),
          c * ({{r0, mult, f}} # n) =
          {{r0 * c, mult, f}} # n.
      Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
        intros.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) *)
        induction n.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        - simpl. ring.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        - rewrite evalBR_step.
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r bop (@evalAtIx BR R loopVariantBR (CR_to_BR cr'))) (S n)) (bop (@evalAtIx BR R loopVariantBR (mkBR r bop (@evalAtIx BR R loopVariantBR (CR_to_BR cr'))) n) (evalBR (CR_to_BR cr') (S n))) *)
          rewrite evalBR_step.
(* Goal: @eq R (mult r (mult (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)))) (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) *)
          ring_simplify.
(* Goal: @eq R (mult (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
          rewrite IHn.
(* Goal: @eq R (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
          ring.
      Qed.

      
      Hint Resolve mul_constant_mul_br : Recurrence.
      Hint Rewrite @mul_constant_mul_br : Recurrence.
    End BR_CONSTANTS.

    Section BR_BR.
      (* Lemma 12 *)
      Definition add_add_br_add_br: forall `{Ring R} (n: nat)
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      (c1 c2: R) (f1 f2: nat -> R),
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
        ({{c1, plus, f1 }} # n) + ({{c2, plus, f2}} # n) =
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
        ({{ (c1 + c2), plus, (fun n => f1 n + f2 n) }}) # n.
      Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
        intros.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) *)
        induction n.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        - simpl. ring.
(* Goal: @eq R (mult (@evalAtIx BR R loopVariantBR (mkBR r1 mult f1) (S n)) (@evalAtIx BR R loopVariantBR (mkBR r2 mult f2) (S n))) (@evalAtIx BR R loopVariantBR (mkBR (mult r1 r2) mult (fun n : nat => mult (f1 n) (f2 n))) (S n)) *)
          repeat rewrite evalBR_step.
(* Goal: @eq R (mult r (mult (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)))) (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) *)
          ring_simplify.
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
          replace ((mkBR c1 plus f1 # n) +
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
                   (f1 # (S n)) +
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
                   (mkBR c2 plus f2 # n) +
                   (f2 # (S n))) with
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
              ((mkBR c1 plus f1 # n) +
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
               (mkBR c2 plus f2 # n) +
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
               (f1 # (S n)) +
(* Goal: @eq R (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
               (f2 # (S n))); try ring.
(* Goal: @eq R (mult (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
          rewrite IHn.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          simpl.
(* Goal: @eq R (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
          ring.
      Qed.

      
      Definition mulCRFn `{Ring R} (c1 c2: R)
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
                 (f1 f2: nat -> R)
                 (n: nat): R:=
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        (((f2 # n) * {{c1, plus, f1}} # (n - 1))  +
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
         ((f1 # n) * {{c2, plus, f2}} # (n - 1))  +
         (f1 # n) * (f2 # n)).

      (* Lemma 13 *)
      (* Definition in paper is WRONG. They index both br1, br2 and the
    functions with the _same index_. It should be one minus *)
      Lemma mul_add_br_add_br:
        forall `{Ring R}
          (c1 c2: R)
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
          (f1 f2: nat -> R)
          (n: nat),
          ({{c1, plus, f1}} # n) * ({{c2, plus, f2}} # n) =
          ((mkBR (c1 * c2) plus (mulCRFn c1 c2 f1 f2)) # n).
      Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
        intros.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) *)
        induction n.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        - simpl. ring.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        - (** induction **)
(* Goal: @eq R (mult (@evalAtIx BR R loopVariantBR (mkBR r1 mult f1) (S n)) (@evalAtIx BR R loopVariantBR (mkBR r2 mult f2) (S n))) (@evalAtIx BR R loopVariantBR (mkBR (mult r1 r2) mult (fun n : nat => mult (f1 n) (f2 n))) (S n)) *)
          repeat rewrite evalBR_step.
(* Goal: @eq R (mult r (mult (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)))) (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) *)
          ring_simplify.

          (** This is because I need to be able to simplify the #
          evaluation of functions *)
          Opaque loopVariantBR.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          simpl.

          replace
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
            ({{c1, plus, f1}} # n * {{c2, plus, f2}} # n +
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
             {{c1, plus, f1}} # n * f2 (S n) +
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
             f1 (S n) * {{c2, plus, f2}} # n +
             f1 (S n) * f2 (S n)) with
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
              ({{c1, plus, f1}} # n * {{c2, plus, f2}} # n +
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
               ({{c1, plus, f1}} # n * f2 (S n) +
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
                {{c2, plus, f2}} # n * f1 (S n) +
(* Goal: @eq R (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
                f1 (S n) * f2 (S n))); try ring.

(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
          replace ({{c1, plus, f1}} # n * f2 (S n) +
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
                   {{c2, plus, f2}} # n * f1 (S n) +
                   f1 (S n) * f2 (S n)) with
              (mulCRFn c1 c2 f1 f2 (S n));
            try (unfold mulCRFn; simpl;
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
                 replace (n - 0)%nat with n; try omega; auto; ring; fail).

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
          rewrite <- IHn.
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r1 bop (@const R nat r2)) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
          reflexivity.
          Transparent loopVariantBR.
      Qed.

      Hint Resolve mul_add_br_add_br : Recurrence.
      Hint Rewrite @mul_add_br_add_br : Recurrence.

      
      (* Lemma 14 *)
      Lemma mul_mul_br_mul_br: forall `{Ring R} (n: nat)
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        (r1 r2: R) (f1 f2: nat -> R),
          ({{r1, mult, f1}} # n) * ({{r2, mult, f2}} # n) =
          ((mkBR (r1 * r2) mult (fun n => (f1 n * f2 n))) # n).
      Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
        intros.

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) *)
        induction n.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        - simpl. ring.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        - repeat rewrite evalBR_step.
          
(* Goal: @eq R (mult r (mult (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)))) (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) *)
          ring_simplify.
          replace ((mkBR r1 mult f1 # n) * (f1 # (S n)) *
                   (mkBR r2 mult f2 # n) * (f2 # (S n))) with
              ((mkBR r1 mult f1 # n) * (mkBR r2 mult f2 # n) *
(* Goal: @eq R (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
               (f1 # (S n)) * (f2 # (S n))); try ring.
(* Goal: @eq R (mult (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
          rewrite IHn.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          simpl.
(* Goal: @eq R (mult r (mult (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)))) (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) *)
          ring_simplify.
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r1 bop (@const R nat r2)) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
          reflexivity.
      Qed.

      
      Hint Resolve mul_mul_br_mul_br : Recurrence.
      Hint Rewrite @mul_mul_br_mul_br : Recurrence.

      End BR_BR.

      
      Hint Resolve add_add_br_add_br: Recurrence.
      Hint Rewrite @add_add_br_add_br: Recurrence.

      
    Opaque evalBR.
  End BR.

  (** I need to define the notation outside again as wel **)
  Notation "'{{' const ',' bop ',' fn  '}}'" :=
    (mkBR const bop fn) (at level 30): recurrence_scope.

  (** Define a chain of recurrences *)
  Section CR.
    Open Scope recurrence_scope.
    
    Inductive CR :=
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    | liftBRToCR: BR -> CR
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    | recurCR: R -> (R -> R -> R) -> CR -> CR
    .
    

    

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    (** Interpret a CR as nested BRs as described in section 2 -
       Chains of Recurrences *)
    Fixpoint CR_to_BR (cr: CR): BR :=
      match cr with
      | liftBRToCR br =>  br
      | recurCR r0 bop cr' => mkBR r0 bop (evalAtIx (CR_to_BR cr'))
      end.


    Definition evalCR(cr: CR) (n: nat): R := (CR_to_BR cr) # n.

    Lemma evalBR_CR_to_BR: forall (cr: CR) (n: nat),
        evalBR (CR_to_BR cr) n = evalCR cr n.
    Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      intros.
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r1 bop (@const R nat r2)) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
      reflexivity.
    Qed.
      

    (** Define what it means to evaluate a CR *)
    Global Instance loopVariantCR : LoopVariant CR R :=
      {
        evalAtIx (cr: CR) (n: nat) := evalCR cr n
      }.

    Lemma creval_lift_br_to_cr_inverses: forall (br: BR) (n: nat),
       (liftBRToCR br) # n = br # n.
    Proof.
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
      intros; auto.
    Qed.

    Hint Resolve creval_lift_br_to_cr_inverses: Recurrence.

    (** Show what happens at n = 0 *)
    Lemma evalCR_zero: forall
        `{Ring R}
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        (cr': CR) (r: R) (bop: R -> R -> R),
        (recurCR r bop cr') # 0 = r.
    Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      intros.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      simpl.
(* Goal: @eq R (evalCR (recurCR r bop cr') (S n)) (bop (evalCR (recurCR r bop cr') n) (evalBR (CR_to_BR cr') (S n))) *)
      unfold evalCR.
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
      auto.
    Qed.
    Hint Rewrite @evalCR_zero: Recurrence.

    
    (** Basic theorem, show how to unfold CReval *)
    Lemma evalCR_step: forall
        `{Ring R}
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        (cr': CR) (r: R) (bop: R -> R -> R) (n: nat),
        (recurCR r bop cr') # (S n) =
          bop ((recurCR r bop cr') # n)
              ((evalAtIx (CR_to_BR cr')) # (S n)).
    Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      intros.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      simpl.
(* Goal: @eq R (evalCR (recurCR r bop cr') (S n)) (bop (evalCR (recurCR r bop cr') n) (evalBR (CR_to_BR cr') (S n))) *)
      unfold evalCR.

(* Goal: @eq R (@evalAtIx BR R loopVariantBR (CR_to_BR (recurCR r bop cr')) (S n)) (bop (@evalAtIx BR R loopVariantBR (CR_to_BR (recurCR r bop cr')) n) (evalBR (CR_to_BR cr') (S n))) *)
      unfold CR_to_BR.
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r bop (@evalAtIx BR R loopVariantBR ((fix CR_to_BR (cr : CR) : BR := match cr with | liftBRToCR br => br | recurCR r0 bop cr' => mkBR r0 bop (@evalAtIx BR R loopVariantBR (CR_to_BR cr')) end) cr'))) (S n)) (bop (@evalAtIx BR R loopVariantBR (mkBR r bop (@evalAtIx BR R loopVariantBR ((fix CR_to_BR (cr : CR) : BR := match cr with | liftBRToCR br => br | recurCR r0 bop cr' => mkBR r0 bop (@evalAtIx BR R loopVariantBR (CR_to_BR cr')) end) cr'))) n) (evalBR ((fix CR_to_BR (cr : CR) : BR := match cr with | liftBRToCR br => br | recurCR r0 bop cr' => mkBR r0 bop (@evalAtIx BR R loopVariantBR (CR_to_BR cr')) end) cr') (S n))) *)
      fold CR_to_BR.

(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r bop (@evalAtIx BR R loopVariantBR (CR_to_BR cr'))) (S n)) (bop (@evalAtIx BR R loopVariantBR (mkBR r bop (@evalAtIx BR R loopVariantBR (CR_to_BR cr'))) n) (evalBR (CR_to_BR cr') (S n))) *)
      rewrite evalBR_step.
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
      auto.
    Qed.


    Hint Rewrite @evalCR_step: Recurrence.

    (** Now that we know what happens at 0 and inductive case, we're done *)
    Opaque evalCR.


    (** Lemma 16 *)
    Lemma add_const_to_CR:
      forall `{Ring R} (r c0: R) (cr: CR) (n: nat),
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
        r + ((recurCR c0 plus cr) # n) =
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
        ((recurCR (c0 + r) plus cr) # n).
    Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      intros.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      simpl.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) *)
      induction n.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      - repeat rewrite evalCR_zero. ring.
        
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      - repeat rewrite evalCR_step.
(* Goal: @eq R (mult r (mult (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)))) (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) *)
        ring_simplify.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
        simpl.
(* Goal: @eq R (mult (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
        rewrite IHn.
(* Goal: @eq R (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
        ring.
    Qed.

    Hint Resolve add_const_to_CR : Recurrence.
    Hint Rewrite @add_const_to_CR : Recurrence.

    

    (** Lemma 17 *)
    Lemma mul_const_to_CR:
      forall `{Ring R} (r c0: R) (cr: CR) (n: nat),
        r * ((recurCR c0 mult cr) # n) =
        ((recurCR (c0 * r) mult cr) # n).
    Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      intros.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) *)
      induction n.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      - (** n = 0 *)
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
        repeat rewrite evalCR_zero; auto. ring.
        
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      - (** n = S n *)
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        repeat rewrite evalCR_step.
(* Goal: @eq R (mult r (mult (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)))) (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) *)
        ring_simplify.
(* Goal: @eq R (mult (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
        rewrite IHn.
(* Goal: @eq R (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
        ring.
    Qed.
      
    (** Theory of pure CRs (CRs that have only one binary operator *)
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    Inductive PureCR (bop: R -> R -> R): Type :=
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    | PureBR: R -> R -> PureCR bop
    |  PureCRRec:
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
         R -> 
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        PureCR bop ->
        PureCR bop
    .
    

    (** Convert a `PureCR` into a CR by inserting the correct
        `bop` everywhere *)
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    Fixpoint purecr_to_cr (bop: R -> R -> R) (pure: PureCR bop): CR :=
      match pure with
      | PureBR r1 r2 => liftBRToCR (mkBR r1 bop (const r2))
      | PureCRRec r cr' => (recurCR r bop (purecr_to_cr cr'))
      end.

    (** Give a way to simplify the evaluation of a PureBR *)
    Lemma purecr_to_cr_eval_cr_inverses:
      forall `{Ring R}
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
        (bop: R -> R -> R)
        (r1 r2: R)
        (n: nat),
        purecr_to_cr (PureBR bop r1 r2) # n =  {{r1, bop, (const r2)}} # n.
    Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      intros.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
      simpl.
(* Goal: @eq R (evalCR (liftBRToCR (mkBR r1 bop (@const R nat r2))) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
      rewrite creval_lift_br_to_cr_inverses.
(* Goal: @eq R (@evalAtIx BR R loopVariantBR (mkBR r1 bop (@const R nat r2)) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
      reflexivity.
    Qed.
        

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    Global Instance loopVariantPureCR (f: R -> R -> R):
      LoopVariant (PureCR f) (R : Type) :=
    {
      evalAtIx (purecr: PureCR f) (n: nat) := (purecr_to_cr purecr) # n
    }.

  (** Evaluation of pureCR at 0 *)
  Lemma evalPureCR_zero:
    forall `{Ring R}
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      (bop: R -> R -> R)
      (r: R)
      (pcr': PureCR bop),
      (PureCRRec r pcr') # 0 = r.
  Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
    intros.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
    simpl.
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
    erewrite evalCR_zero; eauto.
  Qed.


  
  (** Step the evaluation of a pure CR *)
  Lemma evalPureCR_step:
    forall `{Ring R}
      (n: nat)
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      (bop: R -> R -> R)
      (r: R)
      (pcr': PureCR bop),
      (PureCRRec r pcr') # (S n) =
      bop ((PureCRRec r pcr') # n) (pcr' # (S n)).
  Proof.
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
    intros.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
    simpl.
(* Goal: @eq R (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) (S n)) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
    rewrite evalCR_step.
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
    auto.
  Qed.

    (** Zip the two pureCRs together, to construct a longer PureCR.
     NOTE: This assumes that cr1 and cr2 have the same length
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
     NOTE: If they do not, we can always ammend a CR with {0, +, 0}
    **)
  Fixpoint zip_purecrs_eq_len
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
           {bop: R -> R -> R}
           (cr1 cr2: PureCR bop):
      option (PureCR bop) :=
      match (cr1, cr2) with
      (** recurrence *)
      | (PureCRRec r1 cr'1, PureCRRec r2 cr'2) =>
        option_map (PureCRRec (bop r1 r2)) (zip_purecrs_eq_len cr'1 cr'2)
      (** Base case when cr1 and cr2 have the same length *)
      | (PureBR r11 r12, PureBR r21 r22) =>
           Some (PureBR bop (bop r11 r21) (bop r12 r22))
      | _ => None
      end.


(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
    (* Define pure-sum and pure-product CRs *)
    Notation PureSumCR := (PureCR plus).
    Notation PureProdCR := (PureCR mult).

    (** Lemma 22 *)
    Lemma rewrite_pure_sum_cr_on_add_cr: forall
        `{Ring R}
        (cr1 cr2: PureSumCR)
        (pureout: PureSumCR)
        (ZIP: zip_purecrs_eq_len cr1 cr2 = Some pureout)
        (n: nat),
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
        cr1 # n + cr2 # n = pureout # n.
    Proof.
      intros until cr1.

      (** induction on cr1 *)
      induction cr1 as [begin1 delta1 | begin1' cr1].
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      - (** cr1 = purebr **)
        intros until cr2.
        induction cr2 as [begin2 delta2 | begin2' cr2].

(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
        + (** cr2 = purebr *)
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          intros.
          simpl in ZIP.
          inversion ZIP.
          Opaque evalBR.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          simpl.
(* Goal: @eq R (evalCR (liftBRToCR (mkBR r1 bop (@const R nat r2))) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
          repeat rewrite creval_lift_br_to_cr_inverses.
          rewrite add_add_br_add_br.
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
          apply evalBR_funext_delta; auto.

(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
        + (**cr2 = cr *)
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          intros.
          simpl in ZIP.
          inversion ZIP.

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      - (** cr1 = PureCRRec begin1' cr1 *)
        intros cr2.
        induction cr2 as [begin2 delta2 | begin2' cr2].

(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
        + (** cr2 = PureBR *)
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          intros.
          simpl in ZIP.
          inversion ZIP.

(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
        + (** cr2 = PureCR *)
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          intros.
          simpl in ZIP.
          destruct (zip_purecrs_eq_len cr1 cr2) eqn:ZIP_CR1_CR2;
            simpl in ZIP;
            inversion ZIP.

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) *)
          induction n.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          * (* n = 0 *)simpl. auto.
          (** TODO: why do I need to make this
                       explicit *)
          * rewrite evalPureCR_step with
                (r := begin1')
                (pcr' := cr1).
           rewrite evalPureCR_step with
                (r := begin2')
                (pcr' := cr2).

           rewrite evalPureCR_step with
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
                (r := (begin1' + begin2'))
                (pcr' := p).
(* Goal: @eq R (mult r (mult (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)))) (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) *)
           ring_simplify.

(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
           replace ((PureCRRec begin1' cr1) # n +
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
                    cr1 # (S n) +
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
                    (PureCRRec begin2' cr2) # n +
                    cr2 # (S n)) with
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
               (((PureCRRec begin1' cr1) # n +
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
                 (PureCRRec begin2' cr2) # n) +
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
                (cr1 # (S n) + cr2 # (S n))); try ring.
(* Goal: @eq R (mult (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) (mult (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n)) *)
           rewrite IHn.

           assert (CR1_PLUS_CR2:
(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
                     cr1 # (S n) + cr2 # (S n) = p # (S n)).
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
           erewrite IHcr1; eauto.
           congruence.
    Qed.

    
    (** Lemma 22 *)
    Lemma rewrite_pure_mul_cr_on_mul_cr: forall
        `{Ring R}
        (cr1 cr2: PureProdCR)
        (pureout: PureProdCR)
        (ZIP: zip_purecrs_eq_len cr1 cr2 = Some pureout)
        (n: nat),
        (cr1 # n) * (cr2 # n) = pureout # n.
    Proof.
      intros until cr1.

      (** induction on cr1 *)
      induction cr1 as [begin1 delta1 | begin1' cr1].
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      - (** cr1 = purebr **)
        intros until cr2.
        induction cr2 as [begin2 delta2 | begin2' cr2].

(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
        + (** cr2 = purebr *)
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          intros.
          simpl in ZIP.
          inversion ZIP.
          Opaque evalBR.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          simpl.
(* Goal: @eq R (evalCR (liftBRToCR (mkBR r1 bop (@const R nat r2))) n) (@fold_left R R bop (@map nat R (@const R nat r2) (seq (S O) n)) r1) *)
          repeat rewrite creval_lift_br_to_cr_inverses.
(* Goal: @eq R (mult r (mult (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)))) (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) *)
          ring_simplify.
          rewrite mul_mul_br_mul_br.
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
          apply evalBR_funext_delta; auto.

(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
        + (**cr2 = cr *)
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          intros.
          simpl in ZIP.
          inversion ZIP.

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
      - (** cr1 = PureCRRec begin1' cr1 *)
        intros cr2.
        induction cr2 as [begin2 delta2 | begin2' cr2].

(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
        + (** cr2 = PureBR *)
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          intros.
          simpl in ZIP.
          inversion ZIP.

(* Goal: @eq (list nat) (seq n (S l)) (@app nat (seq n (sub (S l) (S O))) (@cons nat (sub (add n (S l)) (S O)) (@nil nat))) *)
        + (** cr2 = PureCR *)
(* Goal: forall (ring0 ring1 : R) (add0 mul0 sub0 : forall (_ : R) (_ : R), R) (opp : forall _ : R, R) (ring_eq : forall (_ : R) (_ : R), Prop) (Ro : @Ring_ops R ring0 ring1 add0 mul0 sub0 opp ring_eq) (_ : @Ring R ring0 ring1 add0 mul0 sub0 opp ring_eq Ro) (n : nat) (bop : forall (_ : R) (_ : R), R) (r : R) (pcr' : PureCR bop), @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          intros.
          simpl in ZIP.
          destruct (zip_purecrs_eq_len cr1 cr2) eqn:ZIP_CR1_CR2;
            simpl in ZIP;
            inversion ZIP.

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n)) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) *)
          induction n.
(* Goal: @eq R (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') (S n)) (bop (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) (@PureCRRec bop r pcr') n) (@evalAtIx (PureCR bop) R (loopVariantPureCR bop) pcr' (S n))) *)
          * (* n = 0 *)simpl. auto.
          (** TODO: why do I need to make this
                       explicit *)
          * rewrite evalPureCR_step with
                (r := begin1')
                (pcr' := cr1).
           rewrite evalPureCR_step with
                (r := begin2')
                (pcr' := cr2).

           rewrite evalPureCR_step with
                (r := (begin1' * begin2'))
                (pcr' := p).
(* Goal: @eq R (mult r (mult (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)))) (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) *)
           ring_simplify.

(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
           rewrite <- IHn.


           assert (CR1_PLUS_CR2:
                     cr1 # (S n) * cr2 # (S n) = p # (S n)).
(* Goal: @eq R (bop (@evalAtIx CR R loopVariantCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR (@purecr_to_cr bop pcr'))) (S n))) (bop (evalCR (recurCR r bop (@purecr_to_cr bop pcr')) n) (evalCR (@purecr_to_cr bop pcr') (S n))) *)
           erewrite IHcr1; eauto.
(* Goal: @eq R (mult r (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) (S n))) (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) (S n)) *)
           rewrite <- CR1_PLUS_CR2.
(* Goal: @eq R (mult r (mult (@evalAtIx CR R loopVariantCR (recurCR c0 mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n)))) (mult (@evalAtIx CR R loopVariantCR (recurCR (mult c0 r) mult cr) n) (@evalAtIx (forall _ : nat, R) R (loopVariantFn R) (@evalAtIx BR R loopVariantBR (CR_to_BR cr)) (S n))) *)
           ring_simplify. 
           congruence.
    Qed.
  End CR.
End RECURRENCE.

