From 6e53e3e2f6879fff5b1056ecb5b05c402549271c Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 12 Apr 2024 10:08:36 +0200 Subject: [PATCH] wip --- cylinder.v | 143 +++++-- formula.v | 159 ++++--- semialgebraic.v | 1092 +++++++++++++++++++++++++++++++---------------- subresultant.v | 17 +- 4 files changed, 949 insertions(+), 462 deletions(-) diff --git a/cylinder.v b/cylinder.v index 21f6a3e..ba08cb8 100644 --- a/cylinder.v +++ b/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. diff --git a/formula.v b/formula.v index 6733de9..a4404ff 100644 --- a/formula.v +++ b/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. diff --git a/semialgebraic.v b/semialgebraic.v index b2a36d9..b45d7a8 100644 --- a/semialgebraic.v +++ b/semialgebraic.v @@ -52,6 +52,10 @@ Local Open Scope fmap_scope. Local Open Scope quotient_scope. Local Open Scope type_scope. +Declare Scope sa_scope. +Delimit Scope sa_scope with SA. +Local Open Scope sa_scope. + Reserved Notation "{ 'SAset' F }" (format "{ 'SAset' F }"). Reserved Notation "{ 'SAfun' T }" @@ -111,6 +115,20 @@ exists (fun (x : k.-tuple F) => (\row_(i < k) (tnth x i))) => x. by rewrite ngraph_tnth. Qed. +Lemma take_ngraph m (x : 'rV[F]_(n + m)) : + take n (ngraph x) = ngraph (lsubmx x). +Proof. +move: (lsubmx x) (rsubmx x) (hsubmxK x) => l r <- {x}. +by rewrite ngraph_cat take_cat size_ngraph ltnn subnn take0 cats0. +Qed. + +Lemma drop_ngraph m (x : 'rV[F]_(n + m)) : + drop n (ngraph x) = ngraph (rsubmx x). +Proof. +move: (lsubmx x) (rsubmx x) (hsubmxK x) => l r <- {x}. +by rewrite ngraph_cat drop_cat size_ngraph ltnn subnn drop0. +Qed. + End Ngraph. Section Var_n. @@ -261,6 +279,10 @@ have [lt_in|leq_ni] := ltnP i n; last first. by rewrite cat0s /=; move=> []. Qed. +Lemma pi_form (f : {formula_n F}) (x : 'rV[F]_n) : + (x \in \pi_{SAset F^n} f) = rcf_sat (ngraph x) f. +Proof. by rewrite inE; apply/rcf_satP/rcf_satP => ?; apply/holds_repr_pi. Qed. + Lemma SAsetP (s1 s2 : {SAset F^n}) : reflect (s1 =i s2) (s1 == s2). Proof. move: s1 s2; apply: quotW => f1; apply: quotW => f2. @@ -272,6 +294,27 @@ Qed. End SemiAlgebraicSet. +Section Comprehension. + +Variables (F : rcfType) (n : nat) (f : formula F). + +Definition SAset_comprehension := \pi_({SAset F^n}) (cut n f). + +Lemma SAin_setP x : reflect (holds (ngraph x) f) (x \in SAset_comprehension). +Proof. +apply/(iffP (rcf_satP _ _)) => [/holds_repr_pi/holds_subst|hf]. + by rewrite -{1}[ngraph x : seq _]cats0 subst_env_iota_catl ?size_ngraph. +apply/holds_repr_pi/holds_subst. +by rewrite -[ngraph x : seq _]cats0 subst_env_iota_catl ?size_ngraph. +Qed. + +End Comprehension. + +Notation "[ 'set' : T | f ]" := ((@SAset_comprehension _ _ (f)%oT) : T) + (at level 0, only parsing) : sa_scope. +Notation "[ 'set' | f ]" := (@SAset_comprehension _ _ (f)%oT) + (at level 0, f at level 99, format "[ 'set' | f ]") : sa_scope. + Section Projection. Variables (F : rcfType) (n : nat) (i : 'I_n). @@ -313,248 +356,520 @@ Qed. End Projection. -Section Next. +Section Ops. Variables (F : rcfType) (n : nat). -Definition SAset0 := \pi_{SAset F^n} (Bool false). +Definition SAset_seq (r : seq 'rV[F]_n) : {SAset F^n} := + [set | \big[Or/False]_(x <- r) + \big[And/True]_(i < n) ('X_i == (x ord0 i)%:T)%oT ]. -Lemma pi_form (f : {formula_n F}) (x : 'rV[F]_n) : - (x \in \pi_{SAset F^n} f) = rcf_sat (ngraph x) f. -Proof. by rewrite inE; apply/rcf_satP/rcf_satP => ?; apply/holds_repr_pi. Qed. +Lemma inSAset_seq r x : x \in SAset_seq r = (x \in r). +Proof. +apply/SAin_setP/idP => [/holdsOr [y][+][_] /holdsAnd hy|xr]. + congr in_mem; apply/rowP => i. + move: hy => /(_ i); rewrite mem_index_enum /= (nth_map i) ?size_enum_ord//. + by rewrite nth_ord_enum => ->. +apply/holdsOr; exists x; split=> //; split=> //. +apply/holdsAnd => i _ _ /=. +by rewrite (nth_map i) ?size_enum_ord// nth_ord_enum. +Qed. + +Definition SAset0 : {SAset F^n} := SAset_seq [::]. + +Lemma inSAset0 (x : 'rV[F]_n) : x \in SAset0 = false. +Proof. by rewrite inSAset_seq. Qed. + +Lemma inSAset1 (x y : 'rV[F]_n) : x \in SAset_seq [:: y] = (x == y). +Proof. by rewrite inSAset_seq in_cons in_nil orbF. Qed. -Lemma inSAset0 (x : 'rV[F]_n) : (x \in SAset0) = false. -Proof. by rewrite pi_form. Qed. +Definition SAsetT : {SAset F^n} := [set | True%oT ]. -Definition SAset1_formula (x : 'rV[F]_n) := - \big[And/True%oT]_(i < n) ('X_i == (x ord0 i)%:T)%oT. +Lemma inSAsetT (x : 'rV[F]_n) : x \in SAsetT. +Proof. exact/SAin_setP. Qed. -Lemma SAset1_formulaP (x y : 'rV[F]_n) : - rcf_sat (ngraph x) (SAset1_formula y) = (x == y). +Definition SAsetU (f g : {SAset F^n}) := + \pi_({SAset F^n}) (formulan_or f g). + +Lemma inSAsetU f g x : x \in SAsetU f g = (x \in f) || (x \in g). Proof. -rewrite rcf_sat_forallP; apply/forallP/eqP; last first. - by move=> -> i; rewrite simp_rcf_sat /= nth_ngraph. -move=> h; apply/rowP => i; move/(_ i) : h. -by rewrite simp_rcf_sat /= nth_ngraph => /eqP. +rewrite /SAsetU pi_form !inE. +by apply/rcf_satP/orP; (case=> [l|r]; [left|right]; apply/rcf_satP). Qed. -Lemma SAset1_proof (x : 'rV[F]_n) : @nvar F n (SAset1_formula x). +Definition SAsetU1 x f := SAsetU (SAset_seq [:: x]) f. + +Lemma inSAsetU1 x f y : y \in SAsetU1 x f = (y == x) || (y \in f). +Proof. by rewrite inSAsetU inSAset1. Qed. + +Definition SAsetI (f g : {SAset F^n}) := + \pi_({SAset F^n}) (formulan_and f g). + +Lemma inSAsetI f g x : x \in SAsetI f g = (x \in f) && (x \in g). Proof. -rewrite /SAset1_formula; elim/big_ind: _; rewrite /nvar. -- exact: fsub0set. -- by move=> ???? /=; apply/fsubUsetP. -- by move=> i /= _; rewrite fsetU0 fsub1set mnfsetE /=. +rewrite /SAsetI pi_form !inE. +by apply/rcf_satP/andP => [/=|] [l r]; split; apply/rcf_satP. Qed. -Definition SAset1 (x : 'rV[F]_n) : {SAset F^n} := - \pi_{SAset F^n} (MkFormulan (SAset1_proof x)). +Definition SAsetC (s : {SAset F^n}) := \pi_{SAset F^n} (formulan_not s). -Lemma inSAset1 (x y : 'rV[F]_n) : (x \in SAset1 y) = (x == y). -Proof. by rewrite pi_form SAset1_formulaP. Qed. +Lemma inSAsetC f x : x \in SAsetC f = ~~ (x \in f). +Proof. +rewrite /SAsetC pi_form !inE. +apply/rcf_satP/negP => /= [hn /rcf_satP//|hn h]. +by apply/hn/rcf_satP. +Qed. -End Next. +Definition SAsetD (s1 s2 : {SAset F^n}) : {SAset F^n} := + SAsetI s1 (SAsetC s2). -Section POrder. +Lemma inSAsetD s1 s2 x : x \in SAsetD s1 s2 = (x \in s1) && ~~ (x \in s2). +Proof. by rewrite inSAsetI inSAsetC. Qed. -Variable F : rcfType. +Definition SAsetD1 s x := SAsetD s (SAset_seq [:: x]). -Variable n : nat. +Lemma inSAsetD1 s x y : y \in SAsetD1 s x = (y \in s) && (y != x). +Proof. by rewrite inSAsetD inSAset1. Qed. -Definition SAsub (s1 s2 : {SAset F^n}) := - rcf_sat [::] (nquantify O n Forall (s1 ==> s2)). +Definition SAsetX m (s1 : {SAset F^n}) (s2 : {SAset F^m}) : {SAset F^(n + m)} := + [set | s1 /\ subst_formula (iota n m) s2 ]. -Lemma reflexive_SAsub : reflexive SAsub. -Proof. by move=> s; apply/rcf_satP/nforallP => u; rewrite cat0s. Qed. +Lemma inSAsetX m (s1 : {SAset F^n}) (s2 : {SAset F^m}) (x : 'rV[F]_(n + m)) : + x \in SAsetX s1 s2 = (lsubmx x \in s1) && (rsubmx x \in s2). +Proof. +move: (lsubmx x) (rsubmx x) (hsubmxK x) => l r <- {x}. +apply/SAin_setP/andP => /= -[]; rewrite ngraph_cat. + move=> /holds_take + /holds_subst. + rewrite take_size_cat ?size_ngraph// subst_env_iota_catr ?size_ngraph//. + by split; apply/rcf_satP. +move=> ls rs; split. + by apply/holds_take; rewrite take_size_cat ?size_ngraph//; apply/rcf_satP. +apply/holds_subst; rewrite subst_env_iota_catr ?size_ngraph//. +exact/rcf_satP. +Qed. + +Definition SAset_sub s1 s2 := SAsetD s1 s2 == SAset0. -Lemma antisymetry_SAsub : antisymmetric SAsub. +Lemma SAset_subP s1 s2 : reflect {subset s1 <= s2} (SAset_sub s1 s2). Proof. -apply: quotP => f1 _; apply: quotP => f2 _. -move => /andP [/rcf_satP/nforallP sub1 /rcf_satP/nforallP sub2]. -apply/eqP; rewrite eqmodE; apply/rcf_satP/nforallP => u. -split; move/holds_repr_pi=> hf. -+ move/(_ u) : sub1; rewrite cat0s => sub1. - by apply/holds_repr_pi; apply: sub1. -+ by move/(_ u) : sub2 => sub2; apply/holds_repr_pi; apply: sub2. +apply/(iffP idP) => [/SAsetP|] s12; last first. + by apply/SAsetP => x; rewrite inSAsetD inSAset0; apply/negP => /andP[/s12 ->]. +move=> x x1; apply/negP => /negP x2. +suff: x \in SAset0 by rewrite inSAset0. +by rewrite -s12 inSAsetD x1. Qed. -Lemma transitive_SAsub : transitive SAsub. +Definition SAset_proper s1 s2 := SAset_sub s1 s2 && ~~ SAset_sub s2 s1. + +End Ops. + +Definition SAset_cast (F : rcfType) (n m : nat) (s : {SAset F^n}) : {SAset F^m} := + [set | (\big[And/True]_(i <- iota n (m-n)) ('X_i == 0)) /\ + nquantify m (n-m) Exists s]. + +Notation "[ 'set' x1 ; .. ; xn ]" := + (SAset_seq (cons x1 .. (cons xn nil) .. )): sa_scope. +Notation "A :|: B" := (SAsetU A B) : sa_scope. +Notation "x |: A" := (SAsetU1 x A) : sa_scope. +Notation "A :&: B" := (SAsetI A B) : sa_scope. +Notation "~: A" := (SAsetC A) : sa_scope. +Notation "A :\: B" := (SAsetD A B) : sa_scope. +Notation "A :\ x" := (SAsetD1 A x) : sa_scope. +Notation "A :*: B" := (SAsetX A B) (at level 35) : sa_scope. +Notation "A :<=: B" := (SAset_sub A B) (at level 49) : sa_scope. +Notation "A :<: B" := (SAset_proper A B) (at level 49) : sa_scope. + +Definition SAset_pos (F : rcfType) : {SAset F^1} := [set | (0 <% 'X_0)%oT]. + +Section SAsetTheory. +Variables (F : rcfType) (n : nat). +Implicit Types (A B C : {SAset F^n}) (x y z : 'rV[F]_n) (s t : seq 'rV[F]_n). + +Lemma eqEsubset A B : (A == B) = (A :<=: B) && (B :<=: A). Proof. -apply: quotP => f1 _; apply: quotP => f2 _; apply: quotP => f3 _. -move/rcf_satP/nforallP => sub21; move/rcf_satP/nforallP => sub13. -apply/rcf_satP/nforallP => u. -move/holds_repr_pi => holds_uf2. -by apply: sub13; apply: sub21; apply/holds_repr_pi. +apply/SAsetP/andP => [AB|[] /SAset_subP AB /SAset_subP BA x]. + by split; apply/SAset_subP => x; rewrite AB. +by apply/idP/idP => [/AB|/BA]. Qed. -Fact SAset_disp : unit. Proof. exact tt. Qed. +Lemma subEproper A B : (A :<=: B) = (A == B) || (A :<: B). +Proof. by rewrite eqEsubset -andb_orr orbN andbT. Qed. + +Lemma properEneq A B : (A :<: B) = (A != B) && (A :<=: B). +Proof. by rewrite andbC eqEsubset negb_and andb_orr [X in X || _]andbN. Qed. -Fact nvar_False : @formula_fv F False `<=` mnfset 0 n. -Proof. by rewrite fsub0set. Qed. +(* lt_def does things the other way. Should we have a fixed convention? *) +Lemma properEneq' A B : (A :<: B) = (B != A) && (A :<=: B). +Proof. by rewrite properEneq eq_sym. Qed. -Definition SAset_bottom := \pi_{SAset F^n} (MkFormulan nvar_False). +Lemma proper_neq A B : A :<: B -> A != B. +Proof. by rewrite properEneq; case/andP. Qed. -Lemma SAset_bottomP (s : {SAset F^n}) : SAsub SAset_bottom s. -Proof. by apply/rcf_satP/nforallP => u; move/holds_repr_pi. Qed. +Lemma eqEproper A B : (A == B) = (A :<=: B) && ~~ (A :<: B). +Proof. by rewrite negb_and negbK andb_orr andbN eqEsubset. Qed. -(* TODO: Why does {SAset F^n} not have a structure of bPOrderType yet? *) +Lemma sub0set A : SAset0 F n :<=: A. +Proof. by apply/SAset_subP => x; rewrite inSAset0. Qed. -Definition SAset_meet (s1 s2 : {SAset F^n}) : {SAset F^n} := - \pi_{SAset F^n} (formulan_and s1 s2). +Lemma subset0 A : (A :<=: SAset0 F n) = (A == SAset0 F n). +Proof. by rewrite eqEsubset sub0set andbT. Qed. -Definition SAset_join (s1 s2 : {SAset F^n}) : {SAset F^n} := - \pi_{SAset F^n} (formulan_or s1 s2). +Lemma proper0 A : (SAset0 F n :<: A) = (A != SAset0 F n). +Proof. by rewrite properEneq sub0set andbT eq_sym. Qed. -Fact commutative_meet : commutative SAset_meet. +Lemma set0Vmem A : (A = SAset0 F n) + {x | x \in A}. Proof. -move=> s1 s2; apply/eqP; rewrite eqmodE. -by apply/rcf_satP/nforallP => u; split => [[h1 h2] | [h2 h1]]; split. +case/boolP: (A == SAset0 F n) => [/eqP|] A0; first by left. +right; move: A A0; apply: quotW => /= f; rewrite eqmodE /=. +move=> /rcf_satP/n_nforall_formula/nexistsP P. +apply: sigW; move: P => [x hx] /=; exists (\row_(i < n) x`_i). +rewrite inE ngraph_nth rcf_sat_repr_pi. +move/rcf_satP: hx; rewrite cat0s !simp_rcf_sat; case: rcf_sat => //=. +by rewrite implybF negbK big_nil => /rcf_satP/holds_subst. Qed. -Fact commutative_join : commutative SAset_join. +Lemma subsetT A : A :<=: SAsetT F n. +Proof. by apply/SAset_subP => x; rewrite inSAsetT. Qed. + +Lemma subTset A : (SAsetT F n :<=: A) = (A == SAsetT F n). +Proof. by rewrite eqEsubset subsetT. Qed. + +Lemma properT A : (A :<: SAsetT F n) = (A != SAsetT F n). +Proof. by rewrite properEneq subsetT andbT. Qed. + +Lemma perm_SAset_seq s t : + perm_eq s t -> SAset_seq s = SAset_seq t. Proof. -move=> s1 s2; apply/eqP; rewrite eqmodE; apply/rcf_satP/nforallP => u. -by split => h; apply/or_comm. +by move=> st; apply/eqP/SAsetP => x; rewrite !inSAset_seq (perm_mem st). Qed. -Fact associative_meet : associative SAset_meet. +Lemma SAset_nil : SAset_seq [::] = SAset0 F n. +Proof. by []. Qed. + +Lemma SAset_cons x s : SAset_seq (x :: s) = x |: SAset_seq s. +Proof. by apply/eqP/SAsetP => y; rewrite inSAsetU1 !inSAset_seq in_cons. Qed. + +Lemma SAset_cat s t : SAset_seq (s ++ t) = SAset_seq s :|: SAset_seq t. +Proof. by apply/eqP/SAsetP => y; rewrite inSAsetU !inSAset_seq mem_cat. Qed. + +Lemma SAset_rev s : SAset_seq (rev s) = SAset_seq s. +Proof. exact/perm_SAset_seq/permPl/perm_rev. Qed. + +Lemma SAset0U A : SAset0 F n :|: A = A. +Proof. by apply/eqP/SAsetP => x; rewrite inSAsetU inSAset0. Qed. + +Lemma SAsetUC A B : A :|: B = B :|: A. +Proof. by apply/eqP/SAsetP => x; rewrite !inSAsetU orbC. Qed. + +Lemma SAsetUA A B C : A :|: (B :|: C) = A :|: B :|: C. +Proof. by apply/eqP/SAsetP => x; rewrite !inSAsetU orbA. Qed. + +HB.instance Definition _ := Monoid.isComLaw.Build {SAset F^n} (SAset0 F n) (@SAsetU F n) SAsetUA SAsetUC SAset0U. + +Lemma SAsetIC A B : A :&: B = B :&: A. +Proof. by apply/eqP/SAsetP => x; rewrite !inSAsetI andbC. Qed. + +Lemma SAsetIA A B C : A :&: (B :&: C) = A :&: B :&: C. +Proof. by apply/eqP/SAsetP => x; rewrite !inSAsetI andbA. Qed. + +Lemma SAsetCU A B : ~: (A :|: B) = ~: A :&: ~: B. Proof. -move => s1 s2 s3; apply/eqP; rewrite eqmodE; apply/rcf_satP/nforallP => u. -split=> [[h1 /holds_repr_pi [h2 h3]]|[/holds_repr_pi [h1 h2] h3]]; -by split=> //; apply/holds_repr_pi => []; split. +by apply/eqP/SAsetP => x; rewrite inSAsetI !inSAsetC inSAsetU negb_or. Qed. -Fact associative_join : associative SAset_join. +Lemma SAsetCI A B : ~: (A :&: B) = ~: A :|: ~: B. Proof. -move=> s1 s2 s3; apply/eqP; rewrite eqmodE. -apply/rcf_satP/nforallP => u. -split => [ [ | /holds_repr_pi [|]] | [/holds_repr_pi [|] | ] ]. -+ by left; apply/holds_repr_pi; left. -+ by left; apply/holds_repr_pi; right. -+ by right. -+ by left. -+ by right; apply/holds_repr_pi; left. -+ by right; apply/holds_repr_pi; right. +by apply/eqP/SAsetP => x; rewrite inSAsetU !inSAsetC inSAsetI negb_and. Qed. -Fact meet_join (s1 s2 : {SAset F^n}) : SAset_meet s2 (SAset_join s2 s1) = s2. +Lemma SAsubset_refl : reflexive (@SAset_sub F n). +Proof. by move=> A; apply/SAset_subP. Qed. + +Lemma SAsubset_anti : antisymmetric (@SAset_sub F n). +Proof. by move=> A B /andP[] AB BA; apply/eqP; rewrite eqEsubset AB. Qed. + +Lemma SAsubset_trans : transitive (@SAset_sub F n). Proof. -apply/eqP/SAsetP => x; rewrite !inE. -rewrite !rcf_sat_repr_pi simp_rcf_sat rcf_sat_repr_pi. -by rewrite simp_rcf_sat andbC orbK. +by move=> A B C /SAset_subP BA /SAset_subP AC; apply/SAset_subP => x /BA /AC. Qed. -Fact join_meet (s1 s2 : {SAset F^n}) : SAset_join s2 (SAset_meet s2 s1) = s2. +Lemma SAsetIUr A B C : A :&: (B :|: C) = (A :&: B) :|: (A :&: C). Proof. -apply/eqP/SAsetP => x; rewrite !inE !rcf_sat_repr_pi. -by rewrite simp_rcf_sat rcf_sat_repr_pi simp_rcf_sat andbC andKb. +by apply/eqP/SAsetP => x; rewrite inSAsetI !inSAsetU !inSAsetI andb_orr. Qed. -Fact le_meet (s1 s2 : {SAset F^n}) : SAsub s1 s2 = (SAset_meet s1 s2 == s1). +Lemma SAsetIUl A B C : (A :|: B) :&: C = (A :&: C) :|: (B :&: C). +Proof. by rewrite ![_ :&: C]SAsetIC SAsetIUr. Qed. + +Lemma SAsetUIr A B C : A :|: (B :&: C) = (A :|: B) :&: (A :|: C). Proof. -apply/idP/idP=> [sub12| /SAsetP h]. -+ apply/SAsetP => x; move : (ngraph x) => e. - rewrite !inE rcf_sat_repr_pi simp_rcf_sat. - apply : andb_idr; apply/implyP. - move : sub12 => /rcf_satP/nforallP sub12. - apply/implyP; move/rcf_satP => holds_e_s1. - apply/rcf_satP; move : holds_e_s1. - exact: sub12. -+ apply/rcf_satP/nforallP => e. - by move/holds_tuple; rewrite -h; move/holds_tuple/holds_repr_pi => []. +by apply/eqP/SAsetP => x; rewrite inSAsetU !inSAsetI !inSAsetU orb_andr. Qed. -Fact left_distributive_meet_join : left_distributive SAset_meet SAset_join. +Lemma SAsubsetIl A B : A :&: B :<=: A. +Proof. by apply/SAset_subP => x; rewrite inSAsetI => /andP[]. Qed. + +Lemma SAsubsetIidl A B : (A :<=: A :&: B) = (A :<=: B). Proof. -set vw := holds_repr_pi; move=> s1 s2 s3; apply/eqP; rewrite eqmodE. -apply/rcf_satP/nforallP => t. -split=> [[/vw /= [h1|h2] h3]|[/vw [h1 h3]| /vw [h2 h3]]]. -+ by left; apply/vw. -+ by right; apply/vw. -+ by split => //; apply/vw; left. -+ by split => //; apply/vw; right. +apply/SAset_subP/SAset_subP => AB x /[dup] xA /AB; rewrite inSAsetI. + by move=> /andP[]. +by rewrite xA. Qed. -Fact idempotent_meet : idempotent SAset_meet. +Lemma SAsubsetEI A B : A :<=: B = (A :&: B == A). +Proof. by rewrite eqEsubset SAsubsetIl SAsubsetIidl. Qed. + +Lemma SAsetI_idem : idempotent (@SAsetI F n). Proof. -move=> x; apply/eqP/SAsetP => i. -by rewrite !inE rcf_sat_repr_pi simp_rcf_sat andbb. +by move=> A; apply/eqP; rewrite eqEsubset SAsubsetIl SAsubsetIidl SAsubset_refl. Qed. -#[non_forgetful_inheritance] -HB.instance Definition SAset_latticeType := - Order.isMeetJoinDistrLattice.Build SAset_disp {SAset _} - le_meet (fun _ _ => erefl) commutative_meet commutative_join - associative_meet associative_join meet_join join_meet left_distributive_meet_join idempotent_meet. +Lemma SAsetKU A B : A :&: (B :|: A) = A. +Proof. by apply/eqP/SAsetP => x; rewrite inSAsetI inSAsetU orKb. Qed. -HB.instance Definition _ := - Order.hasBottom.Build SAset_disp {SAset F^n} SAset_bottomP. +Lemma SAsetKU' B A : A :&: (A :|: B) = A. +Proof. by rewrite SAsetUC SAsetKU. Qed. + +Lemma SAsetKI A B : A :|: (B :&: A) = A. +Proof. by apply/eqP/SAsetP => x; rewrite inSAsetU inSAsetI andKb. Qed. + +Lemma SAsetKI' B A : A :|: (A :&: B) = A. +Proof. by rewrite SAsetIC SAsetKI. Qed. -Definition SAset_top : {SAset F^n} := - \pi_{SAset F^n} (Bool true). +Lemma SAsetICr A : A :&: ~: A = SAset0 F n. +Proof. by apply/eqP/SAsetP => x; rewrite inSAsetI inSAsetC andbN inSAset0. Qed. -Lemma SAset_topP (s : {SAset F^n}) : (s <= SAset_top)%O. -Proof. by apply/rcf_satP/nforallP => t h; apply/holds_repr_pi. Qed. +Lemma SAset0I A : SAset0 F n :&: A = SAset0 F n. +Proof. by apply/eqP/SAsetP => x; rewrite inSAsetI inSAset0. Qed. -Canonical SAset_tblatticeType := - Order.hasTop.Build _ _ SAset_topP. +Lemma SAsetID0 A B : SAsetI B (SAsetD A B) = (SAset0 F n). +Proof. by rewrite /SAsetD [A :&: _]SAsetIC SAsetIA SAsetICr SAset0I. Qed. -Definition SAset_sub (s1 s2 : {SAset F^n}) : {SAset F^n} := - \pi_{SAset F^n} (formulan_and s1 (formulan_not s2)). +Lemma SAsetUCr A : A :|: ~: A = SAsetT F n. +Proof. by apply/eqP/SAsetP => x; rewrite inSAsetU inSAsetC orbN inSAsetT. Qed. -Fact meet_sub (s1 s2 : {SAset F^n}) : - SAset_meet s2 (SAset_sub s1 s2) = SAset_bottom. +Lemma SAsetIT A : A :&: SAsetT F n = A. +Proof. by apply/eqP/SAsetP => x; rewrite inSAsetI inSAsetT andbT. Qed. + +Lemma SAsetUID A B : A :&: B :|: A :\: B = A. +Proof. by rewrite -SAsetIUr SAsetUCr SAsetIT. Qed. + +Lemma SAset_cast_id m (A : {SAset F^m}) : SAset_cast m A = A. Proof. -apply/eqP; rewrite eqmodE; apply/rcf_satP/nforallP => t. -by split => //; move => [? /holds_repr_pi [_ ?]]. +apply/eqP/SAsetP => x; apply/SAin_setP/rcf_satP => /= [[] _|hx]; + rewrite subnn nquantify0//. +by split=> //; apply/holdsAnd. Qed. -Fact join_meet_sub (s1 s2 : {SAset F^n}) : - SAset_join (SAset_meet s1 s2) (SAset_sub s1 s2) = s1. +Lemma SAset_cast_le m k (A : {SAset F^m}) : (k <= m)%N -> + SAset_cast k A = [set | nquantify k (m - k) Exists A]. Proof. -apply/eqP/SAsetP => x; rewrite !inE. -rewrite !rcf_sat_repr_pi !simp_rcf_sat !rcf_sat_repr_pi. -by rewrite !simp_rcf_sat -andb_orr orbN andbT. +rewrite -subn_eq0 => /eqP km; apply/eqP/SAsetP => x. +apply/Bool.eq_iff_eq_true. +rewrite [X in X <-> _](iff_sym (rwP (SAin_setP _ _))). +rewrite [X in _ <-> X](iff_sym (rwP (SAin_setP _ _))). +rewrite km big_nil/=. +by split=> // -[]. Qed. -HB.instance Definition _ := Order.hasRelativeComplement.Build SAset_disp {SAset F^n} meet_sub join_meet_sub. +Lemma SAset_cast_ge m k (A : {SAset F^m}) : (m <= k)%N -> + SAset_cast k A = [set | A /\ \big[And/True]_(i <- iota m (k - m)) ('X_i == 0)]. +Proof. +rewrite -subn_eq0 => /eqP km; apply/eqP/SAsetP => x. +apply/Bool.eq_iff_eq_true. +rewrite [X in X <-> _](iff_sym (rwP (SAin_setP _ _))). +rewrite [X in _ <-> X](iff_sym (rwP (SAin_setP _ _))). +rewrite km nquantify0/=. +by split=> -[]. +Qed. + +Lemma inSAset_castDn m k (A : {SAset F^(m+k)}) (x : 'rV[F]_m) : + reflect (exists y : 'rV[F]_(m+k), y \in A /\ x = lsubmx y) (x \in SAset_cast m A). +Proof. +rewrite SAset_cast_le ?leq_addr// subDnCA// subnn addn0 -[X in nquantify X](size_ngraph x). +apply/(iffP (SAin_setP _ _)) => [/nexistsP [y] hxy|[y][yA]->]. + exists (row_mx x (\row_i tnth y i)); rewrite row_mxKl; split=> //. + by apply/rcf_satP; rewrite ngraph_cat ngraph_tnth. +apply/nexistsP; exists (ngraph (rsubmx y)); rewrite -ngraph_cat hsubmxK. +exact/rcf_satP. +Qed. + +Lemma inSAset_castnD m k (A : {SAset F^m}) (x : 'rV[F]_(m+k)) : + x \in SAset_cast (m+k) A = (lsubmx x \in A) && (rsubmx x == 0). +Proof. +rewrite SAset_cast_ge ?leq_addr//. +apply/SAin_setP/andP => /=; rewrite -holds_take take_ngraph holdsAnd /= => -[/rcf_satP hx]. + move=> h0; split=> //; apply/eqP/rowP => i. + move/(_ (@unsplit m k (inr i))): h0; rewrite nth_ngraph mem_iota subnKC ?leq_addr//= -addnS leq_add// => /(_ Logic.eq_refl Logic.eq_refl). + by rewrite !mxE. +move=> /eqP /rowP x0; split=> // => i; rewrite mem_iota subnKC ?leq_addr// => /andP[mi im] _. +rewrite (nth_ngraph _ _ (Ordinal im)) -(splitK (Ordinal im)). +move: mi; rewrite leqNgt -{1}[i]/(Ordinal im : nat). +case: splitP => // j _ _. +by move: (x0 j); rewrite !mxE. +Qed. + +Lemma SAset_cast_trans k m A : (minn n k <= m)%N -> + SAset_cast k (SAset_cast m A) = SAset_cast k A. +Proof. +case: (ltnP m n) => [mn|nm _]; last first. + case/orP: (leq_total m k) => [mk|km]. + rewrite -(subnKC mk) -(subnKC nm) [X in (k-X)%N]subnKC//. + apply/eqP/SAsetP => x. + rewrite 2!inSAset_castnD. + move: (lsubmx x) (rsubmx x) (hsubmxK x) => l r <- {x}. + move: (lsubmx l) (rsubmx l) (hsubmxK l) => ll lr <- {l}. + rewrite SAset_cast_ge; last by rewrite subnKC// subnKC// (leq_trans nm mk). + apply/andP/SAin_setP => /=; rewrite holdsAnd -holds_take -(take_takel _ (@leq_addr (m-n) n)%N) !take_ngraph !row_mxKl (rwP (rcf_satP _ _)) subDnCA ?leq_addr// subDnCA// subnn addn0 addnC. + move=> [] /andP[] llA /eqP -> /eqP ->; split=> //= i. + rewrite mem_iota addnA => /andP[+ ilt] _. + rewrite -[i]/(Ordinal ilt : nat) nth_ngraph mxE. + case: (splitP (Ordinal ilt)) => j ->; rewrite mxE//. + by case: (splitP j) => j' ->; rewrite leqNgt ?ltn_ord// mxE. + move=> [llA /= h0]; split; last first. + apply/eqP/rowP => i. + move/(_ (unsplit (inr i) : 'I_(n + (m - n) + (k - m))%N)): h0. + rewrite nth_ngraph !mxE unsplitK. + by rewrite mem_iota addnA ltn_ord/= -addnA leq_addr; apply. + apply/andP; split=> //. + apply/eqP/rowP => i. + move/(_ (unsplit (inl (unsplit (inr i))) : 'I_(n + (m - n) + (k - m))%N)): h0. + rewrite nth_ngraph !mxE unsplitK mxE unsplitK. + by rewrite mem_iota addnA ltn_ord/= leq_addr; apply. + case/orP: (leq_total n k) => [nk|kn]. + rewrite -(subnKC km) -(subnKC nk) [X in (m-X)%N]subnKC//. + apply/eqP/SAsetP => x. + rewrite inSAset_castnD. + move: (lsubmx x) (rsubmx x) (hsubmxK x) => l r <- {x}. + apply/inSAset_castDn/andP => [[y]|[lA] /eqP ->]; + rewrite SAset_cast_ge -?addnA ?leq_addr//. + move: (lsubmx y) (rsubmx y) (hsubmxK y) => yl yr <- {y} [] /[swap] <- {yl}. + move=> /SAin_setP/= [] /holds_take. + rewrite -(take_takel _ (@leq_addr (k - n)%N n)) !take_ngraph !row_mxKl => /rcf_satP lA /holdsAnd. + rewrite subDnCA ?leq_addr// subDnCA// subnn addn0 addnC /= => h0. + split=> //; apply/eqP/rowP => i. + move/(_ (unsplit (inl (unsplit (inr i))) : 'I_(n + (k - n) + (m - k))%N)): h0. + by rewrite nth_ngraph !mxE unsplitK mxE unsplitK mem_iota addnA ltn_ord/= leq_addr; apply. + exists (row_mx (row_mx l 0) 0); rewrite row_mxKl; split=> //. + apply/SAin_setP => /=; split. + apply/holds_take. + rewrite -(take_takel _ (@leq_addr (k - n)%N n)) !take_ngraph !row_mxKl. + exact/rcf_satP. + apply/holdsAnd => i; rewrite mem_iota subDnCA ?leq_addr// subDnCA// subnn addn0 [X in (n + X)%N]addnC /= addnA => /andP[+ ilt] _. + rewrite -[i]/(Ordinal ilt : nat) nth_ngraph mxE. + case: (splitP (Ordinal ilt)) => j ->; rewrite mxE//. + by case: (splitP j) => j' ->; rewrite leqNgt ?ltn_ord// mxE. + move: A; rewrite -(subnKC nm) -(subnKC kn) [X in (m - X)%N]subnKC// -addnA => A. + apply/eqP/SAsetP => x; apply/inSAset_castDn/inSAset_castDn => -[y]. + rewrite [_ _ A]SAset_cast_ge ?addnA ?leq_addr// => -[] /SAin_setP /= [] /holds_take + _. + rewrite takeD take_ngraph drop_ngraph take_ngraph -ngraph_cat => yA -> {x}. + exists (row_mx (lsubmx y) (lsubmx (rsubmx y))); split; first exact/rcf_satP. + by rewrite row_mxKl. + move=> [] /rcf_satP yA -> {x}; exists (row_mx (lsubmx y) (row_mx (rsubmx y) 0)); split; last by rewrite row_mxKl. + rewrite [_ _ A]SAset_cast_ge ?addnA ?leq_addr//; apply/SAin_setP => /=; split. + apply/holds_take. + by rewrite takeD take_ngraph drop_ngraph take_ngraph -ngraph_cat row_mxKr !row_mxKl hsubmxK. + apply/holdsAnd => i; rewrite {1}addnA subnKC// subnKC// mem_iota -{1 2}(subnKC kn) -addnA => /andP[] + ilt _ /=. + rewrite -[i]/(Ordinal ilt : nat) nth_ngraph. + rewrite mxE; case: splitP => j ->. + by rewrite leqNgt (leq_trans (ltn_ord j) (leq_addr _ _)). + rewrite leq_add2l mxE; case: splitP => j' ->; last by rewrite mxE. + by rewrite leqNgt ltn_ord. +rewrite geq_min leqNgt mn/= => km. +rewrite SAset_cast_le// SAset_cast_le ?(ltnW mn)// SAset_cast_le ?(ltnW (leq_ltn_trans km mn))//. +apply/eqP/SAsetP => x; rewrite -[X in nquantify X](size_ngraph x); apply/SAin_setP/SAin_setP => /nexistsP [y] => /rcf_satP. + rewrite -[in X in rcf_sat _ X](subnKC km). + rewrite -[y]ngraph_tnth -ngraph_cat => /SAin_setP. + have mE: (k + (m - k))%N = size (ngraph x ++ y) by rewrite size_cat size_ngraph size_tuple subnKC. + rewrite [X in nquantify X]mE -{2}[y]ngraph_tnth -ngraph_cat => /nexistsP [] {mE}. + rewrite ngraph_cat (subnKC km) ngraph_tnth => z hA. + apply/nexistsP. + have ->: (n - k)%N = (n - m + m - k)%N by rewrite subnK// (ltnW mn). + have /eqP scat: size (y ++ z) = (n - m + m - k)%N. + by rewrite size_cat !size_tuple addnC addnBA. + by exists (Tuple scat) => /=; rewrite catA. +move=> /rcf_satP hy; apply/nexistsP. +have /eqP ts: size (take (m - k)%N y) = (m - k)%N. + by rewrite size_takel// size_tuple leq_sub// ltnW. +exists (Tuple ts); rewrite -[in X in holds _ X](subnKC km). +rewrite -[Tuple ts]ngraph_tnth -ngraph_cat. +apply/rcf_satP/SAin_setP. +have mE: (k + (m - k))%N = size (ngraph x ++ Tuple ts) by rewrite size_cat size_ngraph size_tuple subnKC. +rewrite [X in nquantify X]mE -{2}[Tuple ts]ngraph_tnth -ngraph_cat. +apply/nexistsP. +rewrite ngraph_cat subnKC//. +have /eqP ds: size (drop (m - k)%N y) = (n - m)%N. + by rewrite size_drop size_tuple subnBA// addnC subnKC// (ltnW (leq_ltn_trans km mn)). +by exists (Tuple ds); rewrite -catA ngraph_tnth/= cat_take_drop. +Qed. + +Definition SAset_proj m (s : {SAset F^n}) := SAset_cast n (SAset_cast m s). + +Lemma SAset_proj_ge m (s : {SAset F^n}) : (n <= m)%N -> SAset_proj m s = s. +Proof. by move=> nm; rewrite /SAset_proj SAset_cast_trans ?minnn// SAset_cast_id. Qed. + +Lemma inSAset_proj m (s : {SAset F^n}) (x : 'rV[F]_n) : + reflect (exists y, y \in s /\ x = y *m @diag_mx F n (\row_i (i < m)%N%:R))%R (x \in SAset_proj m s). +Proof. +case: (ltnP m n) => [mn|nm]; last first. + have ->: diag_mx (\row_i (i < m)%:R)%R = (1%:M)%R :> 'M[F]_n. + by apply/matrixP => i j; rewrite !mxE (leq_trans (ltn_ord i) nm). + rewrite SAset_proj_ge//; apply/(iffP idP) => [xs|[y][ys]->]; last by rewrite mulmx1. + by exists x; split=> //; rewrite mulmx1. +rewrite /SAset_proj. +move: s x; rewrite -(subnKC (ltnW mn)) => s' x. +rewrite -(hsubmxK x); move: (lsubmx x) (rsubmx x) => l r {x}. +rewrite inSAset_castnD. +apply/(iffP andP) => [[] /inSAset_castDn [y][ys]|[y][ys]]. + rewrite row_mxKl row_mxKr => -> /eqP -> {l r}; exists y; split=> //. + rewrite -(hsubmxK y); move: (lsubmx y) (rsubmx y) => l r {y ys}. + rewrite row_mxKl -[X in diag_mx X]cat_ffun_id diag_mx_row. + rewrite mul_row_block !mulmx0 addr0 add0r; congr row_mx. + rewrite -[LHS]mulmx1; congr (_ *m _)%R. + by apply/matrixP => i j; rewrite !mxE/= ltn_ord. + rewrite -[LHS](mulmx0 _ r); congr (_ *m _)%R. + by apply/matrixP => i j; rewrite !mxE/= ltnNge leq_addr/= mul0rn. +move: ys; rewrite row_mxKl row_mxKr -(hsubmxK y); move: (lsubmx y) (rsubmx y) => yl yr {y} ys. +rewrite -[X in diag_mx X]cat_ffun_id diag_mx_row. +rewrite mul_row_block !mulmx0 addr0 add0r => /eq_row_mx[] -> ->; split. + apply/inSAset_castDn; exists (row_mx yl yr); split=> //. + rewrite row_mxKl -[RHS]mulmx1; congr (_ *m _)%R. + by apply/matrixP => i j; rewrite !mxE/= ltn_ord. +apply/eqP; rewrite -[RHS](mulmx0 _ yr); congr (_ *m _)%R. +by apply/matrixP => i j; rewrite !mxE/= ltnNge leq_addr/= mul0rn. +Qed. + +Definition SAset_disjoint (s1 s2 : {SAset F^n}) := + s1 :&: s2 == SAset0 F n. + +Definition SAset_trivI (I : {fset {SAset F^n}}) := + [forall s1 : I, [forall s2 : I, (val s1 != val s2) ==> SAset_disjoint (val s1) (val s2)]]. + +Definition SAset_partition (I : {fset {SAset F^n}}) := + (SAset0 F n \notin I) && SAset_trivI I && (\big[@SAsetU F n/SAset0 F n]_(s : I) val s == SAsetT F n). + +End SAsetTheory. -Definition SAset_prod_formula m (s1 : {SAset F^n}) (s2 : {SAset F^m}) := - (s1 /\ subst_formula (iota n m) s2)%oT. +Section POrder. -Lemma nvar_SAset_prod_formula m (s1 : {SAset F^n}) (s2 : {SAset F^m}) : - nvar (n + m) (SAset_prod_formula s1 s2). -Proof. -rewrite /nvar /SAset_prod_formula /=; apply/fsubUsetP; split. - apply/(fsubset_trans (fsubset_formulan_fv s1)). - by rewrite mnfset0_sub leq_addr. -apply/(fsubset_trans (fv_subst_formula mnfset_key _ s2)). -case: {s2} m => [|m]; first by rewrite m0fset. -by rewrite mnfset_sub /=. -Qed. +Variable F : rcfType. -Definition SAset_prod m (s1 : {SAset F^n}) (s2 : {SAset F^m}) := - \pi_({SAset F^(n + m)}) (MkFormulan (nvar_SAset_prod_formula s1 s2)). +Variable n : nat. -Lemma SAset_prodP m (s1 : {SAset F^n}) (s2 : {SAset F^m}) (x : 'rV[F]_(n + m)) : - (x \in SAset_prod s1 s2) = (lsubmx x \in s1) && (rsubmx x \in s2). -Proof. -move: (lsubmx x) (rsubmx x) (hsubmxK x) => l r <- {x}. -rewrite /SAset_prod /= pi_form /SAset_prod_formula /= !ngraph_cat. -apply: (sameP (rcf_satP _ _)). -apply: (iffP andP) => [[/rcf_satP h1 /rcf_satP h2] - | /= [/holds_take + /holds_subst]]; last first. - rewrite subst_env_iota_catr ?size_ngraph// take_size_cat ?size_ngraph//. - by move=> h1 h2; split=> //; apply/rcf_satP. -split; first by apply/holds_take; rewrite take_size_cat ?size_ngraph. -by apply/holds_subst; rewrite subst_env_iota_catr ?size_ngraph. -Qed. +Fact SAset_disp : unit. Proof. exact tt. Qed. -Definition SAset_pos_formula : formula F := (0 <% 'X_0)%oT. +HB.instance Definition SAset_latticeType := + Order.isMeetJoinDistrLattice.Build SAset_disp {SAset _} + (@SAsubsetEI F n) (@properEneq' F n) (@SAsetIC F n) (@SAsetUC F n) + (@SAsetIA F n) (@SAsetUA F n) (@SAsetKU' F n) (@SAsetKI' F n) (@SAsetIUl F n) (@SAsetI_idem F n). + +HB.instance Definition _ := + Order.hasBottom.Build SAset_disp {SAset F^n} (@sub0set F n). -Lemma nvar_SAset_pos_formula : nvar 1 SAset_pos_formula. -Proof. by rewrite /nvar /= fset0U fsub1set seq_fsetE. Qed. +HB.instance Definition SAset_tblatticeType := + Order.hasTop.Build SAset_disp {SAset F^n} (@subsetT F n). -Definition SAset_pos := \pi_({SAset F^1}) (MkFormulan nvar_SAset_pos_formula). +HB.instance Definition _ := Order.hasRelativeComplement.Build SAset_disp {SAset F^n} (@SAsetID0 F n) (@SAsetUID F n). End POrder. @@ -576,7 +891,7 @@ Definition SAtot := Definition ext (p : nat) (f : {formula_p F}) : {formula_(p+m) F} := MkFormulan (formuladd m f). -Lemma f_is_ftotalE (f : {formula_(n + m) F}) : +Lemma ftotalP (f : {formula_(n + m) F}) : reflect (forall (t : n.-tuple F), exists (u : m.-tuple F), rcf_sat (t ++ u) f) (rcf_sat [::] (ftotal f)). @@ -600,7 +915,7 @@ Definition functional (f : {formula_(n+m) F}) := Definition SAfunc := [pred s : {SAset F ^ _} | rcf_sat [::] (functional s)]. -Lemma f_is_funcE (f : {formula_(n + m) F}) : +Lemma functionalP (f : {formula_(n + m) F}) : reflect (forall (t : n.-tuple F) (u1 u2 : m.-tuple F), rcf_sat (t ++ u1) f -> rcf_sat (t ++ u2) f -> u1 = u2) @@ -637,12 +952,12 @@ apply: (iffP idP). by move/(congr1 val). Qed. -Lemma SAtotE (s : {SAset F ^ (n + m)}) : +Lemma inSAtot (s : {SAset F ^ (n + m)}) : reflect (forall (x : 'rV[F]_n), exists (y : 'rV[F]_m), (row_mx x y) \in s) (s \in SAtot). Proof. -rewrite inE; apply: (iffP (f_is_ftotalE _)) => s_sat x. +rewrite inE; apply: (iffP (ftotalP _)) => s_sat x. have [y sat_s_xy] := s_sat (ngraph x). exists (\row_(i < m) (nth 0 y i)). by rewrite inE ngraph_cat ngraph_nth. @@ -651,13 +966,13 @@ exists (ngraph y). by move: xy_in_s; rewrite inE ngraph_cat ngraph_nth. Qed. -Lemma SAfuncE (s : {SAset F ^ (n + m)}) : +Lemma inSAfunc (s : {SAset F ^ (n + m)}) : reflect (forall (x : 'rV[F]_n), forall (y1 y2 : 'rV[F]_m), (row_mx x y1) \in s -> (row_mx x y2) \in s -> y1 = y2) (s \in SAfunc). Proof. -rewrite inE; apply: (iffP (f_is_funcE _)) => fun_s x y1 y2. +rewrite inE; apply: (iffP (functionalP _)) => fun_s x y1 y2. rewrite !inE !ngraph_cat => /fun_s fun_s1 /fun_s1. exact/bij_inj/ngraph_bij. move=> s_sat1 s_sat2. @@ -669,19 +984,6 @@ by apply: (fun_s (\row_(i < n) (nth 0 x i))); rewrite inE !ngraph_cat !ngraph_nth. Qed. -Fact nvar_SAimset (f : {SAset F ^ (n + m)}) (s : {SAset F^n}) : - formula_fv (nquantify m n Exists ((subst_formula ((iota m n) - ++ (iota O m)) f) /\ (subst_formula (iota m n) s))) - `<=` mnfset 0 m. -Proof. -rewrite formula_fv_nexists fsubDset fsubUset. -rewrite !(fsubset_trans (fv_subst_formula mnfset_key _ _)); -by rewrite ?fsubsetUl // seq_fset_cat fsubset_refl. -Qed. - -Definition SAimset (f : {SAset F ^ (n + m)}) (s : {SAset F^n}) := - \pi_{SAset F^m} (MkFormulan (nvar_SAimset f s)). - Lemma ex_yE (f : {formula_(n + m) F}) (t : 'rV[F]_n) : reflect (exists (u : 'rV[F]_m), rcf_sat (ngraph (row_mx t u)) f) (ex_y f t). Proof. @@ -724,11 +1026,11 @@ HB.instance Definition SAfun_of_choiceType := Choice.copy {SAfun} SAfun. Lemma SAfun_func (f : {SAfun}) (x : 'rV[F]_n) (y1 y2 : 'rV[F]_m) : row_mx x y1 \in SAgraph f -> row_mx x y2 \in SAgraph f -> y1 = y2. -Proof. by apply: SAfuncE; case: f; move => /= [f h /andP [h1 h2]]. Qed. +Proof. by apply: inSAfunc; case: f; move => /= [f h /andP [h1 h2]]. Qed. Lemma SAfun_tot (f : {SAfun}) (x : 'rV[F]_n) : exists (y : 'rV[F]_m), row_mx x y \in SAgraph f. -Proof. by apply: SAtotE; case: f; move => /= [f h /andP [h1 h2]]. Qed. +Proof. by apply: inSAtot; case: f; move => /= [f h /andP [h1 h2]]. Qed. Definition SAfun_to_fun (f : SAfun) : 'rV[F]_n -> 'rV[F]_m := fun x => proj1_sig (sigW (SAfun_tot f x)). @@ -746,115 +1048,46 @@ Arguments SAfunc {F n m}. Arguments SAtot {F n m}. Notation "{ 'SAfun' T }" := (SAfun_of (Phant T)) : type_scope. -Section SASetTheory. - -Variable F : rcfType. - -Lemma in_SAset_bottom (m : nat) (x : 'rV[F]_m) : - x \in (@SAset_bottom F m) = false. -Proof. by rewrite pi_form. Qed. - -Lemma SAset1_neq0 (n : nat) (x : 'rV[F]_n) : (SAset1 x) != (@SAset_bottom F n). -Proof. -apply/negP; move/SAsetP/(_ x) => h. -by move: h; rewrite inSAset1 eqxx pi_form. -Qed. - -Lemma SAemptyP (n : nat) (x : 'rV[F]_n) : x \notin (@SAset_bottom F n). -Proof. by rewrite in_SAset_bottom. Qed. - -Lemma inSAset1B (n : nat) (x y : 'rV[F]_n) : (x \in SAset1 y) = (x == y). -Proof. by rewrite inSAset1. Qed. - -Lemma sub_SAset1 (n : nat) (x : 'rV[F]_n) (s : {SAset F^n}) : - (SAset1 x <= s)%O = (x \in s). -Proof. -apply: (sameP (rcf_satP _ _)). -apply: (equivP _ (nforallP _ _ _)). -apply: (iffP idP). - move=> h t; rewrite cat0s /=. - move/rcf_satP : h => holds_s. - move/holds_tuple; rewrite inSAset1 => /eqP eq_x. - by move: holds_s; rewrite -eq_x ngraph_tnth. -move/(_ (ngraph x)). -rewrite cat0s inE => /rcf_satP. -rewrite simp_rcf_sat => /implyP; apply. -apply/rcf_satP/holds_tuple; rewrite inSAset1; apply/eqP/rowP => i. -by rewrite mxE (tnth_nth 0) nth_ngraph. -Qed. - -Lemma non_empty : forall (n : nat) (s : {SAset F^n}), - ((@SAset_bottom F n) < s)%O -> {x : 'rV[F]_n | x \in s}. -Proof. -move=> a s /andP [bot_neq_s _]. -move: s bot_neq_s; apply: quotW => /= f; rewrite eqmodE /=. -move=> /rcf_satP/n_nforall_formula/nexistsP P. -apply: sigW; move: P => [x hx] /=; exists (\row_(i < a) x`_i). -rewrite inE ngraph_nth rcf_sat_repr_pi. -by move/rcf_satP: hx; rewrite cat0s !simp_rcf_sat; case: rcf_sat. -Qed. +Section SAfunTheory. -Lemma le_sub : forall (n : nat) (s1 s2 : {SAset F^n}), - (forall (x : 'rV[F]_n), x \in s1 -> x \in s2) -> (s1 <= s2)%O. -Proof. -move=> a s1 s2 sub12; apply/rcf_satP/nforallP => t. -rewrite cat0s /= => /rcf_satP s1_sat; apply/rcf_satP. -by move/(_ ((\row_(i < a) t`_i))): sub12; rewrite !inE ngraph_nth => ->. -Qed. +Variable (F : rcfType) (n m : nat). -Lemma SAunion : forall (n : nat) (x : 'rV[F]_n) (s1 s2 : {SAset F^n}), - (x \in SAset_join s1 s2) = (x \in s1) || (x \in s2). -Proof. -move=> n x s1 s2. -rewrite /SAset_join pi_form !inE. -apply/idP/idP. -move/rcf_satP => /=. -by move=> [l|r]; apply/orP; [left|right]; apply/rcf_satP. -by move/orP => [l|r]; apply/rcf_satP; [left|right]; apply/rcf_satP. -Qed. - -Lemma in_graph_SAfun (n m : nat) (f : {SAfun F^n -> F^m}) (x : 'rV[F]_n) : +Lemma inSAgraph (f : {SAfun F^n -> F^m}) (x : 'rV[F]_n) : row_mx x (f x) \in SAgraph f. Proof. by rewrite /SAfun_to_fun; case: ((sigW (SAfun_tot f x))) => y h. Qed. -Lemma in_SAimset (m n : nat) (x : 'rV[F]_n) +Definition SAimset (f : {SAset F ^ (n + m)}) (s : {SAset F^n}) : {SAset F^m} := + [set | nquantify m n Exists ((subst_formula ((iota m n) + ++ (iota O m)) f) /\ (subst_formula (iota m n) s)) ]. + +Lemma inSAimset (x : 'rV[F]_n) (s : {SAset F^n}) (f : {SAfun F^n -> F^m}) : x \in s -> f x \in SAimset f s. Proof. rewrite pi_form /= => h. -have hsiz : m = size (ngraph (f x)) by rewrite size_ngraph. -rewrite [X in nquantify X _ _]hsiz. -apply/rcf_satP/nexistsP. +apply/rcf_satP/holds_subst. +rewrite -[map _ _]cats0 subst_env_iota_catl ?size_ngraph //. +rewrite -[X in nquantify X _ _](size_ngraph (f x)); apply/nexistsP. exists (ngraph x). -split; last first. -+ apply/holds_subst. - move: h; rewrite inE. - move/rcf_satP. - rewrite -[ngraph (f x) ++ ngraph x]cats0. +split; apply/holds_subst; move: h; rewrite inE => /rcf_satP hs; last first. ++ rewrite -[_ ++ ngraph x]cats0. by rewrite -catA subst_env_iota // size_ngraph. -+ apply/holds_subst. - move: h; rewrite inE. - move/rcf_satP => h. - rewrite subst_env_cat subst_env_iota_catl ?size_ngraph //. - rewrite -[ngraph (f x) ++ ngraph x]cats0. ++ rewrite subst_env_cat subst_env_iota_catl ?size_ngraph //. + rewrite -[_ ++ ngraph x]cats0. rewrite -catA subst_env_iota ?size_ngraph //. - move: (in_graph_SAfun f x); rewrite inE. - by move/rcf_satP; rewrite ngraph_cat. + by move: (inSAgraph f x); rewrite inE => /rcf_satP; rewrite ngraph_cat. Qed. -Lemma SAimsetP (n m: nat) (f : {SAfun F^n -> F^m}) +Lemma SAimsetP (f : {SAfun F^n -> F^m}) (s : {SAset F^n}) (y : 'rV[F]_m) : reflect (exists2 x : 'rV[F]_n, x \in s & y = f x) (y \in (SAimset f s)). Proof. -apply: (iffP idP); last by move=> [x h] ->; apply: in_SAimset. -rewrite /SAimset pi_form. -move/rcf_satP. -rewrite /= -[X in nquantify X _ _ _](size_ngraph y). -move/nexistsP => [t] /=. -rewrite !holds_subst subst_env_cat; move => [h1 h2]. +apply: (iffP idP) => [/SAin_setP|[x h]->]; last exact: inSAimset. +rewrite -[X in nquantify X _ _ _](size_ngraph y) => /nexistsP [t] /=. +rewrite !holds_subst subst_env_cat => -[h1 h2]. exists (\row_(i < n) t`_i). + rewrite inE ngraph_nth. apply/rcf_satP. @@ -869,61 +1102,127 @@ exists (\row_(i < n) t`_i). by rewrite inE ngraph_cat ngraph_nth; apply/rcf_satP. Qed. -(* -Definition SAset_setMixin := - SET.Semiset.Mixin SAemptyP inSAset1B sub_SAset1 non_empty - le_sub SAunion SAimsetP. - -Notation SemisetType set m := - (@SET.Semiset.pack _ _ set _ _ m _ _ (fun => id) _ id). -Canonical SAset_setType := SemisetType (fun n => {SAset F^n}) SAset_setMixin. - *) -(* Import SET.Theory. *) -(* Definition SAset_setMixin := *) -(* SemisetMixin SAemptyP inSAset1B sub_SAset1 non_empty *) -(* le_sub SAunion SAimsetP. *) - -(* Notation SemisetType set m := *) -(* (@SET.Semiset.pack _ _ set _ _ m _ _ (fun => id) _ id). *) - -Lemma in_SAfun (n m : nat) (f : {SAfun F^n -> F^m}) +Lemma inSAfun (f : {SAfun F^n -> F^m}) (x : 'rV[F]_n) (y : 'rV[F]_m): (f x == y) = (row_mx x y \in SAgraph f). Proof. -apply/eqP/idP => [<- | h]; first by rewrite in_graph_SAfun. -exact: (SAfun_func (in_graph_SAfun _ _)). +apply/eqP/idP => [<- | h]; first by rewrite inSAgraph. +exact: (SAfun_func (inSAgraph _ _)). Qed. -Lemma SAfunE (n m : nat) (f1 f2 : {SAfun F^n -> F^m}) : +Lemma SAfunE (f1 f2 : {SAfun F^n -> F^m}) : reflect (f1 =1 f2) (f1 == f2). Proof. apply: (iffP idP); first by move/eqP ->. move=> h; apply/SAsetP => x. -by rewrite -(cat_ffun_id x) -!in_SAfun h. +by rewrite -(cat_ffun_id x) -!inSAfun h. Qed. -Definition max_abs (k : nat) (x : 'rV[F]_k) := - \big[maxr/0]_(i < k) `|(x ord0 i)|. +Definition SAepigraph (f : {SAfun F^n -> F^1}) : {SAset F^(n + 1)} := + [set | nquantify (n + 1) 1 Exists ((subst_formula ((iota 0 n) + ++ [:: n.+1; n]) f) /\ ('X_n.+1 <% 'X_n)) ]. -Definition distance (k : nat) (x y : 'rV[F]_k) := max_abs (x - y). +Definition SAhypograph (f : {SAfun F^n -> F^1}) : {SAset F^(n + 1)} := + [set | nquantify (n + 1) 1 Exists ((subst_formula ((iota 0 n) + ++ [:: n.+1; n]) f) /\ ('X_n <% 'X_n.+1)) ]. -Lemma max_vectP (k : nat) (x : 'rV[F]_k) (i :'I_k) : x ord0 i <= max_abs x. -Proof. -rewrite /max_abs; move: x i. -elim: k => [x [i lt_i0]| k ihk x i] //. -rewrite big_ord_recl le_max. -have [->|] := eqVneq i ord0; first by rewrite ler_norm. -rewrite eq_sym => neq_i0; apply/orP; right. -move: (unlift_some neq_i0) => /= [j lift_0j _]. -move: (ihk (\row_(i < k) x ord0 (lift ord0 i)) j); rewrite mxE /=. -rewrite (eq_big predT (fun i => `|x ord0 (lift ord0 i)|)) //. - by rewrite -lift_0j. -by move=> l _; rewrite mxE. -Qed. +End SAfunTheory. -Definition max_vec (v : seq nat) (n : nat) : formula F := - ((\big[Or/False]_(i < size v) ('X_n == 'X_(nth O v i))) /\ - (\big[And/True]_(i < size v) ('X_(nth O v i) <=% 'X_n)))%oT. +Lemma inSAepigraph (F : rcfType) (n : nat) (f : {SAfun F^n -> F^1}) (x : 'rV[F]_(n + 1)) : + (x \in SAepigraph f) = (f (lsubmx x) ord0 ord0 < rsubmx x ord0 ord0). +Proof. +move: (lsubmx x) (rsubmx x) (hsubmxK x) => l r <- {x}. +apply/SAin_setP/idP; rewrite -[X in nquantify X _ _](size_ngraph (row_mx l r)). + move=> /nexistsP [y] /= [] /holds_subst. + rewrite nth_cat size_map size_enum_ord {11 20}addn1 ltnn subnn. + rewrite nth_cat size_map size_enum_ord {11}addn1 leqnn (nth_map (unsplit (inr ord0))) ?size_enum_ord ?addn1//. + have {26}->: n = @unsplit n 1 (inr ord0) by rewrite /= addn0. + rewrite nth_ord_enum mxE unsplitK ngraph_cat -catA subst_env_cat. + rewrite subst_env_iota_catl ?size_ngraph//= !nth_cat size_map size_enum_ord. + rewrite ltnNge leqnSn/= subSnn size_ngraph/= ltnn !subnn/= (nth_map ord0) ?size_enum_ord//. + rewrite -[X in nth ord0 _ X]/(@ord0 1 : nat) (@nth_ord_enum 1 ord0 ord0). + move=> /holds_take; rewrite take_cat size_ngraph ltnNge {1}addn1 leqnSn/=. + rewrite subDnCA// subnn/= => hf; congr (_ < _). + transitivity ((\row_i tnth y i) ord0 ord0); first by rewrite mxE (tnth_nth 0). + congr (_ _ ord0 ord0); apply/esym/eqP => /=; rewrite inSAfun. + apply/rcf_satP; move: hf; congr holds; apply/(eq_from_nth (x0:=0)) => [|i]. + by rewrite size_cat size_map size_enum_ord size_ngraph. + rewrite size_cat size_map size_enum_ord /= => ilt. + have i0: 'I_(n+1) by rewrite addn1; exact: ord0. + rewrite (nth_map (Ordinal ilt)) ?size_enum_ord// -[i]/(Ordinal ilt : nat) nth_ord_enum. + rewrite mxE -{1}(splitK (Ordinal ilt)); case: (split _) => j. + rewrite nth_cat size_map size_enum_ord ltn_unsplit/=. + by rewrite (nth_map j) ?size_enum_ord// nth_ord_enum /=. + rewrite nth_cat/= size_ngraph ltnNge leq_addr/= subDnCA// subnn addn0. + by case: j; case=> //= jlt; rewrite mxE (tnth_nth 0). +move=> fx; apply/nexistsP; exists (in_tuple [:: f l ord0 ord0]). +split; last first. + rewrite /= !nth_cat size_ngraph {1 10 11}addn1 ltnn leqnn subnn/=. + rewrite (nth_map (unsplit (inr ord0))) ?size_enum_ord ?addn1//. + have {12}->: n = @unsplit n 1 (inr ord0) by rewrite /= addn0. + by rewrite nth_ord_enum mxE unsplitK. +apply/holds_subst; rewrite ngraph_cat -catA subst_env_cat. +rewrite subst_env_iota_catl ?size_ngraph//= !nth_cat !size_ngraph ltnNge. +rewrite leqnSn/= subSnn/= ltnn subnn/=. +apply/holds_take; rewrite take_cat size_ngraph ltnNge leq_addr/=. +rewrite subDnCA// subnn/=. +have ->: (ngraph l) ++ [:: f l ord0 ord0] = ngraph (row_mx l (f l)). + rewrite ngraph_cat; congr (_ ++ _); apply/(eq_from_nth (x0:=0)) => [|/=]. + by rewrite size_ngraph. + case=> //= _; rewrite (nth_map ord0) ?size_enum_ord//. + by rewrite -[X in nth _ _ X]/(@ord0 1 : nat) (@nth_ord_enum 1 ord0 ord0). +by move: (inSAfun f l (f l)); rewrite eqxx => /esym/rcf_satP. +Qed. + +Lemma inSAhypograph (F : rcfType) (n : nat) (f : {SAfun F^n -> F^1}) (x : 'rV[F]_(n + 1)) : + (x \in SAhypograph f) = (rsubmx x ord0 ord0 < f (lsubmx x) ord0 ord0). +Proof. +move: (lsubmx x) (rsubmx x) (hsubmxK x) => l r <- {x}. +apply/SAin_setP/idP; rewrite -[X in nquantify X _ _](size_ngraph (row_mx l r)). + move=> /nexistsP [y] /= [] /holds_subst. + rewrite !nth_cat size_map size_enum_ord {11 21 30}addn1 leqnn ltnn subnn. + rewrite (nth_map (unsplit (inr ord0))) ?size_enum_ord ?addn1//. + have {26}->: n = @unsplit n 1 (inr ord0) by rewrite /= addn0. + rewrite nth_ord_enum mxE unsplitK ngraph_cat -catA subst_env_cat. + rewrite subst_env_iota_catl ?size_ngraph//= !nth_cat size_map size_enum_ord. + rewrite ltnNge leqnSn/= subSnn size_ngraph/= ltnn !subnn/= (nth_map ord0) ?size_enum_ord//. + rewrite -[X in nth ord0 _ X]/(@ord0 1 : nat) (@nth_ord_enum 1 ord0 ord0). + move=> /holds_take; rewrite take_cat size_ngraph ltnNge {1}addn1 leqnSn/=. + rewrite subDnCA// subnn/= => hf; congr (_ < _). + transitivity ((\row_i tnth y i) ord0 ord0); first by rewrite mxE (tnth_nth 0). + congr (_ _ ord0 ord0); apply/esym/eqP => /=; rewrite inSAfun. + apply/rcf_satP; move: hf; congr holds; apply/(eq_from_nth (x0:=0)) => [|i]. + by rewrite size_cat size_map size_enum_ord size_ngraph. + rewrite size_cat size_map size_enum_ord /= => ilt. + have i0: 'I_(n+1) by rewrite addn1; exact: ord0. + rewrite (nth_map (Ordinal ilt)) ?size_enum_ord// -[i]/(Ordinal ilt : nat) nth_ord_enum. + rewrite mxE -{1}(splitK (Ordinal ilt)); case: (split _) => j. + rewrite nth_cat size_map size_enum_ord ltn_unsplit/=. + by rewrite (nth_map j) ?size_enum_ord// nth_ord_enum /=. + rewrite nth_cat/= size_ngraph ltnNge leq_addr/= subDnCA// subnn addn0. + by case: j; case=> //= jlt; rewrite mxE (tnth_nth 0). +move=> fx; apply/nexistsP; exists (in_tuple [:: f l ord0 ord0]). +split; last first. + rewrite /= !nth_cat size_ngraph {1 11 20}addn1 ltnn leqnn subnn/=. + rewrite (nth_map (unsplit (inr ord0))) ?size_enum_ord ?addn1//. + have {11}->: n = @unsplit n 1 (inr ord0) by rewrite /= addn0. + by rewrite nth_ord_enum mxE unsplitK. +apply/holds_subst; rewrite ngraph_cat -catA subst_env_cat. +rewrite subst_env_iota_catl ?size_ngraph//= !nth_cat !size_ngraph ltnNge. +rewrite leqnSn/= subSnn/= ltnn subnn/=. +apply/holds_take; rewrite take_cat size_ngraph ltnNge leq_addr/=. +rewrite subDnCA// subnn/=. +have ->: (ngraph l) ++ [:: f l ord0 ord0] = ngraph (row_mx l (f l)). + rewrite ngraph_cat; congr (_ ++ _); apply/(eq_from_nth (x0:=0)) => [|/=]. + by rewrite size_ngraph. + case=> //= _; rewrite (nth_map ord0) ?size_enum_ord//. + by rewrite -[X in nth _ _ X]/(@ord0 1 : nat) (@nth_ord_enum 1 ord0 ord0). +by move: (inSAfun f l (f l)); rewrite eqxx => /esym/rcf_satP. +Qed. + +Section SAfunOps. + +Variable (F : rcfType). Definition abs (i j : nat) : formula F := ((('X_j == 'X_i) \/ ('X_j == - 'X_i)) /\ (0 <=% 'X_j))%oT. @@ -1052,7 +1351,7 @@ apply/rcf_satP/holds_subst. rewrite ?nth_iota // add0n /= !nth_cat size_tuple ltn_ord. rewrite -ltn_subRL subnn ltn0. (* this line can be used earlier in the code *) rewrite addnC addnK. -move : (in_graph_SAfun f (const_mx t`_i)); rewrite inE. +move : (inSAgraph f (const_mx t`_i)); rewrite inE. move/rcf_satP; apply: eqn_holds => j y. rewrite !mxE /=. rewrite (nth_map 0); last by rewrite size_enum_ord ltn_ord. @@ -1128,28 +1427,28 @@ apply: (iffP idP); last first. - by rewrite size_map size_enum_ord. - by rewrite size_map size_enum_ord. rewrite -[t]ngraph_tnth -!ngraph_cat. - move/holds_ngraph; rewrite -in_SAfun; move/eqP ->. - by move/holds_ngraph; rewrite -in_SAfun; move/eqP ->. + move/holds_ngraph; rewrite -inSAfun; move/eqP ->. + by move/holds_ngraph; rewrite -inSAfun; move/eqP ->. + move/eqP => eq_gfu_v. exists (ngraph (f u)). split; apply/holds_subst; rewrite subst_env_cat. - rewrite -catA subst_env_iota_catl; last by rewrite size_map size_enum_ord. rewrite catA subst_env_iota_catr ?size_tuple ?card_ord // -ngraph_cat. - by apply/holds_ngraph; apply: in_graph_SAfun. + by apply/holds_ngraph; apply: inSAgraph. - rewrite subst_env_iota_catr ?size_tuple ?card_ord //. rewrite -catA subst_env_iota; last 2 first. by rewrite size_map size_enum_ord. by rewrite size_map size_enum_ord. rewrite -ngraph_cat; apply/holds_ngraph; rewrite -eq_gfu_v. - exact: in_graph_SAfun. + exact: inSAgraph. Qed. Fact SAfun_SAcomp (m n p : nat) (f : SAfun F m n) (g : SAfun F n p) : (SAcomp_graph f g \in SAfunc) && (SAcomp_graph f g \in SAtot). Proof. apply/andP; split. - by apply/SAfuncE => x y1 y2; rewrite !SAcomp_graphP; move=> /eqP-> /eqP->. -by apply/SAtotE => x; exists (g (f x)); rewrite SAcomp_graphP. + by apply/inSAfunc => x y1 y2; rewrite !SAcomp_graphP; move=> /eqP-> /eqP->. +by apply/inSAtot => x; exists (g (f x)); rewrite SAcomp_graphP. Qed. Definition SAcomp (m n p : nat) (f : SAfun F m n) (g : SAfun F n p) := @@ -1159,9 +1458,22 @@ Lemma SAcompP (m n p : nat) (f : SAfun F m n) (g : SAfun F n p) : SAcomp f g =1 g \o f. Proof. move=> x; apply/eqP; rewrite eq_sym -SAcomp_graphP. -by move: (in_graph_SAfun (SAcomp f g) x). +by move: (inSAgraph (SAcomp f g) x). +Qed. + +Definition SAfun0_graph n m : {SAset F^(n + m)%N} := + SAset_cast (n + m) (SAsetT F n). + +Lemma SAfun_SAfun0 n m : + (SAfun0_graph n m \in SAfunc) && (SAfun0_graph n m \in SAtot). +Proof. +apply/andP; split. + by apply/inSAfunc => x y1 y2; rewrite /SAfun0_graph !inSAset_castnD !row_mxKl !row_mxKr => /andP[_] /eqP + /andP[_] /eqP ->. +by apply/inSAtot => x; exists 0%R; rewrite /SAfun0_graph inSAset_castnD inSAsetT row_mxKr eqxx. Qed. +Definition SAfun0 n m := MkSAfun (SAfun_SAfun0 n m). + Definition join_formula (m n p : nat) (f : {SAfun F^m -> F^n}) (g : {SAfun F^m -> F^p}) : formula F := (repr (val f)) /\ (subst_formula (iota 0 m ++ iota (m+n) p) (repr (val g))). @@ -1194,24 +1506,24 @@ apply: (iffP eqP) => [|/= [/holds_take + /holds_subst]]; rewrite catA -ngraph_cat subst_env_iota_catr ?size_ngraph//. rewrite take_size_cat ?size_ngraph// -ngraph_cat. move=> /holds_ngraph + /holds_ngraph. - by rewrite -!in_SAfun => /eqP -> /eqP ->. + by rewrite -!inSAfun => /eqP -> /eqP ->. move=> /[dup] /(congr1 lsubmx) + /(congr1 rsubmx). rewrite !row_mxKl !row_mxKr => <- <-. split. rewrite catA -ngraph_cat; apply/holds_take. rewrite take_size_cat ?size_ngraph//. - exact/holds_ngraph/in_graph_SAfun. + exact/holds_ngraph/inSAgraph. apply/holds_subst; rewrite subst_env_cat subst_env_iota_catl ?size_ngraph//. rewrite catA -ngraph_cat subst_env_iota_catr ?size_ngraph// -ngraph_cat. -exact/holds_ngraph/in_graph_SAfun. +exact/holds_ngraph/inSAgraph. Qed. Fact SAfun_SAjoin (m n p : nat) (f : {SAfun F^m -> F^n}) (g : {SAfun F^m -> F^p}) : (SAjoin_graph f g \in SAfunc) && (SAjoin_graph f g \in SAtot). Proof. apply/andP; split. - by apply/SAfuncE => x y1 y2; rewrite !SAjoin_graphP => /eqP <- /eqP. -by apply/SAtotE => x; exists (row_mx (f x) (g x)); rewrite SAjoin_graphP. + by apply/inSAfunc => x y1 y2; rewrite !SAjoin_graphP => /eqP <- /eqP. +by apply/inSAtot => x; exists (row_mx (f x) (g x)); rewrite SAjoin_graphP. Qed. Definition SAjoin (m n p : nat) (f : {SAfun F^m -> F^n}) (g : {SAfun F^m -> F^p}) := @@ -1219,85 +1531,111 @@ Definition SAjoin (m n p : nat) (f : {SAfun F^m -> F^n}) (g : {SAfun F^m -> F^p} Lemma SAjoinP (m n p : nat) (f : {SAfun F^m -> F^n}) (g : {SAfun F^m -> F^p}) (x : 'rV[F]_m) : SAjoin f g x = row_mx (f x) (g x). -Proof. by apply/eqP; rewrite eq_sym -SAjoin_graphP; apply/in_graph_SAfun. Qed. +Proof. by apply/eqP; rewrite eq_sym -SAjoin_graphP; apply/inSAgraph. Qed. -Definition add_formula : formula F := ('X_2 == 'X_0 + 'X_1)%oT. +Definition add_formula (p : nat) : formula F := + (\big[And/True]_(i : 'I_p) ('X_(i + 2 * p) == 'X_i + 'X_(i + p)))%oT. -Lemma nvar_add_formula : nvar 3 add_formula. +Lemma nvar_add_formula p : nvar (p + p + p) (add_formula p). Proof. -apply/fsubsetP => x xf; rewrite seq_fsetE mem_iota /= add0n. -by move: xf => /fset1UP; case=> [-> //|] /fset2P; case=> ->. +apply/fsubsetP => x; rewrite formula_fv_bigAnd => /bigfcupP [i _] /fset1UP. +by case=> [->|/fset2P [|] ->]; + rewrite mnfsetE /= add0n 1?mulSn ?mul1n ?addnA ?ltn_add2r// -[i.+1]add0n; + apply/leq_add. Qed. -Definition SAadd_graph := \pi_{SAset F^3} (MkFormulan (nvar_add_formula)). +Definition SAadd_graph p := + \pi_{SAset F^(p + p + p)} (MkFormulan (nvar_add_formula p)). -Lemma SAadd_graphP (u : 'rV[F]_2) (v : 'rV[F]_1) : - (row_mx u v \in SAadd_graph) = (v 0 0 == u 0 0 + u 0 1)%R. +Lemma SAadd_graphP p (u : 'rV[F]_(p + p)) (v : 'rV[F]_p) : + (row_mx u v \in SAadd_graph p) = (v == lsubmx u + rsubmx u)%R. Proof. +rewrite rowPE. apply/(sameP (rcf_satP _ _))/(equivP _ (iff_sym (holds_repr_pi _ _))) => /=. -rewrite (nth_map ord0) ?size_enum_ord// (nth_ord_enum _ 2). -rewrite (nth_map ord0) ?size_enum_ord// (nth_ord_enum _ 0). -rewrite (nth_map ord0) ?size_enum_ord// (nth_ord_enum _ 1). -rewrite !(@cat_ffunE _ 0 2 _ 1) /=. -rewrite (nth_map ord0) ?size_enum_ord// (nth_ord_enum _ 0). -rewrite (nth_map ord0) ?size_enum_ord// (nth_ord_enum _ 0). -rewrite (nth_map ord0) ?size_enum_ord// (nth_ord_enum _ 1). -exact/eqP. -Qed. - -Fact SAfun_SAadd : - (SAadd_graph \in @SAfunc _ 2 1) && (SAadd_graph \in @SAtot _ 2 1). +apply/(equivP _ (iff_sym (holdsAnd _ _ _ _)))/forallPP => /= i. +rewrite mem_index_enum mul2n -addnn addnA. +rewrite -[(i + p + p)%N]addnA [(i + _)%N]addnC. +rewrite (nth_map (unsplit (inr i))) ?size_enum_ord ?rshift_subproof//. +rewrite (nth_ord_enum _ (rshift (p + p)%N i)) row_mxEr. +have {1}->: i = lshift p i :> nat by []. +rewrite (nth_map (unsplit (inr i))) ?size_enum_ord ?lshift_subproof//. +rewrite (nth_ord_enum _ (lshift p (lshift p i))) row_mxEl. +have ->: (i + p)%N = rshift p i :> nat by rewrite addnC. +rewrite (nth_map (unsplit (inr i))) ?size_enum_ord ?lshift_subproof//. +rewrite (nth_ord_enum _ (lshift p (rshift p i))) row_mxEl !mxE. +by apply/(iffP eqP) => // /(_ Logic.eq_refl) /(_ Logic.eq_refl). +Qed. + +Fact SAfun_SAadd p : + (SAadd_graph p \in @SAfunc _ (p + p) p) + && (SAadd_graph p \in @SAtot _ (p + p) p). Proof. apply/andP; split. - apply/SAfuncE => x y1 y2; rewrite !SAadd_graphP => /eqP y1E /eqP y2E. - by apply/rowP => i; rewrite ord1 y2E. -apply/SAtotE => x; exists (\row_i (x 0 0 + x 0 1))%R. -by rewrite SAadd_graphP mxE. + by apply/inSAfunc => x y1 y2; rewrite !SAadd_graphP => /eqP -> /eqP. +apply/inSAtot => x; exists (lsubmx x + rsubmx x)%R. +by rewrite SAadd_graphP eqxx. Qed. -Definition SAadd := MkSAfun SAfun_SAadd. +Definition SAadd p := MkSAfun (SAfun_SAadd p). -Definition SAfun_add (n : nat) (f g : {SAfun F^n -> F^1}) := - SAcomp (SAjoin f g) SAadd. +Definition SAfun_add (n p : nat) (f g : {SAfun F^n -> F^p}) := + SAcomp (SAjoin f g) (SAadd p). -Definition opp_formula : formula F := ('X_1 == - 'X_0)%oT. +Definition opp_formula (p : nat) : formula F := + (\big[And/True]_(i : 'I_p) ('X_(p + i) == - 'X_i))%oT. -Lemma nvar_opp_formula : nvar 2 opp_formula. +Lemma nvar_opp_formula p : nvar (p + p) (opp_formula p). Proof. -apply/fsubsetP => x xf; rewrite seq_fsetE mem_iota /= add0n. -by move: xf => /fset2P; case=> ->. +apply/fsubsetP => x; rewrite formula_fv_bigAnd => /bigfcupP [i _] /fset2P. +case=> ->; rewrite seq_fsetE mem_iota /= add0n; last exact/ltn_addl. +by rewrite ltn_add2l. Qed. -Definition SAopp_graph := \pi_{SAset F^2} (MkFormulan (nvar_opp_formula)). +Definition SAopp_graph p := + \pi_{SAset F^(p + p)} (MkFormulan (nvar_opp_formula p)). -Lemma SAopp_graphP (u v : 'rV[F]_1) : - (row_mx u v \in SAopp_graph) = (v 0 0 == - u 0 0)%R. +Lemma SAopp_graphP p (u v : 'rV[F]_p) : + (row_mx u v \in SAopp_graph p) = (v == - u)%R. Proof. +rewrite rowPE. apply/(sameP (rcf_satP _ _))/(equivP _ (iff_sym (holds_repr_pi _ _))) => /=. -rewrite (nth_map ord0) ?size_enum_ord// (nth_ord_enum _ 1). -rewrite (nth_map ord0) ?size_enum_ord// (nth_ord_enum _ 0). -rewrite !(@cat_ffunE _ 0 1 _ 1) /=. -rewrite (nth_map ord0) ?size_enum_ord// (nth_ord_enum _ 0). -rewrite (nth_map ord0) ?size_enum_ord// (nth_ord_enum _ 0). -exact/eqP. +apply/(equivP _ (iff_sym (holdsAnd _ _ _ _)))/forallPP => /= i. +rewrite mem_index_enum. +rewrite (nth_map (unsplit (inr i))) ?size_enum_ord ?rshift_subproof//. +rewrite (nth_ord_enum _ (rshift p i)) row_mxEr mxE. +rewrite (nth_map (unsplit (inr i))) ?size_enum_ord ?lshift_subproof//. +rewrite (nth_ord_enum _ (lshift p i)) row_mxEl. +by apply/(iffP eqP) => // /(_ Logic.eq_refl) /(_ Logic.eq_refl). Qed. -Fact SAfun_SAopp : - (SAopp_graph \in @SAfunc _ 1 1) && (SAopp_graph \in @SAtot _ 1 1). +Fact SAfun_SAopp p : + (SAopp_graph p \in @SAfunc _ p p) && (SAopp_graph p \in @SAtot _ p p). Proof. apply/andP; split. - apply/SAfuncE => x y1 y2; rewrite !SAopp_graphP => /eqP y1E /eqP y2E. - by apply/rowP => i; rewrite ord1 y2E. -apply/SAtotE => x; exists (\row_i (- x 0 0))%R. -by rewrite SAopp_graphP mxE. + by apply/inSAfunc => x y1 y2; rewrite !SAopp_graphP => /eqP -> /eqP. +by apply/inSAtot => x; exists (-x)%R; rewrite SAopp_graphP eqxx. Qed. -Definition SAopp := MkSAfun SAfun_SAopp. +Definition SAopp p := MkSAfun (SAfun_SAopp p). -Definition SAfun_sub (n : nat) (f g : {SAfun F^n -> F^1}) := - SAcomp (SAjoin f (SAcomp g SAopp)) SAadd. +Definition SAfun_sub (n p : nat) (f g : {SAfun F^n -> F^p}) := + SAcomp (SAjoin f (SAcomp g (SAopp p))) (SAadd p). Definition SAfun_lt (n : nat) (f g : {SAfun F^n -> F^1}) := - SAsub (SAgraph (SAfun_sub f g)) (SAset_prod (SAset_top F n) (SAset_pos F)). + SAgraph (SAfun_sub f g) :<=: (SAsetT F n) :*: (SAset_pos F). + +Definition partition_of_graphs (n m : nat) (xi : m.-tuple {SAfun F^n -> F^1}) : {fset {SAset F^(n + 1)%N}} := + (\big[@SAsetI F (n + 1)/SAset0 F (n + 1)]_i SAepigraph (tnth xi i)) + |` ((\big[@SAsetI F (n + 1)/SAset0 F (n + 1)]_i SAhypograph (tnth xi i)) + |` ([fset SAgraph f | f in tval xi] + `|` [fset SAepigraph (nth (SAfun0 n 1) xi (val i)) :&: SAhypograph (nth (SAfun0 n 1) xi (val i).+1) | i in 'I_m.-1])). + +Definition partition_of_graphs_above n (s : {SAset F^n}) (m : nat) (xi : m.-tuple {SAfun F^n -> F^1}) : {fset {SAset F^(n + 1)%N}} := + [fset x :&: (s :*: SAsetT F 1) | x in partition_of_graphs xi]. + +Definition SAset_path_connected n (s : {SAset F^n}) := + {in s &, forall x y, exists xi : {SAfun F^1 -> F^n}, xi 0 = x /\ xi 1 = y}. + +End SAfunOps. -End SASetTheory. +Search root. diff --git a/subresultant.v b/subresultant.v index a587970..4f37d8f 100644 --- a/subresultant.v +++ b/subresultant.v @@ -106,7 +106,7 @@ case: odd; rewrite /= (mulN1r, mul1r) ?sgrN. by rewrite variationrr mulr0n. Qed. -(* Notation 4.31. from BPR *) +(* Notation 4.30. from BPR *) (* Warning! must test if n is odd *) Fixpoint pmv_aux (R : numDomainType) (a : R) (n : nat) (s : seq R) := if s is b :: s then @@ -121,7 +121,7 @@ Notation nonzero := (forall x, x != 0). Fixpoint permanences (R : numDomainType) (s : seq R) : nat := (if s is a :: q then (a * (head 0 q) > 0)%R + permanences q else 0)%N. -(* First remark about Notation 4.31 in BPR *) +(* First remark about Notation 4.30 in BPR *) Lemma nonzero_pmvE (R : rcfType) (s : seq R) : {in s, nonzero} -> pmv s = (permanences s)%:Z - (changes s)%:Z. Proof. @@ -144,7 +144,7 @@ have [->|p_neq0]:= eqVneq p 0; first by rewrite lead_coef0 mul0r mulr0. by rewrite polySpred //= negbK addbN addbb mulN1r oppr_lt0. Qed. -(* Second remark about Notation 4.31 in BPR *) +(* Second remark about Notation 4.30 in BPR *) Lemma pmv_changes_poly (R : rcfType) (sp : seq {poly R}) : {in sp, nonzero} -> (forall i, (size sp`_i.+1) = (size sp`_i).-1) -> pmv (map lead_coef sp) = changes_poly sp. @@ -536,5 +536,16 @@ have -> : ((size p).-1 - (size q).-1 = np - nq)%N. by rewrite addbC odd_bin2B ?leq_sub // addKb addnC. Qed. +(* Definition 2.65 from BPR *) + + +Definition jump_at (R : rcfType) (p q : {poly R}) (x : R) := + if even (multiplicity x q - multiplicity x p) then 0 else + +Definition cauchy_index (R : rcfType) (p q : {poly R}) + (* Lemma 4.35 from BPR is cindexR_rec from qe_rcf_th, except it uses rmodp *) +Theorem pmv_subresultant (R : idomainType) (p q : {poly R}) : + size q < size p -> + pmv [seq subresultant i p q | i : 'I_(size p)] =