(Joint Center)Library qe_rcf

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import finfun path matrix.
Require Import bigop ssralg poly polydiv ssrnum zmodp div ssrint.
Require Import polyorder polyrcf interval polyXY.
Require Import qe_rcf_th ordered_qelim mxtens.

Set Implicit Arguments.

Import GRing.Theory Num.Theory.

Local Open Scope nat_scope.
Local Open Scope ring_scope.

Import ord.

Section QF.

Variable R : Type.

Inductive term : Type :=
| Var of nat
| Const of R
| NatConst of nat
| Add of term & term
| Opp of term
| NatMul of term & nat
| Mul of term & term
| Exp of term & nat.

Inductive formula : Type :=
| Bool of bool
| Equal of term & term
| Lt of term & term
| Le of term & term
| And of formula & formula
| Or of formula & formula
| Implies of formula & formula
| Not of formula.

Coercion rterm_to_term := fix loop (t : term) : GRing.term R :=
  match t with
    | Var xGRing.Var _ x
    | Const xGRing.Const x
    | NatConst nGRing.NatConst _ n
    | Add u vGRing.Add (loop u) (loop v)
    | Opp uGRing.Opp (loop u)
    | NatMul u nGRing.NatMul (loop u) n
    | Mul u vGRing.Mul (loop u) (loop v)
    | Exp u nGRing.Exp (loop u) n
  end.

Coercion qfr_to_formula := fix loop (f : formula) : ord.formula R :=
  match f with
    | Bool bord.Bool b
    | Equal x yord.Equal x y
    | Lt x yord.Lt x y
    | Le x yord.Le x y
    | And f gord.And (loop f) (loop g)
    | Or f gord.Or (loop f) (loop g)
    | Implies f gord.Implies (loop f) (loop g)
    | Not ford.Not (loop f)
  end.

Definition to_rterm := fix loop (t : GRing.term R) : term :=
  match t with
    | GRing.Var xVar x
    | GRing.Const xConst x
    | GRing.NatConst nNatConst n
    | GRing.Add u vAdd (loop u) (loop v)
    | GRing.Opp uOpp (loop u)
    | GRing.NatMul u nNatMul (loop u) n
    | GRing.Mul u vMul (loop u) (loop v)
    | GRing.Exp u nExp (loop u) n
    | _NatConst 0
  end.

End QF.


Implicit Arguments Bool [R].

Notation True := (Bool true).
Notation False := (Bool false).

Delimit Scope qf_scope with qfT.
Notation "''X_' i" := (Var _ i) : qf_scope.
Notation "n %:R" := (NatConst _ n) : qf_scope.
Notation "x %:T" := (Const x) : qf_scope.
Notation "0" := 0%:R%qfT : qf_scope.
Notation "1" := 1%:R%qfT : qf_scope.
Infix "+" := Add : qf_scope.
Notation "- t" := (Opp t) : qf_scope.
Notation "t - u" := (Add t (- u)) : qf_scope.
Infix "×" := Mul : qf_scope.
Infix "*+" := NatMul : qf_scope.
Infix "^+" := Exp : qf_scope.
Notation "t ^- n" := (t^-1 ^+ n)%qfT : qf_scope.
Infix "==" := Equal : qf_scope.
Infix "<%" := Lt : qf_scope.
Infix "<=%" := Le : qf_scope.
Infix "∧" := And : qf_scope.
Infix "∨" := Or : qf_scope.
Infix "==>" := Implies : qf_scope.
Notation "~ f" := (Not f) : qf_scope.
Notation "x != y" := (Not (x == y)) : qf_scope.

Section evaluation.

Variable R : realDomainType.

Fixpoint eval (e : seq R) (t : term R) {struct t} : R :=
  match t with
  | ('X_i)%qfTe`_i
  | (x%:T)%qfTx
  | (n%:R)%qfTn%:R
  | (t1 + t2)%qfTeval e t1 + eval e t2
  | (- t1)%qfT- eval e t1
  | (t1 *+ n)%qfTeval e t1 *+ n
  | (t1 × t2)%qfTeval e t1 × eval e t2
  | (t1 ^+ n)%qfTeval e t1 ^+ n
  end.

Lemma evalE (e : seq R) (t : term R) : eval e t = GRing.eval e t.

Definition qf_eval e := fix loop (f : formula R) : bool :=
  match f with
  | Bool bb
  | t1 == t2 ⇒ (eval e t1 == eval e t2)%bool
  | t1 <% t2 ⇒ (eval e t1 < eval e t2)%bool
  | t1 <=% t2 ⇒ (eval e t1 eval e t2)%bool
  | f1 f2loop f1 && loop f2
  | f1 f2loop f1 || loop f2
  | f1 ==> f2 ⇒ (loop f1 ==> loop f2)%bool
  | ¬ f1~~ loop f1
  end%qfT.

Lemma qf_evalE (e : seq R) (f : formula R) : qf_eval e f = ord.qf_eval e f.

Lemma to_rtermE (t : GRing.term R) :
  GRing.rterm tto_rterm t = t :> GRing.term _.

End evaluation.

Import Pdiv.Ring.

Definition bind_def T1 T2 T3 (f : (T1T2) → T3) (k : T1T2) := f k.
Notation "'bind' x <- y ; z" :=
  (bind_def y (fun xz)) (at level 99, x at level 0, y at level 0,
    format "'[hv' 'bind' x <- y ; '/' z ']'").

Section ProjDef.

Variable F : realFieldType.

Notation fF := (formula F).
Notation tF := (term F).
Definition polyF := seq tF.

Lemma qf_formF (f : fF) : qf_form f.

Lemma rtermF (t : tF) : GRing.rterm t.

Lemma rformulaF (f : fF) : rformula f.

Section If.

Implicit Types (pf tf ef : formula F).

Definition If pf tf ef := (pf tf ¬ pf ef)%qfT.

End If.

Notation "'If' c1 'Then' c2 'Else' c3" := (If c1 c2 c3)
  (at level 200, right associativity, format
"'[hv ' 'If' c1 '/' '[' 'Then' c2 ']' '/' '[' 'Else' c3 ']' ']'").

Notation cps T := ((TfF) → fF).

Section Pick.

Variables (I : finType) (pred_f then_f : IfF) (else_f : fF).

Definition Pick :=
  \big[Or/False]_(p : {ffun pred I})
    ((\big[And/True]_i (if p i then pred_f i else ¬ pred_f i))
     (if pick p is Some i then then_f i else else_f))%qfT.

Lemma eval_Pick e (qev := qf_eval e) :
  let P i := qev (pred_f i) in
  qev Pick = (if pick P is Some i then qev (then_f i) else qev else_f).

End Pick.

Fixpoint eval_poly (e : seq F) pf :=
  if pf is c :: qf then (eval_poly e qf) × 'X + (eval e c)%:P else 0.

Lemma eval_polyP e p : eval_poly e p = Poly (map (eval e) p).

Fixpoint Size (p : polyF) : cps nat := fun k
  if p is c :: q then
    bind n <- Size q;
    if n is m.+1 then k m.+2
      else If c == 0 Then k 0%N Else k 1%N
    else k 0%N.

Definition Isnull (p : polyF) : cps bool := fun k
  bind n <- Size p; k (n == 0%N).

Definition LtSize (p q : polyF) : cps bool := fun k
  bind n <- Size p; bind m <- Size q; k (n < m)%N.

Fixpoint LeadCoef p : cps tF := fun k
  if p is c :: q then
    bind l <- LeadCoef q; If l == 0 Then k c Else k l
    else k (Const 0).

Fixpoint AmulXn (a : tF) (n : nat) : polyF:=
  if n is n'.+1 then (Const 0) :: (AmulXn a n') else [::a].

Fixpoint AddPoly (p q : polyF) :=
  if p is a::p' then
    if q is b::q' then (a + b)%qfT :: (AddPoly p' q')
      else p
    else q.
Local Infix "++" := AddPoly : qf_scope.

Definition ScalPoly (c : tF) (p : polyF) : polyF := map (Mul c) p.
Local Infix "*:" := ScalPoly : qf_scope.

Fixpoint MulPoly (p q : polyF) := if p is a :: p'
    then (a *: q ++ (0 :: (MulPoly p' q)))%qfT else [::].
Local Infix "**" := MulPoly (at level 40) : qf_scope.

Lemma map_poly0 (R R' : ringType) (f : RR') : map_poly f 0 = 0.

Definition ExpPoly p n := iterop n MulPoly p [::1%qfT].
Local Infix "^^+" := ExpPoly (at level 29) : qf_scope.

Definition OppPoly := ScalPoly (@Const F (-1)).
Local Notation "-- p" := (OppPoly p) (at level 35) : qf_scope.
Local Notation "p -- q" := (p ++ (-- q))%qfT (at level 50) : qf_scope.

Definition NatMulPoly n := ScalPoly (NatConst F n).
Local Infix "+**" := NatMulPoly (at level 40) : qf_scope.

Fixpoint Horner (p : polyF) (x : tF) : tF :=
  if p is a :: p then (Horner p x × x + a)%qfT else 0%qfT.

Fixpoint Deriv (p : polyF) : polyF :=
  if p is a :: q then (q ++ (0 :: Deriv q))%qfT else [::].

Fixpoint Rediv_rec_loop (q : polyF) sq cq
  (c : nat) (qq r : polyF) (n : nat) {struct n} :
  cps (nat × polyF × polyF) := fun k
  bind sr <- Size r;
  if (sr < sq)%N then k (c, qq, r) else
    bind lr <- LeadCoef r;
    let m := AmulXn lr (sr - sq) in
    let qq1 := (qq ** [::cq] ++ m)%qfT in
    let r1 := (r ** [::cq] -- m ** q)%qfT in
    if n is n1.+1 then Rediv_rec_loop q sq cq c.+1 qq1 r1 n1 k
    else k (c.+1, qq1, r1).

 Definition Rediv (p : polyF) (q : polyF) : cps (nat × polyF × polyF) :=
  fun k
  bind b <- Isnull q;
  if b then k (0%N, [::Const 0], p)
    else bind sq <- Size q;
      bind sp <- Size p;
      bind lq <- LeadCoef q;
      Rediv_rec_loop q sq lq 0 [::Const 0] p sp k.

Definition Rmod (p : polyF) (q : polyF) (k : polyFfF) : fF :=
  Rediv p q (fun dk d.2)%PAIR.
Definition Rdiv (p : polyF) (q : polyF) (k : polyFfF) : fF :=
  Rediv p q (fun dk d.1.2)%PAIR.
Definition Rscal (p : polyF) (q : polyF) (k : natfF) : fF :=
  Rediv p q (fun dk d.1.1)%PAIR.
Definition Rdvd (p : polyF) (q : polyF) (k : boolfF) : fF :=
  bind r <- Rmod p q; bind r_null <- Isnull r; k r_null.

Fixpoint rgcdp_loop n (pp qq : {poly F}) {struct n} :=
  if rmodp pp qq == 0 then qq
    else if n is n1.+1 then rgcdp_loop n1 qq (rmodp pp qq)
        else rmodp pp qq.

Fixpoint Rgcd_loop n pp qq k {struct n} :=
  bind r <- Rmod pp qq; bind b <- Isnull r;
  if b then (k qq)
    else if n is n1.+1 then Rgcd_loop n1 qq r k else k r.

Definition Rgcd (p : polyF) (q : polyF) : cps polyF := fun k
  let aux p1 q1 k := (bind b <- Isnull p1;
    if b then k q1 else bind n <- Size p1; Rgcd_loop n p1 q1 k) in
  bind b <- LtSize p q;
  if b then aux q p k else aux p q k.

Fixpoint BigRgcd (ps : seq polyF) : cps (seq tF) := fun k
  if ps is p :: pr then bind r <- BigRgcd pr; Rgcd p r k else k [::Const 0].

Fixpoint Changes (s : seq tF) : cps nat := fun k
  if s is a :: q then
    bind v <- Changes q;
    If (Lt (a × head 0 q) 0)%qfT Then k (1 + v)%N Else k v
    else k 0%N.

Fixpoint SeqPInfty (ps : seq polyF) : cps (seq tF) := fun k
  if ps is p :: ps then
    bind lp <- LeadCoef p;
    bind lps <- SeqPInfty ps;
    k (lp :: lps)
  else k [::].

Fixpoint SeqMInfty (ps : seq polyF) : cps (seq tF) := fun k
  if ps is p :: ps then
    bind lp <- LeadCoef p;
    bind sp <- Size p;
    bind lps <- SeqMInfty ps;
    k ((-1)%:T ^+ (~~ odd sp) × lp :: lps)%qfT
  else k [::].

Definition ChangesPoly ps : cps int := fun k
  bind mps <- SeqMInfty ps;
  bind pps <- SeqPInfty ps;
  bind vm <- Changes mps; bind vp <- Changes pps; k (vm%:Z - vp%:Z).

Definition NextMod (p q : polyF) : cps polyF := fun k
  bind lq <- LeadCoef q;
  bind spq <- Rscal p q;
  bind rpq <- Rmod p q; k (- lq ^+ spq *: rpq)%qfT.

Fixpoint ModsAux (p q : polyF) n : cps (seq polyF) := fun k
    if n is m.+1
      then
        bind p_eq0 <- Isnull p;
        if p_eq0 then k [::]
        else
          bind npq <- NextMod p q;
          bind ps <- ModsAux q npq m;
          k (p :: ps)
      else k [::].

Definition Mods (p q : polyF) : cps (seq polyF) := fun k
  bind sp <- Size p; bind sq <- Size q;
  ModsAux p q (maxn sp sq.+1) k.

Definition PolyComb (sq : seq polyF) (sc : seq int) :=
  reducebig [::1%qfT] (iota 0 (size sq))
  (fun iBigBody i MulPoly true (nth [::] sq i ^^+ comb_exp sc`_i)%qfT).

Definition Pcq sq i := (nth [::] (map (PolyComb sq) (sg_tab (size sq))) i).

Definition TaqR (p : polyF) (q : polyF) : cps int := fun k
  bind r <- Mods p (Deriv p ** q)%qfT; ChangesPoly r k.

Definition TaqsR (p : polyF) (sq : seq polyF) (i : nat) : cps tF :=
  fun kbind n <- TaqR p (Pcq sq i); k ((n%:~R) %:T)%qfT.

Fixpoint ProdPoly T (s : seq T) (f : Tcps polyF) : cps polyF := fun k
  if s is a :: s then
    bind fa <- f a;
    bind fs <- ProdPoly s f;
    k (fa ** fs)%qfT
  else k [::1%qfT].

Definition BoundingPoly (sq : seq polyF) : polyF :=
  Deriv (reducebig [::1%qfT] sq (fun iBigBody i MulPoly true i)).

Definition Coefs (n i : nat) : tF :=
  Const (match n with
    | 0 ⇒ (i == 0%N)%:R
    | 1 ⇒ [:: 2%:R^-1; 2%:R^-1; 0]`_i
    | ncoefs _ n i
  end).

Definition CcountWeak (p : polyF) (sq : seq polyF) : cps tF := fun k
  let fix aux s (i : nat) k := if i is i'.+1
    then bind x <- TaqsR p sq i';
      aux (x × (Coefs (size sq) i') + s)%qfT i' k
    else k s in
   aux 0%qfT (3 ^ size sq)%N k.

Definition CcountGt0 (sp sq : seq polyF) : fF :=
  bind p <- BigRgcd sp; bind p0 <- Isnull p;
  if ~~ p0 then
    bind c <- CcountWeak p sq;
    Lt 0%qfT c
  else
    let bq := BoundingPoly sq in
      bind cw <- CcountWeak bq sq;
      ((reducebig True sq (fun q
          BigBody q And true (LeadCoef q (fun lqLt 0 lq))))
         ((reducebig True sq (fun q
         BigBody q And true
          (bind sq <- Size q;
          bind lq <- LeadCoef q;
          Lt 0 ((Opp 1) ^+ (sq).-1 × lq)
        ))) Lt 0 cw))%qfT.

Fixpoint abstrX (i : nat) (t : tF) : polyF :=
  (match t with
    | 'X_nif n == i then [::0; 1] else [::t]
    | - x-- abstrX i x
    | x + yabstrX i x ++ abstrX i y
    | x × yabstrX i x ** abstrX i y
    | x *+ nn +** abstrX i x
    | x ^+ nabstrX i x ^^+ n
    | _[::t]
  end)%qfT.

Definition wproj (n : nat) (s : seq (GRing.term F) × seq (GRing.term F)) :
  formula F :=
  let sp := map (abstrX n \o to_rterm) s.1%PAIR in
  let sq := map (abstrX n \o to_rterm) s.2%PAIR in
    CcountGt0 sp sq.

Definition rcf_sat := proj_sat wproj.

End ProjDef.

Section ProjCorrect.

Variable F : rcfType.
Implicit Types (e : seq F).

Notation fF := (formula F).
Notation tF := (term F).
Notation polyF := (polyF F).

Notation "'If' c1 'Then' c2 'Else' c3" := (If c1 c2 c3)
  (at level 200, right associativity, format
"'[hv ' 'If' c1 '/' '[' 'Then' c2 ']' '/' '[' 'Else' c3 ']' ']'").

Notation cps T := ((TfF) → fF).

Local Infix "**" := MulPoly (at level 40) : qf_scope.
Local Infix "+**" := NatMulPoly (at level 40) : qf_scope.
Local Notation "-- p" := (OppPoly p) (at level 35) : qf_scope.
Local Notation "p -- q" := (p ++ (-- q))%qfT (at level 50) : qf_scope.
Local Infix "^^+" := ExpPoly (at level 29) : qf_scope.
Local Infix "**" := MulPoly (at level 40) : qf_scope.
Local Infix "*:" := ScalPoly : qf_scope.
Local Infix "++" := AddPoly : qf_scope.

Lemma eval_If e pf tf ef (ev := qf_eval e) :
  ev (If pf Then tf Else ef) = (if ev pf then ev tf else ev ef).

Lemma eval_Size k p e :
  qf_eval e (Size p k) = qf_eval e (k (size (eval_poly e p))).

Lemma eval_Isnull k p e : qf_eval e (Isnull p k)
  = qf_eval e (k (eval_poly e p == 0)).

Lemma eval_LeadCoef e p k k' :
  ( x, qf_eval e (k x) = (k' (eval e x))) →
  qf_eval e (LeadCoef p k) = k' (lead_coef (eval_poly e p)).

Implicit Arguments eval_LeadCoef [e p k].

Lemma eval_AmulXn a n e : eval_poly e (AmulXn a n) = (eval e a)%:P × 'X^n.

Lemma eval_AddPoly p q e :
  eval_poly e (p ++ q)%qfT = (eval_poly e p) + (eval_poly e q).

Lemma eval_ScalPoly e t p :
  eval_poly e (ScalPoly t p) = (eval e t) *: (eval_poly e p).

Lemma eval_MulPoly e p q :
  eval_poly e (p ** q)%qfT = (eval_poly e p) × (eval_poly e q).

Lemma eval_ExpPoly e p n : eval_poly e (p ^^+ n)%qfT = (eval_poly e p) ^+ n.

Lemma eval_NatMulPoly p n e :
  eval_poly e (n +** p)%qfT = (eval_poly e p) *+ n.

Lemma eval_OppPoly p e : eval_poly e (-- p)%qfT = - eval_poly e p.

Lemma eval_Horner e p x : eval e (Horner p x) = (eval_poly e p).[eval e x].

Lemma eval_ConstPoly e c : eval_poly e [::c] = (eval e c)%:P.

Lemma eval_Deriv e p : eval_poly e (Deriv p) = (eval_poly e p)^`.

Definition eval_OpPoly :=
  (eval_MulPoly, eval_AmulXn, eval_AddPoly, eval_OppPoly, eval_NatMulPoly,
  eval_ConstPoly, eval_Horner, eval_ExpPoly, eval_Deriv, eval_ScalPoly).

Lemma eval_Changes e s k : qf_eval e (Changes s k)
  = qf_eval e (k (changes (map (eval e) s))).

Lemma eval_SeqPInfty e ps k k' :
  ( xs, qf_eval e (k xs) = k' (map (eval e) xs)) →
 qf_eval e (SeqPInfty ps k)
  = k' (map lead_coef (map (eval_poly e) ps)).

Implicit Arguments eval_SeqPInfty [e ps k].

Lemma eval_SeqMInfty e ps k k' :
  ( xs, qf_eval e (k xs) = k' (map (eval e) xs)) →
 qf_eval e (SeqMInfty ps k)
  = k' (map (fun p : {poly F}(-1) ^+ (~~ odd (size p)) × lead_coef p)
            (map (eval_poly e) ps)).

Implicit Arguments eval_SeqMInfty [e ps k].

Lemma eval_ChangesPoly e ps k : qf_eval e (ChangesPoly ps k) =
  qf_eval e (k (changes_poly (map (eval_poly e) ps))).

Fixpoint redivp_rec_loop (q : {poly F}) sq cq
   (k : nat) (qq r : {poly F})(n : nat) {struct n} :=
    if (size r < sq)%N then (k, qq, r) else
    let m := (lead_coef r) *: 'X^(size r - sq) in
    let qq1 := qq × cq%:P + m in
    let r1 := r × cq%:P - m × q in
    if n is n1.+1 then redivp_rec_loop q sq cq k.+1 qq1 r1 n1 else (k.+1, qq1, r1).

Lemma redivp_rec_loopP q c qq r n : redivp_rec q c qq r n
    = redivp_rec_loop q (size q) (lead_coef q) c qq r n.

Lemma eval_Rediv_rec_loop e q sq cq c qq r n k k'
  (d := redivp_rec_loop (eval_poly e q) sq (eval e cq)
    c (eval_poly e qq) (eval_poly e r) n) :
  ( c qq r, qf_eval e (k (c, qq, r))
    = k' (c, eval_poly e qq, eval_poly e r)) →
  qf_eval e (Rediv_rec_loop q sq cq c qq r n k) = k' d.

Implicit Arguments eval_Rediv_rec_loop [e q sq cq c qq r n k].

Lemma eval_Rediv e p q k k' (d := (redivp (eval_poly e p) (eval_poly e q))) :
  ( c qq r, qf_eval e (k (c, qq, r)) = k' (c, eval_poly e qq, eval_poly e r)) →
  qf_eval e (Rediv p q k) = k' d.

Implicit Arguments eval_Rediv [e p q k].

Lemma eval_NextMod e p q k k' :
  ( p, qf_eval e (k p) = k' (eval_poly e p)) →
  qf_eval e (NextMod p q k) =
  k' (next_mod (eval_poly e p) (eval_poly e q)).

Implicit Arguments eval_NextMod [e p q k].

Lemma eval_Rgcd_loop e n p q k k' :
  ( p, qf_eval e (k p) = k' (eval_poly e p))
  → qf_eval e (Rgcd_loop n p q k) =
    k' (rgcdp_loop n (eval_poly e p) (eval_poly e q)).

Lemma eval_Rgcd e p q k k' :
  ( p, qf_eval e (k p) = k' (eval_poly e p)) →
  qf_eval e (Rgcd p q k) =
  k' (rgcdp (eval_poly e p) (eval_poly e q)).

Lemma eval_BigRgcd e ps k k' :
  ( p, qf_eval e (k p) = k' (eval_poly e p)) →
  qf_eval e (BigRgcd ps k) =
  k' (\big[@rgcdp _/0%:P]_(i <- ps) (eval_poly e i)).

Implicit Arguments eval_Rgcd [e p q k].

Fixpoint mods_aux (p q : {poly F}) (n : nat) : seq {poly F} :=
    if n is m.+1
      then if p == 0 then [::]
           else p :: (mods_aux q (next_mod p q) m)
      else [::].

Lemma eval_ModsAux e p q n k k' :
  ( sp, qf_eval e (k sp) = k' (map (eval_poly e) sp)) →
  qf_eval e (ModsAux p q n k) =
  k' (mods_aux (eval_poly e p) (eval_poly e q) n).

Implicit Arguments eval_ModsAux [e p q n k].

Lemma eval_Mods e p q k k' :
  ( sp, qf_eval e (k sp) = k' (map (eval_poly e) sp)) →
  qf_eval e (Mods p q k) = k' (mods (eval_poly e p) (eval_poly e q)).

Implicit Arguments eval_Mods [e p q k].

Lemma eval_TaqR e p q k :
  qf_eval e (TaqR p q k) =
  qf_eval e (k (taqR (eval_poly e p) (eval_poly e q))).

Lemma eval_PolyComb e sq sc :
  eval_poly e (PolyComb sq sc) = poly_comb (map (eval_poly e) sq) sc.

Definition pcq (sq : seq {poly F}) i :=
  (map (poly_comb sq) (sg_tab (size sq)))`_i.

Lemma eval_Pcq e sq i :
  eval_poly e (Pcq sq i) = pcq (map (eval_poly e) sq) i.

Lemma eval_TaqsR e p sq i k k' :
  ( x, qf_eval e (k x) = k' (eval e x)) →
  qf_eval e (TaqsR p sq i k) =
  k' (taqsR (eval_poly e p) (map (eval_poly e) sq) i).

Implicit Arguments eval_TaqsR [e p sq i k].

Fact invmx_ctmat1 : invmx (map_mx (intr : intF) ctmat1) =
  \matrix_(i, j)
  (nth [::] [:: [:: 2%:R^-1; - 2%:R^-1; 0];
                [:: 2%:R^-1; 2%:R^-1; -1];
                [:: 0; 0; 1]] i)`_j :> 'M[F]_3.

Lemma eval_Coefs e n i : eval e (Coefs F n i) = coefs F n i.

Lemma eval_CcountWeak e p sq k k' :
  ( x, qf_eval e (k x) = k' (eval e x)) →
  qf_eval e (CcountWeak p sq k) =
  k' (ccount_weak (eval_poly e p) (map (eval_poly e) sq)).

Implicit Arguments eval_CcountWeak [e p sq k].

Lemma eval_ProdPoly e T s f k f' k' :
  ( x k k', ( p, (qf_eval e (k p) = k' (eval_poly e p))) →
  qf_eval e (f x k) = k' (f' x)) →
  ( p, qf_eval e (k p) = k' (eval_poly e p)) →
  qf_eval e (@ProdPoly _ T s f k) = k' (\prod_(x <- s) f' x).

Implicit Arguments eval_ProdPoly [e T s f k].

Lemma eval_BoundingPoly e sq :
  eval_poly e (BoundingPoly sq) = bounding_poly (map (eval_poly e) sq).

Lemma eval_CcountGt0 e sp sq : qf_eval e (CcountGt0 sp sq) =
  ccount_gt0 (map (eval_poly e) sp) (map (eval_poly e) sq).

Lemma abstrXP e i t x :
  (eval_poly e (abstrX i t)).[x] = eval (set_nth 0 e i x) t.

Lemma wf_QE_wproj i bc (bc_i := @wproj F i bc) :
  dnf_rterm (w_to_oclause bc) → qf_form bc_i && rformula bc_i.

Lemma valid_QE_wproj i bc (bc' := w_to_oclause bc)
    (ex_i_bc := (' 'X_i, odnf_to_oform [:: bc'])%oT) e :
  dnf_rterm bc'reflect (holds e ex_i_bc) (ord.qf_eval e (wproj i bc)).

Lemma rcf_satP e f : reflect (holds e f) (rcf_sat e f).

End ProjCorrect.

Section Example. no chances it computes
Require Import rat.
Eval vm_compute in (54%:R / 289%:R + 2%:R^-1 :rat).
Local Open Scope qf_scope.
Notation polyF := (polyF [realFieldType of rat]). Definition p : polyF := [::'X_2; 'X_1; 'X_0]. Definition q : polyF := [:: 0; 1]. Definition sq := [::q].
Eval vm_compute in MulPoly p q.
Eval vm_compute in Rediv ( [:: 1] : polyF) [::1].
Definition fpq := Eval vm_compute in (CcountWeak p [::q]).
End Example.