Module ssrcomplements

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.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensives.


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 nth_dflt_take x0 (s : seq T1) n :
  forall i, n <= i -> nth x0 (take n s) i = x0.

Lemma flatten_map (g : T1 -> T2) (s : seq (seq T1)) :
  map g (flatten s) = flatten (map (map g) s).

Lemma size_filter (s : seq T1) P : size (filter P s) <= size s.

End seq_Type.

Section seq_eqType.

Variable T1 T2 : eqType.

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 mem_nseq i n (a : T1) : i \in nseq n a -> i = a.

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.

Lemma count_perm_eq (s1 s2 : seq T1) :
  size s1 = size s2 ->
  (forall x, x \in s1 -> count (xpred1 x) s1 = count (xpred1 x) s2) ->
  perm_eq s1 s2.


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.

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 : T -> T -> T).
Variables (opm : Monoid.law idx) (opc : Monoid.com_law idx).

Lemma sumn_big s : sumn s = (\sum_(i <- s) i)%N.

Lemma big_lift_ord n F j :
  \big[opc/idx]_( i < n.+1 | j != i ) F i = \big[opc/idx]_i F (lift j i).

End BigOp.

Notation castmx_nn eqn := (castmx (eqn,eqn)).

Section Matrix.

Local Open Scope ring_scope.
Import GRing.Theory.

Section matrix_Type.

Variable T : Type.

Definition pairxx (x : T) := pair x x.

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)).

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.

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) (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 scale_mxvec m n x (M : 'M[R]_(m,n)) : mxvec (x *: M) = x *: mxvec M.

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.


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.

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.

Section 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_ringType.

Open Scope ring_scope.
Variable R : ringType.

Lemma monic_size_1 (p : {poly R}) : p \is monic -> size p <= 1 -> p = 1.

End poly_ringType.

Section poly_idomainType.

Variable R : idomainType.
Import GRing.Theory.
Local Open Scope ring_scope.

Lemma size_prod_pos (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 lead_coef_scale (a : R) p : lead_coef (a *: p) = a * lead_coef 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.

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.