wip

cylinder.v

@@ -1,51 +1,132 @@
-From mathcomp Require Import ssreflect ssrfun ssrbool eqtype seq ssrnat bigop tuple fintype finfun path ssralg ssrnum matrix finmap.
+From mathcomp Require Import freeg ssreflect ssrfun ssrbool eqtype choice seq ssrnat bigop tuple fintype finfun path ssralg ssrnum poly matrix finmap mpoly complex.
 Require Import semialgebraic.
 (* TODO: the following imports should not be needed after cleanup. *)
 From mathcomp Require Import generic_quotient.
-Require Import formula.
+Require Import formula subresultant.
 
 Local Open Scope fset_scope.
 Local Open Scope fmap_scope.
 Local Open Scope type_scope.
+Local Open Scope sa_scope.
 
-Section SApartition.
-Variables (R : rcfType) (n : nat).
+Import GRing.
 
-Definition SAset_disjoint (s1 s2 : {SAset R^n}) :=
-  SAset_meet s1 s2 == SAset0 R n.
+Section SAfun0.
+Variables (R : rcfType) (n m : nat).
 
-Definition SAset_trivI (I : {fset {SAset R^n}}) :=
-  [forall s1 : I, [forall s2 : I, (val s1 != val s2) ==> SAset_disjoint (val s1) (val s2)]].
 
-Definition SAset_partition (I : {fset {SAset R^n}}) :=
-  (SAset0 R n \notin I) && SAset_trivI I && (\big[@SAset_join R n/SAset0 R n]_(s : I) val s == SAset0 R n).
+End SAfun0.
 
-End SApartition.
+Section SApartition.
+Variables (R : rcfType) (n : nat).
 
-Definition SAset_cast {R : rcfType} {n m : nat} (s : {SAset R^n}) :
-  n = m -> {SAset R^m}.
-by move=> <-.
-Defined.
 
-Section CylindricalDecomposition.
-Variables (R : rcfType) (n : nat).
+End SApartition.
 
-Fact lift0' {k} (i : 'I_k) : (lift ord0 i = i + 1 :> nat)%N.
-Proof. by rewrite lift0 addn1. Qed.
+Section CylindricalDecomposition.
+Variables (R : rcfType).
 
-Definition isCylindricalDecomposition (S : forall i : 'I_n.+1, {fset {SAset R^i}}) :=
+Definition isCylindricalDecomposition n (S : forall i : 'I_n.+1, {fset {SAset R^i}}) :=
   (forall i : 'I_n.+1, SAset_partition R i (S i))
   /\ forall (i : 'I_n) (s : S (lift ord_max i)),
-    exists m, exists xi : m.-tuple {SAfun R^i -> R^1},
-      sorted (@SAfun_lt R i) xi
-      /\ forall s' : S (lift ord0 i),
-        (exists k : 'I_m, SAset_cast (val s') (lift0' i) == SAset_meet (SAgraph (tnth xi k)) (SAset_prod (SAset_cast (val s) (lift_max i)) (@SAset_top R 1)))
-        \/ (exists k : 'I_m, exists km : k.+1 < m,
-          forall (x : 'rV[R]_i) (y : 'rV[R]_1),
-            (row_mx x y \in SAset_cast (val s') (lift0' i)) = (x \in SAset_cast (val s) (lift_max i)) && (tnth xi k x ord0 ord0 < y ord0 ord0)%R && (y ord0 ord0 < tnth xi (Ordinal km) x ord0 ord0)%R)
-        \/ (forall (x : 'rV[R]_i) (y : 'rV[R]_1),
-             (row_mx x y \in SAset_cast (val s') (lift0' i)) = (x \in SAset_cast (val s) (lift_max i)) && [forall k : 'I_m, y ord0 ord0 < tnth xi k x ord0 ord0])%R
-        \/ (forall (x : 'rV[R]_i) (y : 'rV[R]_1),
-             (row_mx x y \in SAset_cast (val s') (lift0' i)) = (x \in SAset_cast (val s) (lift_max i)) && [forall k : 'I_m, tnth xi k x ord0 ord0 < y ord0 ord0])%R.
+    exists m, exists xi : m.-tuple {SAfun R^(lift ord_max i) -> R^1},
+      sorted (@SAfun_lt _ _) xi
+      /\ [fset s' in S (lift ord0 i) | SAset_cast _ s' == val s] = [fset SAset_cast i.+1 x | x in partition_of_graphs_above R _ (val s) m xi].
+
+Local Notation isCD := isCylindricalDecomposition.
+
+Lemma bool_eq_arrow {b b' : bool} : b = b' -> b -> b'.
+Proof. by case: b' => // /negP. Qed.
+
+Lemma isCylindricalDecomposition_restrict n m S (mn : m <= n) : isCD n S -> isCD m (fun i => S (widen_ord (bool_eq_arrow (esym (ltnS m n)) mn) i)).
+Proof.
+move=> [] Spart Scyl; split => [i|i s].
+  exact/(Spart ((widen_ord (m:=n.+1) (bool_eq_arrow (esym (ltnS m n)) mn) i))).
+move/(_ (widen_ord mn i)) : Scyl.
+have ->: lift ord_max (widen_ord mn i) = widen_ord (bool_eq_arrow (esym (ltnS m n)) mn) (lift ord_max i).
+  by apply/val_inj; rewrite /= /bump leqNgt (leq_trans (ltn_ord i) mn) leqNgt ltn_ord.
+move=> /(_ s) [k][xi][xisort] /= partE.
+exists k, xi; split; first by [].
+rewrite -partE.
+congr [fset _ in _ | _]; congr (mem_fin (fset_finpred (S (Ordinal _)))).
+exact/bool_irrelevance.
+Qed.
+
+Definition poly_invariant n (p : {mpoly R[n]}) (s : {SAset R^n}) :=
+  {in s &, forall x y, let x := meval (tnth (ngraph x)) p in let y := meval (tnth (ngraph y)) p in (x / `|x| = y / `|y|)%R}.
+
+Definition poly_adapted n p (S : forall i : 'I_n.+1, {fset {SAset R^i}}) := forall s : S ord_max, poly_invariant n p (val s).
+
+Definition truncate (T : ringType) (p : {poly T}) (d : nat) :=
+  (\poly_(i < size p) (p`_i *+ (i < d)%N))%R.
+
+Definition truncations n (p : {poly {mpoly R[n]}}) : {fset {poly {mpoly R[n]}}} :=
+  (fix F p n :=
+    match n with
+    | 0 => [fset p]
+    | n.+1 => if 0 < mdeg (mlead (lead_coef p)) then
+        p |` F (truncate _ p (size p).-1) n
+      else [fset p]
+    end) p (size p).
+
+Definition elim_subdef0 n (P : {fset {poly {mpoly R[n]}}}) :=
+  \big[fsetU/fset0]_(p : P) \big[fsetU/fset0]_(r : truncations n (val p))
+    (lead_coef (val r) |` [fset subresultant (val j) (val r) (val r)^`() | j in 'I_(size (val r)).-2]).
+
+Definition elim_subdef1 n (P : {fset {poly {mpoly R[n]}}}) :=
+    \big[fsetU/fset0]_(p : P) \big[fsetU/fset0]_(r : truncations n (val p))
+      \big[fsetU/fset0]_(q : P) (\big[fsetU/fset0]_(s : truncations n (val q) | size (val s) < size (val r))
+        (([fset subresultant (val j) (val r) (val s) | j in 'I_((size (val s)).-1)] `|` [fset subresultant (val j) (val s) (val r) | j in 'I_((size (val s)).-1)]))
+        `|` \big[fsetU/fset0]_(s : truncations n (val q) | size (val s) == size (val r))
+          (let rs := ((lead_coef (val s)) *: (val r) - (lead_coef (val r)) *: (val s))%R in
+          [fset subresultant (val j) (val s) (val rs) | j in 'I_((size rs).-1)])).
+
+Definition elim n (P : {fset {poly {mpoly R[n]}}}) :=
+  [fset x in elim_subdef0 n P `|` elim_subdef1 n P | mdeg (mlead x) != 0].
+
+(* Lemma poly_neigh_decomposition (p q : {poly R[i]}) :
+  monic p -> monic q -> coprime p q ->
+   exists rho : R, 0 < rho /\ forall P  *)
+
+From HB Require Import structures.
+From mathcomp Require Import fintype.
+
+Definition SAset_path_connected 
+
+Theorem roots2_on (P Q : {poly {mpoly R[n]}}) (s : {SAset R^n}) :
+  SAset_path_connected s
+  -> {in s, forall x, size
+
+
+Theorem cylindrical_decomposition n (P : {fset {mpoly R[n]}}) :
+  { S | isCD n S /\ forall p : P, poly_adapted n (val p) S}.
+Proof.
+elim: n P => [|n IHn] P.
+  exists (fun i => [fset SAsetT R i]); split=> [|[] p /= _]; last first.
+    case=> _ /= /fset1P -> x y _ _.
+    suff ->: x = y by [].
+    by apply/matrixP => i; case.
+  split=> [[]|[]//]; case=> /= [|//] _.
+  apply/andP; split; last by rewrite big_fset1/= eqxx.
+  apply/andP; split.
+    apply/negP; move=> /fset1P/eqP/SAsetP /(_ (\row_i 0)%R).
+    by rewrite inSAset0 inSAsetT.
+  do 2 (apply/forallP; case => i /= /fset1P -> {i}).
+  by rewrite eqxx.
+move: IHn => /(_ (elim n [fset muni p | p in P])) [S0 [S0CD S0p]].
+simple refine (exist _ _ _).
+  case=> i /=; rewrite ltnS leq_eqVlt.
+  case /boolP: (i == n.+1) => [/eqP -> _|_ /= ilt]; last exact: (S0 (Ordinal ilt)).
+
+
+
+  Search (_ <= _.+1).
+  case/boolP: (val i == n.+1); last first.
+case: (split (cast_ord (esym (addn1 n.+1)) i)).
+  exact S0.
+
+
+Admitted.
+
 
 End CylindricalDecomposition.

formula.v

@@ -230,6 +230,13 @@ Proof. by rewrite size_set_nth size_tuple; apply/eqP/maxn_idPr. Qed.
 Canonical set_nth_tuple (T : Type) (d : T) (n : nat) (x : n.-tuple T) (i : 'I_n) (y : T) :=
     Tuple (set_nth_size d x i y).
 
+Lemma rowPE (R : eqType) (n : nat) (u v : 'rV[R]_n) :
+  (u == v) = [forall i, u 0 i == v 0 i].
+Proof.
+apply/eqP/forallP => [/rowP uv i| uv]; first by apply/eqP.
+by apply/rowP => i; apply/eqP.
+Qed.
+
 End SeqFset.
 
 Section EquivFormula.
@@ -476,6 +483,62 @@ HB.instance Definition formula_choiceMixin (T : choiceType) :=
 HB.instance Definition formulan_choiceType (T : choiceType) n :=
   [Choice of {formula_n T} by <:].
 
+Section TermSubst.
+Variable F : nmodType.
+
+Definition subst_term s :=
+ let fix sterm (t : GRing.term F) := match t with
+  | 'X_i => if (i < size s)%N then 'X_(nth O s i) else 0
+  | t1 + t2 => (sterm t1) + (sterm t2)
+  | - t => - (sterm t)
+  | t *+ i => (sterm t) *+ i
+  | t1 * t2 => (sterm t1) * (sterm t2)
+  | t ^-1 => (sterm t) ^-1
+  | t ^+ i => (sterm t) ^+ i
+  | _ => t
+end%T in sterm.
+
+Fact fv_tsubst_nil (t : GRing.term F) : term_fv (subst_term [::] t) = fset0.
+Proof. by elim: t => //= t1 -> t2 ->; rewrite fsetU0. Qed.
+
+Fact fv_tsubst (k : unit) (s : seq nat) (t : GRing.term F) :
+    term_fv (subst_term s t) `<=` seq_fset k s.
+Proof.
+elim: t => //.
+- move=> i /=.
+  have [lt_is|leq_si] := ltnP i (size s); rewrite ?fsub0set //.
+  by rewrite fsub1set seq_fsetE; apply/(nthP _); exists i.
+- by move=> t1 h1 t2 h2 /=; rewrite fsubUset; apply/andP; split.
+- by move=> t1 h1 t2 h2 /=; rewrite fsubUset; apply/andP; split.
+Qed.
+
+Fact fv_tsubst_map (k : unit) (s : seq nat) (t : GRing.term F) :
+  term_fv (subst_term s t) `<=`
+  seq_fset k [seq nth O s i | i <- (iota O (size s)) & (i \in term_fv t)].
+Proof.
+elim: t => //.
+- move=> i /=.
+  have [lt_is|leq_si] := ltnP i (size s); rewrite ?fsub0set //.
+  rewrite fsub1set seq_fsetE; apply: map_f.
+  by rewrite mem_filter in_fset1 eqxx mem_iota leq0n add0n.
+- move=> t1 h1 t2 h2 /=; rewrite fsubUset; apply/andP; split.
+  + rewrite (fsubset_trans h1) //.
+    apply/seq_fset_sub; apply: sub_map_filter => x.
+    by rewrite in_fsetU => ->.
+  + rewrite (fsubset_trans h2) //.
+    apply/seq_fset_sub; apply: sub_map_filter => x.
+    by rewrite in_fsetU => ->; rewrite orbT.
+- move=> t1 h1 t2 h2 /=; rewrite fsubUset; apply/andP; split.
+  + rewrite (fsubset_trans h1) //.
+    apply/seq_fset_sub; apply: sub_map_filter => x.
+    by rewrite in_fsetU => ->.
+  + rewrite (fsubset_trans h2) //.
+    apply/seq_fset_sub; apply: sub_map_filter => x.
+    by rewrite in_fsetU => ->; rewrite orbT.
+Qed.
+
+End TermSubst.
+
 Section FormulaSubst.
 
 Variable T : Type.
@@ -634,6 +697,39 @@ rewrite nseq_cat; move: e f; elim: i => // i ih e f.
 by apply: (iff_trans _ (ih e f)); apply: holds_rcons_zero.
 Qed.
 
+Lemma holdsAnd (I : eqType) (r : seq I) (P : pred I) (e : seq R) (f : I -> formula R) :
+  holds e (\big[And/True%oT]_(i <- r | P i) f i)
+  <-> forall i, i \in r -> P i -> holds e (f i).
+Proof.
+elim: r => [|i r IHr]; first by rewrite big_nil.
+rewrite big_cons; case/boolP: (P i) => [|/negP] Pi; last first.
+  apply (iff_trans IHr); split=> hr j.
+    by rewrite in_cons => /orP; case=> [/eqP -> //|]; apply: hr.
+  by move=> jr; apply: hr; rewrite in_cons jr orbT.
+split=> /= [[hi /IHr hr j]|hr].
+  by rewrite in_cons => /orP; case=> [/eqP -> //|]; apply: hr.
+split; first by apply: hr => //; rewrite in_cons eq_refl.
+by apply/IHr => j jr; apply: hr; rewrite in_cons jr orbT.
+Qed.
+
+Lemma holdsOr (I : eqType) (r : seq I) (P : pred I) (e : seq R) (f : I -> formula R) :
+  holds e (\big[Or/False%oT]_(i <- r | P i) f i)
+  <-> exists i, i \in r /\ P i /\ holds e (f i).
+Proof.
+elim: r => [|i r IHr].
+  by rewrite big_nil; split=> // [[?]][].
+rewrite big_cons; case/boolP: (P i) => [|/negP] Pi; last first.
+  apply (iff_trans IHr); split=> -[j][+][hj].
+    by move=> jr; exists j; rewrite in_cons jr orbT; split=> //; split.
+  rewrite in_cons => /orP; case=> [/eqP ji|jr]; first by move: Pi; rewrite -ji.
+  by exists j; split=> //; split.
+split=> /= [[hi|/IHr [j][jr hj]]|[j][+][Pj]hj].
+- by exists i; rewrite in_cons eqxx; split=> //; split.
+- by exists j; rewrite in_cons jr orbT; split.
+rewrite in_cons => /orP[/eqP <-|jr]; first by left.
+by right; apply/IHr; exists j; split=> //; split.
+Qed.
+
 Lemma holds_Nfv_ex (e : seq R) (i : nat) (f : formula R) :
   i \notin formula_fv f -> (holds e ('exists 'X_i, f) <-> holds e f).
 Proof.
@@ -1137,57 +1233,6 @@ End Closure.
 Section QuantifierElimination.
 Variable (F : rcfType).
 
-Definition subst_term s :=
- let fix sterm (t : GRing.term F) := match t with
-  | 'X_i => if (i < size s)%N then 'X_(nth O s i) else 0
-  | t1 + t2 => (sterm t1) + (sterm t2)
-  | - t => - (sterm t)
-  | t *+ i => (sterm t) *+ i
-  | t1 * t2 => (sterm t1) * (sterm t2)
-  | t ^-1 => (sterm t) ^-1
-  | t ^+ i => (sterm t) ^+ i
-  | _ => t
-end%T in sterm.
-
-Fact fv_tsubst_nil (t : GRing.term F) : term_fv (subst_term [::] t) = fset0.
-Proof. by elim: t => //= t1 -> t2 ->; rewrite fsetU0. Qed.
-
-Fact fv_tsubst (k : unit) (s : seq nat) (t : GRing.term F) :
-    term_fv (subst_term s t) `<=` seq_fset k s.
-Proof.
-elim: t => //.
-- move=> i /=.
-  have [lt_is|leq_si] := ltnP i (size s); rewrite ?fsub0set //.
-  by rewrite fsub1set seq_fsetE; apply/(nthP _); exists i.
-- by move=> t1 h1 t2 h2 /=; rewrite fsubUset; apply/andP; split.
-- by move=> t1 h1 t2 h2 /=; rewrite fsubUset; apply/andP; split.
-Qed.
-
-Fact fv_tsubst_map (k : unit) (s : seq nat) (t : GRing.term F) :
-  term_fv (subst_term s t) `<=`
-  seq_fset k [seq nth O s i | i <- (iota O (size s)) & (i \in term_fv t)].
-Proof.
-elim: t => //.
-- move=> i /=.
-  have [lt_is|leq_si] := ltnP i (size s); rewrite ?fsub0set //.
-  rewrite fsub1set seq_fsetE; apply: map_f.
-  by rewrite mem_filter in_fset1 eqxx mem_iota leq0n add0n.
-- move=> t1 h1 t2 h2 /=; rewrite fsubUset; apply/andP; split.
-  + rewrite (fsubset_trans h1) //.
-    apply/seq_fset_sub; apply: sub_map_filter => x.
-    by rewrite in_fsetU => ->.
-  + rewrite (fsubset_trans h2) //.
-    apply/seq_fset_sub; apply: sub_map_filter => x.
-    by rewrite in_fsetU => ->; rewrite orbT.
-- move=> t1 h1 t2 h2 /=; rewrite fsubUset; apply/andP; split.
-  + rewrite (fsubset_trans h1) //.
-    apply/seq_fset_sub; apply: sub_map_filter => x.
-    by rewrite in_fsetU => ->.
-  + rewrite (fsubset_trans h2) //.
-    apply/seq_fset_sub; apply: sub_map_filter => x.
-    by rewrite in_fsetU => ->; rewrite orbT.
-Qed.
-
 (* quantifier elim + evaluation of invariant variables to 0 *)
 Definition qf_elim (f : formula F) : formula F :=
   let g := (quantifier_elim (@wproj _) (to_rform f)) in
@@ -1388,6 +1433,18 @@ Proof.
 by apply/eqP; rewrite -fsubset0 -(seq_fset_nil _ tt) fv_subst_formula.
 Qed.
 
+Definition cut(n : nat) (f : formula F) :=
+  subst_formula (iota 0 n) f.
+
+Fact nvar_cut n f : nvar n (cut n f).
+Proof.
+apply/(fsubset_trans (fv_subst_formula_map mnfset_key _ _))/seq_fset_sub => x.
+move=> /mapP[i]; rewrite mem_filter !mem_iota /= !add0n.
+by rewrite size_iota => /andP[_] ilt ->; rewrite nth_iota.
+Qed.
+
+Canonical Structure cut_formulan n f := MkFormulan (nvar_cut n f).
+
 End QuantifierElimination.
 
 Section SubstEnv.