Library mathcomp.field.closed_field
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ A proof that algebraically closed field enjoy quantifier elimination,
+ as described in
+ ``A formal quantifier elimination for algebraically closed fields'',
+ proceedings of Calculemus 2010, by Cyril Cohen and Assia Mahboubi
+
+
+
+ This file constructs an instance of quantifier elimination mixin,
+ (see the ssralg library) from the theory of polynomials with coefficients
+ is an algebraically closed field (see the polydiv library).
+
+
+
+ This file hence deals with the transformation of formulae part, which we
+ address by implementing one CPS style formula transformer per effective
+ operation involved in the proof of quantifier elimination. See the paper
+ for more details.
+
+
+
+
+Set Implicit Arguments.
+ +
+Import GRing.
+Local Open Scope ring_scope.
+ +
+Import Pdiv.Ring.
+Import PreClosedField.
+ +
+Section ClosedFieldQE.
+ +
+Variable F : Field.type.
+ +
+Variable axiom : ClosedField.axiom F.
+ +
+Notation fF := (formula F).
+Notation qf f := (qf_form f && rformula f).
+ +
+Definition polyF := seq (term F).
+ +
+Fixpoint eval_poly (e : seq F) pf :=
+ if pf is c::q then (eval_poly e q)*'X + (eval e c)%:P else 0.
+ +
+Definition rpoly (p : polyF) := all (@rterm F) p.
+ +
+Fixpoint sizeT (k : nat → fF) (p : polyF) :=
+ if p is c::q then
+ sizeT (fun n ⇒
+ if n is m.+1 then k m.+2 else
+ GRing.If (c == 0) (k 0%N) (k 1%N)) q
+ else k O%N.
+ +
+Lemma sizeTP (k : nat → formula F) (pf : polyF) (e : seq F) :
+ qf_eval e (sizeT k pf) = qf_eval e (k (size (eval_poly e pf))).
+ +
+Lemma sizeT_qf (k : nat → formula F) (p : polyF) :
+ (∀ n, qf (k n)) → rpoly p → qf (sizeT k p).
+ +
+Definition isnull (k : bool → fF) (p : polyF) :=
+ sizeT (fun n ⇒ k (n == 0%N)) p.
+ +
+Lemma isnullP (k : bool → formula F) (p : polyF) (e : seq F) :
+ qf_eval e (isnull k p) = qf_eval e (k (eval_poly e p == 0)).
+ +
+Lemma isnull_qf (k : bool → formula F) (p : polyF) :
+ (∀ b, qf (k b)) → rpoly p → qf (isnull k p).
+ +
+Definition lt_sizeT (k : bool → fF) (p q : polyF) : fF :=
+ sizeT (fun n ⇒ sizeT (fun m ⇒ k (n<m)) q) p.
+ +
+Definition lift (p : {poly F}) := let: q := p in map Const q.
+ +
+Lemma eval_lift (e : seq F) (p : {poly F}) : eval_poly e (lift p) = p.
+ +
+Fixpoint lead_coefT (k : term F → fF) p :=
+ if p is c::q then
+ lead_coefT (fun l ⇒ GRing.If (l == 0) (k c) (k l)) q
+ else k (Const 0).
+ +
+Lemma lead_coefTP (k : term F → formula F) :
+ (∀ x e, qf_eval e (k x) = qf_eval e (k (Const (eval e x)))) →
+ ∀ (p : polyF) (e : seq F),
+ qf_eval e (lead_coefT k p) = qf_eval e (k (Const (lead_coef (eval_poly e p)))).
+ +
+Lemma lead_coefT_qf (k : term F → formula F) (p : polyF) :
+ (∀ c, rterm c → qf (k c)) → rpoly p → qf (lead_coefT k p).
+ +
+Fixpoint amulXnT (a : term F) (n : nat) : polyF :=
+ if n is n'.+1 then (Const 0) :: (amulXnT a n') else [::a].
+ +
+Lemma eval_amulXnT (a : term F) (n : nat) (e : seq F) :
+ eval_poly e (amulXnT a n) = (eval e a)%:P × 'X^n.
+ +
+Lemma ramulXnT: ∀ a n, rterm a → rpoly (amulXnT a n).
+ +
+Fixpoint sumpT (p q : polyF) :=
+ if p is a::p' then
+ if q is b::q' then (Add a b)::(sumpT p' q')
+ else p
+ else q.
+ +
+Lemma eval_sumpT (p q : polyF) (e : seq F) :
+ eval_poly e (sumpT p q) = (eval_poly e p) + (eval_poly e q).
+ +
+Lemma rsumpT (p q : polyF) : rpoly p → rpoly q → rpoly (sumpT p q).
+ +
+Fixpoint mulpT (p q : polyF) :=
+ if p is a :: p' then sumpT (map (Mul a) q) (Const 0::(mulpT p' q)) else [::].
+ +
+Lemma eval_mulpT (p q : polyF) (e : seq F) :
+ eval_poly e (mulpT p q) = (eval_poly e p) × (eval_poly e q).
+ +
+Lemma rpoly_map_mul (t : term F) (p : polyF) (rt : rterm t) :
+ rpoly (map (Mul t) p) = rpoly p.
+ +
+Lemma rmulpT (p q : polyF) : rpoly p → rpoly q → rpoly (mulpT p q).
+ +
+Definition opppT := map (Mul (@Const F (-1))).
+ +
+Lemma eval_opppT (p : polyF) (e : seq F) :
+ eval_poly e (opppT p) = - eval_poly e p.
+ +
+Definition natmulpT n := map (Mul (@NatConst F n)).
+ +
+Lemma eval_natmulpT (p : polyF) (n : nat) (e : seq F) :
+ eval_poly e (natmulpT n p) = (eval_poly e p) *+ n.
+ +
+Fixpoint redivp_rec_loopT (q : polyF) sq cq (k : nat × polyF × polyF → fF)
+ (c : nat) (qq r : polyF) (n : nat) {struct n}:=
+ sizeT (fun sr ⇒
+ if sr < sq then k (c, qq, r) else
+ lead_coefT (fun lr ⇒
+ let m := amulXnT lr (sr - sq) in
+ let qq1 := sumpT (mulpT qq [::cq]) m in
+ let r1 := sumpT (mulpT r ([::cq])) (opppT (mulpT m q)) in
+ if n is n1.+1 then redivp_rec_loopT q sq cq k c.+1 qq1 r1 n1
+ else k (c.+1, qq1, r1)
+ ) r
+ ) r.
+ +
+Fixpoint redivp_rec_loop (q : {poly F}) sq cq
+ (k : nat) (qq r : {poly F})(n : nat) {struct n} :=
+ if size r < sq 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_loopTP (k : nat × polyF × polyF → formula F) :
+ (∀ c qq r e, qf_eval e (k (c,qq,r))
+ = qf_eval e (k (c, lift (eval_poly e qq), lift (eval_poly e r))))
+ → ∀ q sq cq c qq r n e
+ (d := redivp_rec_loop (eval_poly e q) sq (eval e cq)
+ c (eval_poly e qq) (eval_poly e r) n),
+ qf_eval e (redivp_rec_loopT q sq cq k c qq r n)
+ = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)).
+ +
+Lemma redivp_rec_loopT_qf (q : polyF) (sq : nat) (cq : term F)
+ (k : nat × polyF × polyF → formula F) (c : nat) (qq r : polyF) (n : nat) :
+ (∀ r, [&& rpoly r.1.2 & rpoly r.2] → qf (k r)) →
+ rpoly q → rterm cq → rpoly qq → rpoly r →
+ qf (redivp_rec_loopT q sq cq k c qq r n).
+ +
+Definition redivpT (p : polyF) (k : nat × polyF × polyF → fF)
+ (q : polyF) : fF :=
+ isnull (fun b ⇒
+ if b then k (0%N, [::Const 0], p) else
+ sizeT (fun sq ⇒
+ sizeT (fun sp ⇒
+ lead_coefT (fun lq ⇒
+ redivp_rec_loopT q sq lq k 0 [::Const 0] p sp
+ ) q
+ ) p
+ ) q
+ ) q.
+ +
+Lemma redivp_rec_loopP (q : {poly F}) (c : nat) (qq r : {poly F}) (n : nat) :
+ redivp_rec q c qq r n = redivp_rec_loop q (size q) (lead_coef q) c qq r n.
+ +
+Lemma redivpTP (k : nat × polyF × polyF → formula F) :
+ (∀ c qq r e,
+ qf_eval e (k (c,qq,r)) =
+ qf_eval e (k (c, lift (eval_poly e qq), lift (eval_poly e r)))) →
+ ∀ p q e (d := redivp (eval_poly e p) (eval_poly e q)),
+ qf_eval e (redivpT p k q) = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)).
+ +
+Lemma redivpT_qf (p : polyF) (k : nat × polyF × polyF → formula F) (q : polyF) :
+ (∀ r, [&& rpoly r.1.2 & rpoly r.2] → qf (k r)) →
+ rpoly p → rpoly q → qf (redivpT p k q).
+ +
+Definition rmodpT (p : polyF) (k : polyF → fF) (q : polyF) : fF :=
+ redivpT p (fun d ⇒ k d.2) q.
+Definition rdivpT (p : polyF) (k:polyF → fF) (q : polyF) : fF :=
+ redivpT p (fun d ⇒ k d.1.2) q.
+Definition rscalpT (p : polyF) (k: nat → fF) (q : polyF) : fF :=
+ redivpT p (fun d ⇒ k d.1.1) q.
+Definition rdvdpT (p : polyF) (k:bool → fF) (q : polyF) : fF :=
+ rmodpT p (isnull k) q.
+ +
+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 rgcdp_loopT (pp : polyF) (k : polyF → formula F) n (qq : polyF) :=
+ rmodpT pp (isnull
+ (fun b ⇒ if b then (k qq)
+ else (if n is n1.+1
+ then rmodpT pp (rgcdp_loopT qq k n1) qq
+ else rmodpT pp k qq)
+ )
+ ) qq.
+ +
+Lemma rgcdp_loopP (k : polyF → formula F) :
+ (∀ p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
+ ∀ n p q e,
+ qf_eval e (rgcdp_loopT p k n q) =
+ qf_eval e (k (lift (rgcdp_loop n (eval_poly e p) (eval_poly e q)))).
+ +
+Lemma rgcdp_loopT_qf (p : polyF) (k : polyF → formula F) (q : polyF) (n : nat) :
+ (∀ r, rpoly r → qf (k r)) →
+ rpoly p → rpoly q → qf (rgcdp_loopT p k n q).
+ +
+Definition rgcdpT (p : polyF) k (q : polyF) : fF :=
+ let aux p1 k q1 := isnull
+ (fun b ⇒ if b
+ then (k q1)
+ else (sizeT (fun n ⇒ (rgcdp_loopT p1 k n q1)) p1)) p1
+ in (lt_sizeT (fun b ⇒ if b then (aux q k p) else (aux p k q)) p q).
+ +
+Lemma rgcdpTP (k : seq (term F) → formula F) :
+ (∀ p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
+ ∀ p q e, qf_eval e (rgcdpT p k q) =
+ qf_eval e (k (lift (rgcdp (eval_poly e p) (eval_poly e q)))).
+ +
+Lemma rgcdpT_qf (p : polyF) (k : polyF → formula F) (q : polyF) :
+ (∀ r, rpoly r → qf (k r)) → rpoly p → rpoly q → qf (rgcdpT p k q).
+ +
+Fixpoint rgcdpTs k (ps : seq polyF) : fF :=
+ if ps is p::pr then rgcdpTs (rgcdpT p k) pr else k [::Const 0].
+ +
+Lemma rgcdpTsP (k : polyF → formula F) :
+ (∀ p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
+ ∀ ps e,
+ qf_eval e (rgcdpTs k ps) =
+ qf_eval e (k (lift (\big[@rgcdp _/0%:P]_(i <- ps)(eval_poly e i)))).
+ +
+Definition rseq_poly ps := all rpoly ps.
+ +
+Lemma rgcdpTs_qf (k : polyF → formula F) (ps : seq polyF) :
+ (∀ r, rpoly r → qf (k r)) → rseq_poly ps → qf (rgcdpTs k ps).
+ +
+Fixpoint rgdcop_recT (q : polyF) k (p : polyF) n :=
+ if n is m.+1 then
+ rgcdpT p (sizeT (fun sd ⇒
+ if sd == 1%N then k p
+ else rgcdpT p (rdivpT p (fun r ⇒ rgdcop_recT q k r m)) q
+ )) q
+ else isnull (fun b ⇒ k [::Const b%:R]) q.
+ +
+Lemma rgdcop_recTP (k : polyF → formula F) :
+ (∀ p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p))))
+ → ∀ p q n e, qf_eval e (rgdcop_recT p k q n)
+ = qf_eval e (k (lift (rgdcop_rec (eval_poly e p) (eval_poly e q) n))).
+ +
+Lemma rgdcop_recT_qf (p : polyF) (k : polyF → formula F) (q : polyF) (n : nat) :
+ (∀ r, rpoly r → qf (k r)) →
+ rpoly p → rpoly q → qf (rgdcop_recT p k q n).
+ +
+Definition rgdcopT q k p := sizeT (rgdcop_recT q k p) p.
+ +
+Lemma rgdcopTP (k : polyF → formula F) :
+ (∀ p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
+ ∀ p q e, qf_eval e (rgdcopT p k q) =
+ qf_eval e (k (lift (rgdcop (eval_poly e p) (eval_poly e q)))).
+ +
+Lemma rgdcopT_qf (p : polyF) (k : polyF → formula F) (q : polyF) :
+ (∀ r, rpoly r → qf (k r)) → rpoly p → rpoly q → qf (rgdcopT p k q).
+ +
+Definition ex_elim_seq (ps : seq polyF) (q : polyF) :=
+ (rgcdpTs (rgdcopT q (sizeT (fun n ⇒ Bool (n != 1%N)))) ps).
+ +
+Lemma ex_elim_seqP (ps : seq polyF) (q : polyF) (e : seq F) :
+ let gp := (\big[@rgcdp _/0%:P]_(p <- ps)(eval_poly e p)) in
+ qf_eval e (ex_elim_seq ps q) = (size (rgdcop (eval_poly e q) gp) != 1%N).
+ +
+Lemma ex_elim_seq_qf (ps : seq polyF) (q : polyF) :
+ rseq_poly ps → rpoly q → qf (ex_elim_seq ps q).
+ +
+Fixpoint abstrX (i : nat) (t : term F) :=
+ match t with
+ | (Var n) ⇒ if n == i then [::Const 0; Const 1] else [::t]
+ | (Opp x) ⇒ opppT (abstrX i x)
+ | (Add x y) ⇒ sumpT (abstrX i x) (abstrX i y)
+ | (Mul x y) ⇒ mulpT (abstrX i x) (abstrX i y)
+ | (NatMul x n) ⇒ natmulpT n (abstrX i x)
+ | (Exp x n) ⇒ let ax := (abstrX i x) in
+ iter n (mulpT ax) [::Const 1]
+ | _ ⇒ [::t]
+ end.
+ +
+Lemma abstrXP (i : nat) (t : term F) (e : seq F) (x : F) :
+ rterm t → (eval_poly e (abstrX i t)).[x] = eval (set_nth 0 e i x) t.
+ +
+Lemma rabstrX (i : nat) (t : term F) : rterm t → rpoly (abstrX i t).
+ +
+Implicit Types tx ty : term F.
+ +
+Lemma abstrX_mulM (i : nat) : {morph abstrX i : x y / Mul x y >-> mulpT x y}.
+ +
+Lemma abstrX1 (i : nat) : abstrX i (Const 1) = [::Const 1].
+ +
+Lemma eval_poly_mulM e : {morph eval_poly e : x y / mulpT x y >-> mul x y}.
+ +
+Lemma eval_poly1 e : eval_poly e [::Const 1] = 1.
+ +
+Notation abstrX_bigmul := (big_morph _ (abstrX_mulM _) (abstrX1 _)).
+Notation eval_bigmul := (big_morph _ (eval_poly_mulM _) (eval_poly1 _)).
+Notation bigmap_id := (big_map _ (fun _ ⇒ true) id).
+ +
+Lemma rseq_poly_map (x : nat) (ts : seq (term F)) :
+ all (@rterm _) ts → rseq_poly (map (abstrX x) ts).
+ +
+Definition ex_elim (x : nat) (pqs : seq (term F) × seq (term F)) :=
+ ex_elim_seq (map (abstrX x) pqs.1)
+ (abstrX x (\big[Mul/Const 1]_(q <- pqs.2) q)).
+ +
+Lemma ex_elim_qf (x : nat) (pqs : seq (term F) × seq (term F)) :
+ dnf_rterm pqs → qf (ex_elim x pqs).
+ +
+Lemma holds_conj : ∀ e i x ps, all (@rterm _) ps →
+ (holds (set_nth 0 e i x) (foldr (fun t : term F ⇒ And (t == 0)) True ps)
+ ↔ all ((@root _)^~ x) (map (eval_poly e \o abstrX i) ps)).
+ +
+Lemma holds_conjn (e : seq F) (i : nat) (x : F) (ps : seq (term F)) :
+ all (@rterm _) ps →
+ (holds (set_nth 0 e i x) (foldr (fun t : term F ⇒ And (t != 0)) True ps) ↔
+ all (fun p ⇒ ~~root p x) (map (eval_poly e \o abstrX i) ps)).
+ +
+Lemma holds_ex_elim: GRing.valid_QE_proj ex_elim.
+ +
+Lemma wf_ex_elim : GRing.wf_QE_proj ex_elim.
+ +
+Definition closed_fields_QEMixin :=
+ QEdecFieldMixin wf_ex_elim holds_ex_elim.
+ +
+End ClosedFieldQE.
+
++Set Implicit Arguments.
+ +
+Import GRing.
+Local Open Scope ring_scope.
+ +
+Import Pdiv.Ring.
+Import PreClosedField.
+ +
+Section ClosedFieldQE.
+ +
+Variable F : Field.type.
+ +
+Variable axiom : ClosedField.axiom F.
+ +
+Notation fF := (formula F).
+Notation qf f := (qf_form f && rformula f).
+ +
+Definition polyF := seq (term F).
+ +
+Fixpoint eval_poly (e : seq F) pf :=
+ if pf is c::q then (eval_poly e q)*'X + (eval e c)%:P else 0.
+ +
+Definition rpoly (p : polyF) := all (@rterm F) p.
+ +
+Fixpoint sizeT (k : nat → fF) (p : polyF) :=
+ if p is c::q then
+ sizeT (fun n ⇒
+ if n is m.+1 then k m.+2 else
+ GRing.If (c == 0) (k 0%N) (k 1%N)) q
+ else k O%N.
+ +
+Lemma sizeTP (k : nat → formula F) (pf : polyF) (e : seq F) :
+ qf_eval e (sizeT k pf) = qf_eval e (k (size (eval_poly e pf))).
+ +
+Lemma sizeT_qf (k : nat → formula F) (p : polyF) :
+ (∀ n, qf (k n)) → rpoly p → qf (sizeT k p).
+ +
+Definition isnull (k : bool → fF) (p : polyF) :=
+ sizeT (fun n ⇒ k (n == 0%N)) p.
+ +
+Lemma isnullP (k : bool → formula F) (p : polyF) (e : seq F) :
+ qf_eval e (isnull k p) = qf_eval e (k (eval_poly e p == 0)).
+ +
+Lemma isnull_qf (k : bool → formula F) (p : polyF) :
+ (∀ b, qf (k b)) → rpoly p → qf (isnull k p).
+ +
+Definition lt_sizeT (k : bool → fF) (p q : polyF) : fF :=
+ sizeT (fun n ⇒ sizeT (fun m ⇒ k (n<m)) q) p.
+ +
+Definition lift (p : {poly F}) := let: q := p in map Const q.
+ +
+Lemma eval_lift (e : seq F) (p : {poly F}) : eval_poly e (lift p) = p.
+ +
+Fixpoint lead_coefT (k : term F → fF) p :=
+ if p is c::q then
+ lead_coefT (fun l ⇒ GRing.If (l == 0) (k c) (k l)) q
+ else k (Const 0).
+ +
+Lemma lead_coefTP (k : term F → formula F) :
+ (∀ x e, qf_eval e (k x) = qf_eval e (k (Const (eval e x)))) →
+ ∀ (p : polyF) (e : seq F),
+ qf_eval e (lead_coefT k p) = qf_eval e (k (Const (lead_coef (eval_poly e p)))).
+ +
+Lemma lead_coefT_qf (k : term F → formula F) (p : polyF) :
+ (∀ c, rterm c → qf (k c)) → rpoly p → qf (lead_coefT k p).
+ +
+Fixpoint amulXnT (a : term F) (n : nat) : polyF :=
+ if n is n'.+1 then (Const 0) :: (amulXnT a n') else [::a].
+ +
+Lemma eval_amulXnT (a : term F) (n : nat) (e : seq F) :
+ eval_poly e (amulXnT a n) = (eval e a)%:P × 'X^n.
+ +
+Lemma ramulXnT: ∀ a n, rterm a → rpoly (amulXnT a n).
+ +
+Fixpoint sumpT (p q : polyF) :=
+ if p is a::p' then
+ if q is b::q' then (Add a b)::(sumpT p' q')
+ else p
+ else q.
+ +
+Lemma eval_sumpT (p q : polyF) (e : seq F) :
+ eval_poly e (sumpT p q) = (eval_poly e p) + (eval_poly e q).
+ +
+Lemma rsumpT (p q : polyF) : rpoly p → rpoly q → rpoly (sumpT p q).
+ +
+Fixpoint mulpT (p q : polyF) :=
+ if p is a :: p' then sumpT (map (Mul a) q) (Const 0::(mulpT p' q)) else [::].
+ +
+Lemma eval_mulpT (p q : polyF) (e : seq F) :
+ eval_poly e (mulpT p q) = (eval_poly e p) × (eval_poly e q).
+ +
+Lemma rpoly_map_mul (t : term F) (p : polyF) (rt : rterm t) :
+ rpoly (map (Mul t) p) = rpoly p.
+ +
+Lemma rmulpT (p q : polyF) : rpoly p → rpoly q → rpoly (mulpT p q).
+ +
+Definition opppT := map (Mul (@Const F (-1))).
+ +
+Lemma eval_opppT (p : polyF) (e : seq F) :
+ eval_poly e (opppT p) = - eval_poly e p.
+ +
+Definition natmulpT n := map (Mul (@NatConst F n)).
+ +
+Lemma eval_natmulpT (p : polyF) (n : nat) (e : seq F) :
+ eval_poly e (natmulpT n p) = (eval_poly e p) *+ n.
+ +
+Fixpoint redivp_rec_loopT (q : polyF) sq cq (k : nat × polyF × polyF → fF)
+ (c : nat) (qq r : polyF) (n : nat) {struct n}:=
+ sizeT (fun sr ⇒
+ if sr < sq then k (c, qq, r) else
+ lead_coefT (fun lr ⇒
+ let m := amulXnT lr (sr - sq) in
+ let qq1 := sumpT (mulpT qq [::cq]) m in
+ let r1 := sumpT (mulpT r ([::cq])) (opppT (mulpT m q)) in
+ if n is n1.+1 then redivp_rec_loopT q sq cq k c.+1 qq1 r1 n1
+ else k (c.+1, qq1, r1)
+ ) r
+ ) r.
+ +
+Fixpoint redivp_rec_loop (q : {poly F}) sq cq
+ (k : nat) (qq r : {poly F})(n : nat) {struct n} :=
+ if size r < sq 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_loopTP (k : nat × polyF × polyF → formula F) :
+ (∀ c qq r e, qf_eval e (k (c,qq,r))
+ = qf_eval e (k (c, lift (eval_poly e qq), lift (eval_poly e r))))
+ → ∀ q sq cq c qq r n e
+ (d := redivp_rec_loop (eval_poly e q) sq (eval e cq)
+ c (eval_poly e qq) (eval_poly e r) n),
+ qf_eval e (redivp_rec_loopT q sq cq k c qq r n)
+ = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)).
+ +
+Lemma redivp_rec_loopT_qf (q : polyF) (sq : nat) (cq : term F)
+ (k : nat × polyF × polyF → formula F) (c : nat) (qq r : polyF) (n : nat) :
+ (∀ r, [&& rpoly r.1.2 & rpoly r.2] → qf (k r)) →
+ rpoly q → rterm cq → rpoly qq → rpoly r →
+ qf (redivp_rec_loopT q sq cq k c qq r n).
+ +
+Definition redivpT (p : polyF) (k : nat × polyF × polyF → fF)
+ (q : polyF) : fF :=
+ isnull (fun b ⇒
+ if b then k (0%N, [::Const 0], p) else
+ sizeT (fun sq ⇒
+ sizeT (fun sp ⇒
+ lead_coefT (fun lq ⇒
+ redivp_rec_loopT q sq lq k 0 [::Const 0] p sp
+ ) q
+ ) p
+ ) q
+ ) q.
+ +
+Lemma redivp_rec_loopP (q : {poly F}) (c : nat) (qq r : {poly F}) (n : nat) :
+ redivp_rec q c qq r n = redivp_rec_loop q (size q) (lead_coef q) c qq r n.
+ +
+Lemma redivpTP (k : nat × polyF × polyF → formula F) :
+ (∀ c qq r e,
+ qf_eval e (k (c,qq,r)) =
+ qf_eval e (k (c, lift (eval_poly e qq), lift (eval_poly e r)))) →
+ ∀ p q e (d := redivp (eval_poly e p) (eval_poly e q)),
+ qf_eval e (redivpT p k q) = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)).
+ +
+Lemma redivpT_qf (p : polyF) (k : nat × polyF × polyF → formula F) (q : polyF) :
+ (∀ r, [&& rpoly r.1.2 & rpoly r.2] → qf (k r)) →
+ rpoly p → rpoly q → qf (redivpT p k q).
+ +
+Definition rmodpT (p : polyF) (k : polyF → fF) (q : polyF) : fF :=
+ redivpT p (fun d ⇒ k d.2) q.
+Definition rdivpT (p : polyF) (k:polyF → fF) (q : polyF) : fF :=
+ redivpT p (fun d ⇒ k d.1.2) q.
+Definition rscalpT (p : polyF) (k: nat → fF) (q : polyF) : fF :=
+ redivpT p (fun d ⇒ k d.1.1) q.
+Definition rdvdpT (p : polyF) (k:bool → fF) (q : polyF) : fF :=
+ rmodpT p (isnull k) q.
+ +
+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 rgcdp_loopT (pp : polyF) (k : polyF → formula F) n (qq : polyF) :=
+ rmodpT pp (isnull
+ (fun b ⇒ if b then (k qq)
+ else (if n is n1.+1
+ then rmodpT pp (rgcdp_loopT qq k n1) qq
+ else rmodpT pp k qq)
+ )
+ ) qq.
+ +
+Lemma rgcdp_loopP (k : polyF → formula F) :
+ (∀ p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
+ ∀ n p q e,
+ qf_eval e (rgcdp_loopT p k n q) =
+ qf_eval e (k (lift (rgcdp_loop n (eval_poly e p) (eval_poly e q)))).
+ +
+Lemma rgcdp_loopT_qf (p : polyF) (k : polyF → formula F) (q : polyF) (n : nat) :
+ (∀ r, rpoly r → qf (k r)) →
+ rpoly p → rpoly q → qf (rgcdp_loopT p k n q).
+ +
+Definition rgcdpT (p : polyF) k (q : polyF) : fF :=
+ let aux p1 k q1 := isnull
+ (fun b ⇒ if b
+ then (k q1)
+ else (sizeT (fun n ⇒ (rgcdp_loopT p1 k n q1)) p1)) p1
+ in (lt_sizeT (fun b ⇒ if b then (aux q k p) else (aux p k q)) p q).
+ +
+Lemma rgcdpTP (k : seq (term F) → formula F) :
+ (∀ p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
+ ∀ p q e, qf_eval e (rgcdpT p k q) =
+ qf_eval e (k (lift (rgcdp (eval_poly e p) (eval_poly e q)))).
+ +
+Lemma rgcdpT_qf (p : polyF) (k : polyF → formula F) (q : polyF) :
+ (∀ r, rpoly r → qf (k r)) → rpoly p → rpoly q → qf (rgcdpT p k q).
+ +
+Fixpoint rgcdpTs k (ps : seq polyF) : fF :=
+ if ps is p::pr then rgcdpTs (rgcdpT p k) pr else k [::Const 0].
+ +
+Lemma rgcdpTsP (k : polyF → formula F) :
+ (∀ p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
+ ∀ ps e,
+ qf_eval e (rgcdpTs k ps) =
+ qf_eval e (k (lift (\big[@rgcdp _/0%:P]_(i <- ps)(eval_poly e i)))).
+ +
+Definition rseq_poly ps := all rpoly ps.
+ +
+Lemma rgcdpTs_qf (k : polyF → formula F) (ps : seq polyF) :
+ (∀ r, rpoly r → qf (k r)) → rseq_poly ps → qf (rgcdpTs k ps).
+ +
+Fixpoint rgdcop_recT (q : polyF) k (p : polyF) n :=
+ if n is m.+1 then
+ rgcdpT p (sizeT (fun sd ⇒
+ if sd == 1%N then k p
+ else rgcdpT p (rdivpT p (fun r ⇒ rgdcop_recT q k r m)) q
+ )) q
+ else isnull (fun b ⇒ k [::Const b%:R]) q.
+ +
+Lemma rgdcop_recTP (k : polyF → formula F) :
+ (∀ p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p))))
+ → ∀ p q n e, qf_eval e (rgdcop_recT p k q n)
+ = qf_eval e (k (lift (rgdcop_rec (eval_poly e p) (eval_poly e q) n))).
+ +
+Lemma rgdcop_recT_qf (p : polyF) (k : polyF → formula F) (q : polyF) (n : nat) :
+ (∀ r, rpoly r → qf (k r)) →
+ rpoly p → rpoly q → qf (rgdcop_recT p k q n).
+ +
+Definition rgdcopT q k p := sizeT (rgdcop_recT q k p) p.
+ +
+Lemma rgdcopTP (k : polyF → formula F) :
+ (∀ p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
+ ∀ p q e, qf_eval e (rgdcopT p k q) =
+ qf_eval e (k (lift (rgdcop (eval_poly e p) (eval_poly e q)))).
+ +
+Lemma rgdcopT_qf (p : polyF) (k : polyF → formula F) (q : polyF) :
+ (∀ r, rpoly r → qf (k r)) → rpoly p → rpoly q → qf (rgdcopT p k q).
+ +
+Definition ex_elim_seq (ps : seq polyF) (q : polyF) :=
+ (rgcdpTs (rgdcopT q (sizeT (fun n ⇒ Bool (n != 1%N)))) ps).
+ +
+Lemma ex_elim_seqP (ps : seq polyF) (q : polyF) (e : seq F) :
+ let gp := (\big[@rgcdp _/0%:P]_(p <- ps)(eval_poly e p)) in
+ qf_eval e (ex_elim_seq ps q) = (size (rgdcop (eval_poly e q) gp) != 1%N).
+ +
+Lemma ex_elim_seq_qf (ps : seq polyF) (q : polyF) :
+ rseq_poly ps → rpoly q → qf (ex_elim_seq ps q).
+ +
+Fixpoint abstrX (i : nat) (t : term F) :=
+ match t with
+ | (Var n) ⇒ if n == i then [::Const 0; Const 1] else [::t]
+ | (Opp x) ⇒ opppT (abstrX i x)
+ | (Add x y) ⇒ sumpT (abstrX i x) (abstrX i y)
+ | (Mul x y) ⇒ mulpT (abstrX i x) (abstrX i y)
+ | (NatMul x n) ⇒ natmulpT n (abstrX i x)
+ | (Exp x n) ⇒ let ax := (abstrX i x) in
+ iter n (mulpT ax) [::Const 1]
+ | _ ⇒ [::t]
+ end.
+ +
+Lemma abstrXP (i : nat) (t : term F) (e : seq F) (x : F) :
+ rterm t → (eval_poly e (abstrX i t)).[x] = eval (set_nth 0 e i x) t.
+ +
+Lemma rabstrX (i : nat) (t : term F) : rterm t → rpoly (abstrX i t).
+ +
+Implicit Types tx ty : term F.
+ +
+Lemma abstrX_mulM (i : nat) : {morph abstrX i : x y / Mul x y >-> mulpT x y}.
+ +
+Lemma abstrX1 (i : nat) : abstrX i (Const 1) = [::Const 1].
+ +
+Lemma eval_poly_mulM e : {morph eval_poly e : x y / mulpT x y >-> mul x y}.
+ +
+Lemma eval_poly1 e : eval_poly e [::Const 1] = 1.
+ +
+Notation abstrX_bigmul := (big_morph _ (abstrX_mulM _) (abstrX1 _)).
+Notation eval_bigmul := (big_morph _ (eval_poly_mulM _) (eval_poly1 _)).
+Notation bigmap_id := (big_map _ (fun _ ⇒ true) id).
+ +
+Lemma rseq_poly_map (x : nat) (ts : seq (term F)) :
+ all (@rterm _) ts → rseq_poly (map (abstrX x) ts).
+ +
+Definition ex_elim (x : nat) (pqs : seq (term F) × seq (term F)) :=
+ ex_elim_seq (map (abstrX x) pqs.1)
+ (abstrX x (\big[Mul/Const 1]_(q <- pqs.2) q)).
+ +
+Lemma ex_elim_qf (x : nat) (pqs : seq (term F) × seq (term F)) :
+ dnf_rterm pqs → qf (ex_elim x pqs).
+ +
+Lemma holds_conj : ∀ e i x ps, all (@rterm _) ps →
+ (holds (set_nth 0 e i x) (foldr (fun t : term F ⇒ And (t == 0)) True ps)
+ ↔ all ((@root _)^~ x) (map (eval_poly e \o abstrX i) ps)).
+ +
+Lemma holds_conjn (e : seq F) (i : nat) (x : F) (ps : seq (term F)) :
+ all (@rterm _) ps →
+ (holds (set_nth 0 e i x) (foldr (fun t : term F ⇒ And (t != 0)) True ps) ↔
+ all (fun p ⇒ ~~root p x) (map (eval_poly e \o abstrX i) ps)).
+ +
+Lemma holds_ex_elim: GRing.valid_QE_proj ex_elim.
+ +
+Lemma wf_ex_elim : GRing.wf_QE_proj ex_elim.
+ +
+Definition closed_fields_QEMixin :=
+ QEdecFieldMixin wf_ex_elim holds_ex_elim.
+ +
+End ClosedFieldQE.
+