diff options
| author | Cyril Cohen | 2015-07-17 18:03:31 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2015-07-17 18:03:31 +0200 |
| commit | 532de9b68384a114c6534a0736ed024c900447f9 (patch) | |
| tree | e100a6a7839bf7548ab8a9e053033f8eef3c7492 /mathcomp/algebra | |
| parent | f180c539a00fd83d8b3b5fd2d5710eb16e971e2e (diff) | |
Updating files + reorganizing everything
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/Make | 3 | ||||
| -rw-r--r-- | mathcomp/algebra/all_algebra.v (renamed from mathcomp/algebra/all.v) | 0 | ||||
| -rw-r--r-- | mathcomp/algebra/cyclic.v | 870 | ||||
| -rw-r--r-- | mathcomp/algebra/finalg.v | 29 | ||||
| -rw-r--r-- | mathcomp/algebra/fraction.v | 9 | ||||
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 28 | ||||
| -rw-r--r-- | mathcomp/algebra/interval.v | 21 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 33 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 85 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 21 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 65 | ||||
| -rw-r--r-- | mathcomp/algebra/polyXY.v | 13 | ||||
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 149 | ||||
| -rw-r--r-- | mathcomp/algebra/rat.v | 11 | ||||
| -rw-r--r-- | mathcomp/algebra/ring_quotient.v | 27 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 170 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 16 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 49 | ||||
| -rw-r--r-- | mathcomp/algebra/vector.v | 13 | ||||
| -rw-r--r-- | mathcomp/algebra/zmodp.v | 21 |
20 files changed, 390 insertions, 1243 deletions
diff --git a/mathcomp/algebra/Make b/mathcomp/algebra/Make index d9f4c63..7d12cb4 100644 --- a/mathcomp/algebra/Make +++ b/mathcomp/algebra/Make @@ -1,4 +1,4 @@ -all.v +all_algebra.v finalg.v fraction.v intdiv.v @@ -16,6 +16,5 @@ ssrint.v ssrnum.v vector.v zmodp.v -cyclic.v -R . mathcomp.algebra diff --git a/mathcomp/algebra/all.v b/mathcomp/algebra/all_algebra.v index 8a93ca9..8a93ca9 100644 --- a/mathcomp/algebra/all.v +++ b/mathcomp/algebra/all_algebra.v diff --git a/mathcomp/algebra/cyclic.v b/mathcomp/algebra/cyclic.v deleted file mode 100644 index 4365406..0000000 --- a/mathcomp/algebra/cyclic.v +++ /dev/null @@ -1,870 +0,0 @@ -(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import div fintype bigop prime finset. -From mathcomp.fingroup -Require Import fingroup morphism perm automorphism quotient gproduct. -Require Import ssralg finalg zmodp poly. - -(******************************************************************************) -(* Properties of cyclic groups. *) -(* Definitions: *) -(* Defined in fingroup.v: *) -(* <[x]> == the cycle (cyclic group) generated by x. *) -(* #[x] == the order of x, i.e., the cardinal of <[x]>. *) -(* Defined in prime.v: *) -(* totient n == Euler's totient function *) -(* Definitions in this file: *) -(* cyclic G <=> G is a cyclic group. *) -(* metacyclic G <=> G is a metacyclic group (i.e., a cyclic extension of a *) -(* cyclic group). *) -(* generator G x <=> x is a generator of the (cyclic) group G. *) -(* Zpm x == the isomorphism mapping the additive group of integers *) -(* mod #[x] to the cyclic group <[x]>. *) -(* cyclem x n == the endomorphism y |-> y ^+ n of <[x]>. *) -(* Zp_unitm x == the isomorphism mapping the multiplicative group of the *) -(* units of the ring of integers mod #[x] to the group of *) -(* automorphisms of <[x]> (i.e., Aut <[x]>). *) -(* Zp_unitm x maps u to cyclem x u. *) -(* eltm dvd_y_x == the smallest morphism (with domain <[x]>) mapping x to *) -(* y, given a proof dvd_y_x : #[y] %| #[x]. *) -(* expg_invn G k == if coprime #|G| k, the inverse of exponent k in G. *) -(* Basic results for these notions, plus the classical result that any finite *) -(* group isomorphic to a subgroup of a field is cyclic, hence that Aut G is *) -(* cyclic when G is of prime order. *) -(******************************************************************************) - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Import GroupScope GRing.Theory. - -(***********************************************************************) -(* Cyclic groups. *) -(***********************************************************************) - -Section Cyclic. - -Variable gT : finGroupType. -Implicit Types (a x y : gT) (A B : {set gT}) (G K H : {group gT}). - -Definition cyclic A := [exists x, A == <[x]>]. - -Lemma cyclicP A : reflect (exists x, A = <[x]>) (cyclic A). -Proof. exact: exists_eqP. Qed. - -Lemma cycle_cyclic x : cyclic <[x]>. -Proof. by apply/cyclicP; exists x. Qed. - -Lemma cyclic1 : cyclic [1 gT]. -Proof. by rewrite -cycle1 cycle_cyclic. Qed. - -(***********************************************************************) -(* Isomorphism with the additive group *) -(***********************************************************************) - -Section Zpm. - -Variable a : gT. - -Definition Zpm (i : 'Z_#[a]) := a ^+ i. - -Lemma ZpmM : {in Zp #[a] &, {morph Zpm : x y / x * y}}. -Proof. -rewrite /Zpm; case: (eqVneq a 1) => [-> | nta] i j _ _. - by rewrite !expg1n ?mulg1. -by rewrite /= {3}Zp_cast ?order_gt1 // expg_mod_order expgD. -Qed. - -Canonical Zpm_morphism := Morphism ZpmM. - -Lemma im_Zpm : Zpm @* Zp #[a] = <[a]>. -Proof. -apply/eqP; rewrite eq_sym eqEcard cycle_subG /= andbC morphimEdom. -rewrite (leq_trans (leq_imset_card _ _)) ?card_Zp //= /Zp order_gt1. -case: eqP => /= [a1 | _]; first by rewrite imset_set1 morph1 a1 set11. -by apply/imsetP; exists 1%R; rewrite ?expg1 ?inE. -Qed. - -Lemma injm_Zpm : 'injm Zpm. -Proof. -apply/injmP/dinjectiveP/card_uniqP. -rewrite size_map -cardE card_Zp //= {7}/order -im_Zpm morphimEdom /=. -by apply: eq_card => x; apply/imageP/imsetP=> [] [i Zp_i ->]; exists i. -Qed. - -Lemma eq_expg_mod_order m n : (a ^+ m == a ^+ n) = (m == n %[mod #[a]]). -Proof. -have [->|] := eqVneq a 1; first by rewrite order1 !modn1 !expg1n eqxx. -rewrite -order_gt1 => lt1a; have ZpT: Zp #[a] = setT by rewrite /Zp lt1a. -have: injective Zpm by move=> i j; apply (injmP injm_Zpm); rewrite /= ZpT inE. -move/inj_eq=> eqZ; symmetry; rewrite -(Zp_cast lt1a). -by rewrite -[_ == _](eqZ (inZp m) (inZp n)) /Zpm /= Zp_cast ?expg_mod_order. -Qed. - -Lemma Zp_isom : isom (Zp #[a]) <[a]> Zpm. -Proof. by apply/isomP; rewrite injm_Zpm im_Zpm. Qed. - -Lemma Zp_isog : isog (Zp #[a]) <[a]>. -Proof. exact: isom_isog Zp_isom. Qed. - -End Zpm. - -(***********************************************************************) -(* Central and direct product of cycles *) -(***********************************************************************) - -Lemma cyclic_abelian A : cyclic A -> abelian A. -Proof. by case/cyclicP=> a ->; exact: cycle_abelian. Qed. - -Lemma cycleMsub a b : - commute a b -> coprime #[a] #[b] -> <[a]> \subset <[a * b]>. -Proof. -move=> cab co_ab; apply/subsetP=> _ /cycleP[k ->]. -apply/cycleP; exists (chinese #[a] #[b] k 0); symmetry. -rewrite expgMn // -expg_mod_order chinese_modl // expg_mod_order. -by rewrite /chinese addn0 -mulnA mulnCA expgM expg_order expg1n mulg1. -Qed. - -Lemma cycleM a b : - commute a b -> coprime #[a] #[b] -> <[a * b]> = <[a]> * <[b]>. -Proof. -move=> cab co_ab; apply/eqP; rewrite eqEsubset -(cent_joinEl (cents_cycle cab)). -rewrite join_subG {3}cab !cycleMsub // 1?coprime_sym //. -by rewrite -genM_join cycle_subG mem_gen // mem_imset2 ?cycle_id. -Qed. - -Lemma cyclicM A B : - cyclic A -> cyclic B -> B \subset 'C(A) -> coprime #|A| #|B| -> - cyclic (A * B). -Proof. -move=> /cyclicP[a ->] /cyclicP[b ->]; rewrite cent_cycle cycle_subG => cab coab. -by rewrite -cycleM ?cycle_cyclic //; exact/esym/cent1P. -Qed. - -Lemma cyclicY K H : - cyclic K -> cyclic H -> H \subset 'C(K) -> coprime #|K| #|H| -> - cyclic (K <*> H). -Proof. by move=> cycK cycH cKH coKH; rewrite cent_joinEr // cyclicM. Qed. - -(***********************************************************************) -(* Order properties *) -(***********************************************************************) - -Lemma order_dvdn a n : #[a] %| n = (a ^+ n == 1). -Proof. by rewrite (eq_expg_mod_order a n 0) mod0n. Qed. - -Lemma order_inf a n : a ^+ n.+1 == 1 -> #[a] <= n.+1. -Proof. by rewrite -order_dvdn; exact: dvdn_leq. Qed. - -Lemma order_dvdG G a : a \in G -> #[a] %| #|G|. -Proof. by move=> Ga; apply: cardSg; rewrite cycle_subG. Qed. - -Lemma expg_cardG G a : a \in G -> a ^+ #|G| = 1. -Proof. by move=> Ga; apply/eqP; rewrite -order_dvdn order_dvdG. Qed. - -Lemma expg_znat G x k : x \in G -> x ^+ (k%:R : 'Z_(#|G|))%R = x ^+ k. -Proof. -case: (eqsVneq G 1) => [-> /set1P-> | ntG Gx]; first by rewrite !expg1n. -apply/eqP; rewrite val_Zp_nat ?cardG_gt1 // eq_expg_mod_order. -by rewrite modn_dvdm ?order_dvdG. -Qed. - -Lemma expg_zneg G x (k : 'Z_(#|G|)) : x \in G -> x ^+ (- k)%R = x ^- k. -Proof. -move=> Gx; apply/eqP; rewrite eq_sym eq_invg_mul -expgD. -by rewrite -(expg_znat _ Gx) natrD natr_Zp natr_negZp subrr. -Qed. - -Lemma nt_gen_prime G x : prime #|G| -> x \in G^# -> G :=: <[x]>. -Proof. -move=> Gpr /setD1P[]; rewrite -cycle_subG -cycle_eq1 => ntX sXG. -apply/eqP; rewrite eqEsubset sXG andbT. -by apply: contraR ntX => /(prime_TIg Gpr); rewrite (setIidPr sXG) => ->. -Qed. - -Lemma nt_prime_order p x : prime p -> x ^+ p = 1 -> x != 1 -> #[x] = p. -Proof. -move=> p_pr xp ntx; apply/prime_nt_dvdP; rewrite ?order_eq1 //. -by rewrite order_dvdn xp. -Qed. - -Lemma orderXdvd a n : #[a ^+ n] %| #[a]. -Proof. by apply: order_dvdG; exact: mem_cycle. Qed. - -Lemma orderXgcd a n : #[a ^+ n] = #[a] %/ gcdn #[a] n. -Proof. -apply/eqP; rewrite eqn_dvd; apply/andP; split. - rewrite order_dvdn -expgM -muln_divCA_gcd //. - by rewrite expgM expg_order expg1n. -have [-> | n_gt0] := posnP n; first by rewrite gcdn0 divnn order_gt0 dvd1n. -rewrite -(dvdn_pmul2r n_gt0) divn_mulAC ?dvdn_gcdl // dvdn_lcm. -by rewrite order_dvdn mulnC expgM expg_order eqxx dvdn_mulr. -Qed. - -Lemma orderXdiv a n : n %| #[a] -> #[a ^+ n] = #[a] %/ n. -Proof. by case/dvdnP=> q defq; rewrite orderXgcd {2}defq gcdnC gcdnMl. Qed. - -Lemma orderXexp p m n x : #[x] = (p ^ n)%N -> #[x ^+ (p ^ m)] = (p ^ (n - m))%N. -Proof. -move=> ox; have [n_le_m | m_lt_n] := leqP n m. - rewrite -(subnKC n_le_m) subnDA subnn expnD expgM -ox. - by rewrite expg_order expg1n order1. -rewrite orderXdiv ox ?dvdn_exp2l ?expnB ?(ltnW m_lt_n) //. -by have:= order_gt0 x; rewrite ox expn_gt0 orbC -(ltn_predK m_lt_n). -Qed. - -Lemma orderXpfactor p k n x : - #[x ^+ (p ^ k)] = n -> prime p -> p %| n -> #[x] = (p ^ k * n)%N. -Proof. -move=> oxp p_pr dv_p_n. -suffices pk_x: p ^ k %| #[x] by rewrite -oxp orderXdiv // mulnC divnK. -rewrite pfactor_dvdn // leqNgt; apply: contraL dv_p_n => lt_x_k. -rewrite -oxp -p'natE // -(subnKC (ltnW lt_x_k)) expnD expgM. -rewrite (pnat_dvd (orderXdvd _ _)) // -p_part // orderXdiv ?dvdn_part //. -by rewrite -{1}[#[x]](partnC p) // mulKn // part_pnat. -Qed. - -Lemma orderXprime p n x : - #[x ^+ p] = n -> prime p -> p %| n -> #[x] = (p * n)%N. -Proof. exact: (@orderXpfactor p 1). Qed. - -Lemma orderXpnat m n x : #[x ^+ m] = n -> \pi(n).-nat m -> #[x] = (m * n)%N. -Proof. -move=> oxm n_m; have [m_gt0 _] := andP n_m. -suffices m_x: m %| #[x] by rewrite -oxm orderXdiv // mulnC divnK. -apply/dvdn_partP=> // p; rewrite mem_primes => /and3P[p_pr _ p_m]. -have n_p: p \in \pi(n) by apply: (pnatP _ _ n_m). -have p_oxm: p %| #[x ^+ (p ^ logn p m)]. - apply: dvdn_trans (orderXdvd _ m`_p^'); rewrite -expgM -p_part ?partnC //. - by rewrite oxm; rewrite mem_primes in n_p; case/and3P: n_p. -by rewrite (orderXpfactor (erefl _) p_pr p_oxm) p_part // dvdn_mulr. -Qed. - -Lemma orderM a b : - commute a b -> coprime #[a] #[b] -> #[a * b] = (#[a] * #[b])%N. -Proof. by move=> cab co_ab; rewrite -coprime_cardMg -?cycleM. Qed. - -Definition expg_invn A k := (egcdn k #|A|).1. - -Lemma expgK G k : - coprime #|G| k -> {in G, cancel (expgn^~ k) (expgn^~ (expg_invn G k))}. -Proof. -move=> coGk x /order_dvdG Gx; apply/eqP. -rewrite -expgM (eq_expg_mod_order _ _ 1) -(modn_dvdm 1 Gx). -by rewrite -(chinese_modl coGk 1 0) /chinese mul1n addn0 modn_dvdm. -Qed. - -Lemma cyclic_dprod K H G : - K \x H = G -> cyclic K -> cyclic H -> cyclic G = coprime #|K| #|H| . -Proof. -case/dprodP=> _ defKH cKH tiKH cycK cycH; pose m := lcmn #|K| #|H|. -apply/idP/idP=> [/cyclicP[x defG] | coKH]; last by rewrite -defKH cyclicM. -rewrite /coprime -dvdn1 -(@dvdn_pmul2l m) ?lcmn_gt0 ?cardG_gt0 //. -rewrite muln_lcm_gcd muln1 -TI_cardMg // defKH defG order_dvdn. -have /mulsgP[y z Ky Hz ->]: x \in K * H by rewrite defKH defG cycle_id. -rewrite -[1]mulg1 expgMn; last exact/commute_sym/(centsP cKH). -apply/eqP; congr (_ * _); apply/eqP; rewrite -order_dvdn. - exact: dvdn_trans (order_dvdG Ky) (dvdn_lcml _ _). -exact: dvdn_trans (order_dvdG Hz) (dvdn_lcmr _ _). -Qed. - -(***********************************************************************) -(* Generator *) -(***********************************************************************) - -Definition generator (A : {set gT}) a := A == <[a]>. - -Lemma generator_cycle a : generator <[a]> a. -Proof. exact: eqxx. Qed. - -Lemma cycle_generator a x : generator <[a]> x -> x \in <[a]>. -Proof. by move/(<[a]> =P _)->; exact: cycle_id. Qed. - -Lemma generator_order a b : generator <[a]> b -> #[a] = #[b]. -Proof. by rewrite /order => /(<[a]> =P _)->. Qed. - -End Cyclic. - -Arguments Scope cyclic [_ group_scope]. -Arguments Scope generator [_ group_scope group_scope]. -Arguments Scope expg_invn [_ group_scope nat_scope]. -Implicit Arguments cyclicP [gT A]. -Prenex Implicits cyclic Zpm generator expg_invn. - -(* Euler's theorem *) -Theorem Euler_exp_totient a n : coprime a n -> a ^ totient n = 1 %[mod n]. -Proof. -case: n => [|[|n']] //; [by rewrite !modn1 | set n := n'.+2] => co_a_n. -have{co_a_n} Ua: coprime n (inZp a : 'I_n) by rewrite coprime_sym coprime_modl. -have: FinRing.unit 'Z_n Ua ^+ totient n == 1. - by rewrite -card_units_Zp // -order_dvdn order_dvdG ?inE. -by rewrite -2!val_eqE unit_Zp_expg /= -/n modnXm => /eqP. -Qed. - -Section Eltm. - -Variables (aT rT : finGroupType) (x : aT) (y : rT). - -Definition eltm of #[y] %| #[x] := fun x_i => y ^+ invm (injm_Zpm x) x_i. - -Hypothesis dvd_y_x : #[y] %| #[x]. - -Lemma eltmE i : eltm dvd_y_x (x ^+ i) = y ^+ i. -Proof. -apply/eqP; rewrite eq_expg_mod_order. -have [x_le1 | x_gt1] := leqP #[x] 1. - suffices: #[y] %| 1 by rewrite dvdn1 => /eqP->; rewrite !modn1. - by rewrite (dvdn_trans dvd_y_x) // dvdn1 order_eq1 -cycle_eq1 trivg_card_le1. -rewrite -(expg_znat i (cycle_id x)) invmE /=; last by rewrite /Zp x_gt1 inE. -by rewrite val_Zp_nat // modn_dvdm. -Qed. - -Lemma eltm_id : eltm dvd_y_x x = y. Proof. exact: (eltmE 1). Qed. - -Lemma eltmM : {in <[x]> &, {morph eltm dvd_y_x : x_i x_j / x_i * x_j}}. -Proof. -move=> _ _ /cycleP[i ->] /cycleP[j ->]. -by apply/eqP; rewrite -expgD !eltmE expgD. -Qed. -Canonical eltm_morphism := Morphism eltmM. - -Lemma im_eltm : eltm dvd_y_x @* <[x]> = <[y]>. -Proof. by rewrite morphim_cycle ?cycle_id //= eltm_id. Qed. - -Lemma ker_eltm : 'ker (eltm dvd_y_x) = <[x ^+ #[y]]>. -Proof. -apply/eqP; rewrite eq_sym eqEcard cycle_subG 3!inE mem_cycle /= eltmE. -rewrite expg_order eqxx (orderE y) -im_eltm card_morphim setIid -orderE. -by rewrite orderXdiv ?dvdn_indexg //= leq_divRL ?indexg_gt0 ?Lagrange ?subsetIl. -Qed. - -Lemma injm_eltm : 'injm (eltm dvd_y_x) = (#[x] %| #[y]). -Proof. by rewrite ker_eltm subG1 cycle_eq1 -order_dvdn. Qed. - -End Eltm. - -Section CycleSubGroup. - -Variable gT : finGroupType. - -(* Gorenstein, 1.3.1 (i) *) -Lemma cycle_sub_group (a : gT) m : - m %| #[a] -> - [set H : {group gT} | H \subset <[a]> & #|H| == m] - = [set <[a ^+ (#[a] %/ m)]>%G]. -Proof. -move=> m_dv_a; have m_gt0: 0 < m by apply: dvdn_gt0 m_dv_a. -have oam: #|<[a ^+ (#[a] %/ m)]>| = m. - apply/eqP; rewrite [#|_|]orderXgcd -(divnMr m_gt0) muln_gcdl divnK //. - by rewrite gcdnC gcdnMr mulKn. -apply/eqP; rewrite eqEsubset sub1set inE /= cycleX oam eqxx !andbT. -apply/subsetP=> X; rewrite in_set1 inE -val_eqE /= eqEcard oam. -case/andP=> sXa /eqP oX; rewrite oX leqnn andbT. -apply/subsetP=> x Xx; case/cycleP: (subsetP sXa _ Xx) => k def_x. -have: (x ^+ m == 1)%g by rewrite -oX -order_dvdn cardSg // gen_subG sub1set. -rewrite {x Xx}def_x -expgM -order_dvdn -[#[a]](Lagrange sXa) -oX mulnC. -rewrite dvdn_pmul2r // mulnK // => /dvdnP[i ->]. -by rewrite mulnC expgM groupX // cycle_id. -Qed. - -Lemma cycle_subgroup_char a (H : {group gT}) : H \subset <[a]> -> H \char <[a]>. -Proof. -move=> sHa; apply: lone_subgroup_char => // J sJa isoJH. -have dvHa: #|H| %| #[a] by exact: cardSg. -have{dvHa} /setP Huniq := esym (cycle_sub_group dvHa). -move: (Huniq H) (Huniq J); rewrite !inE /=. -by rewrite sHa sJa (card_isog isoJH) eqxx => /eqP<- /eqP<-. -Qed. - -End CycleSubGroup. - -(***********************************************************************) -(* Reflected boolean property and morphic image, injection, bijection *) -(***********************************************************************) - -Section MorphicImage. - -Variables aT rT : finGroupType. -Variables (D : {group aT}) (f : {morphism D >-> rT}) (x : aT). -Hypothesis Dx : x \in D. - -Lemma morph_order : #[f x] %| #[x]. -Proof. by rewrite order_dvdn -morphX // expg_order morph1. Qed. - -Lemma morph_generator A : generator A x -> generator (f @* A) (f x). -Proof. by move/(A =P _)->; rewrite /generator morphim_cycle. Qed. - -End MorphicImage. - -Section CyclicProps. - -Variables gT : finGroupType. -Implicit Types (aT rT : finGroupType) (G H K : {group gT}). - -Lemma cyclicS G H : H \subset G -> cyclic G -> cyclic H. -Proof. -move=> sHG /cyclicP[x defG]; apply/cyclicP. -exists (x ^+ (#[x] %/ #|H|)); apply/congr_group/set1P. -by rewrite -cycle_sub_group /order -defG ?cardSg // inE sHG eqxx. -Qed. - -Lemma cyclicJ G x : cyclic (G :^ x) = cyclic G. -Proof. -apply/cyclicP/cyclicP=> [[y /(canRL (conjsgK x))] | [y ->]]. - by rewrite -cycleJ; exists (y ^ x^-1). -by exists (y ^ x); rewrite cycleJ. -Qed. - -Lemma eq_subG_cyclic G H K : - cyclic G -> H \subset G -> K \subset G -> (H :==: K) = (#|H| == #|K|). -Proof. -case/cyclicP=> x -> sHx sKx; apply/eqP/eqP=> [-> //| eqHK]. -have def_GHx := cycle_sub_group (cardSg sHx); set GHx := [set _] in def_GHx. -have []: H \in GHx /\ K \in GHx by rewrite -def_GHx !inE sHx sKx eqHK /=. -by do 2!move/set1P->. -Qed. - -Lemma cardSg_cyclic G H K : - cyclic G -> H \subset G -> K \subset G -> (#|H| %| #|K|) = (H \subset K). -Proof. -move=> cycG sHG sKG; apply/idP/idP; last exact: cardSg. -case/cyclicP: (cyclicS sKG cycG) => x defK; rewrite {K}defK in sKG *. -case/dvdnP=> k ox; suffices ->: H :=: <[x ^+ k]> by exact: cycleX. -apply/eqP; rewrite (eq_subG_cyclic cycG) ?(subset_trans (cycleX _ _)) //. -rewrite -orderE orderXdiv orderE ox ?dvdn_mulr ?mulKn //. -by have:= order_gt0 x; rewrite orderE ox; case k. -Qed. - -Lemma sub_cyclic_char G H : cyclic G -> (H \char G) = (H \subset G). -Proof. -case/cyclicP=> x ->; apply/idP/idP => [/andP[] //|]. -exact: cycle_subgroup_char. -Qed. - -Lemma morphim_cyclic rT G H (f : {morphism G >-> rT}) : - cyclic H -> cyclic (f @* H). -Proof. -move=> cycH; wlog sHG: H cycH / H \subset G. - by rewrite -morphimIdom; apply; rewrite (cyclicS _ cycH, subsetIl) ?subsetIr. -case/cyclicP: cycH sHG => x ->; rewrite gen_subG sub1set => Gx. -by apply/cyclicP; exists (f x); rewrite morphim_cycle. -Qed. - -Lemma quotient_cycle x H : x \in 'N(H) -> <[x]> / H = <[coset H x]>. -Proof. exact: morphim_cycle. Qed. - -Lemma quotient_cyclic G H : cyclic G -> cyclic (G / H). -Proof. exact: morphim_cyclic. Qed. - -Lemma quotient_generator x G H : - x \in 'N(H) -> generator G x -> generator (G / H) (coset H x). -Proof. by move=> Nx; apply: morph_generator. Qed. - -Lemma prime_cyclic G : prime #|G| -> cyclic G. -Proof. -case/primeP; rewrite ltnNge -trivg_card_le1. -case/trivgPn=> x Gx ntx /(_ _ (order_dvdG Gx)). -rewrite order_eq1 (negbTE ntx) => /eqnP oxG; apply/cyclicP. -by exists x; apply/eqP; rewrite eq_sym eqEcard -oxG cycle_subG Gx leqnn. -Qed. - -Lemma dvdn_prime_cyclic G p : prime p -> #|G| %| p -> cyclic G. -Proof. -move=> p_pr pG; case: (eqsVneq G 1) => [-> | ntG]; first exact: cyclic1. -by rewrite prime_cyclic // (prime_nt_dvdP p_pr _ pG) -?trivg_card1. -Qed. - -Lemma cyclic_small G : #|G| <= 3 -> cyclic G. -Proof. -rewrite 4!(ltnS, leq_eqVlt) -trivg_card_le1 orbA orbC. -case/predU1P=> [-> | oG]; first exact: cyclic1. -by apply: prime_cyclic; case/pred2P: oG => ->. -Qed. - -End CyclicProps. - -Section IsoCyclic. - -Variables gT rT : finGroupType. -Implicit Types (G H : {group gT}) (M : {group rT}). - -Lemma injm_cyclic G H (f : {morphism G >-> rT}) : - 'injm f -> H \subset G -> cyclic (f @* H) = cyclic H. -Proof. -move=> injf sHG; apply/idP/idP; last exact: morphim_cyclic. -rewrite -{2}(morphim_invm injf sHG); exact: morphim_cyclic. -Qed. - -Lemma isog_cyclic G M : G \isog M -> cyclic G = cyclic M. -Proof. by case/isogP=> f injf <-; rewrite injm_cyclic. Qed. - -Lemma isog_cyclic_card G M : cyclic G -> isog G M = cyclic M && (#|M| == #|G|). -Proof. -move=> cycG; apply/idP/idP=> [isoGM | ]. - by rewrite (card_isog isoGM) -(isog_cyclic isoGM) cycG /=. -case/cyclicP: cycG => x ->{G} /andP[/cyclicP[y ->] /eqP oy]. -by apply: isog_trans (isog_symr _) (Zp_isog y); rewrite /order oy Zp_isog. -Qed. - -Lemma injm_generator G H (f : {morphism G >-> rT}) x : - 'injm f -> x \in G -> H \subset G -> - generator (f @* H) (f x) = generator H x. -Proof. -move=> injf Gx sHG; apply/idP/idP; last exact: morph_generator. -rewrite -{2}(morphim_invm injf sHG) -{2}(invmE injf Gx). -by apply: morph_generator; exact: mem_morphim. -Qed. - -End IsoCyclic. - -(* Metacyclic groups. *) -Section Metacyclic. - -Variable gT : finGroupType. -Implicit Types (A : {set gT}) (G H : {group gT}). - -Definition metacyclic A := - [exists H : {group gT}, [&& cyclic H, H <| A & cyclic (A / H)]]. - -Lemma metacyclicP A : - reflect (exists H : {group gT}, [/\ cyclic H, H <| A & cyclic (A / H)]) - (metacyclic A). -Proof. exact: 'exists_and3P. Qed. - -Lemma metacyclic1 : metacyclic 1. -Proof. -by apply/existsP; exists 1%G; rewrite normal1 trivg_quotient !cyclic1. -Qed. - -Lemma cyclic_metacyclic A : cyclic A -> metacyclic A. -Proof. -case/cyclicP=> x ->; apply/existsP; exists (<[x]>)%G. -by rewrite normal_refl cycle_cyclic trivg_quotient cyclic1. -Qed. - -Lemma metacyclicS G H : H \subset G -> metacyclic G -> metacyclic H. -Proof. -move=> sHG /metacyclicP[K [cycK nsKG cycGq]]; apply/metacyclicP. -exists (H :&: K)%G; rewrite (cyclicS (subsetIr H K)) ?(normalGI sHG) //=. -rewrite setIC (isog_cyclic (second_isog _)) ?(cyclicS _ cycGq) ?quotientS //. -by rewrite (subset_trans sHG) ?normal_norm. -Qed. - -End Metacyclic. - -Arguments Scope metacyclic [_ group_scope]. -Prenex Implicits metacyclic. -Implicit Arguments metacyclicP [gT A]. - -(* Automorphisms of cyclic groups. *) -Section CyclicAutomorphism. - -Variable gT : finGroupType. - -Section CycleAutomorphism. - -Variable a : gT. - -Section CycleMorphism. - -Variable n : nat. - -Definition cyclem of gT := fun x : gT => x ^+ n. - -Lemma cyclemM : {in <[a]> & , {morph cyclem a : x y / x * y}}. -Proof. -by move=> x y ax ay; apply: expgMn; exact: (centsP (cycle_abelian a)). -Qed. - -Canonical cyclem_morphism := Morphism cyclemM. - -End CycleMorphism. - -Section ZpUnitMorphism. - -Variable u : {unit 'Z_#[a]}. - -Lemma injm_cyclem : 'injm (cyclem (val u) a). -Proof. -apply/subsetP=> x /setIdP[ax]; rewrite !inE -order_dvdn. -case: (eqVneq a 1) => [a1 | nta]; first by rewrite a1 cycle1 inE in ax. -rewrite -order_eq1 -dvdn1; move/eqnP: (valP u) => /= <-. -by rewrite dvdn_gcd {2}Zp_cast ?order_gt1 // order_dvdG. -Qed. - -Lemma im_cyclem : cyclem (val u) a @* <[a]> = <[a]>. -Proof. -apply/morphim_fixP=> //; first exact: injm_cyclem. -by rewrite morphim_cycle ?cycle_id ?cycleX. -Qed. - -Definition Zp_unitm := aut injm_cyclem im_cyclem. - -End ZpUnitMorphism. - -Lemma Zp_unitmM : {in units_Zp #[a] &, {morph Zp_unitm : u v / u * v}}. -Proof. -move=> u v _ _; apply: (eq_Aut (Aut_aut _ _)) => [|x a_x]. - by rewrite groupM ?Aut_aut. -rewrite permM !autE ?groupX //= /cyclem -expgM. -rewrite -expg_mod_order modn_dvdm ?expg_mod_order //. -case: (leqP #[a] 1) => [lea1 | lt1a]; last by rewrite Zp_cast ?order_dvdG. -by rewrite card_le1_trivg // in a_x; rewrite (set1P a_x) order1 dvd1n. -Qed. - -Canonical Zp_unit_morphism := Morphism Zp_unitmM. - -Lemma injm_Zp_unitm : 'injm Zp_unitm. -Proof. -case: (eqVneq a 1) => [a1 | nta]. - by rewrite subIset //= card_le1_trivg ?subxx // card_units_Zp a1 order1. -apply/subsetP=> /= u /morphpreP[_ /set1P/= um1]. -have{um1}: Zp_unitm u a == Zp_unitm 1 a by rewrite um1 morph1. -rewrite !autE ?cycle_id // eq_expg_mod_order. -by rewrite -[n in _ == _ %[mod n]]Zp_cast ?order_gt1 // !modZp inE. -Qed. - -Lemma generator_coprime m : generator <[a]> (a ^+ m) = coprime #[a] m. -Proof. -rewrite /generator eq_sym eqEcard cycleX -/#[a] [#|_|]orderXgcd /=. -apply/idP/idP=> [le_a_am|co_am]; last by rewrite (eqnP co_am) divn1. -have am_gt0: 0 < gcdn #[a] m by rewrite gcdn_gt0 order_gt0. -by rewrite /coprime eqn_leq am_gt0 andbT -(@leq_pmul2l #[a]) ?muln1 -?leq_divRL. -Qed. - -Lemma im_Zp_unitm : Zp_unitm @* units_Zp #[a] = Aut <[a]>. -Proof. -rewrite morphimEdom; apply/setP=> f; pose n := invm (injm_Zpm a) (f a). -apply/imsetP/idP=> [[u _ ->] | Af]; first exact: Aut_aut. -have [a1 | nta] := eqVneq a 1. - by rewrite a1 cycle1 Aut1 in Af; exists 1; rewrite // morph1 (set1P Af). -have a_fa: <[a]> = <[f a]>. - by rewrite -(autmE Af) -morphim_cycle ?im_autm ?cycle_id. -have def_n: a ^+ n = f a. - by rewrite -/(Zpm n) invmK // im_Zpm a_fa cycle_id. -have co_a_n: coprime #[a].-2.+2 n. - by rewrite {1}Zp_cast ?order_gt1 // -generator_coprime def_n; exact/eqP. -exists (FinRing.unit 'Z_#[a] co_a_n); rewrite ?inE //. -apply: eq_Aut (Af) (Aut_aut _ _) _ => x ax. -rewrite autE //= /cyclem; case/cycleP: ax => k ->{x}. -by rewrite -(autmE Af) morphX ?cycle_id //= autmE -def_n -!expgM mulnC. -Qed. - -Lemma Zp_unit_isom : isom (units_Zp #[a]) (Aut <[a]>) Zp_unitm. -Proof. by apply/isomP; rewrite ?injm_Zp_unitm ?im_Zp_unitm. Qed. - -Lemma Zp_unit_isog : isog (units_Zp #[a]) (Aut <[a]>). -Proof. exact: isom_isog Zp_unit_isom. Qed. - -Lemma card_Aut_cycle : #|Aut <[a]>| = totient #[a]. -Proof. by rewrite -(card_isog Zp_unit_isog) card_units_Zp. Qed. - -Lemma totient_gen : totient #[a] = #|[set x | generator <[a]> x]|. -Proof. -have [lea1 | lt1a] := leqP #[a] 1. - rewrite /order card_le1_trivg // cards1 (@eq_card1 _ 1) // => x. - by rewrite !inE -cycle_eq1 eq_sym. -rewrite -(card_injm (injm_invm (injm_Zpm a))) /= ?im_Zpm; last first. - by apply/subsetP=> x; rewrite inE; exact: cycle_generator. -rewrite -card_units_Zp // cardsE card_sub morphim_invmE; apply: eq_card => /= d. -by rewrite !inE /= qualifE /= /Zp lt1a inE /= generator_coprime {1}Zp_cast. -Qed. - -Lemma Aut_cycle_abelian : abelian (Aut <[a]>). -Proof. by rewrite -im_Zp_unitm morphim_abelian ?units_Zp_abelian. Qed. - -End CycleAutomorphism. - -Variable G : {group gT}. - -Lemma Aut_cyclic_abelian : cyclic G -> abelian (Aut G). -Proof. by case/cyclicP=> x ->; exact: Aut_cycle_abelian. Qed. - -Lemma card_Aut_cyclic : cyclic G -> #|Aut G| = totient #|G|. -Proof. by case/cyclicP=> x ->; exact: card_Aut_cycle. Qed. - -Lemma sum_ncycle_totient : - \sum_(d < #|G|.+1) #|[set <[x]> | x in G & #[x] == d]| * totient d = #|G|. -Proof. -pose h (x : gT) : 'I_#|G|.+1 := inord #[x]. -symmetry; rewrite -{1}sum1_card (partition_big h xpredT) //=. -apply: eq_bigr => d _; set Gd := finset _. -rewrite -sum_nat_const sum1dep_card -sum1_card (_ : finset _ = Gd); last first. - apply/setP=> x; rewrite !inE; apply: andb_id2l => Gx. - by rewrite /eq_op /= inordK // ltnS subset_leq_card ?cycle_subG. -rewrite (partition_big_imset cycle) {}/Gd; apply: eq_bigr => C /=. -case/imsetP=> x /setIdP[Gx /eqP <-] -> {C d}. -rewrite sum1dep_card totient_gen; apply: eq_card => y; rewrite !inE /generator. -move: Gx; rewrite andbC eq_sym -!cycle_subG /order. -by case: eqP => // -> ->; rewrite eqxx. -Qed. - -End CyclicAutomorphism. - -Lemma sum_totient_dvd n : \sum_(d < n.+1 | d %| n) totient d = n. -Proof. -case: n => [|[|n']]; try by rewrite big_mkcond !big_ord_recl big_ord0. -set n := n'.+2; pose x1 : 'Z_n := 1%R. -have ox1: #[x1] = n by rewrite /order -Zp_cycle card_Zp. -rewrite -[rhs in _ = rhs]ox1 -[#[_]]sum_ncycle_totient [#|_|]ox1 big_mkcond /=. -apply: eq_bigr => d _; rewrite -{2}ox1; case: ifP => [|ndv_dG]; last first. - rewrite eq_card0 // => C; apply/imsetP=> [[x /setIdP[Gx oxd] _{C}]]. - by rewrite -(eqP oxd) order_dvdG in ndv_dG. -move/cycle_sub_group; set Gd := [set _] => def_Gd. -rewrite (_ : _ @: _ = @gval _ @: Gd); first by rewrite imset_set1 cards1 mul1n. -apply/setP=> C; apply/idP/imsetP=> [| [gC GdC ->{C}]]. - case/imsetP=> x /setIdP[_ oxd] ->; exists <[x]>%G => //. - by rewrite -def_Gd inE -Zp_cycle subsetT. -have:= GdC; rewrite -def_Gd => /setIdP[_ /eqP <-]. -by rewrite (set1P GdC) /= mem_imset // inE eqxx (mem_cycle x1). -Qed. - -Section FieldMulCyclic. - -(***********************************************************************) -(* A classic application to finite multiplicative subgroups of fields. *) -(***********************************************************************) - -Import GRing.Theory. - -Variables (gT : finGroupType) (G : {group gT}). - -Lemma order_inj_cyclic : - {in G &, forall x y, #[x] = #[y] -> <[x]> = <[y]>} -> cyclic G. -Proof. -move=> ucG; apply: negbNE (contra _ (negbT (ltnn #|G|))) => ncG. -rewrite -{2}[#|G|]sum_totient_dvd big_mkcond (bigD1 ord_max) ?dvdnn //=. -rewrite -{1}[#|G|]sum_ncycle_totient (bigD1 ord_max) //= -addSn leq_add //. - rewrite eq_card0 ?totient_gt0 ?cardG_gt0 // => C. - apply/imsetP=> [[x /setIdP[Gx /eqP oxG]]]; case/cyclicP: ncG. - by exists x; apply/eqP; rewrite eq_sym eqEcard cycle_subG Gx -oxG /=. -elim/big_ind2: _ => // [m1 n1 m2 n2 | d _]; first exact: leq_add. -set Gd := _ @: _; case: (set_0Vmem Gd) => [-> | [C]]; first by rewrite cards0. -rewrite {}/Gd => /imsetP[x /setIdP[Gx /eqP <-] _ {C d}]. -rewrite order_dvdG // (@eq_card1 _ <[x]>) ?mul1n // => C. -apply/idP/eqP=> [|-> {C}]; last by rewrite mem_imset // inE Gx eqxx. -by case/imsetP=> y /setIdP[Gy /eqP/ucG->]. -Qed. - -Lemma div_ring_mul_group_cyclic (R : unitRingType) (f : gT -> R) : - f 1 = 1%R -> {in G &, {morph f : u v / u * v >-> (u * v)%R}} -> - {in G^#, forall x, f x - 1 \in GRing.unit}%R -> - abelian G -> cyclic G. -Proof. -move=> f1 fM f1P abelG. -have fX n: {in G, {morph f : u / u ^+ n >-> (u ^+ n)%R}}. - by case: n => // n x Gx; elim: n => //= n IHn; rewrite expgS fM ?groupX ?IHn. -have fU x: x \in G -> f x \in GRing.unit. - by move=> Gx; apply/unitrP; exists (f x^-1); rewrite -!fM ?groupV ?gsimp. -apply: order_inj_cyclic => x y Gx Gy; set n := #[x] => yn. -apply/eqP; rewrite eq_sym eqEcard -[#|_|]/n yn leqnn andbT cycle_subG /=. -suff{y Gy yn} ->: <[x]> = G :&: [set z | #[z] %| n] by rewrite !inE Gy yn /=. -apply/eqP; rewrite eqEcard subsetI cycle_subG {}Gx /= cardE; set rs := enum _. -apply/andP; split; first by apply/subsetP=> y xy; rewrite inE order_dvdG. -pose P : {poly R} := ('X^n - 1)%R; have n_gt0: n > 0 by exact: order_gt0. -have szP: size P = n.+1 by rewrite size_addl size_polyXn ?size_opp ?size_poly1. -rewrite -ltnS -szP -(size_map f) max_ring_poly_roots -?size_poly_eq0 ?{}szP //. - apply/allP=> fy /mapP[y]; rewrite mem_enum !inE order_dvdn => /andP[Gy]. - move/eqP=> yn1 ->{fy}; apply/eqP. - by rewrite !(hornerE, hornerXn) -fX // yn1 f1 subrr. -have: uniq rs by exact: enum_uniq. -have: all (mem G) rs by apply/allP=> y; rewrite mem_enum; case/setIP. -elim: rs => //= y rs IHrs /andP[Gy Grs] /andP[y_rs]; rewrite andbC. -move/IHrs=> -> {IHrs}//; apply/allP=> _ /mapP[z rs_z ->]. -have{Grs} Gz := allP Grs z rs_z; rewrite /diff_roots -!fM // (centsP abelG) //. -rewrite eqxx -[f y]mul1r -(mulgKV y z) fM ?groupM ?groupV //=. -rewrite -mulNr -mulrDl unitrMl ?fU ?f1P // !inE. -by rewrite groupM ?groupV // andbT -eq_mulgV1; apply: contra y_rs; move/eqP <-. -Qed. - -Lemma field_mul_group_cyclic (F : fieldType) (f : gT -> F) : - {in G &, {morph f : u v / u * v >-> (u * v)%R}} -> - {in G, forall x, f x = 1%R <-> x = 1} -> - cyclic G. -Proof. -move=> fM f1P; have f1 : f 1 = 1%R by exact/f1P. -apply: (div_ring_mul_group_cyclic f1 fM) => [x|]. - case/setD1P=> x1 Gx; rewrite unitfE; apply: contra x1. - by rewrite subr_eq0 => /eqP/f1P->. -apply/centsP=> x Gx y Gy; apply/commgP/eqP. -apply/f1P; rewrite ?fM ?groupM ?groupV //. -by rewrite mulrCA -!fM ?groupM ?groupV // mulKg mulVg. -Qed. - -End FieldMulCyclic. - -Lemma field_unit_group_cyclic (F : finFieldType) (G : {group {unit F}}) : - cyclic G. -Proof. -apply: field_mul_group_cyclic FinRing.uval _ _ => // u _. -by split=> /eqP ?; exact/eqP. -Qed. - -Section PrimitiveRoots. - -Open Scope ring_scope. -Import GRing.Theory. - -Lemma has_prim_root (F : fieldType) (n : nat) (rs : seq F) : - n > 0 -> all n.-unity_root rs -> uniq rs -> size rs >= n -> - has n.-primitive_root rs. -Proof. -move=> n_gt0 rsn1 Urs; rewrite leq_eqVlt ltnNge max_unity_roots // orbF eq_sym. -move/eqP=> sz_rs; pose r := val (_ : seq_sub rs). -have rn1 x: r x ^+ n = 1. - by apply/eqP; rewrite -unity_rootE (allP rsn1) ?(valP x). -have prim_r z: z ^+ n = 1 -> z \in rs. - by move/eqP; rewrite -unity_rootE -(mem_unity_roots n_gt0). -pose r' := SeqSub (prim_r _ _); pose sG_1 := r' _ (expr1n _ _). -have sG_VP: r _ ^+ n.-1 ^+ n = 1. - by move=> x; rewrite -exprM mulnC exprM rn1 expr1n. -have sG_MP: (r _ * r _) ^+ n = 1 by move=> x y; rewrite exprMn !rn1 mul1r. -pose sG_V := r' _ (sG_VP _); pose sG_M := r' _ (sG_MP _ _). -have sG_Ag: associative sG_M by move=> x y z; apply: val_inj; rewrite /= mulrA. -have sG_1g: left_id sG_1 sG_M by move=> x; apply: val_inj; rewrite /= mul1r. -have sG_Vg: left_inverse sG_1 sG_V sG_M. - by move=> x; apply: val_inj; rewrite /= -exprSr prednK ?rn1. -pose sgT := BaseFinGroupType _ (FinGroup.Mixin sG_Ag sG_1g sG_Vg). -pose gT := @FinGroupType sgT sG_Vg. -have /cyclicP[x gen_x]: @cyclic gT setT. - apply: (@field_mul_group_cyclic gT [set: _] F r) => // x _. - by split=> [ri1 | ->]; first exact: val_inj. -apply/hasP; exists (r x); first exact: (valP x). -have [m prim_x dvdmn] := prim_order_exists n_gt0 (rn1 x). -rewrite -((m =P n) _) // eqn_dvd {}dvdmn -sz_rs -(card_seq_sub Urs) -cardsT. -rewrite gen_x (@order_dvdn gT) /(_ == _) /= -{prim_x}(prim_expr_order prim_x). -by apply/eqP; elim: m => //= m IHm; rewrite exprS expgS /= -IHm. -Qed. - -End PrimitiveRoots. - -(***********************************************************************) -(* Cycles of prime order *) -(***********************************************************************) - -Section AutPrime. - -Variable gT : finGroupType. - -Lemma Aut_prime_cycle_cyclic (a : gT) : prime #[a] -> cyclic (Aut <[a]>). -Proof. -move=> pr_a; have inj_um := injm_Zp_unitm a; have eq_a := Fp_Zcast pr_a. -pose fm := cast_ord (esym eq_a) \o val \o invm inj_um. -apply: (@field_mul_group_cyclic _ _ _ fm) => [f g Af Ag | f Af] /=. - by apply: val_inj; rewrite /= morphM ?im_Zp_unitm //= eq_a. -split=> [/= fm1 |->]; last by apply: val_inj; rewrite /= morph1. -apply: (injm1 (injm_invm inj_um)); first by rewrite /= im_Zp_unitm. -by do 2!apply: val_inj; move/(congr1 val): fm1. -Qed. - -Lemma Aut_prime_cyclic (G : {group gT}) : prime #|G| -> cyclic (Aut G). -Proof. -move=> pr_G; case/cyclicP: (prime_cyclic pr_G) (pr_G) => x ->. -exact: Aut_prime_cycle_cyclic. -Qed. - -End AutPrime. diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v index 13daa31..0155a1b 100644 --- a/mathcomp/algebra/finalg.v +++ b/mathcomp/algebra/finalg.v @@ -1,12 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import choice fintype finset. -From mathcomp.fingroup -Require Import fingroup morphism perm action. -Require Import ssralg. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. +From mathcomp +Require Import ssralg finset fingroup morphism perm action. (*****************************************************************************) (* This file clones the entire ssralg hierachy for finite types; this allows *) @@ -155,7 +152,7 @@ Lemma zmodMgE x y : (x * y)%g = x + y. Proof. by []. Qed. Lemma zmodXgE n x : (x ^+ n)%g = x *+ n. Proof. by []. Qed. Lemma zmod_mulgC x y : commute x y. Proof. exact: GRing.addrC. Qed. Lemma zmod_abelian (A : {set U}) : abelian A. -Proof. by apply/centsP=> x _ y _; exact: zmod_mulgC. Qed. +Proof. by apply/centsP=> x _ y _; apply: zmod_mulgC. Qed. End AdditiveGroup. @@ -447,11 +444,11 @@ Lemma unit_mul_proof u v : val u * val v \is a GRing.unit. Proof. by rewrite (GRing.unitrMr _ (valP u)) ?(valP v). Qed. Definition unit_mul u v := Unit phR (unit_mul_proof u v). Lemma unit_muluA : associative unit_mul. -Proof. move=> u v w; apply: val_inj; exact: GRing.mulrA. Qed. +Proof. by move=> u v w; apply: val_inj; apply: GRing.mulrA. Qed. Lemma unit_mul1u : left_id unit1 unit_mul. -Proof. move=> u; apply: val_inj; exact: GRing.mul1r. Qed. +Proof. by move=> u; apply: val_inj; apply: GRing.mul1r. Qed. Lemma unit_mulVu : left_inverse unit1 unit_inv unit_mul. -Proof. move=> u; apply: val_inj; exact: GRing.mulVr (valP u). Qed. +Proof. by move=> u; apply: val_inj; apply: GRing.mulVr (valP u). Qed. Definition unit_GroupMixin := FinGroup.Mixin unit_muluA unit_mul1u unit_mulVu. Canonical unit_baseFinGroupType := @@ -829,12 +826,12 @@ Lemma decidable : GRing.DecidableField.axiom sat. Proof. move=> e f; elim: f e; try by move=> f1 IH1 f2 IH2 e /=; case IH1; case IH2; constructor; tauto. -- by move=> b e; exact: idP. -- by move=> t1 t2 e; exact: eqP. -- by move=> t e; exact: idP. +- by move=> b e; apply: idP. +- by move=> t1 t2 e; apply: eqP. +- by move=> t e; apply: idP. - by move=> f IH e /=; case: IH; constructor. -- by move=> i f IH e; apply: (iffP existsP) => [] [x fx]; exists x; exact/IH. -by move=> i f IH e; apply: (iffP forallP) => f_ x; exact/IH. +- by move=> i f IH e; apply: (iffP existsP) => [] [x fx]; exists x; apply/IH. +by move=> i f IH e; apply: (iffP forallP) => f_ x; apply/IH. Qed. Definition DecidableFieldMixin := DecFieldMixin decidable. diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v index 9ce2718..896a287 100644 --- a/mathcomp/algebra/fraction.v +++ b/mathcomp/algebra/fraction.v @@ -1,10 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import div choice tuple bigop generic_quotient. -Require Import ssralg poly polydiv. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat div seq choice tuple. +From mathcomp +Require Import bigop ssralg poly polydiv generic_quotient. (* This file builds the field of fraction of any integral domain. *) (* The main result of this file is the existence of the field *) diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index cdfde3c..4e4148a 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -1,13 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import path div choice fintype tuple finfun bigop prime. -From mathcomp.fingroup -Require Import perm. -Require Import ssralg poly ssrnum ssrint rat. -Require Import polydiv finalg zmodp matrix mxalgebra vector. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq path div choice. +From mathcomp +Require Import fintype tuple finfun bigop prime ssralg poly ssrnum ssrint rat. +From mathcomp +Require Import polydiv finalg perm zmodp matrix mxalgebra vector. (******************************************************************************) (* This file provides various results on divisibility of integers. *) @@ -489,7 +487,7 @@ have [-> | m_gt0] := posnP m; first by rewrite modz0. case: n => n; first by rewrite modz_nat gcdn_modr. rewrite modNz_nat // NegzE abszN {2}(divn_eq n m) -addnS gcdnMDl. rewrite -addrA -opprD -intS /=; set m1 := _.+1. -have le_m1m: (m1 <= m)%N by exact: ltn_pmod. +have le_m1m: (m1 <= m)%N by apply: ltn_pmod. by rewrite subzn // !(gcdnC m) -{2 3}(subnK le_m1m) gcdnDl gcdnDr gcdnC. Qed. @@ -851,13 +849,13 @@ Qed. Local Notation pZtoQ := (map_poly (intr : int -> rat)). Lemma size_rat_int_poly p : size (pZtoQ p) = size p. -Proof. by apply: size_map_inj_poly; first exact: intr_inj. Qed. +Proof. by apply: size_map_inj_poly; first apply: intr_inj. Qed. Lemma rat_poly_scale (p : {poly rat}) : {q : {poly int} & {a | a != 0 & p = a%:~R^-1 *: pZtoQ q}}. Proof. pose a := \prod_(i < size p) denq p`_i. -have nz_a: a != 0 by apply/prodf_neq0=> i _; exact: denq_neq0. +have nz_a: a != 0 by apply/prodf_neq0=> i _; apply: denq_neq0. exists (map_poly numq (a%:~R *: p)), a => //. apply: canRL (scalerK _) _; rewrite ?intr_eq0 //. apply/polyP=> i; rewrite !(coefZ, coef_map_id0) // numqK // Qint_def mulrC. @@ -927,7 +925,7 @@ wlog [j a'Mij]: m n M i Da le_mn / {j | ~~ (a %| M i j)%Z}; last first. have{leA} ltA: (`|b| < A)%N. rewrite -ltnS (leq_trans _ leA) // ltnS ltn_neqAle andbC. rewrite dvdn_leq ?absz_gt0 ? dvdn_gcdl //=. - by rewrite (contraNneq _ a'Mij) ?dvdzE // => <-; exact: dvdn_gcdr. + by rewrite (contraNneq _ a'Mij) ?dvdzE // => <-; apply: dvdn_gcdr. pose t2 := [fun j : 'I_2 => [tuple _; _]`_j : int]; pose a1 := M i 1. pose Uul := \matrix_(k, j) t2 (t2 u (- (a1 %/ b)%Z) j) (t2 v (a %/ b)%Z j) k. pose U : 'M_(2 + n) := block_mx Uul 0 0 1%:M; pose M1 := M *m U. @@ -995,7 +993,7 @@ exists (block_mx 1 0 Ml L). exists (block_mx 1 Mu 0 R). by rewrite unitmxE det_ublock det_scalar1 mul1r. exists (1 :: d); set D1 := \matrix_(i, j) _ in dM1. - by rewrite /= path_min_sorted // => g _; exact: dvd1n. + by rewrite /= path_min_sorted // => g _; apply: dvd1n. rewrite [D in _ *m D *m _](_ : _ = block_mx 1 0 0 D1); last first. by apply/matrixP=> i j; do 3?[rewrite ?mxE ?ord1 //=; case: splitP => ? ->]. rewrite !mulmx_block !(mul0mx, mulmx0, addr0) !mulmx1 add0r mul1mx -Da -dM1. @@ -1023,7 +1021,7 @@ have [K kerK]: {K : 'M_(k, m) | map_mx intr K == kermx S}%MS. apply/matrixP=> i j; rewrite 3!mxE mulrC [d](bigD1 (i, j)) // rmorphM mulrA. by rewrite -numqE -rmorphM numq_int. suffices nz_d: d%:Q != 0 by rewrite !eqmx_scale // !eq_row_base andbb. - by rewrite intr_eq0; apply/prodf_neq0 => i _; exact: denq_neq0. + by rewrite intr_eq0; apply/prodf_neq0 => i _; apply: denq_neq0. have [L _ [G uG [D _ defK]]] := int_Smith_normal_form K. pose Gud := castmx (Dm, Em) G; pose G'lr := castmx (Em, Dm) (invmx G). have{K L D defK kerK} kerGu: map_mx intr (usubmx Gud) *m S = 0. @@ -1046,7 +1044,7 @@ have{K L D defK kerK} kerGu: map_mx intr (usubmx Gud) *m S = 0. by rewrite -{2}[Gud]vsubmxK map_col_mx mul_row_col mul0mx addr0. pose T := map_mx intr (dsubmx Gud) *m S. have{kerGu} defS: map_mx intr (rsubmx G'lr) *m T = S. - have: G'lr *m Gud = 1%:M by rewrite /G'lr /Gud; case: _ / (Dm); exact: mulVmx. + have: G'lr *m Gud = 1%:M by rewrite /G'lr /Gud; case: _ / (Dm); apply: mulVmx. rewrite -{1}[G'lr]hsubmxK -[Gud]vsubmxK mulmxA mul_row_col -map_mxM. move/(canRL (addKr _))->; rewrite -mulNmx raddfD /= map_mx1 map_mxM /=. by rewrite mulmxDl -mulmxA kerGu mulmx0 add0r mul1mx. diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index bed19fa..fbc6f16 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -1,12 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import div choice fintype bigop finset. -From mathcomp.fingroup -Require Import fingroup. -Require Import ssralg zmodp ssrint ssrnum. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq div choice fintype. +From mathcomp +Require Import bigop ssralg finset fingroup zmodp ssrint ssrnum. (*****************************************************************************) (* This file provide support for intervals in numerical and real domains. *) @@ -31,8 +28,8 @@ Require Import ssralg zmodp ssrint ssrnum. (* when R is a real domain: we could provide a specific theory for this *) (* important case. *) (* *) -(* See also "Formal proofs in real algebraic geometry: from ordered fields *) -(* to quantifier elimination", LMCS journal, 2012 *) +(* See also ``Formal proofs in real algebraic geometry: from ordered fields *) +(* to quantifier elimination'', LMCS journal, 2012 *) (* by Cyril Cohen and Assia Mahboubi *) (* *) (* And "Formalized algebraic numbers: construction and first-order theory" *) @@ -148,10 +145,10 @@ Lemma lersifxx x b: (x <= x ?< if b) = ~~ b. Proof. by case: b; rewrite /= lterr. Qed. Lemma lersif_trans x y z b1 b2 : - x <= y ?< if b1 -> y <= z ?< if b2 -> x <= z ?< if b1 || b2. + x <= y ?< if b1 -> y <= z ?< if b2 -> x <= z ?< if b1 || b2. Proof. -move: b1 b2 => [] [] //=; -by [exact: ler_trans|exact: ler_lt_trans|exact: ltr_le_trans|exact: ltr_trans]. +case: b1; first by case: b2; [apply: ltr_trans | apply: ltr_le_trans]. +by case: b2; [apply: ler_lt_trans | apply: ler_trans]. Qed. Lemma lersifW b x y : x <= y ?< if b -> x <= y. diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 9339e67..b842c67 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1,12 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import div choice fintype finfun bigop prime binomial finset. -From mathcomp.fingroup -Require Import fingroup perm. -Require Import ssralg finalg zmodp. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. +From mathcomp +Require Import finfun bigop prime binomial ssralg finset fingroup finalg. +From mathcomp +Require Import perm zmodp. (******************************************************************************) (* Basic concrete linear algebra : definition of type for matrices, and all *) @@ -229,7 +228,7 @@ Proof. by move=> i j; rewrite unlock /fun_of_matrix /= ffunE. Qed. Lemma matrixP (A B : matrix) : A =2 B <-> A = B. Proof. rewrite /fun_of_matrix; split=> [/= eqAB | -> //]. -by apply/val_inj/ffunP=> [[i j]]; exact: eqAB. +by apply/val_inj/ffunP=> [[i j]]; apply: eqAB. Qed. End MatrixDef. @@ -573,7 +572,7 @@ Proof. by apply/matrixP=> i j; rewrite mxE row_mxEr. Qed. Lemma hsubmxK A : row_mx (lsubmx A) (rsubmx A) = A. Proof. apply/matrixP=> i j; rewrite !mxE. -case: splitP => k Dk //=; rewrite !mxE //=; congr (A _ _); exact: val_inj. +by case: splitP => k Dk //=; rewrite !mxE //=; congr (A _ _); apply: val_inj. Qed. Lemma col_mxEu A1 A2 i j : col_mx A1 A2 (lshift m2 i) j = A1 i j. @@ -1960,7 +1959,7 @@ Lemma mulmxE : mulmx = *%R. Proof. by []. Qed. Lemma idmxE : 1%:M = 1 :> 'M_n. Proof. by []. Qed. Lemma scalar_mx_is_multiplicative : multiplicative (@scalar_mx n). -Proof. by split=> //; exact: scalar_mxM. Qed. +Proof. by split=> //; apply: scalar_mxM. Qed. Canonical scalar_mx_rmorphism := AddRMorphism scalar_mx_is_multiplicative. End MatrixRing. @@ -2120,7 +2119,7 @@ Proof. by rewrite map_mx_sub map_mx1 map_pid_mx. Qed. Lemma map_mx_is_multiplicative n' (n := n'.+1) : multiplicative ((map_mx f) n n). -Proof. by split; [exact: map_mxM | exact: map_mx1]. Qed. +Proof. by split; [apply: map_mxM | apply: map_mx1]. Qed. Canonical map_mx_rmorphism n' := AddRMorphism (map_mx_is_multiplicative n'). @@ -2321,7 +2320,7 @@ transitivity (\sum_(f : F) \sum_(s : 'S_n) (-1) ^+ s * \prod_i AB s i (f i)). rewrite (bigID (fun f : F => injectiveb f)) /= addrC big1 ?add0r => [|f Uf]. rewrite (reindex (@pval _)) /=; last first. pose in_Sn := insubd (1%g : 'S_n). - by exists in_Sn => /= f Uf; first apply: val_inj; exact: insubdK. + by exists in_Sn => /= f Uf; first apply: val_inj; apply: insubdK. apply: eq_big => /= [s | s _]; rewrite ?(valP s) // big_distrr /=. rewrite (reindex_inj (mulgI s)); apply: eq_bigr => t _ /=. rewrite big_split /= mulrA mulrCA mulrA mulrCA mulrA. @@ -2766,13 +2765,13 @@ Local Notation "A ^f" := (map_mx f A) : ring_scope. Lemma map_mx_inj m n : injective ((map_mx f) m n). Proof. move=> A B eq_AB; apply/matrixP=> i j. -by move/matrixP/(_ i j): eq_AB; rewrite !mxE; exact: fmorph_inj. +by move/matrixP/(_ i j): eq_AB; rewrite !mxE; apply: fmorph_inj. Qed. Lemma map_mx_is_scalar n (A : 'M_n) : is_scalar_mx A^f = is_scalar_mx A. Proof. rewrite /is_scalar_mx; case: (insub _) => // i. -by rewrite mxE -map_scalar_mx inj_eq //; exact: map_mx_inj. +by rewrite mxE -map_scalar_mx inj_eq //; apply: map_mx_inj. Qed. Lemma map_unitmx n (A : 'M_n) : (A^f \in unitmx) = (A \in unitmx). @@ -2829,7 +2828,7 @@ Proof. elim: n => [|n IHn] /= in A *; first exact: is_perm_mx1. set A' := _ - _; move/(_ A'): IHn; case: cormen_lup => [[P L U]] {A'}/=. rewrite (is_perm_mxMr _ (perm_mx_is_perm _ _)). -case/is_perm_mxP => s ->; exact: lift0_mx_is_perm. +by case/is_perm_mxP => s ->; apply: lift0_mx_is_perm. Qed. Lemma cormen_lup_correct n (A : 'M_n.+1) : @@ -2861,7 +2860,7 @@ Proof. elim: n => [|n IHn] /= in A i j *; first by rewrite [i]ord1 [j]ord1 mxE. set A' := _ - _; move/(_ A'): IHn; case: cormen_lup => [[P L U]] {A'}/= Ll. rewrite !mxE split1; case: unliftP => [i'|] -> /=; rewrite !mxE split1. - by case: unliftP => [j'|] -> //; exact: Ll. + by case: unliftP => [j'|] -> //; apply: Ll. by case: unliftP => [j'|] ->; rewrite /= mxE. Qed. @@ -2871,7 +2870,7 @@ Proof. elim: n => [|n IHn] /= in A i j *; first by rewrite [i]ord1. set A' := _ - _; move/(_ A'): IHn; case: cormen_lup => [[P L U]] {A'}/= Uu. rewrite !mxE split1; case: unliftP => [i'|] -> //=; rewrite !mxE split1. -by case: unliftP => [j'|] ->; [exact: Uu | rewrite /= mxE]. +by case: unliftP => [j'|] ->; [apply: Uu | rewrite /= mxE]. Qed. End CormenLUP. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index cb1717c..bb5caab 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -1,12 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import div choice fintype finfun bigop prime binomial finset. -From mathcomp.fingroup -Require Import fingroup perm. -Require Import ssralg finalg zmodp matrix. +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. +From mathcomp +Require Import finfun bigop prime binomial ssralg finset fingroup finalg. +From mathcomp +Require Import perm zmodp matrix. (*****************************************************************************) (* In this file we develop the rank and row space theory of matrices, based *) @@ -440,7 +439,7 @@ Proof. set MN := M *m N; set rMN := \rank _. pose L : 'M_(rMN, m) := pid_mx rMN *m invmx (col_ebase MN). pose U : 'M_(n, rMN) := invmx (row_ebase MN) *m pid_mx rMN. -suffices: L *m M *m (N *m U) = 1%:M by exact: mulmx1_min. +suffices: L *m M *m (N *m U) = 1%:M by apply: mulmx1_min. rewrite mulmxA -(mulmxA L) -[M *m N]mulmx_ebase -/MN. by rewrite !mulmxA mulmxKV // mulmxK // !pid_mx_id /rMN ?pid_mx_1. Qed. @@ -531,14 +530,14 @@ Proof. by case/submxP=> D ->; rewrite mulmxA submxMl. Qed. Lemma submx_trans m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) : (A <= B -> B <= C -> A <= C)%MS. -Proof. by case/submxP=> D ->{A}; exact: mulmx_sub. Qed. +Proof. by case/submxP=> D ->{A}; apply: mulmx_sub. Qed. Lemma ltmx_sub_trans m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) : (A < B)%MS -> (B <= C)%MS -> (A < C)%MS. Proof. case/andP=> sAB ltAB sBC; rewrite ltmxE (submx_trans sAB) //. -by apply: contra ltAB; exact: submx_trans. +by apply: contra ltAB; apply: submx_trans. Qed. Lemma sub_ltmx_trans m1 m2 m3 n @@ -546,11 +545,11 @@ Lemma sub_ltmx_trans m1 m2 m3 n (A <= B)%MS -> (B < C)%MS -> (A < C)%MS. Proof. move=> sAB /andP[sBC ltBC]; rewrite ltmxE (submx_trans sAB) //. -by apply: contra ltBC => sCA; exact: submx_trans sAB. +by apply: contra ltBC => sCA; apply: submx_trans sAB. Qed. Lemma ltmx_trans m n : transitive (@ltmx m m n). -Proof. by move=> A B C; move/ltmxW; exact: sub_ltmx_trans. Qed. +Proof. by move=> A B C; move/ltmxW; apply: sub_ltmx_trans. Qed. Lemma ltmx_irrefl m n : irreflexive (@ltmx m m n). Proof. by move=> A; rewrite /ltmx submx_refl andbF. Qed. @@ -563,7 +562,7 @@ Lemma submx0null m1 m2 n (A : 'M[F]_(m1, n)) : Proof. by case/submxP=> D; rewrite mulmx0. Qed. Lemma submx0 m n (A : 'M_(m, n)) : (A <= (0 : 'M_n))%MS = (A == 0). -Proof. by apply/idP/eqP=> [|->]; [exact: submx0null | exact: sub0mx]. Qed. +Proof. by apply/idP/eqP=> [|->]; [apply: submx0null | apply: sub0mx]. Qed. Lemma lt0mx m n (A : 'M_(m, n)) : ((0 : 'M_n) < A)%MS = (A != 0). Proof. by rewrite /ltmx sub0mx submx0. Qed. @@ -572,7 +571,7 @@ Lemma ltmx0 m n (A : 'M[F]_(m, n)) : (A < (0 : 'M_n))%MS = false. Proof. by rewrite /ltmx sub0mx andbF. Qed. Lemma eqmx0P m n (A : 'M_(m, n)) : reflect (A = 0) (A == (0 : 'M_n))%MS. -Proof. by rewrite submx0 sub0mx andbT; exact: eqP. Qed. +Proof. by rewrite submx0 sub0mx andbT; apply: eqP. Qed. Lemma eqmx_eq0 m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :=: B)%MS -> (A == 0) = (B == 0). @@ -588,7 +587,7 @@ Lemma summx_sub m1 m2 n (B : 'M_(m2, n)) I (r : seq I) (P : pred I) (A_ : I -> 'M_(m1, n)) : (forall i, P i -> A_ i <= B)%MS -> ((\sum_(i <- r | P i) A_ i)%R <= B)%MS. Proof. -move=> leAB; elim/big_ind: _ => // [|A1 A2]; [exact: sub0mx | exact: addmx_sub]. +by move=> leAB; elim/big_ind: _ => // [|C D]; [apply/sub0mx | apply/addmx_sub]. Qed. Lemma scalemx_sub m1 m2 n a (A : 'M_(m1, n)) (B : 'M_(m2, n)) : @@ -608,7 +607,7 @@ Lemma row_subP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (forall i, row i A <= B)%MS (A <= B)%MS. Proof. apply: (iffP idP) => [sAB i|sAB]. - by apply: submx_trans sAB; exact: row_sub. + by apply: submx_trans sAB; apply: row_sub. rewrite submxE; apply/eqP/row_matrixP=> i; apply/eqP. by rewrite row_mul row0 -submxE. Qed. @@ -624,7 +623,7 @@ Implicit Arguments rV_subP [m1 m2 n A B]. Lemma row_subPn m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (exists i, ~~ (row i A <= B)%MS) (~~ (A <= B)%MS). -Proof. by rewrite (sameP row_subP forallP) negb_forall; exact: existsP. Qed. +Proof. by rewrite (sameP row_subP forallP) negb_forall; apply: existsP. Qed. Lemma sub_rVP n (u v : 'rV_n) : reflect (exists a, u = a *: v) (u <= v)%MS. Proof. @@ -636,14 +635,14 @@ Qed. Lemma rank_rV n (v : 'rV_n) : \rank v = (v != 0). Proof. case: eqP => [-> | nz_v]; first by rewrite mxrank0. -by apply/eqP; rewrite eqn_leq rank_leq_row lt0n mxrank_eq0; exact/eqP. +by apply/eqP; rewrite eqn_leq rank_leq_row lt0n mxrank_eq0; apply/eqP. Qed. Lemma rowV0Pn m n (A : 'M_(m, n)) : reflect (exists2 v : 'rV_n, v <= A & v != 0)%MS (A != 0). Proof. rewrite -submx0; apply: (iffP idP) => [| [v svA]]; last first. - by rewrite -submx0; exact: contra (submx_trans _). + by rewrite -submx0; apply: contra (submx_trans _). by case/row_subPn=> i; rewrite submx0; exists (row i A); rewrite ?row_sub. Qed. @@ -651,7 +650,7 @@ Lemma rowV0P m n (A : 'M_(m, n)) : reflect (forall v : 'rV_n, v <= A -> v = 0)%MS (A == 0). Proof. rewrite -[A == 0]negbK; case: rowV0Pn => IH. - by right; case: IH => v svA nzv IH; case/eqP: nzv; exact: IH. + by right; case: IH => v svA nzv IH; case/eqP: nzv; apply: IH. by left=> v svA; apply/eqP; apply/idPn=> nzv; case: IH; exists v. Qed. @@ -703,7 +702,7 @@ Lemma mxrank_unit n (A : 'M_n) : A \in unitmx -> \rank A = n. Proof. by rewrite -row_full_unit =>/eqnP. Qed. Lemma mxrank1 n : \rank (1%:M : 'M_n) = n. -Proof. by apply: mxrank_unit; exact: unitmx1. Qed. +Proof. by apply: mxrank_unit; apply: unitmx1. Qed. Lemma mxrank_delta m n i j : \rank (delta_mx i j : 'M_(m, n)) = 1%N. Proof. @@ -736,8 +735,8 @@ Lemma eqmxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : Proof. apply: (iffP andP) => [[sAB sBA] | eqAB]; last by rewrite !eqAB. split=> [|m3 C]; first by apply/eqP; rewrite eqn_leq !mxrankS. -split; first by apply/idP/idP; exact: submx_trans. -by apply/idP/idP=> sC; exact: submx_trans sC _. +split; first by apply/idP/idP; apply: submx_trans. +by apply/idP/idP=> sC; apply: submx_trans sC _. Qed. Implicit Arguments eqmxP [m1 m2 n A B]. @@ -872,7 +871,7 @@ by rewrite qidmx_eq1 row_full_unit unitmx1 => /eqP. Qed. Lemma genmx_id m n (A : 'M_(m, n)) : (<<<<A>>>> = <<A>>)%MS. -Proof. by apply: eq_genmx; exact: genmxE. Qed. +Proof. by apply: eq_genmx; apply: genmxE. Qed. Lemma row_base_free m n (A : 'M_(m, n)) : row_free (row_base A). Proof. by apply/eqnP; rewrite eq_row_base. Qed. @@ -899,7 +898,7 @@ Qed. Lemma mxrank_leqif_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A <= B)%MS -> \rank A <= \rank B ?= iff (A == B)%MS. -Proof. by move=> sAB; rewrite sAB; exact: mxrank_leqif_sup. Qed. +Proof. by move=> sAB; rewrite sAB; apply: mxrank_leqif_sup. Qed. Lemma ltmxErank m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A < B)%MS = (A <= B)%MS && (\rank A < \rank B). @@ -1044,7 +1043,7 @@ Qed. Lemma addsmx_addKr n m1 m2 (A B : 'M_(m1, n)) (C : 'M_(m2, n)) : (B <= C)%MS -> ((A + B)%R + C :=: A + C)%MS. -Proof. by rewrite -!(addsmxC C) addrC; exact: addsmx_addKl. Qed. +Proof. by rewrite -!(addsmxC C) addrC; apply: addsmx_addKl. Qed. Lemma adds_eqmx m1 m2 m3 m4 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) (D : 'M_(m4, n)) : @@ -1114,7 +1113,7 @@ Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I -> 'M_n) : (A <= \sum_(i | P i) B_ i)%MS. Proof. apply: (iffP idP) => [| [u_ ->]]; last first. - by apply: summx_sub_sums => i _; exact: submxMl. + by apply: summx_sub_sums => i _; apply: submxMl. elim: {P}_.+1 {-2}P A (ltnSn #|P|) => // b IHb P A. case: (pickP P) => [i Pi | P0 _]; last first. rewrite big_pred0 //; move/submx0null->. @@ -1137,7 +1136,7 @@ Qed. Lemma sumsmxMr P n (A_ : I -> 'M[F]_n) (B : 'M_n) : ((\sum_(i | P i) A_ i)%MS *m B :=: \sum_(i | P i) (A_ i *m B))%MS. Proof. -by apply: eqmx_trans (sumsmxMr_gen _ _ _) (eqmx_sums _) => i _; exact: genmxE. +by apply: eqmx_trans (sumsmxMr_gen _ _ _) (eqmx_sums _) => i _; apply: genmxE. Qed. Lemma rank_pid_mx m n r : r <= m -> r <= n -> \rank (pid_mx r : 'M_(m, n)) = r. @@ -1194,7 +1193,7 @@ Lemma mulmx0_rank_max m n p (A : 'M_(m, n)) (B : 'M_(n, p)) : A *m B = 0 -> \rank A + \rank B <= n. Proof. move=> AB0; rewrite -{3}(subnK (rank_leq_row B)) leq_add2r. -rewrite -mxrank_ker mxrankS //; exact/sub_kermxP. +by rewrite -mxrank_ker mxrankS //; apply/sub_kermxP. Qed. Lemma mxrank_Frobenius m n p q (A : 'M_(m, n)) B (C : 'M_(p, q)) : @@ -1261,14 +1260,14 @@ move=> eqABid /eqmxP eqAB. have{eqABid eqAB} eqAB: equivmx A (qidmx A) =1 equivmx B (qidmx B). by move=> C; rewrite /equivmx eqABid !eqAB. rewrite {1}/capmx_norm (eq_choose eqAB). -by apply: choose_id; first rewrite -eqAB; exact: capmx_witnessP. +by apply: choose_id; first rewrite -eqAB; apply: capmx_witnessP. Qed. Let capmx_nopP m n (A : 'M_(m, n)) : equivmx_spec A (qidmx A) (capmx_nop A). Proof. rewrite /capmx_nop; case: (eqVneq m n) => [-> | ne_mn] in A *. by rewrite conform_mx_id. -rewrite nonconform_mx ?ne_mn //; exact: capmx_normP. +by rewrite nonconform_mx ?ne_mn //; apply: capmx_normP. Qed. Let sub_qidmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : @@ -1340,7 +1339,7 @@ Qed. Lemma capmx_idPl n m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (A :&: B :=: A)%MS (A <= B)%MS. -Proof. by rewrite capmxC; exact: capmx_idPr. Qed. +Proof. by rewrite capmxC; apply: capmx_idPr. Qed. Lemma capmxS m1 m2 m3 m4 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) (D : 'M_(m4, n)) : @@ -1449,7 +1448,7 @@ Qed. Lemma matrix_modr m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) : (C <= A -> (A :&: B) + C :=: A :&: (B + C))%MS. -Proof. by rewrite !(capmxC A) -!(addsmxC C); exact: matrix_modl. Qed. +Proof. by rewrite !(capmxC A) -!(addsmxC C); apply: matrix_modl. Qed. Lemma capmx_compl m n (A : 'M_(m, n)) : (A :&: A^C)%MS = 0. Proof. @@ -1477,7 +1476,7 @@ Lemma mxrank_injP m n p (A : 'M_(m, n)) (f : 'M_(n, p)) : reflect (\rank (A *m f) = \rank A) ((A :&: kermx f)%MS == 0). Proof. rewrite -mxrank_eq0 -(eqn_add2l (\rank (A *m f))). -by rewrite mxrank_mul_ker addn0 eq_sym; exact: eqP. +by rewrite mxrank_mul_ker addn0 eq_sym; apply: eqP. Qed. Lemma mxrank_disjoint_sum m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : @@ -1828,7 +1827,7 @@ Qed. Lemma mxdirect_addsP (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (A :&: B = 0)%MS (mxdirect (A + B)). -Proof. by rewrite mxdirect_addsE !mxdirect_trivial; exact: eqP. Qed. +Proof. by rewrite mxdirect_addsE !mxdirect_trivial; apply: eqP. Qed. End BinaryDirect. @@ -1870,7 +1869,7 @@ Lemma mxdirect_sumsE (S_ : I -> mxsum_expr n n) (xunwrap := unwrap) : Proof. apply: (iffP (mxdirect_sums_recP _)) => [dxS | [dxS_ dxS] i Pi]. by do [split; last apply/mxdirect_sumsP] => i; case/dxS. -by split; [exact: dxS_ | exact: mxdirect_sumsP Pi]. +by split; [apply: dxS_ | apply: mxdirect_sumsP Pi]. Qed. End NaryDirect. @@ -1937,7 +1936,7 @@ Lemma eigenspaceP a m (W : 'M_(m, n)) : reflect (W *m g = a *: W) (W <= eigenspace a)%MS. Proof. rewrite (sameP (sub_kermxP _ _) eqP). -by rewrite mulmxBr subr_eq0 mul_mx_scalar; exact: eqP. +by rewrite mulmxBr subr_eq0 mul_mx_scalar; apply: eqP. Qed. Lemma eigenvalueP a : @@ -1961,7 +1960,7 @@ have nz_aij: a_ i - a_ j != 0. case: (sub_dsumsmx dxVi' (sub0mx 1 _)) => C _ _ uniqC. rewrite -(eqmx_eq0 (eqmx_scale _ nz_aij)). rewrite (uniqC (fun k => (a_ i - a_ k) *: u k)) => // [|k Pi'k|]. -- by rewrite -(uniqC (fun _ => 0)) ?big1 // => k Pi'k; exact: sub0mx. +- by rewrite -(uniqC (fun _ => 0)) ?big1 // => k Pi'k; apply: sub0mx. - by rewrite scalemx_sub ?Vi'u. rewrite -{1}(subrr (v *m g)) {1}def_vg def_v scaler_sumr mulmx_suml -sumrB. by apply: eq_bigr => k /Vi'u/eigenspaceP->; rewrite scalerBl. @@ -2220,7 +2219,7 @@ Lemma memmx_subP m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) : reflect (forall A, A \in R1 -> A \in R2) (R1 <= R2)%MS. Proof. apply: (iffP idP) => [sR12 A R1_A | sR12]; first exact: submx_trans sR12. -by apply/rV_subP=> vA; rewrite -(vec_mxK vA); exact: sR12. +by apply/rV_subP=> vA; rewrite -(vec_mxK vA); apply: sR12. Qed. Implicit Arguments memmx_subP [m1 m2 n R1 R2]. @@ -2270,7 +2269,7 @@ rewrite -{2}rankS (ltn_leqif (mxrank_leqif_sup sSR)). apply: (iffP idP) => [/row_subPn[i] | [A sAR]]. rewrite -[row i R]vec_mxK memmx1; set A := vec_mx _ => nsA. by exists A; rewrite // vec_mxK row_sub. -by rewrite -memmx1; apply: contra; exact: submx_trans. +by rewrite -memmx1; apply/contra/submx_trans. Qed. Definition mulsmx m1 m2 n (R1 : 'A[F]_(m1, n)) (R2 : 'A_(m2, n)) := @@ -2313,7 +2312,7 @@ Lemma mulsmxS m1 m2 m3 m4 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R1 <= R3 -> R2 <= R4 -> R1 * R2 <= R3 * R4)%MS. Proof. move=> sR13 sR24; apply/mulsmx_subP=> A1 A2 R_A1 R_A2. -by apply: mem_mulsmx; [exact: submx_trans sR13 | exact: submx_trans sR24]. +by apply: mem_mulsmx; [apply: submx_trans sR13 | apply: submx_trans sR24]. Qed. Lemma muls_eqmx m1 m2 m3 m4 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) @@ -2481,7 +2480,7 @@ Qed. Implicit Arguments cent_mxP [m n B R]. Lemma scalar_mx_cent m n a (R : 'A_(m, n)) : (a%:M \in 'C(R))%MS. -Proof. by apply/cent_mxP=> A _; exact: scalar_mxC. Qed. +Proof. by apply/cent_mxP=> A _; apply: scalar_mxC. Qed. Lemma center_mx_sub m n (R : 'A_(m, n)) : ('Z(R) <= R)%MS. Proof. exact: capmxSl. Qed. @@ -2762,7 +2761,7 @@ by rewrite map_mx_sub ? map_mxM. Qed. Lemma map_center_mx m n (E : 'A_(m, n)) : (('Z(E))^f :=: 'Z(E^f))%MS. -Proof. by rewrite /center_mx -map_cent_mx; exact: map_capmx. Qed. +Proof. by rewrite /center_mx -map_cent_mx; apply: map_capmx. Qed. End MapMatrixSpaces. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index bc5a998..7071687 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -1,12 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import div fintype tuple finfun bigop. -From mathcomp.fingroup -Require Import fingroup perm. -Require Import ssralg zmodp matrix mxalgebra poly polydiv. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq div fintype tuple. +From mathcomp +Require Import finfun bigop fingroup perm ssralg zmodp matrix mxalgebra. +From mathcomp +Require Import poly polydiv. (******************************************************************************) (* This file provides basic support for formal computation with matrices, *) @@ -384,7 +383,7 @@ pose Msize (A : M_RX) := \max_i \max_j size (A i j). pose phi (A : M_RX) := \poly_(k < Msize A) \matrix_(i, j) (A i j)`_k. have coef_phi A i j k: (phi A)`_k i j = (A i j)`_k. rewrite coef_poly; case: (ltnP k _) => le_m_k; rewrite mxE // nth_default //. - apply: leq_trans (leq_trans (leq_bigmax i) le_m_k); exact: (leq_bigmax j). + by apply: leq_trans (leq_trans (leq_bigmax i) le_m_k); apply: (leq_bigmax j). have phi_is_rmorphism : rmorphism phi. do 2?[split=> [A B|]]; apply/polyP=> k; apply/matrixP=> i j; last 1 first. - rewrite coef_phi mxE coefMn !coefC. @@ -496,7 +495,7 @@ Qed. Lemma minpoly_mx_ring : mxring Ad. Proof. -apply/andP; split; first by apply/mulsmx_subP; exact: minpoly_mxM. +apply/andP; split; first by apply/mulsmx_subP; apply: minpoly_mxM. apply/mxring_idP; exists 1%:M; split=> *; rewrite ?mulmx1 ?mul1mx //. by rewrite -mxrank_eq0 mxrank1. exact: minpoly_mx1. @@ -562,7 +561,7 @@ by rewrite -rmorphM horner_mx_C -rmorphD /= scalar_mx_is_scalar. Qed. Lemma mxminpoly_dvd_char : p_A %| char_poly A. -Proof. by apply: mxminpoly_min; exact: Cayley_Hamilton. Qed. +Proof. by apply: mxminpoly_min; apply: Cayley_Hamilton. Qed. Lemma eigenvalue_root_min a : eigenvalue A a = root p_A a. Proof. @@ -784,7 +783,7 @@ have{mon_p pw0 intRp intRq}: genI S. split; set S1 := _ ++ _; first exists p. split=> // i; rewrite -[p]coefK coef_poly; case: ifP => // lt_i_p. by apply: genS; rewrite mem_cat orbC mem_nth. - have: all (mem S1) S1 by exact/allP. + have: all (mem S1) S1 by apply/allP. elim: {-1}S1 => //= y S2 IH /andP[S1y S12]; split; last exact: IH. have{q S S1 IH S1y S12 intRp intRq} [q mon_q qx0]: integralOver RtoK y. by move: S1y; rewrite mem_cat => /orP[]; [apply: intRq | apply: intRp]. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 2757b30..9b2366e 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1,11 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. -From mathcomp.discrete -Require Import div choice fintype bigop binomial. -Require Import ssralg. - +From mathcomp +Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. +From mathcomp +Require Import bigop ssralg binomial. (******************************************************************************) (* This file provides a library for univariate polynomials over ring *) @@ -195,7 +193,7 @@ Proof. split=> [eq_pq | -> //]; apply: poly_inj. without loss lt_pq: p q eq_pq / size p < size q. move=> IH; case: (ltngtP (size p) (size q)); try by move/IH->. - move/(@eq_from_nth _ 0); exact. + by move/(@eq_from_nth _ 0); apply. case: q => q nz_q /= in lt_pq eq_pq *; case/eqP: nz_q. by rewrite (last_nth 0) -(subnKC lt_pq) /= -eq_pq nth_default ?leq_addr. Qed. @@ -236,7 +234,7 @@ by rewrite !polyseqC !eqxx nz_c. Qed. Lemma polyseqK p : Poly p = p. -Proof. by apply: poly_inj; exact: PolyK (valP p). Qed. +Proof. by apply: poly_inj; apply: PolyK (valP p). Qed. Lemma size_Poly s : size (Poly s) <= size s. Proof. @@ -364,7 +362,7 @@ Lemma nil_poly p : nilp p = (p == 0). Proof. exact: size_poly_eq0. Qed. Lemma poly0Vpos p : {p = 0} + {size p > 0}. -Proof. by rewrite lt0n size_poly_eq0; exact: eqVneq. Qed. +Proof. by rewrite lt0n size_poly_eq0; apply: eqVneq. Qed. Lemma polySpred p : p != 0 -> size p = (size p).-1.+1. Proof. by rewrite -size_poly_eq0 -lt0n => /prednK. Qed. @@ -612,7 +610,7 @@ Lemma polyC_mul : {morph polyC : a b / a * b}. Proof. by move=> a b; apply/polyP=> [[|i]]; rewrite coefCM !coefC ?simp. Qed. Fact polyC_multiplicative : multiplicative polyC. -Proof. by split; first exact: polyC_mul. Qed. +Proof. by split; first apply: polyC_mul. Qed. Canonical polyC_rmorphism := AddRMorphism polyC_multiplicative. Lemma polyC_exp n : {morph polyC : c / c ^+ n}. @@ -744,7 +742,7 @@ Lemma poly_ind (K : {poly R} -> Type) : K 0 -> (forall p c, K p -> K (p * 'X + c%:P)) -> (forall p, K p). Proof. move=> K0 Kcons p; rewrite -[p]polyseqK. -elim: {p}(p : seq R) => //= p c IHp; rewrite cons_poly_def; exact: Kcons. +by elim: {p}(p : seq R) => //= p c IHp; rewrite cons_poly_def; apply: Kcons. Qed. Lemma polyseqXsubC a : 'X - a%:P = [:: - a; 1] :> seq R. @@ -804,7 +802,7 @@ Lemma size_polyXn n : size 'X^n = n.+1. Proof. by rewrite polyseqXn size_rcons size_nseq. Qed. Lemma commr_polyXn p n : GRing.comm p 'X^n. -Proof. by apply: commrX; exact: commr_polyX. Qed. +Proof. by apply: commrX; apply: commr_polyX. Qed. Lemma lead_coefXn n : lead_coef 'X^n = 1. Proof. by rewrite /lead_coef nth_last polyseqXn last_rcons. Qed. @@ -848,7 +846,7 @@ Lemma monicX : 'X \is monic. Proof. exact/eqP/lead_coefX. Qed. Lemma monicXn n : 'X^n \is monic. Proof. exact/eqP/lead_coefXn. Qed. Lemma monic_neq0 p : p \is monic -> p != 0. -Proof. by rewrite -lead_coef_eq0 => /eqP->; exact: oner_neq0. Qed. +Proof. by rewrite -lead_coef_eq0 => /eqP->; apply: oner_neq0. Qed. Lemma lead_coef_monicM p q : p \is monic -> lead_coef (p * q) = lead_coef q. Proof. @@ -898,7 +896,7 @@ Proof. exact/eqP/lead_coefXsubC. Qed. Lemma monic_prod_XsubC I rI (P : pred I) (F : I -> R) : \prod_(i <- rI | P i) ('X - (F i)%:P) \is monic. -Proof. by apply: monic_prod => i _; exact: monicXsubC. Qed. +Proof. by apply: monic_prod => i _; apply: monicXsubC. Qed. Lemma size_prod_XsubC I rI (F : I -> R) : size (\prod_(i <- rI) ('X - (F i)%:P)) = (size rI).+1. @@ -968,7 +966,7 @@ Qed. Lemma monic_comreg p : p \is monic -> GRing.comm p (lead_coef p)%:P /\ GRing.rreg (lead_coef p). -Proof. by move/monicP->; split; [exact: commr1 | exact: rreg1]. Qed. +Proof. by move/monicP->; split; [apply: commr1 | apply: rreg1]. Qed. (* Horner evaluation of polynomials *) Implicit Types s rs : seq R. @@ -1191,7 +1189,7 @@ by rewrite /root_of_unity rootE hornerD hornerN hornerXn hornerC subr_eq0. Qed. Lemma unity_rootP n z : reflect (z ^+ n = 1) (n.-unity_root z). -Proof. by rewrite unity_rootE; exact: eqP. Qed. +Proof. by rewrite unity_rootE; apply: eqP. Qed. Definition primitive_root_of_unity n z := (n > 0) && [forall i : 'I_n, i.+1.-unity_root z == (i.+1 == n)]. @@ -1257,7 +1255,7 @@ set q := (n %/ d)%N; rewrite /q.-primitive_root ltn_divRL // n_gt0. apply/forallP=> i; rewrite unity_rootE -exprM -prim_order_dvd. rewrite -(divnK d_dv_n) -/q -(divnK d_dv_k) mulnAC dvdn_pmul2r //. apply/eqP; apply/idP/idP=> [|/eqP->]; last by rewrite dvdn_mull. -rewrite Gauss_dvdr; first by rewrite eqn_leq ltn_ord; exact: dvdn_leq. +rewrite Gauss_dvdr; first by rewrite eqn_leq ltn_ord; apply: dvdn_leq. by rewrite /coprime gcdnC -(eqn_pmul2r d_gt0) mul1n muln_gcdl !divnK. Qed. @@ -1326,7 +1324,7 @@ by rewrite qualifE polyseqC; case: eqP => [->|] /=; rewrite ?andbT ?rpred0. Qed. Fact polyOver_addr_closed : addr_closed (polyOver kS). -Proof. +Proof. split=> [|p q Sp Sq]; first exact: polyOver0. by apply/polyOverP=> i; rewrite coefD rpredD ?(polyOverP _). Qed. @@ -1356,7 +1354,7 @@ Canonical polyOver_semiringPred := SemiringPred polyOver_mulr_closed. Lemma polyOverZ : {in kS & polyOver kS, forall c p, c *: p \is a polyOver kS}. Proof. -by move=> c p Sc /polyOverP Sp; apply/polyOverP=> i; rewrite coefZ rpredM ?Sp. +by move=> c p Sc /polyOverP Sp; apply/polyOverP=> i; rewrite coefZ rpredM ?Sp. Qed. Lemma polyOverX : 'X \in polyOver kS. @@ -1461,7 +1459,7 @@ by rewrite deriv_mulC IHp !mulrDl -!mulrA !commr_polyX !addrA. Qed. Definition derivE := Eval lazy beta delta [morphism_2 morphism_1] in - (derivZ, deriv_mulC, derivC, derivX, derivMXaddC, derivXsubC, derivM, derivB, + (derivZ, deriv_mulC, derivC, derivX, derivMXaddC, derivXsubC, derivM, derivB, derivD, derivN, derivXn, derivM, derivMn). (* Iterated derivative. *) @@ -1544,7 +1542,7 @@ by apply: leq_trans le_p_n _; apply leq_addr. Qed. Lemma lt_size_deriv (p : {poly R}) : p != 0 -> size p^`() < size p. -Proof. by move=> /polySpred->; exact: size_poly. Qed. +Proof. by move=> /polySpred->; apply: size_poly. Qed. (* A normalising version of derivation to get the division by n! in Taylor *) @@ -2035,10 +2033,10 @@ Canonical polynomial_algType := Eval hnf in [algType R of polynomial R for poly_algType]. Lemma hornerM p q x : (p * q).[x] = p.[x] * q.[x]. -Proof. by rewrite hornerM_comm //; exact: mulrC. Qed. +Proof. by rewrite hornerM_comm //; apply: mulrC. Qed. Lemma horner_exp p x n : (p ^+ n).[x] = p.[x] ^+ n. -Proof. by rewrite horner_exp_comm //; exact: mulrC. Qed. +Proof. by rewrite horner_exp_comm //; apply: mulrC. Qed. Lemma horner_prod I r (P : pred I) (F : I -> {poly R}) x : (\prod_(i <- r | P i) F i).[x] = \prod_(i <- r | P i) (F i).[x]. @@ -2053,7 +2051,7 @@ Lemma horner_evalE x p : horner_eval x p = p.[x]. Proof. by []. Qed. Fact horner_eval_is_lrmorphism x : lrmorphism_for *%R (horner_eval x). Proof. -have cxid: commr_rmorph idfun x by exact: mulrC. +have cxid: commr_rmorph idfun x by apply: mulrC. have evalE : horner_eval x =1 horner_morph cxid. by move=> p; congr _.[x]; rewrite map_poly_id. split=> [|c p]; last by rewrite !evalE /= -linearZ. @@ -2067,7 +2065,7 @@ Canonical horner_eval_lrmorphism x := [lrmorphism of horner_eval x]. Fact comp_poly_multiplicative q : multiplicative (comp_poly q). Proof. split=> [p1 p2|]; last by rewrite comp_polyC. -by rewrite /comp_poly rmorphM hornerM_comm //; exact: mulrC. +by rewrite /comp_poly rmorphM hornerM_comm //; apply: mulrC. Qed. Canonical comp_poly_rmorphism q := AddRMorphism (comp_poly_multiplicative q). Canonical comp_poly_lrmorphism q := [lrmorphism of comp_poly q]. @@ -2281,6 +2279,19 @@ rewrite coefZ (nth_default 0 (leq_trans _ le_qp_i)) ?mulr0 //=. by rewrite polySpred ?expf_neq0 // !size_exp -(subnKC q_gt1) ltn_pmul2l. Qed. +Theorem max_poly_roots p rs : + p != 0 -> all (root p) rs -> uniq rs -> size rs < size p. +Proof. +elim: rs p => [p pn0 _ _ | r rs ihrs p pn0] /=; first by rewrite size_poly_gt0. +case/andP => rpr arrs /andP [rnrs urs]; case/factor_theorem: rpr => q epq. +case: (altP (q =P 0)) => [q0 | ?]; first by move: pn0; rewrite epq q0 mul0r eqxx. +have -> : size p = (size q).+1. + by rewrite epq size_Mmonic ?monicXsubC // size_XsubC addnC. +suff /eq_in_all h : {in rs, root q =1 root p} by apply: ihrs => //; rewrite h. +move=> x xrs; rewrite epq rootM root_XsubC orbC; case: (altP (x =P r)) => // exr. +by move: rnrs; rewrite -exr xrs. +Qed. + End PolynomialIdomain. Section MapFieldPoly. @@ -2400,10 +2411,6 @@ elim: rs => //= r rs ->; congr (_ && _); rewrite -has_pred1 -all_predC. by apply: eq_all => t; rewrite /diff_roots mulrC eqxx unitfE subr_eq0. Qed. -Theorem max_poly_roots p rs : - p != 0 -> all (root p) rs -> uniq rs -> size rs < size p. -Proof. by rewrite -uniq_rootsE; exact: max_ring_poly_roots. Qed. - Section UnityRoots. Variable n : nat. diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v index d79b2bf..770b4cc 100644 --- a/mathcomp/algebra/polyXY.v +++ b/mathcomp/algebra/polyXY.v @@ -1,12 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import choice div fintype tuple finfun bigop binomial. -From mathcomp.fingroup -Require Import fingroup perm. -Require Import ssralg zmodp matrix mxalgebra poly polydiv mxpoly. +From mathcomp +Require Import ssrfun ssrbool choice eqtype ssrnat seq div fintype. +From mathcomp +Require Import tuple finfun bigop fingroup perm ssralg zmodp matrix mxalgebra. +From mathcomp +Require Import poly polydiv mxpoly binomial. (******************************************************************************) (* This file provides additional primitives and theory for bivariate *) diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index 5910586..3c27a2b 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -1,10 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import bigop choice fintype. -Require Import ssralg poly. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. +From mathcomp +Require Import bigop ssralg poly. (******************************************************************************) (* This file provides a library for the basic theory of Euclidean and pseudo- *) @@ -132,7 +131,7 @@ Definition redivp_expanded_def p q := if q == 0 then (0%N, 0, p) else redivp_rec q 0 0 p (size p). Fact redivp_key : unit. Proof. by []. Qed. Definition redivp : {poly R} -> {poly R} -> nat * {poly R} * {poly R} := - locked_with redivp_key redivp_expanded_def. + locked_with redivp_key redivp_expanded_def. Canonical redivp_unlockable := [unlockable fun redivp]. Definition rdivp p q := ((redivp p q).1).2. @@ -154,22 +153,22 @@ Proof. by rewrite /rdivp unlock eqxx. Qed. Lemma rdivp_small p q : size p < size q -> rdivp p q = 0. Proof. -rewrite /rdivp unlock; case: eqP => Eq; first by rewrite Eq size_poly0. -by case sp: (size p) => [| s] hs /=; rewrite sp hs. +rewrite /rdivp unlock; have [-> | _ ltpq] := eqP; first by rewrite size_poly0. +by case: (size p) => [|s]; rewrite /= ltpq. Qed. -Lemma leq_rdivp p q : (size (rdivp p q) <= size p). +Lemma leq_rdivp p q : size (rdivp p q) <= size p. Proof. -case: (ltnP (size p) (size q)); first by move/rdivp_small->; rewrite size_poly0. -rewrite /rdivp /rmodp /rscalp unlock; case q0 : (q == 0) => /=. - by rewrite size_poly0. -have : (size (0 : {poly R})) <= size p by rewrite size_poly0. -move: (leqnn (size p)); move: {2 3 4 6}(size p)=> A. -elim: (size p) 0%N (0 : {poly R}) {1 3 4}p (leqnn (size p)) => [| n ihn] k q1 r. - by move/size_poly_leq0P->; rewrite /= size_poly0 lt0n size_poly_eq0 q0. -move=> /= hrn hr hq1 hq; case: ltnP=> //= hqr. -have sr: 0 < size r by apply: leq_trans hqr; rewrite size_poly_gt0 q0. +have [/rdivp_small->|] := ltnP (size p) (size q); first by rewrite size_poly0. +rewrite /rdivp /rmodp /rscalp unlock. +case q0: (q == 0) => /=; first by rewrite size_poly0. +have: size (0 : {poly R}) <= size p by rewrite size_poly0. +move: (leqnn (size p)); move: {2 3 4 6}(size p) => A. +elim: (size p) 0%N (0 : {poly R}) {1 3 4}p (leqnn (size p)) => [|n ihn] k q1 r. + by move/size_poly_leq0P->; rewrite /= size_poly0 lt0n size_poly_eq0 q0. +move=> /= hrn hr hq1 hq; case: ltnP => //= hqr. have sq: 0 < size q by rewrite size_poly_gt0 q0. +have sr: 0 < size r by apply: leq_trans sq hqr. apply: ihn => //. - apply/leq_sizeP => j hnj. rewrite coefB -scalerAl coefZ coefXnM ltn_subRL ltnNge. @@ -487,7 +486,7 @@ Qed. Lemma rdivp_eq p : p * (lead_coef d ^+ (rscalp p d))%:P = (rdivp p d) * d + (rmodp p d). Proof. -rewrite /rdivp /rmodp /rscalp; case: comm_redivpP=> k q1 r1 Hc _; exact: Hc. +by rewrite /rdivp /rmodp /rscalp; case: comm_redivpP=> k q1 r1 Hc _; apply: Hc. Qed. (* section variables impose an inconvenient order on parameters *) @@ -543,7 +542,7 @@ by rewrite polyC_exp; apply: commrX. Qed. Lemma rdvdpp : rdvdp d d. -Proof. apply/eqP; exact: rmodpp. Qed. +Proof. by apply/eqP; apply: rmodpp. Qed. Lemma rdivpK p : rdvdp d p -> (rdivp p d) * d = p * (lead_coef d ^+ rscalp p d)%:P. @@ -617,12 +616,12 @@ Proof. by rewrite -[p * d]addr0 rdivp_addl_mul rdiv0p addr0. Qed. Lemma rmodp_mull p : rmodp (p * d) d = 0. Proof. -apply: rmodp_mull; rewrite (eqP mond); [exact: commr1 | exact: rreg1]. +by apply: rmodp_mull; rewrite (eqP mond); [apply: commr1 | apply: rreg1]. Qed. Lemma rmodpp : rmodp d d = 0. Proof. -apply: rmodpp; rewrite (eqP mond); [exact: commr1 | exact: rreg1]. +by apply: rmodpp; rewrite (eqP mond); [apply: commr1 | apply: rreg1]. Qed. Lemma rmodp_addl_mul_small q r : @@ -644,12 +643,12 @@ Proof. have -> : rmodp q d = q - (rdivp q d) * d. by rewrite {2}(rdivp_eq q) addrAC subrr add0r. rewrite mulrDr rmodp_add -mulNr mulrA. -rewrite -{2}[rmodp _ _]addr0; congr (_ + _); exact: rmodp_mull. +by rewrite -{2}[rmodp _ _]addr0; congr (_ + _); apply: rmodp_mull. Qed. Lemma rdvdpp : rdvdp d d. Proof. -apply: rdvdpp; rewrite (eqP mond); [exact: commr1 | exact: rreg1]. +by apply: rdvdpp; rewrite (eqP mond); [apply: commr1 | apply: rreg1]. Qed. (* section variables impose an inconvenient order on parameters *) @@ -664,7 +663,7 @@ Qed. Lemma rdvdp_mull p : rdvdp d (p * d). Proof. -apply: rdvdp_mull; rewrite (eqP mond) //; [exact: commr1 | exact: rreg1]. +by apply: rdvdp_mull; rewrite (eqP mond) //; [apply: commr1 | apply: rreg1]. Qed. Lemma rdvdpP p : reflect (exists qq, p = qq * d) (rdvdp d p). @@ -699,7 +698,7 @@ Lemma rdvdp_XsubCl p x : rdvdp ('X - x%:P) p = root p x. Proof. have [HcX Hr] := (monic_comreg (monicXsubC x)). apply/rmodp_eq0P/factor_theorem; last first. - case=> p1 ->; apply: rmodp_mull; exact: monicXsubC. + by case=> p1 ->; apply: rmodp_mull; apply: monicXsubC. move=> e0; exists (rdivp p ('X - x%:P)). by rewrite {1}(rdivp_eq (monicXsubC x) p) e0 addr0. Qed. @@ -742,7 +741,7 @@ Qed. Lemma rdivp_eq d p : (lead_coef d ^+ (rscalp p d)) *: p = (rdivp p d) * d + (rmodp p d). Proof. -rewrite /rdivp /rmodp /rscalp; case: redivpP=> k q1 r1 Hc _; exact: Hc. +by rewrite /rdivp /rmodp /rscalp; case: redivpP=> k q1 r1 Hc _; apply: Hc. Qed. Lemma rdvdp_eqP d p : rdvdp_spec p d (rmodp p d) (rdvdp d p). @@ -775,8 +774,8 @@ Lemma uniq_roots_rdvdp p rs : all (root p) rs -> uniq_roots rs -> rdvdp (\prod_(z <- rs) ('X - z%:P)) p. Proof. -move=> rrs; case/(uniq_roots_prod_XsubC rrs)=> q ->; apply: RingMonic.rdvdp_mull. -exact: monic_prod_XsubC. +move=> rrs; case/(uniq_roots_prod_XsubC rrs)=> q ->. +exact/RingMonic.rdvdp_mull/monic_prod_XsubC. Qed. End UnitRingPseudoDivision. @@ -900,7 +899,7 @@ Qed. Lemma edivp_eq d q r : size r < size d -> lead_coef d \in GRing.unit -> edivp (q * d + r) d = (0%N, q, r). Proof. -have hC : GRing.comm d (lead_coef d)%:P by exact: mulrC. +have hC : GRing.comm d (lead_coef d)%:P by apply: mulrC. move=> hsrd hu; rewrite unlock hu; case et: (redivp _ _) => [[s qq] rr]. have cdn0 : lead_coef d != 0. by move: hu; case d0: (lead_coef d == 0) => //; rewrite (eqP d0) unitr0. @@ -973,9 +972,9 @@ rewrite modpE RingComRreg.rmodp_mull ?scaler0 ?if_same //. by apply/rregP; rewrite lead_coef_eq0. Qed. -Lemma mulKp p q : q != 0 -> +Lemma mulKp p q : q != 0 -> q * p %/ q = lead_coef q ^+ scalp (p * q) q *: p. -Proof. move=> ?; rewrite mulrC; exact: mulpK. Qed. +Proof. by move=> nzq; rewrite mulrC; apply: mulpK. Qed. Lemma divpp p : p != 0 -> p %/ p = (lead_coef p ^+ scalp p p)%:P. Proof. @@ -1089,7 +1088,7 @@ Lemma ltn_divpl d q p : d != 0 -> (size (q %/ d) < size p) = (size q < size (p * d)). Proof. move=> dn0; have sd : size d > 0 by rewrite size_poly_gt0 dn0. -have: (lead_coef d) ^+ (scalp q d) != 0 by exact: lc_expn_scalp_neq0. +have: (lead_coef d) ^+ (scalp q d) != 0 by apply: lc_expn_scalp_neq0. move/size_scale; move/(_ q)<-; rewrite divp_eq; case quo0 : (q %/ d == 0). rewrite (eqP quo0) mul0r add0r size_poly0. case p0 : (p == 0); first by rewrite (eqP p0) mul0r size_poly0 ltnn ltn0. @@ -1170,7 +1169,7 @@ Proof. by move=> pq hq; apply: contraL pq=> /eqP ->; rewrite dvd0p. Qed. Lemma dvdp1 d : (d %| 1) = ((size d) == 1%N). Proof. rewrite /dvdp modpE; case ud: (lead_coef d \in GRing.unit); last exact: rdvdp1. -rewrite -size_poly_eq0 size_scale; first by rewrite size_poly_eq0; exact: rdvdp1. +rewrite -size_poly_eq0 size_scale; first by rewrite size_poly_eq0 -rdvdp1. by rewrite invr_eq0 expf_neq0 //; apply: contraTneq ud => ->; rewrite unitr0. Qed. @@ -1284,7 +1283,7 @@ by rewrite mulrDl -!scalerAl -Eq1 -Eq2 !scalerA mulrC addrC scalerDr. Qed. Lemma dvdp_addl n d m : d %| n -> (d %| m + n) = (d %| m). -Proof. by rewrite addrC; exact: dvdp_addr. Qed. +Proof. by rewrite addrC; apply: dvdp_addr. Qed. Lemma dvdp_add d m n : d %| m -> d %| n -> d %| m + n. Proof. by move/dvdp_addr->. Qed. @@ -1334,10 +1333,10 @@ by apply: (@eq_dvdp _ (q2 * q1) _ _ sn0); rewrite -scalerA Hq2 scalerAr Hq1 mulr Qed. Lemma dvdp_mulIl p q : p %| p * q. -Proof. by apply: dvdp_mulr; exact: dvdpp. Qed. +Proof. by apply: dvdp_mulr; apply: dvdpp. Qed. Lemma dvdp_mulIr p q : q %| p * q. -Proof. by apply: dvdp_mull; exact: dvdpp. Qed. +Proof. by apply: dvdp_mull; apply: dvdpp. Qed. Lemma dvdp_mul2r r p q : r != 0 -> (p * r %| q * r) = (p %| q). Proof. @@ -1401,10 +1400,10 @@ by rewrite exprS mulf_neq0. Qed. Lemma dvdp_XsubCl p x : ('X - x%:P) %| p = root p x. -Proof. rewrite dvdpE; exact: Ring.rdvdp_XsubCl. Qed. +Proof. by rewrite dvdpE; apply: Ring.rdvdp_XsubCl. Qed. Lemma polyXsubCP p x : reflect (p.[x] = 0) (('X - x%:P) %| p). -Proof. rewrite dvdpE; exact: Ring.polyXsubCP. Qed. +Proof. by rewrite dvdpE; apply: Ring.polyXsubCP. Qed. Lemma eqp_div_XsubC p c : (p == (p %/ ('X - c%:P)) * ('X - c%:P)) = ('X - c%:P %| p). @@ -1549,15 +1548,13 @@ by rewrite /eqp; case/andP=> dd' d'd dp; apply: (dvdp_trans d'd). Qed. Lemma dvdp_scaler c m n : c != 0 -> m %| c *: n = (m %| n). -Proof. move=> cn0; apply: eqp_dvdr; exact: eqp_scale. Qed. +Proof. by move=> cn0; apply: eqp_dvdr; apply: eqp_scale. Qed. Lemma dvdp_scalel c m n : c != 0 -> (c *: m %| n) = (m %| n). -Proof. move=> cn0; apply: eqp_dvdl; exact: eqp_scale. Qed. +Proof. by move=> cn0; apply: eqp_dvdl; apply: eqp_scale. Qed. Lemma dvdp_opp d p : d %| (- p) = (d %| p). -Proof. -by apply: eqp_dvdr; rewrite -scaleN1r eqp_scale // oppr_eq0 oner_eq0. -Qed. +Proof. by apply: eqp_dvdr; rewrite -scaleN1r eqp_scale ?oppr_eq0 ?oner_eq0. Qed. Lemma eqp_mul2r r p q : r != 0 -> (p * r %= q * r) = (p %= q). Proof. by move => nz_r; rewrite /eqp !dvdp_mul2r. Qed. @@ -1602,7 +1599,7 @@ case (p =P 0)=> [->|]; [|move/eqP => Hp]. move: pq; rewrite dvdp_eq; set c := _ ^+ _; set x := _ %/ _; move/eqP=> eqpq. move:(eqpq); move/(congr1 (size \o (@polyseq R)))=> /=. have cn0 : c != 0 by rewrite expf_neq0 // lead_coef_eq0. -rewrite (@eqp_size _ q); last by exact: eqp_scale. +rewrite (@eqp_size _ q); last by apply: eqp_scale. rewrite size_mul ?p0 // => [-> HH|]; last first. apply/eqP=> HH; move: eqpq; rewrite HH mul0r. by move/eqP; rewrite scale_poly_eq0 (negPf Hq) (negPf cn0). @@ -1814,7 +1811,7 @@ rewrite gcdpE modp_mull gcd0p size_mul //; case: ifP; first by rewrite eqpxx. rewrite (polySpred mn0) addSn /= -{1}[size n]add0n ltn_add2r; move/negbT. rewrite -ltnNge prednK ?size_poly_gt0 // leq_eqVlt ltnS leqn0 size_poly_eq0. rewrite (negPf mn0) orbF; case/size_poly1P=> c cn0 -> {mn0 m}; rewrite mul_polyC. -suff -> : n %% (c *: n) = 0 by rewrite gcd0p; exact: eqp_scale. +suff -> : n %% (c *: n) = 0 by rewrite gcd0p; apply: eqp_scale. by apply/modp_eq0P; rewrite dvdp_scalel. Qed. @@ -1832,7 +1829,7 @@ Qed. Lemma gcdp_scaler c m n : c != 0 -> gcdp m (c *: n) %= gcdp m n. Proof. move=> cn0; apply: eqp_trans (gcdpC _ _) _. -apply: eqp_trans (gcdp_scalel _ _ _) _ => //; exact: gcdpC. +by apply: eqp_trans (gcdp_scalel _ _ _) _ => //; apply: gcdpC. Qed. Lemma dvdp_gcd_idl m n : m %| n -> gcdp m n %= m. @@ -1845,15 +1842,15 @@ by rewrite expf_neq0 // lead_coef_eq0. Qed. Lemma dvdp_gcd_idr m n : n %| m -> gcdp m n %= n. -Proof. move/dvdp_gcd_idl => h; apply: eqp_trans h; exact: gcdpC. Qed. +Proof. by move/dvdp_gcd_idl => h; apply: eqp_trans h; apply: gcdpC. Qed. Lemma gcdp_exp p k l : gcdp (p ^+ k) (p ^+ l) %= p ^+ minn k l. Proof. wlog leqmn: k l / k <= l. move=> hwlog; case: (leqP k l); first exact: hwlog. - move/ltnW; rewrite minnC; move/hwlog=> h; apply: eqp_trans h; exact: gcdpC. + by move/ltnW; rewrite minnC; move/hwlog=> h; apply: eqp_trans h; apply: gcdpC. rewrite (minn_idPl leqmn); move/subnK: leqmn<-; rewrite exprD. -apply: eqp_trans (gcdp_mull _ _) _; exact: eqpxx. +by apply: eqp_trans (gcdp_mull _ _) _; apply: eqpxx. Qed. Lemma gcdp_eq0 p q : gcdp p q == 0 = (p == 0) && (q == 0). @@ -1918,7 +1915,7 @@ Lemma gcdp_def d m n : gcdp m n %= d. Proof. move=> dm dn h; rewrite /eqp dvdp_gcd dm dn !andbT. -apply: h; [exact: dvdp_gcdl | exact: dvdp_gcdr]. +by apply: h; [apply: dvdp_gcdl | apply: dvdp_gcdr]. Qed. Definition coprimep p q := size (gcdp p q) == 1%N. @@ -2019,7 +2016,7 @@ by rewrite -!gcdp_eqp1; move/(eqp_gcdr p) => h1; apply: (eqp_ltrans h1). Qed. Lemma eqp_coprimepl p q r : q %= r -> coprimep q p = coprimep r p. -Proof. rewrite !(coprimep_sym _ p); exact: eqp_coprimepr. Qed. +Proof. by rewrite !(coprimep_sym _ p); apply: eqp_coprimepr. Qed. (* This should be implemented with an extended remainder sequence *) Fixpoint egcdp_rec p q k {struct k} : {poly R} * {poly R} := @@ -2072,7 +2069,7 @@ rewrite gcdpE ltnNge qsp //= (eqp_ltrans (gcdpC _ _)); split; last first. have : size v + size (p %/ q) > 0 by rewrite addn_gt0 size_poly_gt0 vn0. have : size q + size (p %/ q) > 0 by rewrite addn_gt0 size_poly_gt0 qn0. do 2! move/prednK=> {1}<-; rewrite ltnS => h; apply: leq_trans h _. - rewrite size_divp // addnBA; last by apply: leq_trans qsp; exact: leq_pred. + rewrite size_divp // addnBA; last by apply: leq_trans qsp; apply: leq_pred. rewrite addnC -addnBA ?leq_pred //; move: qn0; rewrite -size_poly_eq0 -lt0n. by move/prednK=> {1}<-; rewrite subSnn addn1. - by rewrite size_scale // lc_expn_scalp_neq0. @@ -2110,7 +2107,7 @@ Lemma Bezout_coprimepP : forall p q, reflect (exists u, u.1 * p + u.2 * q %= 1) (coprimep p q). Proof. move=> p q; rewrite -gcdp_eqp1; apply:(iffP idP)=> [g1|]. - case: (Bezoutp p q) => [[u v] Puv]; exists (u, v); exact: eqp_trans g1. + by case: (Bezoutp p q) => [[u v] Puv]; exists (u, v); apply: eqp_trans g1. case=>[[u v]]; rewrite eqp_sym=> Puv; rewrite /eqp (eqp_dvdr _ Puv). by rewrite dvdp_addr dvdp_mull ?dvdp_gcdl ?dvdp_gcdr //= dvd1p. Qed. @@ -2134,7 +2131,7 @@ by rewrite mulrA dvdp_mull ?dvdpp. Qed. Lemma Gauss_dvdpr p q d: coprimep d q -> (d %| q * p) = (d %| p). -Proof. rewrite mulrC; exact: Gauss_dvdpl. Qed. +Proof. by rewrite mulrC; apply: Gauss_dvdpl. Qed. (* This could be simplified with the introduction of lcmp *) Lemma Gauss_dvdp m n p : coprimep m n -> (m * n %| p) = (m %| p) && (n %| p). @@ -2171,12 +2168,12 @@ Proof. by move=> co_pn; rewrite mulrC Gauss_gcdpr. Qed. Lemma coprimep_mulr p q r : coprimep p (q * r) = (coprimep p q && coprimep p r). Proof. -apply/coprimepP/andP=> [hp|[/coprimepP hq hr]]. - split; apply/coprimepP=> d dp dq; rewrite hp //; - [exact: dvdp_mulr|exact: dvdp_mull]. +apply/coprimepP/andP=> [hp | [/coprimepP-hq hr]]. + by split; apply/coprimepP=> d dp dq; rewrite hp //; + [apply/dvdp_mulr | apply/dvdp_mull]. move=> d dp dqr; move/(_ _ dp) in hq. rewrite Gauss_dvdpl in dqr; first exact: hq. -by move/coprimep_dvdr:hr; apply. +by move/coprimep_dvdr: hr; apply. Qed. Lemma coprimep_mull p q r: coprimep (q * r) p = (coprimep q p && coprimep r p). @@ -2203,7 +2200,7 @@ Lemma coprimep_expl k m n : coprimep m n -> coprimep (m ^+ k) n. Proof. by case: k => [|k] co_pm; rewrite ?coprime1p // coprimep_pexpl. Qed. Lemma coprimep_expr k m n : coprimep m n -> coprimep m (n ^+ k). -Proof. by rewrite !(coprimep_sym m); exact: coprimep_expl. Qed. +Proof. by rewrite !(coprimep_sym m); apply: coprimep_expl. Qed. Lemma gcdp_mul2l p q r : gcdp (p * q) (p * r) %= (p * gcdp q r). Proof. @@ -2383,7 +2380,7 @@ have sp' : size (p %/ (gcdp p q)) <= k. by rewrite [_ == _]cop ltnS leqn0 size_poly_eq0 (negPf gn0). case (ihk _ sp')=> r' dr'p'; first rewrite p'n0 orbF=> cr'q maxr'. constructor=> //=; rewrite ?(negPf p0) ?orbF //. - apply: (dvdp_trans dr'p'); apply: divp_dvd; exact: dvdp_gcdl. + exact/(dvdp_trans dr'p')/divp_dvd/dvdp_gcdl. move=> d dp cdq; apply: maxr'; last by rewrite cdq. case dpq: (d %| gcdp p q). move: (dpq); rewrite dvdp_gcd dp /= => dq; apply: dvdUp; move: cdq. @@ -2589,7 +2586,7 @@ Lemma mulpK p : p * q %/ q = p. Proof. by rewrite mulpK ?monic_neq0 // (eqP monq) expr1n scale1r. Qed. Lemma mulKp p : q * p %/ q = p. -Proof. by rewrite mulrC; exact: mulpK. Qed. +Proof. by rewrite mulrC; apply: mulpK. Qed. End MonicDivisor. @@ -2741,7 +2738,7 @@ by rewrite -lead_coef_eq0; apply: contraTneq ulcd => ->; rewrite unitr0. Qed. Lemma mulKp q : (d * q) %/ d = q. -Proof. rewrite mulrC; exact: mulpK. Qed. +Proof. by rewrite mulrC; apply: mulpK. Qed. Lemma divp_addl_mul_small q r : size r < size d -> (q * d + r) %/ d = q. @@ -2797,7 +2794,7 @@ by move/divpK: hdm<-; rewrite mulrA dvdp_mull // dvdpp. Qed. Lemma divp_mulAC m n : d %| m -> m %/ d * n = m * n %/ d. -Proof. by move=> hdm; rewrite mulrC (mulrC m); exact: divp_mulA. Qed. +Proof. by move=> hdm; rewrite mulrC (mulrC m); apply: divp_mulA. Qed. Lemma divp_mulCA p q : d %| p -> d %| q -> p * (q %/ d) = q * (p %/ d). Proof. by move=> hdp hdq; rewrite mulrC divp_mulAC // divp_mulA. Qed. @@ -2806,7 +2803,7 @@ Lemma modp_mul p q : (p * (q %% d)) %% d = (p * q) %% d. Proof. have -> : q %% d = q - q %/ d * d by rewrite {2}(divp_eq q) -addrA addrC subrK. rewrite mulrDr modp_add // -mulNr mulrA -{2}[_ %% _]addr0; congr (_ + _). -by apply/eqP; apply: dvdp_mull; exact: dvdpp. +by apply/eqP; apply: dvdp_mull; apply: dvdpp. Qed. End UnitDivisor. @@ -2853,7 +2850,7 @@ Lemma divp_divl r p q : Proof. move=> ulcr ulcp. have e : q = (q %/ p %/ r) * (p * r) + ((q %/ p) %% r * p + q %% p). - rewrite addrA (mulrC p) mulrA -mulrDl; rewrite -divp_eq //; exact: divp_eq. + by rewrite addrA (mulrC p) mulrA -mulrDl; rewrite -divp_eq //; apply: divp_eq. have pn0 : p != 0. by rewrite -lead_coef_eq0; apply: contraTneq ulcp => ->; rewrite unitr0. have rn0 : r != 0. @@ -2966,7 +2963,7 @@ Lemma mulpK p q : q != 0 -> p * q %/ q = p. Proof. by move=> qn0; rewrite IdomainUnit.mulpK // unitfE lead_coef_eq0. Qed. Lemma mulKp p q : q != 0 -> q * p %/ q = p. -Proof. by rewrite mulrC; exact: mulpK. Qed. +Proof. by rewrite mulrC; apply: mulpK. Qed. Lemma divp_scalel c p q : (c *: p) %/ q = c *: (p %/ q). Proof. @@ -3015,7 +3012,7 @@ Qed. Lemma eqp_mod p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> p1 %% q1 %= p2 %% q2. Proof. move=> e1 e2; apply: eqp_trans (eqp_modpr _ e2). -apply: eqp_trans (eqp_modpl _ e1); exact: eqpxx. +by apply: eqp_trans (eqp_modpl _ e1); apply: eqpxx. Qed. Lemma eqp_divr (d m n : {poly F}) : m %= n -> (d %/ m) %= (d %/ n). @@ -3028,7 +3025,7 @@ Qed. Lemma eqp_div p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> p1 %/ q1 %= p2 %/ q2. Proof. move=> e1 e2; apply: eqp_trans (eqp_divr _ e2). -apply: eqp_trans (eqp_divl _ e1); exact: eqpxx. +by apply: eqp_trans (eqp_divl _ e1); apply: eqpxx. Qed. Lemma eqp_gdcor p q r : q %= r -> gdcop p q %= gdcop p r. @@ -3036,7 +3033,7 @@ Proof. move=> eqr; rewrite /gdcop (eqp_size eqr). move: (size r)=> n; elim: n p q r eqr => [|n ihn] p q r; first by rewrite eqpxx. move=> eqr /=; rewrite (eqp_coprimepl p eqr); case: ifP => _ //; apply: ihn. -apply: eqp_div => //; exact: eqp_gcdl. +by apply: eqp_div => //; apply: eqp_gcdl. Qed. Lemma eqp_gdcol p q r : q %= r -> gdcop q p %= gdcop r p. @@ -3048,7 +3045,7 @@ elim: n p q r eqr {1 3}p (eqpxx p) => [|n ihn] p q r eqr s esp /=. suff rn0 : r != 0 by rewrite (negPf nq0) (negPf rn0) eqpxx. by apply: contraTneq eqr => ->; rewrite eqp0. rewrite (eqp_coprimepr _ eqr) (eqp_coprimepl _ esp); case: ifP=> _ //. -apply: ihn => //; apply: eqp_div => //; exact: eqp_gcd. +by apply: ihn => //; apply: eqp_div => //; apply: eqp_gcd. Qed. Lemma eqp_rgdco_gdco q p : rgdcop q p %= gdcop q p. @@ -3140,7 +3137,7 @@ by apply: IdomainUnit.divp_mulA; rewrite unitfE lead_coef_eq0. Qed. Lemma divp_mulAC d m n : d %| m -> m %/ d * n = m * n %/ d. -Proof. by move=> hdm; rewrite mulrC (mulrC m); exact: divp_mulA. Qed. +Proof. by move=> hdm; rewrite mulrC (mulrC m); apply: divp_mulA. Qed. Lemma divp_mulCA d p q : d %| p -> d %| q -> p * (q %/ d) = q * (p %/ d). Proof. by move=> hdp hdq; rewrite mulrC divp_mulAC // divp_mulA. Qed. @@ -3209,14 +3206,14 @@ Qed. Lemma edivp_eq d q r : size r < size d -> edivp (q * d + r) d = (0%N, q, r). Proof. move=> srd; apply: Idomain.edivp_eq ; rewrite // unitfE lead_coef_eq0. -rewrite -size_poly_gt0; exact: leq_trans srd. +by rewrite -size_poly_gt0; apply: leq_trans srd. Qed. Lemma modp_mul p q m : (p * (q %% m)) %% m = (p * q) %% m. Proof. have ->: q %% m = q - q %/ m * m by rewrite {2}(divp_eq q m) -addrA addrC subrK. rewrite mulrDr modp_add // -mulNr mulrA -{2}[_ %% _]addr0; congr (_ + _). -by apply/eqP; apply: dvdp_mull; exact: dvdpp. +by apply/eqP; apply: dvdp_mull; apply: dvdpp. Qed. Lemma dvdpP p q : reflect (exists qq, p = qq * q) (q %| p). @@ -3362,10 +3359,10 @@ Proof. by rewrite /eqp !dvdp_map. Qed. Lemma gcdp_map p q : (gcdp p q)^f = gcdp p^f q^f. Proof. wlog lt_p_q: p q / size p < size q. - move=> IH; case: (ltnP (size p) (size q)) => [|le_q_p]; first exact: IH. + move=> IHpq; case: (ltnP (size p) (size q)) => [|le_q_p]; first exact: IHpq. rewrite gcdpE (gcdpE p^f) !size_map_poly ltnNge le_q_p /= -map_modp. case: (eqVneq q 0) => [-> | q_nz]; first by rewrite rmorph0 !gcdp0. - by rewrite IH ?ltn_modp. + by rewrite IHpq ?ltn_modp. elim: {q}_.+1 p {-2}q (ltnSn (size q)) lt_p_q => // m IHm p q le_q_m lt_p_q. rewrite gcdpE (gcdpE p^f) !size_map_poly lt_p_q -map_modp. case: (eqVneq p 0) => [-> | q_nz]; first by rewrite rmorph0 !gcdp0. diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 398d8de..d82fab0 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -1,10 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import div choice fintype bigop. -Require Import ssralg ssrnum ssrint. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. +From mathcomp +Require Import bigop ssralg div ssrnum ssrint. (******************************************************************************) (* This file defines a datatype for rational numbers and equips it with a *) @@ -727,7 +726,7 @@ Variable F : numFieldType. Fact ratr_is_rmorphism : rmorphism (@ratr F). Proof. -have injZtoQ: @injective rat int intr by exact: intr_inj. +have injZtoQ: @injective rat int intr by apply: intr_inj. have nz_den x: (denq x)%:~R != 0 :> F by rewrite intr_eq0 denq_eq0. do 2?split; rewrite /ratr ?divr1 // => x y; last first. rewrite mulrC mulrAC; apply: canLR (mulKf (nz_den _)) _; rewrite !mulrA. diff --git a/mathcomp/algebra/ring_quotient.v b/mathcomp/algebra/ring_quotient.v index ea41744..c1427f3 100644 --- a/mathcomp/algebra/ring_quotient.v +++ b/mathcomp/algebra/ring_quotient.v @@ -1,10 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq. -From mathcomp.discrete -Require Import choice generic_quotient. -Require Import ssralg. +From mathcomp +Require Import eqtype choice ssreflect ssrbool ssrnat ssrfun seq. +From mathcomp +Require Import ssralg generic_quotient. + (******************************************************************************) (* This file describes quotients of algebraic structures. *) @@ -47,15 +46,15 @@ Require Import ssralg. (* right, prime ideal of the ring R. *) (* *) (* The formalization of ideals features the following constructions: *) -(* nontrivial_ideal S == the collective predicate (S : pred R) on the *) +(* proper_ideal S == the collective predicate (S : pred R) on the *) (* ring R is stable by the ring product and does *) (* contain R's one. *) (* prime_idealr_closed S := u * v \in S -> (u \in S) || (v \in S) *) (* idealr_closed S == the collective predicate (S : pred R) on the *) (* ring R represents a (right) ideal. This *) -(* implies its being a nontrivial_ideal. *) +(* implies its being a proper_ideal. *) (* *) -(* MkIdeal idealS == packs idealS : nontrivial_ideal S into an *) +(* MkIdeal idealS == packs idealS : proper_ideal S into an *) (* idealr S interface structure associating the *) (* idealr_closed property to the canonical *) (* pred_key S (see ssrbool), which must already *) @@ -428,7 +427,7 @@ Notation UnitRingQuotMixin Q mU mV := Section IdealDef. -Definition nontrivial_ideal (R : ringType) (S : predPredType R) : Prop := +Definition proper_ideal (R : ringType) (S : predPredType R) : Prop := 1 \notin S /\ forall a, {in S, forall u, a * u \in S}. Definition prime_idealr_closed (R : ringType) (S : predPredType R) : Prop := @@ -437,18 +436,18 @@ Definition prime_idealr_closed (R : ringType) (S : predPredType R) : Prop := Definition idealr_closed (R : ringType) (S : predPredType R) := [/\ 0 \in S, 1 \notin S & forall a, {in S &, forall u v, a * u + v \in S}]. -Lemma idealr_closed_nontrivial R S : @idealr_closed R S -> nontrivial_ideal S. +Lemma idealr_closed_nontrivial R S : @idealr_closed R S -> proper_ideal S. Proof. by case=> S0 S1 hS; split => // a x xS; rewrite -[_ * _]addr0 hS. Qed. Lemma idealr_closedB R S : @idealr_closed R S -> zmod_closed S. Proof. by case=> S0 _ hS; split=> // x y xS yS; rewrite -mulN1r addrC hS. Qed. Coercion idealr_closedB : idealr_closed >-> zmod_closed. -Coercion idealr_closed_nontrivial : idealr_closed >-> nontrivial_ideal. +Coercion idealr_closed_nontrivial : idealr_closed >-> proper_ideal. Structure idealr (R : ringType) (S : predPredType R) := MkIdeal { idealr_zmod :> zmodPred S; - _ : nontrivial_ideal S + _ : proper_ideal S }. Structure prime_idealr (R : ringType) (S : predPredType R) := MkPrimeIdeal { @@ -457,7 +456,7 @@ Structure prime_idealr (R : ringType) (S : predPredType R) := MkPrimeIdeal { }. Definition Idealr (R : ringType) (I : predPredType R) (zmodI : zmodPred I) - (kI : keyed_pred zmodI) : nontrivial_ideal I -> idealr I. + (kI : keyed_pred zmodI) : proper_ideal I -> idealr I. Proof. by move=> kI1; split => //. Qed. Section IdealTheory. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 820a4b9..cadf4c2 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -1,9 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import div choice fintype finfun bigop prime binomial. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat div seq choice fintype. +From mathcomp +Require Import finfun bigop prime binomial. (******************************************************************************) (* The algebraic part of the Algebraic Hierarchy, as described in *) @@ -703,12 +703,18 @@ Proof. by move=> x y; rewrite -addrA addrN addr0. Qed. Lemma addrNK : @rev_right_loop V V -%R +%R. Proof. by move=> x y; rewrite -addrA addNr addr0. Qed. Definition subrK := addrNK. +Lemma subKr x : involutive (fun y => x - y). +Proof. by move=> y; apply: (canLR (addrK _)); rewrite addrC subrK. Qed. Lemma addrI : @right_injective V V V +%R. -Proof. move=> x; exact: can_inj (addKr x). Qed. +Proof. by move=> x; apply: can_inj (addKr x). Qed. Lemma addIr : @left_injective V V V +%R. -Proof. move=> y; exact: can_inj (addrK y). Qed. +Proof. by move=> y; apply: can_inj (addrK y). Qed. +Lemma subrI : right_injective (fun x y => x - y). +Proof. by move=> x; apply: can_inj (subKr x). Qed. +Lemma subIr : left_injective (fun x y => x - y). +Proof. by move=> y; apply: addIr. Qed. Lemma opprK : @involutive V -%R. -Proof. by move=> x; apply: (@addIr (- x)); rewrite addNr addrN. Qed. +Proof. by move=> x; apply: (@subIr x); rewrite addNr addrN. Qed. Lemma oppr_inj : @injective V V -%R. Proof. exact: inv_inj opprK. Qed. Lemma oppr0 : -0 = 0 :> V. @@ -719,13 +725,14 @@ Proof. by rewrite (inv_eq opprK) oppr0. Qed. Lemma subr0 x : x - 0 = x. Proof. by rewrite oppr0 addr0. Qed. Lemma sub0r x : 0 - x = - x. Proof. by rewrite add0r. Qed. +Lemma opprB x y : - (x - y) = y - x. +Proof. by apply: (canRL (addrK x)); rewrite addrC subKr. Qed. + Lemma opprD : {morph -%R: x y / x + y : V}. -Proof. -by move=> x y; apply: (@addrI (x + y)); rewrite addrA subrr addrAC addrK subrr. -Qed. +Proof. by move=> x y; rewrite -[y in LHS]opprK opprB addrC. Qed. -Lemma opprB x y : - (x - y) = y - x. -Proof. by rewrite opprD addrC opprK. Qed. +Lemma subr0_eq x y : x - y = 0 -> x = y. +Proof. by rewrite -(subrr y) => /addIr. Qed. Lemma subr_eq x y z : (x - z == y) = (x == y + z). Proof. exact: can2_eq (subrK z) (addrK z) x y. Qed. @@ -734,7 +741,7 @@ Lemma subr_eq0 x y : (x - y == 0) = (x == y). Proof. by rewrite subr_eq add0r. Qed. Lemma addr_eq0 x y : (x + y == 0) = (x == - y). -Proof. by rewrite -[x == _]subr_eq0 opprK. Qed. +Proof. by rewrite -[y in LHS]opprK subr_eq0. Qed. Lemma eqr_opp x y : (- x == - y) = (x == y). Proof. exact: can_eq opprK x y. Qed. @@ -1054,7 +1061,7 @@ Lemma commrN x y : comm x y -> comm x (- y). Proof. by move=> com_xy; rewrite /comm mulrN com_xy mulNr. Qed. Lemma commrN1 x : comm x (-1). -Proof. apply: commrN; exact: commr1. Qed. +Proof. exact/commrN/commr1. Qed. Lemma commrD x y z : comm x y -> comm x z -> comm x (y + z). Proof. by rewrite /comm mulrDl mulrDr => -> ->. Qed. @@ -1069,7 +1076,7 @@ Lemma commrM x y z : comm x y -> comm x z -> comm x (y * z). Proof. by move=> com_xy; rewrite /comm mulrA com_xy -!mulrA => ->. Qed. Lemma commr_nat x n : comm x n%:R. -Proof. by apply: commrMn; exact: commr1. Qed. +Proof. exact/commrMn/commr1. Qed. Lemma commrX x y n : comm x y -> comm x (y ^+ n). Proof. @@ -1096,7 +1103,7 @@ Qed. Lemma exprM x m n : x ^+ (m * n) = x ^+ m ^+ n. Proof. elim: m => [|m IHm]; first by rewrite expr1n. -by rewrite mulSn exprD IHm exprS exprMn_comm //; exact: commrX. +by rewrite mulSn exprD IHm exprS exprMn_comm //; apply: commrX. Qed. Lemma exprAC x m n : (x ^+ m) ^+ n = (x ^+ n) ^+ m. @@ -1178,7 +1185,7 @@ Proof. by move=> reg_x reg_y z t; rewrite -!mulrA => /reg_x/reg_y. Qed. Lemma lregX x n : lreg x -> lreg (x ^+ n). Proof. -by move=> reg_x; elim: n => [|n]; [exact: lreg1 | rewrite exprS; exact: lregM]. +by move=> reg_x; elim: n => [|n]; [apply: lreg1 | rewrite exprS; apply: lregM]. Qed. Lemma lreg_sign n : lreg ((-1) ^+ n : R). @@ -1320,14 +1327,14 @@ Qed. Lemma Frobenius_autMn x n : (x *+ n)^f = x^f *+ n. Proof. elim: n => [|n IHn]; first exact: Frobenius_aut0. -rewrite !mulrS Frobenius_autD_comm ?IHn //; exact: commrMn. +by rewrite !mulrS Frobenius_autD_comm ?IHn //; apply: commrMn. Qed. Lemma Frobenius_aut_nat n : (n%:R)^f = n%:R. Proof. by rewrite Frobenius_autMn Frobenius_aut1. Qed. Lemma Frobenius_autM_comm x y : comm x y -> (x * y)^f = x^f * y^f. -Proof. by exact: exprMn_comm. Qed. +Proof. exact: exprMn_comm. Qed. Lemma Frobenius_autX x n : (x ^+ n)^f = x^f ^+ n. Proof. by rewrite !fE -!exprM mulnC. Qed. @@ -1445,7 +1452,7 @@ Lemma rreg1 : rreg (1 : R). Proof. exact: (@lreg1 Rc). Qed. Lemma rregM x y : rreg x -> rreg y -> rreg (x * y). -Proof. by move=> reg_x reg_y; exact: (@lregM Rc). Qed. +Proof. by move=> reg_x reg_y; apply: (@lregM Rc). Qed. Lemma revrX x n : (x : Rc) ^+ n = (x : R) ^+ n. Proof. by elim: n => // n IHn; rewrite exprS exprSr IHn. Qed. @@ -2415,7 +2422,7 @@ Lemma lrmorphismP : lrmorphism f. Proof. exact: LRMorphism.class. Qed. Lemma can2_lrmorphism f' : cancel f f' -> cancel f' f -> lrmorphism f'. Proof. -move=> fK f'K; split; [exact: (can2_rmorphism fK) | exact: (can2_linear fK)]. +by move=> fK f'K; split; [apply: (can2_rmorphism fK) | apply: (can2_linear fK)]. Qed. Lemma bij_lrmorphism : @@ -2496,7 +2503,7 @@ Lemma mulrAC : @right_commutative R R *%R. Proof. exact: mulmAC. Qed. Lemma mulrACA : @interchange R *%R *%R. Proof. exact: mulmACA. Qed. Lemma exprMn n : {morph (fun x => x ^+ n) : x y / x * y}. -Proof. move=> x y; apply: exprMn_comm; exact: mulrC. Qed. +Proof. by move=> x y; apply: exprMn_comm; apply: mulrC. Qed. Lemma prodrXl n I r (P : pred I) (F : I -> R) : \prod_(i <- r | P i) F i ^+ n = (\prod_(i <- r | P i) F i) ^+ n. @@ -2508,16 +2515,16 @@ Proof. exact: big_undup_iterop_count. Qed. Lemma exprDn x y n : (x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) * y ^+ i) *+ 'C(n, i). -Proof. by rewrite exprDn_comm //; exact: mulrC. Qed. +Proof. by rewrite exprDn_comm //; apply: mulrC. Qed. Lemma exprBn x y n : (x - y) ^+ n = \sum_(i < n.+1) ((-1) ^+ i * x ^+ (n - i) * y ^+ i) *+ 'C(n, i). -Proof. by rewrite exprBn_comm //; exact: mulrC. Qed. +Proof. by rewrite exprBn_comm //; apply: mulrC. Qed. Lemma subrXX x y n : x ^+ n - y ^+ n = (x - y) * (\sum_(i < n) x ^+ (n.-1 - i) * y ^+ i). -Proof. by rewrite -subrXX_comm //; exact: mulrC. Qed. +Proof. by rewrite -subrXX_comm //; apply: mulrC. Qed. Lemma sqrrD x y : (x + y) ^+ 2 = x ^+ 2 + x * y *+ 2 + y ^+ 2. Proof. by rewrite exprDn !big_ord_recr big_ord0 /= add0r mulr1 mul1r. Qed. @@ -2810,10 +2817,10 @@ Proof. by move=> x Ux y; rewrite -mulrA mulVr ?mulr1. Qed. Definition divrK := mulrVK. Lemma mulrI : {in @unit R, right_injective *%R}. -Proof. by move=> x Ux; exact: can_inj (mulKr Ux). Qed. +Proof. by move=> x Ux; apply: can_inj (mulKr Ux). Qed. Lemma mulIr : {in @unit R, left_injective *%R}. -Proof. by move=> x Ux; exact: can_inj (mulrK Ux). Qed. +Proof. by move=> x Ux; apply: can_inj (mulrK Ux). Qed. (* Due to noncommutativity, fractions are inverted. *) Lemma telescope_prodr n m (f : nat -> R) : @@ -2868,10 +2875,14 @@ Proof. by rewrite dvdn_eq => /eqP def_m unit_d; rewrite -{2}def_m natrM mulrK. Qed. +Lemma divrI : {in unit, right_injective (fun x y => x / y)}. +Proof. by move=> x /mulrI/inj_comp; apply; apply: invr_inj. Qed. + +Lemma divIr : {in unit, left_injective (fun x y => x / y)}. +Proof. by move=> x; rewrite -unitrV => /mulIr. Qed. + Lemma unitr0 : (0 \is a @unit R) = false. -Proof. -by apply/unitrP=> [[x [_]]]; apply/eqP; rewrite mul0r eq_sym oner_neq0. -Qed. +Proof. by apply/unitrP=> [[x [_ /esym/eqP]]]; rewrite mul0r oner_eq0. Qed. Lemma invr0 : 0^-1 = 0 :> R. Proof. by rewrite invr_out ?unitr0. Qed. @@ -3031,7 +3042,7 @@ Fact mulC_mulrV : {in unit, right_inverse 1 inv *%R}. Proof. by move=> x Ux /=; rewrite mulrC mulVx. Qed. Fact mulC_unitP x y : y * x = 1 /\ x * y = 1 -> unit x. -Proof. case=> yx _; exact: unitPl yx. Qed. +Proof. by case=> yx _; apply: unitPl yx. Qed. Definition Mixin := UnitRingMixin mulVx mulC_mulrV mulC_unitP. @@ -3175,13 +3186,16 @@ Variable R : comUnitRingType. Implicit Types x y : R. Lemma unitrM x y : (x * y \in unit) = (x \in unit) && (y \in unit). -Proof. by apply: unitrM_comm; exact: mulrC. Qed. +Proof. by apply: unitrM_comm; apply: mulrC. Qed. Lemma unitrPr x : reflect (exists y, x * y = 1) (x \in unit). Proof. by apply: (iffP (unitrP x)) => [[y []] | [y]]; exists y; rewrite // mulrC. Qed. +Lemma divKr x : x \is a unit -> {in unit, involutive (fun y => x / y)}. +Proof. by move=> Ux y Uy; rewrite /= invrM ?unitrV // invrK mulrC divrK. Qed. + Lemma expr_div_n x y n : (x / y) ^+ n = x ^+ n / y ^+ n. Proof. by rewrite exprMn exprVn. Qed. @@ -3485,7 +3499,7 @@ Proof. by case: rpred0D. Qed. Lemma rpred_sum I r (P : pred I) F : (forall i, P i -> F i \in kS) -> \sum_(i <- r | P i) F i \in kS. -Proof. by move=> IH; elim/big_ind: _; [exact: rpred0 | exact: rpredD |]. Qed. +Proof. by move=> IH; elim/big_ind: _; [apply: rpred0 | apply: rpredD |]. Qed. Lemma rpredMn n : {in kS, forall u, u *+ n \in kS}. Proof. by move=> u Su; rewrite -(card_ord n) -sumr_const rpred_sum. Qed. @@ -3558,7 +3572,7 @@ Proof. by case: rpred1M. Qed. Lemma rpred_prod I r (P : pred I) F : (forall i, P i -> F i \in kS) -> \prod_(i <- r | P i) F i \in kS. -Proof. by move=> IH; elim/big_ind: _; [exact: rpred1 | exact: rpredM |]. Qed. +Proof. by move=> IH; elim/big_ind: _; [apply: rpred1 | apply: rpredM |]. Qed. Lemma rpredX n : {in kS, forall u, u ^+ n \in kS}. Proof. by move=> u Su; rewrite -(card_ord n) -prodr_const rpred_prod. Qed. @@ -3952,7 +3966,7 @@ suffices eq0_ring t1: rformula (eq0_rform t1) by elim: f => //= => f1 ->. rewrite /eq0_rform; move: (ub_var t1) => m; set tr := _ m. suffices: all rterm (tr.1 :: tr.2). case: tr => {t1} t1 r /= /andP[t1_r]. - by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; exact: IHr. + by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; apply: IHr. have: all rterm [::] by []. rewrite {}/tr; elim: t1 [::] => //=. - move=> t1 IHt1 t2 IHt2 r. @@ -3978,11 +3992,11 @@ suffices{e f} equal0_equiv e t1 t2: - elim: f e => /=; try tauto. + move=> t1 t2 e. by split; [move/equal0_equiv/eqP | move/eqP/equal0_equiv]. - + move=> t1 e; rewrite unitrE; exact: equal0_equiv. - + move=> f1 IHf1 f2 IHf2 e; move: (IHf1 e) (IHf2 e); tauto. - + move=> f1 IHf1 f2 IHf2 e; move: (IHf1 e) (IHf2 e); tauto. - + move=> f1 IHf1 f2 IHf2 e; move: (IHf1 e) (IHf2 e); tauto. - + move=> f1 IHf1 e; move: (IHf1 e); tauto. + + by move=> t1 e; rewrite unitrE; apply: equal0_equiv. + + by move=> f1 IHf1 f2 IHf2 e; move: (IHf1 e) (IHf2 e); tauto. + + by move=> f1 IHf1 f2 IHf2 e; move: (IHf1 e) (IHf2 e); tauto. + + by move=> f1 IHf1 f2 IHf2 e; move: (IHf1 e) (IHf2 e); tauto. + + by move=> f1 IHf1 e; move: (IHf1 e); tauto. + by move=> n f1 IHf1 e; split=> [] [x] /IHf1; exists x. + by move=> n f1 IHf1 e; split=> Hx x; apply/IHf1. rewrite -(add0r (eval e t2)) -(can2_eq (subrK _) (addrK _)). @@ -4086,8 +4100,8 @@ Definition qf_eval e := fix loop (f : formula R) : bool := (* qf_eval is equivalent to holds *) Lemma qf_evalP e f : qf_form f -> reflect (holds e f) (qf_eval e f). Proof. -elim: f => //=; try by move=> *; exact: idP. -- move=> t1 t2 _; exact: eqP. +elim: f => //=; try by move=> *; apply: idP. +- by move=> t1 t2 _; apply: eqP. - move=> f1 IHf1 f2 IHf2 /= /andP[/IHf1[] f1T]; last by right; case. by case/IHf2; [left | right; case]. - move=> f1 IHf1 f2 IHf2 /= /andP[/IHf1[] f1F]; first by do 2 left. @@ -4183,7 +4197,7 @@ Lemma qf_to_dnf_rterm f b : rformula f -> all dnf_rterm (qf_to_dnf f b). Proof. set ok := all dnf_rterm. have cat_ok bcs1 bcs2: ok bcs1 -> ok bcs2 -> ok (bcs1 ++ bcs2). - by move=> ok1 ok2; rewrite [ok _]all_cat; exact/andP. + by move=> ok1 ok2; rewrite [ok _]all_cat; apply/andP. have and_ok bcs1 bcs2: ok bcs1 -> ok bcs2 -> ok (and_dnf bcs1 bcs2). rewrite /and_dnf unlock; elim: bcs1 => //= cl1 bcs1 IH1; rewrite -andbA. case/and3P=> ok11 ok12 ok1 ok2; rewrite cat_ok ?{}IH1 {bcs1 ok1}//. @@ -4283,7 +4297,7 @@ Lemma foldForallP I e : <-> holds e (foldr Forall f I). Proof. elim: I e => /= [|i I IHi] e. - by split=> [|f_e e' eq_e]; [exact | apply: eq_holds f_e => i; rewrite eq_e]. + by split=> [|f_e e' eq_e]; [apply | apply: eq_holds f_e => i; rewrite eq_e]. split=> [f_e' x | f_e e' eq_e]; first set e_x := set_nth 0 e i x. apply/IHi=> e' eq_e; apply: f_e' => j. by have:= eq_e j; rewrite nth_set_nth /= !inE; case: eqP. @@ -4387,12 +4401,12 @@ Lemma prodf_seq_eq0 I r (P : pred I) (F : I -> R) : Proof. by rewrite (big_morph _ mulf_eq0 (oner_eq0 _)) big_has_cond. Qed. Lemma mulf_neq0 x y : x != 0 -> y != 0 -> x * y != 0. -Proof. move=> x0 y0; rewrite mulf_eq0; exact/norP. Qed. +Proof. by move=> x0 y0; rewrite mulf_eq0; apply/norP. Qed. Lemma prodf_neq0 (I : finType) (P : pred I) (F : I -> R) : reflect (forall i, P i -> (F i != 0)) (\prod_(i | P i) F i != 0). Proof. -by rewrite (sameP (prodf_eq0 _ _) exists_inP) negb_exists_in; exact: forall_inP. +by rewrite (sameP (prodf_eq0 _ _) exists_inP) negb_exists_in; apply: forall_inP. Qed. Lemma prodf_seq_neq0 I r (P : pred I) (F : I -> R) : @@ -4450,13 +4464,18 @@ Proof. by rewrite -subr_eq0 subr_sqr mulf_eq0 subr_eq0 addr_eq0. Qed. Lemma mulfI x : x != 0 -> injective ( *%R x). Proof. -move=> nz_x y z; rewrite -[x * z]add0r; move/(canLR (addrK _))/eqP. -rewrite -mulrN -mulrDr mulf_eq0 (negbTE nz_x) /=. -by move/eqP/(canRL (subrK _)); rewrite add0r. +move=> nz_x y z; apply: contra_eq => neq_yz. +by rewrite -subr_eq0 -mulrBr mulf_neq0 ?subr_eq0. Qed. Lemma mulIf x : x != 0 -> injective ( *%R^~ x). -Proof. by move=> nz_x y z; rewrite -!(mulrC x); exact: mulfI. Qed. +Proof. by move=> nz_x y z; rewrite -!(mulrC x); apply: mulfI. Qed. + +Lemma divfI x : x != 0 -> injective (fun y => x / y). +Proof. by move/mulfI/inj_comp; apply; apply: invr_inj. Qed. + +Lemma divIf y : y != 0 -> injective (fun x => x / y). +Proof. by rewrite -invr_eq0; apply: mulIf. Qed. Lemma sqrf_eq1 x : (x ^+ 2 == 1) = (x == 1) || (x == -1). Proof. by rewrite -subr_eq0 subr_sqr_1 mulf_eq0 subr_eq0 addr_eq0. Qed. @@ -4589,18 +4608,18 @@ Lemma unitfE x : (x \in unit) = (x != 0). Proof. by apply/idP/idP=> [/(memPn _)-> | /fieldP]; rewrite ?unitr0. Qed. Lemma mulVf x : x != 0 -> x^-1 * x = 1. -Proof. by rewrite -unitfE; exact: mulVr. Qed. +Proof. by rewrite -unitfE; apply: mulVr. Qed. Lemma divff x : x != 0 -> x / x = 1. -Proof. by rewrite -unitfE; exact: divrr. Qed. +Proof. by rewrite -unitfE; apply: divrr. Qed. Definition mulfV := divff. Lemma mulKf x : x != 0 -> cancel ( *%R x) ( *%R x^-1). -Proof. by rewrite -unitfE; exact: mulKr. Qed. +Proof. by rewrite -unitfE; apply: mulKr. Qed. Lemma mulVKf x : x != 0 -> cancel ( *%R x^-1) ( *%R x). -Proof. by rewrite -unitfE; exact: mulVKr. Qed. +Proof. by rewrite -unitfE; apply: mulVKr. Qed. Lemma mulfK x : x != 0 -> cancel ( *%R^~ x) ( *%R^~ x^-1). -Proof. by rewrite -unitfE; exact: mulrK. Qed. +Proof. by rewrite -unitfE; apply: mulrK. Qed. Lemma mulfVK x : x != 0 -> cancel ( *%R^~ x^-1) ( *%R^~ x). -Proof. by rewrite -unitfE; exact: divrK. Qed. +Proof. by rewrite -unitfE; apply: divrK. Qed. Definition divfK := mulfVK. Lemma invfM : {morph @inv F : x y / x * y}. @@ -4613,6 +4632,9 @@ Qed. Lemma invf_div x y : (x / y)^-1 = y / x. Proof. by rewrite invfM invrK mulrC. Qed. +Lemma divKf x : x != 0 -> involutive (fun y => x / y). +Proof. by move=> nz_x y; rewrite invf_div mulrC divfK. Qed. + Lemma expfB_cond m n x : (x == 0) + n <= m -> x ^+ (m - n) = x ^+ m / x ^+ n. Proof. move/subnK=> <-; rewrite addnA addnK !exprD. @@ -4687,7 +4709,7 @@ Variables (R : unitRingType) (f : {rmorphism F -> R}). Lemma fmorph_unit x : (f x \in unit) = (x != 0). Proof. have [-> |] := altP (x =P _); first by rewrite rmorph0 unitr0. -by rewrite -unitfE; exact: rmorph_unit. +by rewrite -unitfE; apply: rmorph_unit. Qed. Lemma fmorphV : {morph f: x / x^-1}. @@ -4712,10 +4734,10 @@ Lemma scalerK a : a != 0 -> cancel ( *:%R a : V -> V) ( *:%R a^-1). Proof. by move=> nz_a v; rewrite scalerA mulVf // scale1r. Qed. Lemma scalerKV a : a != 0 -> cancel ( *:%R a^-1 : V -> V) ( *:%R a). -Proof. by rewrite -invr_eq0 -{3}[a]invrK; exact: scalerK. Qed. +Proof. by rewrite -invr_eq0 -{3}[a]invrK; apply: scalerK. Qed. Lemma scalerI a : a != 0 -> injective ( *:%R a : V -> V). -Proof. move=> nz_a; exact: can_inj (scalerK nz_a). Qed. +Proof. by move=> nz_a; apply: can_inj (scalerK nz_a). Qed. Lemma scaler_eq0 a v : (a *: v == 0) = (a == 0) || (v == 0). Proof. @@ -4740,16 +4762,16 @@ Section Predicates. Context (S : pred_class) (divS : @divrPred F S) (kS : keyed_pred divS). Lemma fpredMl x y : x \in kS -> x != 0 -> (x * y \in kS) = (y \in kS). -Proof. by rewrite -!unitfE; exact: rpredMl. Qed. +Proof. by rewrite -!unitfE; apply: rpredMl. Qed. Lemma fpredMr x y : x \in kS -> x != 0 -> (y * x \in kS) = (y \in kS). -Proof. by rewrite -!unitfE; exact: rpredMr. Qed. +Proof. by rewrite -!unitfE; apply: rpredMr. Qed. Lemma fpred_divl x y : x \in kS -> x != 0 -> (x / y \in kS) = (y \in kS). -Proof. by rewrite -!unitfE; exact: rpred_divl. Qed. +Proof. by rewrite -!unitfE; apply: rpred_divl. Qed. Lemma fpred_divr x y : x \in kS -> x != 0 -> (y / x \in kS) = (y \in kS). -Proof. by rewrite -!unitfE; exact: rpred_divr. Qed. +Proof. by rewrite -!unitfE; apply: rpred_divr. Qed. End Predicates. @@ -4943,7 +4965,7 @@ suffices or_wf fs : let ofs := foldr Or False fs in - apply: or_wf. suffices map_proj_wf bcs: let mbcs := map (proj n) bcs in all dnf_rterm bcs -> all (@qf_form _) mbcs && all (@rformula _) mbcs. - by apply: map_proj_wf; exact: qf_to_dnf_rterm. + by apply: map_proj_wf; apply: qf_to_dnf_rterm. elim: bcs => [|bc bcs ihb] bcsr //= /andP[rbc rbcs]. by rewrite andbAC andbA wf_proj //= andbC ihb. elim: fs => //= g gs ihg; rewrite -andbA => /and4P[-> qgs -> rgs] /=. @@ -4960,7 +4982,7 @@ have auxP f0 e0 n0: qf_form f0 && rformula f0 -> apply: (@iffP (rc e0 n0 (dnf_to_form bcs))); last first. - by case=> x; rewrite -qf_to_dnfP //; exists x. - by case=> x; rewrite qf_to_dnfP //; exists x. - have: all dnf_rterm bcs by case/andP: cf => _; exact: qf_to_dnf_rterm. + have: all dnf_rterm bcs by case/andP: cf => _; apply: qf_to_dnf_rterm. elim: {f0 cf}bcs => [|bc bcs IHbcs] /=; first by right; case. case/andP=> r_bc /IHbcs {IHbcs}bcsP. have f_qf := dnf_to_form_qf [:: bc]. @@ -4972,8 +4994,8 @@ have auxP f0 e0 n0: qf_form f0 && rformula f0 -> case/orP => [bc_x|]; last by exists x. by case: no_x; exists x; apply/(qf_evalP _ f_qf); rewrite /= bc_x. elim: f e => //. -- move=> b e _; exact: idP. -- move=> t1 t2 e _; exact: eqP. +- by move=> b e _; apply: idP. +- by move=> t1 t2 e _; apply: eqP. - move=> f1 IH1 f2 IH2 e /= /andP[/IH1[] f1e]; last by right; case. by case/IH2; [left | right; case]. - move=> f1 IH1 f2 IH2 e /= /andP[/IH1[] f1e]; first by do 2!left. @@ -4982,7 +5004,7 @@ elim: f e => //. by case/IH2; [left | right; move/(_ f1e)]. - by move=> f IHf e /= /IHf[]; [right | left]. - move=> n f IHf e /= rf; have rqf := quantifier_elim_wf rf. - by apply: (iffP (auxP _ _ _ rqf)) => [] [x]; exists x; exact/IHf. + by apply: (iffP (auxP _ _ _ rqf)) => [] [x]; exists x; apply/IHf. move=> n f IHf e /= rf; have rqf := quantifier_elim_wf rf. case: auxP => // [f_x|no_x]; first by right=> no_x; case: f_x => x /IHf[]. by left=> x; apply/IHf=> //; apply/idPn=> f_x; case: no_x; exists x. @@ -5299,10 +5321,15 @@ Definition addNKr := addNKr. Definition addrK := addrK. Definition addrNK := addrNK. Definition subrK := subrK. +Definition subKr := subKr. Definition addrI := @addrI. Definition addIr := @addIr. +Definition subrI := @subrI. +Definition subIr := @subIr. Implicit Arguments addrI [[V] x1 x2]. Implicit Arguments addIr [[V] x1 x2]. +Implicit Arguments subrI [[V] x1 x2]. +Implicit Arguments subIr [[V] x1 x2]. Definition opprK := opprK. Definition oppr_inj := @oppr_inj. Implicit Arguments oppr_inj [[V] x1 x2]. @@ -5313,6 +5340,7 @@ Definition opprB := opprB. Definition subr0 := subr0. Definition sub0r := sub0r. Definition subr_eq := subr_eq. +Definition subr0_eq := subr0_eq. Definition subr_eq0 := subr_eq0. Definition addr_eq0 := addr_eq0. Definition eqr_opp := eqr_opp. @@ -5480,6 +5508,8 @@ Definition mulrVK := mulrVK. Definition divrK := divrK. Definition mulrI := mulrI. Definition mulIr := mulIr. +Definition divrI := divrI. +Definition divIr := divIr. Definition telescope_prodr := telescope_prodr. Definition commrV := commrV. Definition unitrE := unitrE. @@ -5554,6 +5584,7 @@ Definition holds_fsubst := holds_fsubst. Definition unitrM := unitrM. Definition unitrPr {R x} := @unitrPr R x. Definition expr_div_n := expr_div_n. +Definition divKr := divKr. Definition mulf_eq0 := mulf_eq0. Definition prodf_eq0 := prodf_eq0. Definition prodf_seq_eq0 := prodf_seq_eq0. @@ -5570,6 +5601,8 @@ Definition charf0P := charf0P. Definition eqf_sqr := eqf_sqr. Definition mulfI := mulfI. Definition mulIf := mulIf. +Definition divfI := divfI. +Definition divIf := divIf. Definition sqrf_eq1 := sqrf_eq1. Definition expfS_eq1 := expfS_eq1. Definition fieldP := fieldP. @@ -5582,6 +5615,7 @@ Definition mulVKf := mulVKf. Definition mulfK := mulfK. Definition mulfVK := mulfVK. Definition divfK := divfK. +Definition divKf := divKf. Definition invfM := invfM. Definition invf_div := invf_div. Definition expfB_cond := expfB_cond. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index 48c78dd..5a0bafa 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -1,11 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import choice fintype finfun bigop. -Require Import ssralg ssrnum poly. - +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat choice seq. +From mathcomp +Require Import fintype finfun bigop ssralg ssrnum poly. Import GRing.Theory Num.Theory. (******************************************************************************) @@ -594,11 +592,11 @@ Proof. by rewrite -scalezrE scaler_nat. Qed. Lemma mulrz_sumr : forall x I r (P : pred I) F, x *~ (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) x *~ F i. -Proof. by rewrite -/M^z; exact: scaler_suml. Qed. +Proof. by rewrite -/M^z; apply: scaler_suml. Qed. Lemma mulrz_suml : forall n I r (P : pred I) (F : I -> M), (\sum_(i <- r | P i) F i) *~ n= \sum_(i <- r | P i) F i *~ n. -Proof. by rewrite -/M^z; exact: scaler_sumr. Qed. +Proof. by rewrite -/M^z; apply: scaler_sumr. Qed. Canonical intmul_additive x := Additive (@mulrzBr x). @@ -1751,7 +1749,7 @@ Canonical Znat_keyd := KeyedQualifier Znat_key. Lemma Znat_def n : (n \is a Znat) = (0 <= n). Proof. by []. Qed. Lemma Znat_semiring_closed : semiring_closed Znat. -Proof. by do 2?split => //; [exact: addr_ge0 | exact: mulr_ge0]. Qed. +Proof. by do 2?split => //; [apply: addr_ge0 | apply: mulr_ge0]. Qed. Canonical Znat_addrPred := AddrPred Znat_semiring_closed. Canonical Znat_mulrPred := MulrPred Znat_semiring_closed. Canonical Znat_semiringPred := SemiringPred Znat_semiring_closed. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index aecb910..997602c 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1,12 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import div choice fintype bigop finset. -From mathcomp.fingroup -Require Import fingroup. -Require Import ssralg zmodp poly. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq div choice fintype. +From mathcomp +Require Import bigop ssralg finset fingroup zmodp poly. (******************************************************************************) (* *) @@ -873,7 +870,7 @@ Canonical nneg_mulrPred := MulrPred nneg_divr_closed. Canonical nneg_divrPred := DivrPred nneg_divr_closed. Fact nneg_addr_closed : addr_closed (@nneg R). -Proof. by split; [exact: lerr | exact: addr_ge0]. Qed. +Proof. by split; [apply: lerr | apply: addr_ge0]. Qed. Canonical nneg_addrPred := AddrPred nneg_addr_closed. Canonical nneg_semiringPred := SemiringPred nneg_divr_closed. @@ -1019,8 +1016,8 @@ Lemma le0r x : (0 <= x) = (x == 0) || (0 < x). Proof. exact: le0r. Qed. Lemma lt0r_neq0 (x : R) : 0 < x -> x != 0. Proof. by rewrite lt0r; case/andP. Qed. -Lemma ltr0_neq0 (x : R) : 0 < x -> x != 0. -Proof. by rewrite lt0r; case/andP. Qed. +Lemma ltr0_neq0 (x : R) : x < 0 -> x != 0. +Proof. by rewrite ltr_neqAle; case/andP. Qed. Lemma gtr_eqF x y : y < x -> x == y = false. Proof. by rewrite ltr_def; case/andP; move/negPf=> ->. Qed. @@ -1037,7 +1034,7 @@ by rewrite !le0r mulf_eq0; case: eqP => // [-> /negPf[] | _ /pmulr_rgt0->]. Qed. (* Integer comparisons and characteristic 0. *) -Lemma ler01 : 0 <= 1 :> R. Proof. exact: ler01. Qed. +Lemma ler01 : 0 <= 1 :> R. Proof. exact: ler01. Qed. Lemma ltr01 : 0 < 1 :> R. Proof. exact: ltr01. Qed. Lemma ler0n n : 0 <= n%:R :> R. Proof. by rewrite -nnegrE rpred_nat. Qed. Hint Resolve ler01 ltr01 ler0n. @@ -2163,19 +2160,23 @@ elim/big_rec2: _ => // i x2 x1 /leE12/andP[le0Ei leEi12] [x1ge0 le_x12]. by rewrite mulr_ge0 // ler_pmul. Qed. -Lemma ltr_prod (E1 E2 : nat -> R) (n m : nat) : +Lemma ltr_prod I r (P : pred I) (E1 E2 : I -> R) : + has P r -> (forall i, P i -> 0 <= E1 i < E2 i) -> + \prod_(i <- r | P i) E1 i < \prod_(i <- r | P i) E2 i. +Proof. +elim: r => //= i r IHr; rewrite !big_cons; case: ifP => {IHr}// Pi _ ltE12. +have /andP[le0E1i ltE12i] := ltE12 i Pi; set E2r := \prod_(j <- r | P j) E2 j. +apply: ler_lt_trans (_ : E1 i * E2r < E2 i * E2r). + by rewrite ler_wpmul2l ?ler_prod // => j /ltE12/andP[-> /ltrW]. +by rewrite ltr_pmul2r ?prodr_gt0 // => j /ltE12/andP[le0E1j /ler_lt_trans->]. +Qed. + +Lemma ltr_prod_nat (E1 E2 : nat -> R) (n m : nat) : (m < n)%N -> (forall i, (m <= i < n)%N -> 0 <= E1 i < E2 i) -> \prod_(m <= i < n) E1 i < \prod_(m <= i < n) E2 i. Proof. -elim: n m => // n ihn m; rewrite ltnS leq_eqVlt; case/orP => [/eqP -> | ltnm hE]. - by move/(_ n) => /andb_idr; rewrite !big_nat1 leqnn ltnSn /=; case/andP. -rewrite big_nat_recr ?[X in _ < X]big_nat_recr ?(ltnW ltnm) //=. -move/andb_idr: (hE n); rewrite leqnn ltnW //=; case/andP => h1n h12n. -rewrite big_nat_cond [X in _ < X * _]big_nat_cond; apply: ltr_pmul => //=. -- apply: prodr_ge0 => i; rewrite andbT; case/andP=> hm hn. - by move/andb_idr: (hE i); rewrite hm /= ltnS ltnW //=; case/andP. -rewrite -!big_nat_cond; apply: ihn => // i /andP [hm hn]; apply: hE. -by rewrite hm ltnW. +move=> lt_mn ltE12; rewrite !big_nat ltr_prod {ltE12}//. +by apply/hasP; exists m; rewrite ?mem_index_iota leqnn. Qed. (* real of mul *) @@ -2981,7 +2982,7 @@ by move=> xR; rewrite ger0_def eq_sym; apply: lerif_eq; rewrite real_ler_norm. Qed. Lemma lerif_pmul x1 x2 y1 y2 C1 C2 : - 0 <= x1 -> 0 <= x2 -> x1 <= y1 ?= iff C1 -> x2 <= y2 ?= iff C2 -> + 0 <= x1 -> 0 <= x2 -> x1 <= y1 ?= iff C1 -> x2 <= y2 ?= iff C2 -> x1 * x2 <= y1 * y2 ?= iff (y1 * y2 == 0) || C1 && C2. Proof. move=> x1_ge0 x2_ge0 le_xy1 le_xy2; have [y_0 | ] := altP (_ =P 0). @@ -2998,7 +2999,7 @@ by apply: lerif_trans; rewrite (mono_lerif _ (ler_pmul2r _)) // ltr_def x2nz. Qed. Lemma lerif_nmul x1 x2 y1 y2 C1 C2 : - y1 <= 0 -> y2 <= 0 -> x1 <= y1 ?= iff C1 -> x2 <= y2 ?= iff C2 -> + y1 <= 0 -> y2 <= 0 -> x1 <= y1 ?= iff C1 -> x2 <= y2 ?= iff C2 -> y1 * y2 <= x1 * x2 ?= iff (x1 * x2 == 0) || C1 && C2. Proof. rewrite -!oppr_ge0 -mulrNN -[x1 * x2]mulrNN => y1le0 y2le0 le_xy1 le_xy2. @@ -3082,7 +3083,7 @@ rewrite prodrMn exprMn_n -/n' ler_pmuln2r ?expn_gt0; last by case: (n'). have ->: \prod_(k in A') E' k = E' j * pi. by rewrite (bigD1 j) //=; congr *%R; apply: eq_bigr => k /andP[_ /negPf->]. rewrite -(ler_pmul2l mu_gt0) -exprS -Dn mulrA; apply: ltr_le_trans. -rewrite ltr_pmul2r //= eqxx -addrA mulrDr mulrC -ltr_subl_addl -mulrBl. +rewrite ltr_pmul2r //= eqxx -addrA mulrDr mulrC -ltr_subl_addl -mulrBl. by rewrite mulrC ltr_pmul2r ?subr_gt0. Qed. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 01f2f53..aca5f86 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1,10 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import choice fintype bigop finfun tuple. -Require Import ssralg matrix mxalgebra zmodp. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype bigop. +From mathcomp +Require Import finfun tuple ssralg matrix mxalgebra zmodp. (******************************************************************************) (* * Finite dimensional vector spaces *) @@ -648,7 +647,7 @@ Proof. by rewrite memv_cap; apply: andP. Qed. Lemma vspace_modl U V W : (U <= W -> U + (V :&: W) = (U + V) :&: W)%VS. Proof. -by move=> sUV; apply/vs2mxP; rewrite !(vs2mxD, vs2mxI); exact/eqmxP/matrix_modl. +by move=> sUV; apply/vs2mxP; rewrite !(vs2mxD, vs2mxI); apply/eqmxP/matrix_modl. Qed. Lemma vspace_modr U V W : (W <= U -> (U :&: V) + W = U :&: (V + W))%VS. @@ -1919,7 +1918,7 @@ Canonical vsproj_unlockable := [unlockable fun vsproj]. Lemma vsprojK : {in U, cancel vsproj vsval}. Proof. by rewrite unlock; apply: projv_id. Qed. Lemma vsvalK : cancel vsval vsproj. -Proof. by move=> w; exact/val_inj/vsprojK/subvsP. Qed. +Proof. by move=> w; apply/val_inj/vsprojK/subvsP. Qed. Lemma vsproj_is_linear : linear vsproj. Proof. by move=> k w1 w2; apply: val_inj; rewrite unlock /= linearP. Qed. diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v index 9dd3ff5..0a9bf5e 100644 --- a/mathcomp/algebra/zmodp.v +++ b/mathcomp/algebra/zmodp.v @@ -1,12 +1,9 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) Require Import mathcomp.ssreflect.ssreflect. -From mathcomp.ssreflect -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. -From mathcomp.discrete -Require Import div fintype bigop finset prime. -From mathcomp.fingroup -Require Import fingroup. -Require Import ssralg finalg. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq div. +From mathcomp +Require Import fintype bigop finset prime fingroup ssralg finalg. (******************************************************************************) (* Definition of the additive group and ring Zp, represented as 'I_p *) @@ -170,7 +167,7 @@ Lemma Zp_expg x n : x ^+ n = inZp (x * n). Proof. exact: Zp_mulrn. Qed. Lemma Zp1_expgz x : Zp1 ^+ x = x. -Proof. by rewrite Zp_expg; exact: Zp_mul1z. Qed. +Proof. by rewrite Zp_expg; apply: Zp_mul1z. Qed. Lemma Zp_cycle : setT = <[Zp1]>. Proof. by apply/setP=> x; rewrite -[x]Zp1_expgz inE groupX ?mem_gen ?set11. Qed. @@ -185,13 +182,13 @@ Implicit Arguments Zp1 [[p']]. Implicit Arguments inZp [[p']]. Lemma ord1 : all_equal_to (0 : 'I_1). -Proof. by case=> [[] // ?]; exact: val_inj. Qed. +Proof. by case=> [[] // ?]; apply: val_inj. Qed. Lemma lshift0 m n : lshift m (0 : 'I_n.+1) = (0 : 'I_(n + m).+1). Proof. exact: val_inj. Qed. Lemma rshift1 n : @rshift 1 n =1 lift (0 : 'I_n.+1). -Proof. by move=> i; exact: val_inj. Qed. +Proof. by move=> i; apply: val_inj. Qed. Lemma split1 n i : split (i : 'I_(1 + n)) = oapp (@inr _ _) (inl _ 0) (unlift 0 i). @@ -286,7 +283,7 @@ by move=> p_gt1; rewrite qualifE /= val_Zp_nat ?Zp_cast ?coprime_modr. Qed. Lemma Zp_group_set : group_set Zp. -Proof. rewrite /Zp; case: (p > 1); exact: groupP. Qed. +Proof. by rewrite /Zp; case: (p > 1); apply: groupP. Qed. Canonical Zp_group := Group Zp_group_set. Lemma card_Zp : p > 0 -> #|Zp| = p. @@ -307,7 +304,7 @@ by rewrite totient_count_coprime big_mkord. Qed. Lemma units_Zp_abelian : abelian units_Zp. -Proof. apply/centsP=> u _ v _; exact: unit_Zp_mulgC. Qed. +Proof. by apply/centsP=> u _ v _; apply: unit_Zp_mulgC. Qed. End Groups. |