Library ssrcomplements
This file is part of CoqEAL, the Coq Effective Algebra Library.
(c) Copyright INRIA and University of Gothenburg.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq path.
Require Import ssralg fintype finfun perm matrix bigop zmodp mxalgebra.
Require Import choice poly polydiv mxpoly binomial.
Require Import ssralg fintype finfun perm matrix bigop zmodp mxalgebra.
Require Import choice poly polydiv mxpoly binomial.
This file contains definitions and lemmas that are generic enough that
we could try to integrate them in Math Components' library.
Definitions and theories are gathered according to the file of the
library which they could be moved to.
Set Implicit Arguments.
seq.v
Section Seq.
Section seq_Type.
Variables (T1 T2 T3 : Type) (f : T1 -> T2 -> T3).
Fixpoint zipwith (s1 : seq T1) (s2 : seq T2) :=
if s1 is x1 :: s1' then
if s2 is x2 :: s2' then f x1 x2 :: zipwith s1' s2' else [::]
else [::].
Lemma size_zipwith s1 s2 :
size (zipwith s1 s2) = minn (size s1) (size s2).
Lemma nth_zipwith x1 x2 x3 n s1 s2 :
n < minn (size s1) (size s2) ->
nth x3 (zipwith s1 s2) n = f (nth x1 s1 n) (nth x2 s2 n).
Fixpoint foldl2 (f : T3 -> T1 -> T2 -> T3) z
(s : seq T1) (t : seq T2) {struct s} :=
if s is x :: s' then
if t is y :: t' then foldl2 f (f z x y) s' t' else z
else z.
Lemma seq2_ind (P : seq T1 -> seq T2 -> Prop) : P [::] [::] ->
(forall x1 x2 s1 s2, P s1 s2 -> P (x1 :: s1) (x2 :: s2)) ->
forall s1 s2, size s1 = size s2 -> P s1 s2.
Lemma rcons_nseq k (x : T1) : rcons (nseq k x) x = nseq k.+1 x.
Lemma nseq_cat m n (x : T1) : nseq m x ++ nseq n x = nseq (m + n) x.
Lemma count_rcons P (a : T1) (l : seq T1) :
count P (rcons l a) = (P a + count P l)%N.
Lemma count_nseq P n (a : T1) : count P (nseq n a) = (n * (P a))%N.
Lemma flatten_map (g : T1 -> T2) (s : seq (seq T1)) :
map g (flatten s) = flatten (map (map g) s).
End seq_Type.
Section seq_eqType.
Variable T1 T2 : eqType.
Lemma mem_nseq i n (a : T1) : i \in nseq n a -> i = a.
Lemma undup_nil (s : seq T1) : (undup s == [::]) = (s == [::]).
Lemma mem_flatten (l : seq T1) (ss : seq (seq T1)) x :
x \in l -> l \in ss -> x \in (flatten ss).
Lemma mem_flattenP (ss : seq (seq T1)) x :
reflect (exists2 s, x \in s & s \in ss) (x \in (flatten ss)).
Lemma map_perm_eq (g : T1 -> T2) s1 s2 : injective g ->
perm_eq (map g s1) (map g s2) -> perm_eq s1 s2.
Lemma count_rem P (l : seq T1) x : x \in l ->
count P (rem x l) = if P x then (count P l).-1 else count P l.
Section seq_Type.
Variables (T1 T2 T3 : Type) (f : T1 -> T2 -> T3).
Fixpoint zipwith (s1 : seq T1) (s2 : seq T2) :=
if s1 is x1 :: s1' then
if s2 is x2 :: s2' then f x1 x2 :: zipwith s1' s2' else [::]
else [::].
Lemma size_zipwith s1 s2 :
size (zipwith s1 s2) = minn (size s1) (size s2).
Lemma nth_zipwith x1 x2 x3 n s1 s2 :
n < minn (size s1) (size s2) ->
nth x3 (zipwith s1 s2) n = f (nth x1 s1 n) (nth x2 s2 n).
Fixpoint foldl2 (f : T3 -> T1 -> T2 -> T3) z
(s : seq T1) (t : seq T2) {struct s} :=
if s is x :: s' then
if t is y :: t' then foldl2 f (f z x y) s' t' else z
else z.
Lemma seq2_ind (P : seq T1 -> seq T2 -> Prop) : P [::] [::] ->
(forall x1 x2 s1 s2, P s1 s2 -> P (x1 :: s1) (x2 :: s2)) ->
forall s1 s2, size s1 = size s2 -> P s1 s2.
Lemma rcons_nseq k (x : T1) : rcons (nseq k x) x = nseq k.+1 x.
Lemma nseq_cat m n (x : T1) : nseq m x ++ nseq n x = nseq (m + n) x.
Lemma count_rcons P (a : T1) (l : seq T1) :
count P (rcons l a) = (P a + count P l)%N.
Lemma count_nseq P n (a : T1) : count P (nseq n a) = (n * (P a))%N.
Lemma flatten_map (g : T1 -> T2) (s : seq (seq T1)) :
map g (flatten s) = flatten (map (map g) s).
End seq_Type.
Section seq_eqType.
Variable T1 T2 : eqType.
Lemma mem_nseq i n (a : T1) : i \in nseq n a -> i = a.
Lemma undup_nil (s : seq T1) : (undup s == [::]) = (s == [::]).
Lemma mem_flatten (l : seq T1) (ss : seq (seq T1)) x :
x \in l -> l \in ss -> x \in (flatten ss).
Lemma mem_flattenP (ss : seq (seq T1)) x :
reflect (exists2 s, x \in s & s \in ss) (x \in (flatten ss)).
Lemma map_perm_eq (g : T1 -> T2) s1 s2 : injective g ->
perm_eq (map g s1) (map g s2) -> perm_eq s1 s2.
Lemma count_rem P (l : seq T1) x : x \in l ->
count P (rem x l) = if P x then (count P l).-1 else count P l.
It is not the same lemma as perm_eqP. In perm_eqP
the assertion in Prop is quantified on all predicates.
Lemma count_perm_eq (s1 s2 : seq T1) :
reflect (forall x,count (xpred1 x) s1 = count (xpred1 x) s2) (perm_eq s1 s2).
reflect (forall x,count (xpred1 x) s1 = count (xpred1 x) s2) (perm_eq s1 s2).
Lemma about sorted
Lemma sorted_trans (leT1 leT2 : rel T1) s :
{in s &, (forall x y, leT1 x y -> leT2 x y)} ->
sorted leT1 s -> sorted leT2 s.
Lemma sorted_take (leT : rel T1) (s :seq T1) n :
sorted leT s -> sorted leT (take n s).
Lemma sorted_nth (leT : rel T1) x0 (s :seq T1) :
reflexive leT -> transitive leT ->
sorted leT s -> forall i j, j < size s -> i <= j ->
leT (nth x0 s i) (nth x0 s j).
Lemma sorted_nthr (leT : rel T1) x0 (s :seq T1) :
reflexive leT -> transitive leT -> {in s, (forall x, leT x x0)} ->
sorted leT s -> forall i j, i <= j -> leT (nth x0 s i) (nth x0 s j).
Lemma sorted_map (leT1 : rel T1) (leT2 : rel T2) (g : T1 -> T2) s :
{in s &, (forall x y, leT1 x y -> leT2 (g x) (g y))} -> sorted leT1 s ->
sorted leT2 (map g s).
End seq_eqType.
Section seq_comRingType.
Local Open Scope ring_scope.
Import GRing.Theory.
Variable R : comRingType.
Variable T : eqType.
{in s &, (forall x y, leT1 x y -> leT2 x y)} ->
sorted leT1 s -> sorted leT2 s.
Lemma sorted_take (leT : rel T1) (s :seq T1) n :
sorted leT s -> sorted leT (take n s).
Lemma sorted_nth (leT : rel T1) x0 (s :seq T1) :
reflexive leT -> transitive leT ->
sorted leT s -> forall i j, j < size s -> i <= j ->
leT (nth x0 s i) (nth x0 s j).
Lemma sorted_nthr (leT : rel T1) x0 (s :seq T1) :
reflexive leT -> transitive leT -> {in s, (forall x, leT x x0)} ->
sorted leT s -> forall i j, i <= j -> leT (nth x0 s i) (nth x0 s j).
Lemma sorted_map (leT1 : rel T1) (leT2 : rel T2) (g : T1 -> T2) s :
{in s &, (forall x y, leT1 x y -> leT2 (g x) (g y))} -> sorted leT1 s ->
sorted leT2 (map g s).
End seq_eqType.
Section seq_comRingType.
Local Open Scope ring_scope.
Import GRing.Theory.
Variable R : comRingType.
Variable T : eqType.
This lemma is usefull to prove that \mu_x p = count (xpred1 x) s where
s is the sequence of roots of polynomial p
Lemma prod_seq_count (s : seq T) (F : T -> R) :
\prod_(i <- s) F i =
\prod_(i <- (undup s)) ((F i) ^+ (count (xpred1 i) s)).
End seq_comRingType.
End Seq.
Section FinType.
Lemma enum_ord_enum n : enum 'I_n = ord_enum n.
End FinType.
Section Finfun.
Variables (aT : finType) (rT : eqType).
Variables (f g : aT -> rT).
Variable (P : pred aT).
Hypothesis (Hf : injective f) (Hg : injective g).
Lemma uniq_image (h : aT -> rT):
injective h -> uniq (image h P).
Lemma perm_eq_image : {subset (image f P) <= (image g P)} ->
perm_eq (image f P) (image g P).
End Finfun.
Section BigOp.
Variables (T : Type) (idx : T) (op : Monoid.com_law idx).
Lemma sumn_big s : sumn s = (\sum_(i <- s) i)%N.
Lemma big_lift_ord n F j :
\big[op/idx]_( i < n.+1 | j != i ) F i = \big[op/idx]_i F (lift j i).
End BigOp.
\prod_(i <- s) F i =
\prod_(i <- (undup s)) ((F i) ^+ (count (xpred1 i) s)).
End seq_comRingType.
End Seq.
Section FinType.
Lemma enum_ord_enum n : enum 'I_n = ord_enum n.
End FinType.
Section Finfun.
Variables (aT : finType) (rT : eqType).
Variables (f g : aT -> rT).
Variable (P : pred aT).
Hypothesis (Hf : injective f) (Hg : injective g).
Lemma uniq_image (h : aT -> rT):
injective h -> uniq (image h P).
Lemma perm_eq_image : {subset (image f P) <= (image g P)} ->
perm_eq (image f P) (image g P).
End Finfun.
Section BigOp.
Variables (T : Type) (idx : T) (op : Monoid.com_law idx).
Lemma sumn_big s : sumn s = (\sum_(i <- s) i)%N.
Lemma big_lift_ord n F j :
\big[op/idx]_( i < n.+1 | j != i ) F i = \big[op/idx]_i F (lift j i).
End BigOp.
matrix.v
Notation castmx_nn eqn := (castmx (eqn,eqn)).
Section Matrix.
Local Open Scope ring_scope.
Import GRing.Theory.
Section matrix_Type.
Variable T : Type.
Section Matrix.
Local Open Scope ring_scope.
Import GRing.Theory.
Section matrix_Type.
Variable T : Type.
This lemma is useful to rewrite in a big expression, and it is unsightly
to do a "have" in a proof for proving that.
Lemma matrix_comp k l m n (E : 'I_k -> 'I_l -> T) (F : 'I_n -> 'I_k) G :
\matrix_(i < n, j < m) ((\matrix_(i0 < k, j0 < l) E i0 j0) (F i) (G j)) =
\matrix_(i, j) (E (F i) (G j)).
\matrix_(i < n, j < m) ((\matrix_(i0 < k, j0 < l) E i0 j0) (F i) (G j)) =
\matrix_(i, j) (E (F i) (G j)).
Maybe we can also add row_matrixP
Lemma col_matrixP (m n : nat) :
forall (A B : 'M[T]_(m,n)), (forall i, col i A = col i B) <-> A = B.
Lemma row'_col'C n m (i : 'I_n) (j : 'I_m) (A : 'M[T]_(n,m)) :
row' i (col' j A) = col' j (row' i A).
Lemma row_thin_mx p q (M : 'M_(p,0)) (N : 'M[T]_(p,q)) :
row_mx M N = N.
Lemma col_flat_mx p q (M : 'M[T]_(0, q)) (N : 'M_(p,q)) :
col_mx M N = N.
Lemma block_flat_mx m n (M : 'M[T]_(0,m)) (N : 'M_(n, 0)) (P : 'M_(0,0))
(Q : 'M_(n,m)) : block_mx P M N Q = Q.
Lemma tr_mxvec m n (M : 'M[T]_(m,n)) i j :
(mxvec M) 0 (mxvec_index i j) = (mxvec M^T) 0 (mxvec_index j i).
End matrix_Type.
Section matrix_zmodType.
Variable V : zmodType.
Lemma mxvec0 m n : mxvec (0 : 'M[V]_(m,n)) = 0 :> 'rV[V]_(m * n).
End matrix_zmodType.
Section matrix_ringType.
Variable R : ringType.
forall (A B : 'M[T]_(m,n)), (forall i, col i A = col i B) <-> A = B.
Lemma row'_col'C n m (i : 'I_n) (j : 'I_m) (A : 'M[T]_(n,m)) :
row' i (col' j A) = col' j (row' i A).
Lemma row_thin_mx p q (M : 'M_(p,0)) (N : 'M[T]_(p,q)) :
row_mx M N = N.
Lemma col_flat_mx p q (M : 'M[T]_(0, q)) (N : 'M_(p,q)) :
col_mx M N = N.
Lemma block_flat_mx m n (M : 'M[T]_(0,m)) (N : 'M_(n, 0)) (P : 'M_(0,0))
(Q : 'M_(n,m)) : block_mx P M N Q = Q.
Lemma tr_mxvec m n (M : 'M[T]_(m,n)) i j :
(mxvec M) 0 (mxvec_index i j) = (mxvec M^T) 0 (mxvec_index j i).
End matrix_Type.
Section matrix_zmodType.
Variable V : zmodType.
Lemma mxvec0 m n : mxvec (0 : 'M[V]_(m,n)) = 0 :> 'rV[V]_(m * n).
End matrix_zmodType.
Section matrix_ringType.
Variable R : ringType.
Lemmas about column operations
Lemma colE (m n : nat) i (A : 'M[R]_(m, n)) : col i A = A *m delta_mx i 0.
Lemma col_mul m n p (i : 'I_p) (A : 'M[R]_(m,n)) (B : 'M[R]_(n, p)) :
col i (A *m B) = A *m col i B.
Lemma col_id_mulmx m n (M : 'M[R]_(m,n)) i :
M *m col i 1%:M = col i M.
Lemma row_id_mulmx m n (M : 'M[R]_(m,n)) i :
row i 1%:M *m M = row i M.
Lemma row'_col'_char_poly_mx m i (M : 'M[R]_m) :
row' i (col' i (char_poly_mx M)) = char_poly_mx (row' i (col' i M)).
Lemma char_block_mx m n (A : 'M[R]_m) (D : 'M[R]_n) B C :
char_poly_mx (block_mx A B C D) =
block_mx (char_poly_mx A) (map_mx polyC (-B))
(map_mx polyC (-C)) (char_poly_mx D).
Lemma char_dblock_mx m n (A : 'M[R]_m) (B : 'M[R]_n) :
char_poly_mx (block_mx A 0 0 B) =
block_mx (char_poly_mx A) 0 0 (char_poly_mx B).
Lemma conform_mxX m n (A : 'M[R]_m.+1) (B : 'M[R]_n.+1) k :
(conform_mx A B)^+ k = conform_mx (A^+k) (B^+k).
Lemma col_mul m n p (i : 'I_p) (A : 'M[R]_(m,n)) (B : 'M[R]_(n, p)) :
col i (A *m B) = A *m col i B.
Lemma col_id_mulmx m n (M : 'M[R]_(m,n)) i :
M *m col i 1%:M = col i M.
Lemma row_id_mulmx m n (M : 'M[R]_(m,n)) i :
row i 1%:M *m M = row i M.
Lemma row'_col'_char_poly_mx m i (M : 'M[R]_m) :
row' i (col' i (char_poly_mx M)) = char_poly_mx (row' i (col' i M)).
Lemma char_block_mx m n (A : 'M[R]_m) (D : 'M[R]_n) B C :
char_poly_mx (block_mx A B C D) =
block_mx (char_poly_mx A) (map_mx polyC (-B))
(map_mx polyC (-C)) (char_poly_mx D).
Lemma char_dblock_mx m n (A : 'M[R]_m) (B : 'M[R]_n) :
char_poly_mx (block_mx A 0 0 B) =
block_mx (char_poly_mx A) 0 0 (char_poly_mx B).
Lemma conform_mxX m n (A : 'M[R]_m.+1) (B : 'M[R]_n.+1) k :
(conform_mx A B)^+ k = conform_mx (A^+k) (B^+k).
Lemma about mxvec
about delta_mx
Lemma delta_mul_delta k n (A : 'M[R]_n) (i : 'I_k) (j : 'I_n) :
delta_mx i j *m A *m delta_mx j i = (A j j) *: delta_mx i i.
delta_mx i j *m A *m delta_mx j i = (A j j) *: delta_mx i i.
Lemma about detrminant
there are two proofs of equality to not use the irrelevance
Lemma det_castmx n m(M : 'M[R]_n) (eq1 : n = m) (eq2 : n = m) :
\det (castmx (eq1,eq2) M) = \det M.
Lemma exp_block_mx m n (A: 'M[R]_m.+1) (B : 'M_n.+1) k :
(block_mx A 0 0 B) ^+ k = block_mx (A ^+ k) 0 0 (B ^+ k).
Lemma char_castmx m n(A : 'M[R]_n) (eq : n = m) :
castmx_nn eq (char_poly_mx A) = char_poly_mx (castmx_nn eq A).
End matrix_ringType.
Section matrix_comUnitRingType.
Variable R : comUnitRingType.
Lemma invmx_block n1 n2 (Aul : 'M[R]_n1.+1) (Adr : 'M[R]_n2.+1) :
(block_mx Aul 0 0 Adr) \in unitmx ->
(block_mx Aul 0 0 Adr)^-1 = block_mx Aul^-1 0 0 Adr^-1.
End matrix_comUnitRingType.
Section matrix_fieldType.
Variable F : fieldType.
\det (castmx (eq1,eq2) M) = \det M.
Lemma exp_block_mx m n (A: 'M[R]_m.+1) (B : 'M_n.+1) k :
(block_mx A 0 0 B) ^+ k = block_mx (A ^+ k) 0 0 (B ^+ k).
Lemma char_castmx m n(A : 'M[R]_n) (eq : n = m) :
castmx_nn eq (char_poly_mx A) = char_poly_mx (castmx_nn eq A).
End matrix_ringType.
Section matrix_comUnitRingType.
Variable R : comUnitRingType.
Lemma invmx_block n1 n2 (Aul : 'M[R]_n1.+1) (Adr : 'M[R]_n2.+1) :
(block_mx Aul 0 0 Adr) \in unitmx ->
(block_mx Aul 0 0 Adr)^-1 = block_mx Aul^-1 0 0 Adr^-1.
End matrix_comUnitRingType.
Section matrix_fieldType.
Variable F : fieldType.
mx_poly
Lemma horner_mx_dvdp n (p q : {poly F}) (A : 'M_n.+1) :
(dvdp p q) -> horner_mx A p = 0 -> horner_mx A q = 0.
Lemma mxminpolyP n (A : 'M[F]_n.+1) (p : {poly F}) :
p \is monic -> horner_mx A p = 0 ->
(forall q, horner_mx A q = 0 -> (dvdp p q)) ->
p = mxminpoly A.
End matrix_fieldType.
End Matrix.
(dvdp p q) -> horner_mx A p = 0 -> horner_mx A q = 0.
Lemma mxminpolyP n (A : 'M[F]_n.+1) (p : {poly F}) :
p \is monic -> horner_mx A p = 0 ->
(forall q, horner_mx A q = 0 -> (dvdp p q)) ->
p = mxminpoly A.
End matrix_fieldType.
End Matrix.
Lemmas borrowed from mxtens
Cyril's lemma about cast of row_mx from mxtens
Lemma castmx_row (R : Type) (m m' n1 n2 n1' n2' : nat)
(eq_n1 : n1 = n1') (eq_n2 : n2 = n2') (eq_n12 : (n1 + n2 = n1' + n2')%N)
(eq_m : m = m') (A1 : 'M[R]_(m, n1)) (A2 : 'M_(m, n2)) :
castmx (eq_m, eq_n12) (row_mx A1 A2) =
row_mx (castmx (eq_m, eq_n1) A1) (castmx (eq_m, eq_n2) A2).
End mxtens.
Section Polynomial.
Section binomial_poly.
Variable R : comRingType.
Local Open Scope ring_scope.
Import GRing.Theory.
Lemma Newton (x : R) n :
('X + x%:P)^+n = \poly_(i < n.+1) ((x^+ (n - i)) *+ 'C(n,i)).
Lemma Newton_XsubC (x : R) n :
('X - x%:P)^+n = \poly_(i < n.+1) (((-x)^+ (n - i)) *+ 'C(n,i)).
Lemma Newton_coef (x : R) n i : (('X + x%:P)^+n)`_i = (x^+ (n - i)) *+ 'C(n,i).
Lemma Newton_coef_XsubC (x : R) n i :
(('X - x%:P)^+n)`_i = ((-x)^+ (n - i)) *+ 'C(n,i).
End binomial_poly.
Section poly_idomainType.
Variable R : idomainType.
Import GRing.Theory.
Local Open Scope ring_scope.
Lemma size_prod_gt0 (s : seq {poly R}) : (forall p, p \in s -> 0 < size p) ->
0 < size (\prod_(x <- s) x)%R.
Lemma coprimep_factor (a b : R) : (b - a)%R \is a GRing.unit ->
coprimep ('X - a%:P) ('X - b%:P).
Lemma coprimepn : forall n (sP_ : 'I_n -> {poly R}),
(forall i j, i != j -> coprimep (sP_ i) (sP_ j)) <->
(forall i, coprimep (sP_ i) (\prod_(j | i != j) sP_ j)).
Lemma lead_coef_prod (s : seq {poly R}) :
\prod_(p <- s) lead_coef p = lead_coef (\prod_(p <- s) p).
Lemma monic_leadVMp (p : {poly R}) : (lead_coef p) \is a GRing.unit ->
((lead_coef p)^-1 *: p) \is monic.
Lemma lead_eq_eqp (p q : {poly R}) : (lead_coef p) \is a GRing.unit ->
lead_coef p = lead_coef q -> reflect (p = q) (p %= q).
Lemma coprimep_irreducible (p q : {poly R}) : ~~(p %= q) ->
irreducible_poly p -> irreducible_poly q -> coprimep p q.
Lemma irreducible_dvdp_seq (p r : {poly R}) s :
irreducible_poly p -> p \is monic -> (dvdp p r) ->
(forall q, q \in s -> irreducible_poly q) ->
(forall q, q \in s -> q \is monic) ->
r = \prod_(t <- s) t ->
p \in s.
Lemma unicity_decomposition (s1 s2 : seq {poly R}) : forall (p : {poly R}),
(forall r, r \in s1 -> irreducible_poly r) ->
(forall r, r \in s2 -> irreducible_poly r) ->
(forall r, r \in s1 -> r \is monic) ->
(forall r, r \in s2 -> r \is monic) ->
p = \prod_(r <- s1) r -> p = \prod_(r <- s2) r ->
perm_eq s1 s2.
Lemma gcdpA (p q r : {poly R}):
(gcdp p (gcdp q r) %= gcdp (gcdp p q) r).
End poly_idomainType.
End Polynomial.
(eq_n1 : n1 = n1') (eq_n2 : n2 = n2') (eq_n12 : (n1 + n2 = n1' + n2')%N)
(eq_m : m = m') (A1 : 'M[R]_(m, n1)) (A2 : 'M_(m, n2)) :
castmx (eq_m, eq_n12) (row_mx A1 A2) =
row_mx (castmx (eq_m, eq_n1) A1) (castmx (eq_m, eq_n2) A2).
End mxtens.
Section Polynomial.
Section binomial_poly.
Variable R : comRingType.
Local Open Scope ring_scope.
Import GRing.Theory.
Lemma Newton (x : R) n :
('X + x%:P)^+n = \poly_(i < n.+1) ((x^+ (n - i)) *+ 'C(n,i)).
Lemma Newton_XsubC (x : R) n :
('X - x%:P)^+n = \poly_(i < n.+1) (((-x)^+ (n - i)) *+ 'C(n,i)).
Lemma Newton_coef (x : R) n i : (('X + x%:P)^+n)`_i = (x^+ (n - i)) *+ 'C(n,i).
Lemma Newton_coef_XsubC (x : R) n i :
(('X - x%:P)^+n)`_i = ((-x)^+ (n - i)) *+ 'C(n,i).
End binomial_poly.
Section poly_idomainType.
Variable R : idomainType.
Import GRing.Theory.
Local Open Scope ring_scope.
Lemma size_prod_gt0 (s : seq {poly R}) : (forall p, p \in s -> 0 < size p) ->
0 < size (\prod_(x <- s) x)%R.
Lemma coprimep_factor (a b : R) : (b - a)%R \is a GRing.unit ->
coprimep ('X - a%:P) ('X - b%:P).
Lemma coprimepn : forall n (sP_ : 'I_n -> {poly R}),
(forall i j, i != j -> coprimep (sP_ i) (sP_ j)) <->
(forall i, coprimep (sP_ i) (\prod_(j | i != j) sP_ j)).
Lemma lead_coef_prod (s : seq {poly R}) :
\prod_(p <- s) lead_coef p = lead_coef (\prod_(p <- s) p).
Lemma monic_leadVMp (p : {poly R}) : (lead_coef p) \is a GRing.unit ->
((lead_coef p)^-1 *: p) \is monic.
Lemma lead_eq_eqp (p q : {poly R}) : (lead_coef p) \is a GRing.unit ->
lead_coef p = lead_coef q -> reflect (p = q) (p %= q).
Lemma coprimep_irreducible (p q : {poly R}) : ~~(p %= q) ->
irreducible_poly p -> irreducible_poly q -> coprimep p q.
Lemma irreducible_dvdp_seq (p r : {poly R}) s :
irreducible_poly p -> p \is monic -> (dvdp p r) ->
(forall q, q \in s -> irreducible_poly q) ->
(forall q, q \in s -> q \is monic) ->
r = \prod_(t <- s) t ->
p \in s.
Lemma unicity_decomposition (s1 s2 : seq {poly R}) : forall (p : {poly R}),
(forall r, r \in s1 -> irreducible_poly r) ->
(forall r, r \in s2 -> irreducible_poly r) ->
(forall r, r \in s1 -> r \is monic) ->
(forall r, r \in s2 -> r \is monic) ->
p = \prod_(r <- s1) r -> p = \prod_(r <- s2) r ->
perm_eq s1 s2.
Lemma gcdpA (p q r : {poly R}):
(gcdp p (gcdp q r) %= gcdp (gcdp p q) r).
End poly_idomainType.
End Polynomial.
left pseudo division, it is complement of polydiv.
Import GRing.Theory.
Import Pdiv.Ring.
Import Pdiv.RingMonic.
Local Open Scope ring_scope.
Module RPdiv.
Section RingPseudoDivision.
Variable R : ringType.
Implicit Types d p q r : {poly R}.
Definition id_converse_def := (fun x : R => x : R^c).
Lemma add_id : additive id_converse_def.
Definition id_converse := Additive add_id.
Lemma expr_rev (x : R) k : (x : R^c) ^+ k = x ^+ k.
Definition phi (p : {poly R}^c) := map_poly id_converse p.
Fact phi_is_rmorphism : rmorphism phi.
Canonical phi_rmorphism := RMorphism phi_is_rmorphism.
Definition phi_inv (p : {poly R^c}) :=
map_poly (fun x : R^c => x : R) p : {poly R}^c.
Lemma phiK : cancel phi phi_inv.
Lemma phi_invK : cancel phi_inv phi.
Lemma phi_bij : bijective phi.
Lemma monic_map_inj (aR rR : ringType) (f : aR -> rR) (p : {poly aR}) :
injective f -> f 0 = 0 -> f 1 = 1 -> map_poly f p \is monic = (p \is monic).
Definition redivp_l (p q : {poly R}) : nat * {poly R} * {poly R} :=
let:(d,q,p) := (redivp (phi p) (phi q)) in
(d, phi_inv q, phi_inv p).
Definition rdivp_l p q := ((redivp_l p q).1).2.
Definition rmodp_l p q := (redivp_l p q).2.
Definition rscalp_l p q := ((redivp_l p q).1).1.
Definition rdvdp_l p q := rmodp_l q p == 0.
Definition rmultp_l := [rel m d | rdvdp_l d m].
Lemma ltn_rmodp_l p q : (size (rmodp_l p q) < size q) = (q != 0).
End RingPseudoDivision.
Module mon.
Section MonicDivisor.
Variable R : ringType.
Implicit Types p q r : {poly R}.
Variable d : {poly R}.
Hypothesis mond : d \is monic.
Lemma rdivp_l_eq p :
p = d * (rdivp_l p d) + (rmodp_l p d).
End MonicDivisor.
End mon.
End RPdiv.
This page has been generated by coqdoc