Library Interval.Poly.Datatypes

From Coq Require Import ZArith Reals.
From Coquelicot Require Import Coquelicot.
From mathcomp.ssreflect Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop.
From Flocq Require Import Core.

Require Import Stdlib.
Require Import MathComp.
Require Import Interval.
Require Import Xreal.
Require Import Basic_rec.

Set Implicit Arguments.

Local Open Scope nat_scope.

Reserved Notation "--> e"
  (at level 10, e at level 8, no associativity, format "--> e").
Reserved Notation "i >: x"
  (at level 70, no associativity, format "i >: x").
Reserved Notation "i >:: x"
  (at level 70, no associativity, format "i >:: x").

Module Type BaseOps.
Parameter Inline U : Type.
Parameter Inline T : Type.
Parameter Inline zero : T.
Parameter Inline one : T.
Parameter Inline opp : T → T.
Parameter Inline add : U → T → T → T.
Parameter Inline sub : U → T → T → T.
Parameter Inline mul : U → T → T → T.
End BaseOps.


Module Type PowDivOps.
Include BaseOps.

Parameter Inline mask : T → T → T.
Parameter Inline from_nat : U → nat → T.
Parameter Inline fromZ : U → Z → T.
Parameter Inline power_int : U → T → Z → T.
Parameter Inline sqr : U → T → T.
Parameter Inline inv : U → T → T.
Parameter Inline div : U → T → T → T.
End PowDivOps.

Module Type FullOps.
Include PowDivOps.
Parameter Inline sqrt : U → T → T.
Parameter Inline invsqrt : U → T → T.
Parameter Inline exp : U → T → T.
Parameter Inline sin : U → T → T.
Parameter Inline cos : U → T → T.
Parameter Inline ln : U → T → T.
Parameter Inline atan : U → T → T.
Parameter Inline tan : U → T → T.
End FullOps.

Module FullInt (I : IntervalOps) <: FullOps.
Definition U := I.precision.
Definition T := I.type.
Definition zero := I.zero.
Definition one := I.fromZ_small 1.
Definition opp := I.neg.
Definition add := I.add.
Definition sub := I.sub.
Definition mul := I.mul.
Definition div := I.div.
Definition power_int := I.power_int.
Definition exp := I.exp.
Definition ln := I.ln.
Definition from_nat := fun u n ⇒ I.fromZ u (Z_of_nat n).
Definition fromZ := I.fromZ.
Definition inv := I.inv.
Definition cos := I.cos.
Definition sin := I.sin.
Definition sqr := I.sqr.
Definition sqrt := I.sqrt.
Definition invsqrt := fun prec x ⇒ I.inv prec (I.sqrt prec x).
Definition mask : T → T → T := I.mask.
Definition tan := I.tan.
Definition atan := I.atan.
End FullInt.

Module Type PolyOps (C : PowDivOps) <: BaseOps.
Definition U := C.U.
Parameter T : Type.
Parameter zero : T.
Parameter one : T.
Parameter opp : T → T.
Parameter add : U → T → T → T.
Parameter sub : U → T → T → T.
Parameter mul : U → T → T → T.

Parameter toSeq : T → seq C.T.
Parameter nth : T → nat → C.T.
Parameter size : T → nat.
Parameter rec1 : (C.T → nat → C.T) → C.T → nat → T.
Parameter rec2 : (C.T → C.T → nat → C.T) → C.T → C.T → nat → T.
Parameter grec1 :
  ∀ A : Type,
  (A → nat → A) →
  (A → nat → C.T) → A → seq C.T → nat → T.
Parameter map : ∀ f : C.T → C.T, T → T.
Parameter fold : ∀ V : Type, (C.T → V → V) → V → T → V.
Parameter set_nth : T → nat → C.T → T.
Parameter mul_trunc : U → nat → T → T → T.
Parameter mul_tail : U → nat → T → T → T.

Parameter lift : nat → T → T.
Parameter tail : nat → T → T.
Parameter polyC : C.T → T.
Parameter polyX : T.
Parameter polyNil : T.
Parameter polyCons : C.T → T → T.
Parameter horner : U → T → C.T → C.T.
Parameter deriv : U → T → T.
Parameter mul_mixed : U → C.T → T → T.
Parameter div_mixed_r : U → T → C.T → T.
Parameter dotmuldiv : U → seq Z → seq Z → T → T.
Parameter primitive : U → C.T → T → T.

Parameter horner_seq : ∀ u p x, horner u p x =
  C.mask (foldr (fun a b ⇒ C.add u (C.mul u b x) a) C.zero (toSeq p)) x.
Parameter nth_toSeq : ∀ p n, nth p n = seq.nth (C.zero) (toSeq p) n.

Parameter polyCE : ∀ c, polyC c = polyCons c polyNil.
Parameter polyXE : polyX = lift 1 one.
Parameter oneE : one = polyC C.one.

Parameter poly_ind : ∀ (f : T → Prop),
  f polyNil →
  (∀ a p, f p → f (polyCons a p)) →
  ∀ p, f p.

Parameter size_primitive : ∀ u c p, size (primitive u c p) = (size p).+1.

Parameter size_lift : ∀ n p, size (lift n p) = n + size p.
Parameter size_mul_mixed : ∀ u a p, size (mul_mixed u a p) = size p.
Parameter size_div_mixed_r : ∀ u p b, size (div_mixed_r u p b) = size p.
Parameter size_rec1 : ∀ F x n, size (rec1 F x n) = n.+1.
Parameter size_rec2 : ∀ F x y n, size (rec2 F x y n) = n.+1.
Parameter size_mul_trunc : ∀ u n p q, size (mul_trunc u n p q) = n.+1.
Parameter size_mul_tail :
  ∀ u n p q, size (mul_tail u n p q) = ((size p) + (size q)).-1 - n.+1.
Parameter size_add :
  ∀ u p1 p2, size (add u p1 p2) = maxn (size p1) (size p2).
Parameter size_opp : ∀ p1, size (opp p1) = size p1.
Parameter size_map : ∀ f p, size (map f p) = size p.
Parameter size_sub :
  ∀ u p1 p2, size (sub u p1 p2) = maxn (size p1) (size p2).
Parameter size_polyNil : size polyNil = 0.
Parameter size_polyCons : ∀ a p, size (polyCons a p) = (size p).+1.
Parameter size_grec1 :
  ∀ (A : Type)
  (F : A → nat → A) (G : A → nat → C.T) (q : A) (s : seq C.T) (n : nat),
  size (grec1 F G q s n) = n.+1.
Parameter size_tail :
  ∀ p k, size (tail k p) = size p - k.

Parameter size_dotmuldiv :
  ∀ n u a b p, size p = n → seq.size a = n → seq.size b = n →
  size (dotmuldiv u a b p) = n.
Parameter size_set_nth : ∀ p n val,
  size (set_nth p n val) = maxn n.+1 (size p).

Parameter nth_polyCons : ∀ a p k,
  nth (polyCons a p) k = if k is k'.+1 then nth p k' else a.
Parameter nth_polyNil : ∀ n, nth polyNil n = C.zero.

Parameter fold_polyNil : ∀ U f iv, @fold U f iv polyNil = iv.
Parameter fold_polyCons : ∀ U f iv c p,
  @fold U f iv (polyCons c p) = f c (@fold U f iv p).
Parameter nth_set_nth : ∀ p n val k,
  nth (set_nth p n val) k = if k == n then val else nth p k.

Parameter nth_default : ∀ p n, size p ≤ n → nth p n = C.zero.

Parameter set_nth_nth : ∀ p n, n < size p → set_nth p n (nth p n) = p.

End PolyOps.

Module FullR <: FullOps.
Definition U := unit.
Local Notation "--> e" := (fun _ : U ⇒ e).
Definition T := R.
Definition zero := 0%R.
Definition one := 1%R.
Definition opp := Ropp.
Definition add := --> Rplus.
Definition sub := --> Rminus.
Definition mul := --> Rmult.
Definition div := --> Rdiv.
Definition power_int := --> powerRZ.
Definition exp := --> exp.
Definition ln := --> ln.
Definition from_nat (_:U) := INR.
Definition fromZ (_:U) := IZR.
Definition inv := --> Rinv.
Definition cos := --> cos.
Definition sin := --> sin.
Definition sqr := --> fun x ⇒ Rmult x x.
Definition sqrt := --> sqrt.
Definition invsqrt := --> fun x ⇒ (Rinv (sqrt tt x)).
Definition mask : T → T → T := fun c _ ⇒ c.
Definition tan := --> tan.
Definition atan := --> atan.
End FullR.

Module SeqPoly (C : PowDivOps) <: PolyOps C.
Definition U := C.U.
Definition T := seq C.T.


Definition zero : T := [::].
Definition one : T := [:: C.one].

Definition opp := map C.opp.

Section PrecIsPropagated.
Variable u : U.

Definition add := map2 (C.add u) (fun x ⇒ x).

Definition sub := map2 (C.sub u) C.opp.

Definition nth := nth C.zero.

Definition mul_coeff (p q : T) (k : nat) : C.T :=
  foldl (fun x i ⇒ C.add u (C.mul u (nth p i) (nth q (k - i))) x) (C.zero)
        (rev (iota 0 k.+1)).

Lemma mul_coeffE p q k : mul_coeff p q k =
  \big[C.add u/C.zero]_(0 ≤ i < k.+1) C.mul u (nth p i) (nth q (k - i)).

Definition mul_trunc n p q := mkseq (mul_coeff p q) n.+1.

Definition mul_tail n p q :=
  mkseq (fun i ⇒ mul_coeff p q (n.+1+i)) ((size p + size q).-1 - n.+1).

Definition mul p q :=
  mkseq (mul_coeff p q) (size p + size q).-1.

Definition rec1 := @rec1up C.T.
Definition rec2 := @rec2up C.T.
Definition size := @size C.T.
Definition fold := @foldr C.T.
Definition horner p x :=
  C.mask
  (@fold C.T (fun a b ⇒ C.add u (C.mul u b x) a) C.zero p)
  x.
Definition set_nth := @set_nth C.T C.zero.
Definition map := @map C.T C.T.

Definition polyCons := @Cons C.T.

Definition polyNil := @Nil C.T.

Definition polyC (c : C.T) : T := polyCons c polyNil.

Definition polyX := [:: C.zero; C.one].

Lemma poly_ind : ∀ (f : T → Prop),
  f polyNil →
  (∀ a p, f p → f (polyCons a p)) →
  ∀ p, f p.

Definition deriv_loop := foldri (fun a i s ⇒ C.mul u a (C.from_nat u i) :: s) [::].

Definition deriv (p : T) := deriv_loop (behead p) 1.

Definition grec1 (A : Type) := @grec1up A C.T.

Lemma size_grec1 A F G (q : A) s n : size (grec1 F G q s n) = n.+1.

Lemma size_rec1 F x n: size (rec1 F x n) = n.+1.

Lemma size_rec2 F x y n: size (rec2 F x y n) = n.+1.

Lemma size_mul_trunc n p q: size (mul_trunc n p q) = n.+1.

Lemma size_mul_tail n p q:
  size (mul_tail n p q) = ((size p) + (size q)).-1 - n.+1.

Lemma size_add p1 p2 : size (add p1 p2) = maxn (size p1) (size p2).

Lemma size_opp p1 : size (opp p1) = size p1.

Lemma size_sub p1 p2 : size (sub p1 p2) = maxn (size p1) (size p2).

Lemma size_deriv p : size (deriv p) = (size p).-1.

End PrecIsPropagated.

Definition tail := @drop C.T.

Definition lift (n : nat) p := ncons n C.zero p.

Lemma size_lift n p : size (lift n p) = n + size p.

Definition mul_mixed (u : U) (a : C.T) (p : T) :=
  @foldr C.T T (fun x acc ⇒ (C.mul u a x) :: acc) [::] p.

Definition div_mixed_r (u : U) (p : T) (b : C.T) :=
  @foldr C.T T (fun x acc ⇒ (C.div u x b) :: acc) [::] p.

Lemma size_mul_mixed u a p : size (mul_mixed u a p) = size p.

Lemma size_div_mixed_r u p b : size (div_mixed_r u p b) = size p.

Lemma size_mul u p q : size (mul u p q) = (size p + size q).-1.

Fixpoint dotmuldiv (u : U) (a b : seq Z) (p : T) : T :=
match a, b, p with
| a0 :: a1, b0 :: b1, p0 :: p1 ⇒
  C.mul u (C.div u (C.fromZ u a0) (C.fromZ u b0)) p0 ::
  dotmuldiv u a1 b1 p1
| _, _, _ ⇒ [::]
end.

Lemma fold_polyNil U f iv : @fold U f iv polyNil = iv.

Lemma fold_polyCons U f iv c p :
  @fold U f iv (polyCons c p) = f c (@fold U f iv p).

Lemma size_set_nth p n val :
  size (set_nth p n val) = maxn n.+1 (size p).

Lemma nth_set_nth p n val k :
  nth (set_nth p n val) k = if k == n then val else nth p k.

Lemma nth_default p n : size p ≤ n → nth p n = C.zero.

Lemma set_nth_nth p n : n < size p → set_nth p n (nth p n) = p.

Lemma size_polyNil : size polyNil = 0.

Lemma size_polyCons a p : size (polyCons a p) = (size p).+1.

Lemma nth_polyNil n : nth polyNil n = C.zero.

Lemma nth_polyCons a p k :
  nth (polyCons a p) k = if k is k'.+1 then nth p k' else a.

Lemma size_dotmuldiv (n : nat) (u : U) a b p :
  size p = n → seq.size a = n → seq.size b = n →
  size (dotmuldiv u a b p) = n.

Lemma size_tail p k : size (tail k p) = size p - k.

Definition toSeq (p : T) := p.

Lemma horner_seq u p x :
  horner u p x = C.mask (foldr (fun a b ⇒ C.add u (C.mul u b x) a)
    C.zero (toSeq p)) x.

Lemma nth_toSeq p n : nth p n = seq.nth (C.zero) (toSeq p) n.

Section precSection.
Variable u : U.
Definition int_coeff (p : T) (c : C.T) (n : nat) :=
match n with
| 0 ⇒ c
| S m ⇒ C.div u (nth p m) (C.from_nat u n)
end.

Definition int_coeff_shift (p : T) (k : nat) :=
  C.div u (seq.nth C.zero p k) (C.from_nat u k.+1).

Definition primitive (c : C.T) (p : T) :=
 (c::(mkseq (int_coeff_shift p) (size p))) : T.

Lemma size_primitive (c : C.T) (p : T): size (primitive c p) = (size p).+1.

End precSection.

Lemma size_map f p : size (map f p) = size p.

Lemma polyCE c : polyC c = polyCons c polyNil.

Lemma polyXE : polyX = lift 1 one.

Lemma oneE : one = polyC C.one.

Lemma nth_mul u p q k :
  nth (mul u p q) k =
  if (size p + size q).-1 ≤ k then C.zero
  else mul_coeff u p q k.

Lemma nth_mul_trunc u n p q k :
  nth (mul_trunc u n p q) k =
  if n < k then C.zero
  else mul_coeff u p q k.

Lemma nth_mul_tail u n p q k :
  nth (mul_tail u n p q) k =
  if (size p + size q).-1 - n.+1 ≤ k then C.zero
  else mul_coeff u p q (n.+1 + k).

Lemma nth_dotmuldiv u a b p k :
  nth (dotmuldiv u a b p) k =
  if [|| size p ≤ k, seq.size a ≤ k | seq.size b ≤ k] then C.zero
  else C.mul u (C.div u (C.fromZ u (seq.nth 0%Z a k)) (C.fromZ u (seq.nth 0%Z b k))) (nth p k).

End SeqPoly.

Module PolR <: PolyOps FullR.
Include SeqPoly FullR.

Module Import Notations.
Notation "p .[ x ]" := (PolR.horner tt p x) : R_scope.
Notation "p ^` ()" := (PolR.deriv tt p) : R_scope.
End Notations.

Lemma toSeq_horner0 (u : U) (p : T) : horner u p 0%R = head 0%R (toSeq p).

Lemma mul_coeff_eq0 p q k :
  (∀ i, i ≤ k → nth p i = 0%R ∨ nth q (k - i) = 0%R) →
  (\big[Rplus/R0]_(0 ≤ i < k.+1) (nth p i × nth q (k - i)) = 0)%R.

Lemma nth_mul' u p q k :
  nth (mul u p q) k =
  \big[Rplus/0%R]_(0 ≤ i < k.+1) Rmult (nth p i) (nth q (k - i)).

Lemma hornerE p x :
  horner tt p x =
  \big[Rplus/0%R]_(0 ≤ i < size p) Rmult (nth p i) (x ^ i).

Lemma hornerE_wide n p x :
  size p ≤ n →
  horner tt p x =
  \big[Rplus/R0]_(0 ≤ i < n) Rmult (nth p i) (x ^ i).

Lemma coef_deriv p i :
  nth (deriv tt p) i = (nth p i.+1 × INR i.+1)%R.

Lemma horner_derivE_wide n p x :
  (size p).-1 ≤ n →
  horner tt (deriv tt p) x =
  \big[Rplus/R0]_(0 ≤ i < n) ((nth p i.+1) × (INR i.+1) × (x ^ i))%R.

Lemma horner_derivE p x :
  horner tt (deriv tt p) x =
  \big[Rplus/R0]_(0 ≤ i < (size p).-1)
    ((nth p i.+1) × (INR i.+1) × (x ^ i))%R.

Lemma is_derive_horner p x :
  is_derive (horner tt p) x (horner tt (deriv tt p) x).

Corollary Derive_horner p x :
  Derive (horner tt p) x = horner tt (deriv tt p) x.

Corollary ex_derive_horner p x : ex_derive (horner tt p) x.

Lemma nth_add p1 p2 k :
  nth (add tt p1 p2) k = Rplus (nth p1 k) (nth p2 k).

Lemma nth_opp p1 k : nth (opp p1) k = Ropp (nth p1 k).

Lemma nth_sub p1 p2 k :
  nth (sub tt p1 p2) k = Rminus (nth p1 k) (nth p2 k).

Lemma nth_mul_mixed a p1 k :
  nth (mul_mixed tt a p1) k = Rmult a (nth p1 k).

Lemma nth_div_mixed_r p1 b k :
  nth (div_mixed_r tt p1 b) k = Rdiv (nth p1 k) b.

Lemma nth_lift n p k :
  nth (lift n p) k = if k < n then 0%R else nth p (k - n).

Lemma horner_polyC c x : horner tt (polyC c) x = c.

Lemma horner_opp p x :
  horner tt (opp p) x = Ropp (horner tt p x).

Lemma horner_add p q x :
  horner tt (add tt p q) x = (horner tt p x + horner tt q x)%R.

Lemma horner_sub p q x :
  horner tt (sub tt p q) x = (horner tt p x - horner tt q x)%R.

Lemma horner0 p x : (∀ n, nth p n = 0%R) → p.[x] = 0%R.

Lemma mul_coeff0l p q : size p = 0 → ∀ n, mul_coeff tt p q n = 0%R.

Lemma nth_mulCl c p q i :
  nth (mul tt (c :: p) q) i.+1 =
  (c × nth q i.+1 + nth (mul tt p q) i)%R.

Lemma horner_mulCl c p q x :
  ((mul tt (c :: p) q).[x] = (mul tt p q).[x] × x + c × q.[x])%R.

Lemma horner_mul p q x :
  horner tt (mul tt p q) x = (horner tt p x × horner tt q x)%R.

Lemma horner_lift n p x :
  horner tt (lift n p) x = (horner tt p x × x ^ n)%R.

Lemma horner_mul_mixed a p x :
  horner tt (mul_mixed tt a p) x = (a × horner tt p x)%R.

Lemma horner_div_mixed_r p b x :
  horner tt (div_mixed_r tt p b) x = (horner tt p x / b)%R.

Lemma nth_primitive (p : T) (c : R) (k : nat) :
  nth (primitive tt c p) k = if size p < k then 0%R
                        else int_coeff tt p c k.

End PolR.

Module Type PolyIntOps (I : IntervalOps).
Module Int := FullInt I.
Module J := IntervalExt I.
Include PolyOps Int.

Definition contains_pointwise pi p : Prop :=
  ∀ k, contains (I.convert (nth pi k)) (Xreal (PolR.nth p k)).

Definition seq_contains_pointwise si s : Prop :=
  ∀ k, contains (I.convert (seq.nth Int.zero si k)) (Xreal (PolR.nth s k)).

Notation seq_eq_size si s := (seq.size si = seq.size s).

Module Import Notations.
Notation "i >: x" := (contains (I.convert i) (Xreal x)) : ipoly_scope.
Notation "p >:: x" := (contains_pointwise p x) : ipoly_scope.
Notation eq_size pi p := (size pi = PolR.size p).
End Notations.
Local Open Scope ipoly_scope.

Parameter horner_correct :
  ∀ u pi ci p x, pi >:: p → ci >: x → horner u pi ci >: PolR.horner tt p x.

Parameter polyC_correct : ∀ ci c, ci >: c → polyC ci >:: PolR.polyC c.
Parameter polyX_correct : polyX >:: PolR.polyX.

Parameter zero_correct : zero >:: PolR.zero.
Parameter one_correct : one >:: PolR.one.
Parameter opp_correct : ∀ pi p, pi >:: p → opp pi >:: PolR.opp p.
Parameter map_correct :
  ∀ fi f pi p,
  (f 0%R = 0%R) →
  (∀ xi x, xi >: x → fi xi >: f x) →
  pi >:: p →
  map fi pi >:: PolR.map f p.
Parameter dotmuldiv_correct :
  ∀ u a b pi p,
  seq.size a = seq.size b →
  pi >:: p →
  dotmuldiv u a b pi >:: PolR.dotmuldiv tt a b p.
Parameter add_correct :
  ∀ u pi qi p q, pi >:: p → qi >:: q → add u pi qi >:: PolR.add tt p q.
Parameter sub_correct :
  ∀ u pi qi p q, pi >:: p → qi >:: q → sub u pi qi >:: PolR.sub tt p q.
Parameter mul_correct :
  ∀ u pi qi p q, pi >:: p → qi >:: q → mul u pi qi >:: PolR.mul tt p q.
Parameter mul_trunc_correct :
  ∀ u n pi qi p q, pi >:: p → qi >:: q →
  mul_trunc u n pi qi >:: PolR.mul_trunc tt n p q.
Parameter mul_tail_correct :
  ∀ u n pi qi p q, pi >:: p → qi >:: q →
  mul_tail u n pi qi >:: PolR.mul_tail tt n p q.
Parameter mul_mixed_correct :
  ∀ u ai pi a p, ai >: a → pi >:: p →
  mul_mixed u ai pi >:: PolR.mul_mixed tt a p.
Parameter div_mixed_r_correct :
  ∀ u pi bi p b, pi >:: p → bi >: b →
  div_mixed_r u pi bi >:: PolR.div_mixed_r tt p b.
Parameter horner_propagate : ∀ u pi, J.propagate (horner u pi).
Parameter deriv_correct :
  ∀ u pi p, pi >:: p → deriv u pi >:: (PolR.deriv tt p).
Parameter primitive_correct :
  ∀ u ci c pi p,
  ci >: c →
  pi >:: p →
  primitive u ci pi >:: PolR.primitive tt c p.
Parameter lift_correct : ∀ n pi p, pi >:: p → lift n pi >:: PolR.lift n p.
Parameter tail_correct : ∀ n pi p, pi >:: p → tail n pi >:: PolR.tail n p.
Parameter set_nth_correct :
  ∀ pi p n ai a, pi >:: p → ai >: a → set_nth pi n ai >:: PolR.set_nth p n a.
Parameter polyNil_correct : polyNil >:: PolR.polyNil. Parameter polyCons_correct :
  ∀ pi xi p x, pi >:: p → xi >: x →
  polyCons xi pi >:: PolR.polyCons x p.
Parameter rec1_correct :
  ∀ fi f fi0 f0 n,
    (∀ ai a m, ai >: a → fi ai m >: f a m) → fi0 >: f0 →
    rec1 fi fi0 n >:: PolR.rec1 f f0 n.
Parameter rec2_correct :
  ∀ fi f fi0 f0 fi1 f1 n,
    (∀ ai bi a b m, ai >: a → bi >: b → fi ai bi m >: f a b m) →
    fi0 >: f0 → fi1 >: f1 →
    rec2 fi fi0 fi1 n >:: PolR.rec2 f f0 f1 n.
Parameter grec1_correct :
  ∀ Fi (F : PolR.T → nat → PolR.T) Gi (G : PolR.T → nat → R) ai a si s n,
  (∀ qi q m, qi >:: q → Fi qi m >:: F q m) →
  (∀ qi q m, qi >:: q → Gi qi m >: G q m) →
  ai >:: a →
  seq_contains_pointwise si s →
  seq_eq_size si s →
  grec1 Fi Gi ai si n >:: PolR.grec1 F G a s n.


Parameter nth_default_alt : ∀ pi p, pi >:: p →
  ∀ n : nat, size pi ≤ n → PolR.nth p n = 0%R.

Definition poly_eqNai s := ∀ k, k < size s → I.convert (nth s k) = Inan.

Definition seq_eqNai s := ∀ k, k < seq.size s → I.convert (seq.nth I.zero s k) = Inan.

Parameter grec1_propagate :
  ∀ A (Fi : A → nat → A) (Gi : A → nat → I.type) ai si,
  (∀ qi m, I.convert (Gi qi m) = Inan) →
  seq_eqNai si →
  ∀ n, poly_eqNai (grec1 Fi Gi ai si n).

Parameter dotmuldiv_propagate :
  ∀ u a b p,
  seq.size a = size p →
  seq.size b = size p →
  poly_eqNai p →
  poly_eqNai (dotmuldiv u a b p).

Parameter rec1_propagate :
  ∀ (Fi : I.type → nat → I.type) ai,
  (∀ qi m, I.convert qi = Inan → I.convert (Fi qi m) = Inan) →
  I.convert ai = Inan →
  ∀ n, poly_eqNai (rec1 Fi ai n).

Parameter polyCons_propagate :
  ∀ xi pi,
  I.convert xi = Inan →
  poly_eqNai pi →
  poly_eqNai (polyCons xi pi).
End PolyIntOps.