Library PrimeGapS1.IntPoly

From Stdlib Require Import ZArith List.
Import ListNotations.
Open Scope Z_scope.


Definition pol : Type := list Z.


Fixpoint plead_aux (p : pol) (acc : Z) : Z :=
  match p with
  | [] ⇒ acc
  | x :: xs ⇒ if Z.eqb x 0 then plead_aux xs acc else plead_aux xs x
  end.

Definition plead (p : pol) : Z := plead_aux p 0.


Fixpoint peval_at_rat_aux (p : pol) (num den : Z) : Z × Z :=
  
  match p with
  | [] ⇒ (0, 1)
  | a :: rest ⇒
      let '(rest_val, rest_den_pow) := peval_at_rat_aux rest num den in
      
      (a × (den × rest_den_pow) + num × rest_val, den × rest_den_pow)
  end.

Definition peval_at_rat (p : pol) (num den : Z) : Z :=
  fst (peval_at_rat_aux p num den).