diff options
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 12 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/div.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 27 |
6 files changed, 28 insertions, 25 deletions
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 078fea3..8d6c03b 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -2,7 +2,7 @@ (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice. From mathcomp Require Import fintype finfun bigop finset fingroup perm. -From mathcomp Require Import div prime binomial ssralg finalg zmodp matrix. +From mathcomp Require Import div prime binomial ssralg finalg zmodp matrix. (*****************************************************************************) (* In this file we develop the rank and row space theory of matrices, based *) @@ -683,7 +683,7 @@ Qed. Lemma row_full_unit n (A : 'M_n) : row_full A = (A \in unitmx). Proof. exact: row_free_unit. Qed. - + Lemma mxrank_unit n (A : 'M_n) : A \in unitmx -> \rank A = n. Proof. by rewrite -row_full_unit => /eqnP. Qed. @@ -1488,7 +1488,7 @@ Proof. by rewrite unlock; apply/eqmxP; rewrite !genmxE !capmxE andbb. Qed. Lemma genmx_diff m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (<<A :\: B>> = A :\: B)%MS. Proof. by rewrite [@diffmx]unlock genmx_id. Qed. - + Lemma diffmxSl m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :\: B <= A)%MS. Proof. by rewrite diffmxE capmxSl. Qed. @@ -2202,7 +2202,7 @@ have p_i_gt0: p ^ _ > 0 by move=> i; rewrite expn_gt0 ltnW. rewrite (card_GL _ (ltn0Sn n.-1)) card_ord Fp_cast // big_add1 /=. pose p'gt0 m := m > 0 /\ logn p m = 0%N. suffices [Pgt0 p'P]: p'gt0 (\prod_(0 <= i < n.-1.+1) (p ^ i.+1 - 1))%N. - by rewrite lognM // p'P pfactorK //; case n. + by rewrite lognM // p'P pfactorK // addn0; case n. apply big_ind => [|m1 m2 [m10 p'm1] [m20]|i _]; rewrite {}/p'gt0 ?logn1 //. by rewrite muln_gt0 m10 lognM ?p'm1. rewrite lognE -if_neg subn_gt0 p_pr /= -{1 2}(exp1n i.+1) ltn_exp2r // p_gt1. @@ -2269,7 +2269,7 @@ by rewrite linear_sum; apply: eq_bigr => i _; rewrite mulmxKpV. Qed. Arguments memmx_sumsP {I P n A R_}. -Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) : +Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) : (1%:M \in R)%MS -> reflect (exists2 A, A \in R & ~~ is_scalar_mx A)%MS (1 < \rank R). Proof. @@ -2765,5 +2765,3 @@ 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; apply: map_capmx. Qed. End MapMatrixSpaces. - - diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index 1b1eb77..3c4c002 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -1553,7 +1553,7 @@ Lemma abszN1 : `|-1%R| = 1. Proof. by []. Qed. Lemma absz_id m : `|(`|m|)| = `|m|. Proof. by []. Qed. Lemma abszM m1 m2 : `|(m1 * m2)%R| = `|m1| * `|m2|. -Proof. by case: m1 m2 => [[|m1]|m1] [[|m2]|m2]; rewrite //= mulnS mulnC. Qed. +Proof. by case: m1 m2 => [[|m1]|m1] [[|m2]|m2] //=; rewrite ?mulnS mulnC. Qed. Lemma abszX (n : nat) m : `|m ^+ n| = `|m| ^ n. Proof. by elim: n => // n ihn; rewrite exprS expnS abszM ihn. Qed. diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index c260105..06774ff 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -45,7 +45,7 @@ transitivity (\sum_(1 <= i < n.+1) \sum_(1 <= k < n.+1) (p ^ k %| i)). by apply: andb_idr => /dvdn_leq/(leq_trans (ltn_expl _ (prime_gt1 _)))->. by rewrite exchange_big_nat; apply: eq_bigr => i _; rewrite divn_count_dvd. Qed. - + Theorem Wilson p : p > 1 -> prime p = (p %| ((p.-1)`!).+1). Proof. have dFact n: 0 < n -> (n.-1)`! = \prod_(0 <= i < n | i != 0) i. @@ -310,7 +310,7 @@ Qed. Lemma subn_exp m n k : m ^ k - n ^ k = (m - n) * (\sum_(i < k) m ^ (k.-1 -i) * n ^ i). Proof. -case: k => [|k]; first by rewrite big_ord0. +case: k => [|k]; first by rewrite big_ord0 muln0. rewrite mulnBl !big_distrr big_ord_recl big_ord_recr /= subn0 muln1. rewrite subnn mul1n -!expnS subnDA; congr (_ - _); apply: canRL (addnK _) _. congr (_ + _); apply: eq_bigr => i _. @@ -543,4 +543,3 @@ by apply: val_inj; congr (_ :: _); apply: val_inj; rewrite /= -{1}def_n addnK. Qed. End Combinations. - diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index fda425d..3cb98e8 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -538,7 +538,7 @@ Lemma gcdnDr m n : gcdn m (n + m) = gcdn m n. Proof. by rewrite addnC gcdnDl. Qed. Lemma gcdnMl n m : gcdn n (m * n) = n. -Proof. by case: n => [|n]; rewrite gcdnE modnMl gcd0n. Qed. +Proof. by case: n => [|n]; rewrite gcdnE modnMl // muln0. Qed. Lemma gcdnMr n m : gcdn n (n * m) = n. Proof. by rewrite mulnC gcdnMl. Qed. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 3685c23..76acaca 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -497,7 +497,7 @@ Lemma all_nseqb (b : bool) x : all (nseq b x) = b ==> a x. Proof. by rewrite all_nseq eqb0 implybE. Qed. Lemma find_nseq n x : find (nseq n x) = ~~ a x * n. -Proof. by elim: n => //= n ->; case: (a x). Qed. +Proof. by elim: n => /= [|n ->]; case: (a x). Qed. Lemma nth_find s : has s -> a (nth s (find s)). Proof. by elim: s => //= x s IHs; case Hx: (a x). Qed. @@ -928,7 +928,7 @@ Proof. by rewrite -size_eq0 size_filter has_count lt0n. Qed. Fixpoint mem_seq (s : seq T) := if s is y :: s' then xpredU1 y (mem_seq s') else xpred0. -Definition seq_eqclass := seq T. +Definition seq_eqclass := seq T. Identity Coercion seq_of_eqclass : seq_eqclass >-> seq. Coercion pred_of_seq (s : seq_eqclass) : {pred T} := mem_seq s. @@ -3068,4 +3068,3 @@ Notation perm_uniq := deprecate perm_uniq eq_uniq T s1 s2 eq_sz12 eq_s12) _ _ _) (only parsing). - diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 86f8fb2..ad44d3b 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -106,6 +106,10 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +(* Disable Coq prelude hints to improve proof script robustness. *) + +Remove Hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm : core. + (* Declare legacy Arith operators in new scope. *) Delimit Scope coq_nat_scope with coq_nat. @@ -200,7 +204,7 @@ Lemma add1n n : 1 + n = n.+1. Proof. by []. Qed. Lemma addn0 : right_id 0 addn. Proof. by move=> n; apply/eqP; elim: n. Qed. -Lemma addnS m n : m + n.+1 = (m + n).+1. Proof. by elim: m. Qed. +Lemma addnS m n : m + n.+1 = (m + n).+1. Proof. by apply/eqP; elim: m. Qed. Lemma addSnnS m n : m.+1 + n = m + n.+1. Proof. by rewrite addnS. Qed. @@ -831,7 +835,7 @@ Proof. by move=> eq_op x; apply: eq_iteri; case. Qed. End Iteration. Lemma iter_succn m n : iter n succn m = m + n. -Proof. by elim: n => //= n ->. Qed. +Proof. by rewrite addnC; elim: n => //= n ->. Qed. Lemma iter_succn_0 n : iter n succn 0 = n. Proof. exact: iter_succn. Qed. @@ -1637,24 +1641,27 @@ case=> //=; elim=> //= p; case: (nat_of_pos p) => //= n [<-]. by rewrite natTrecE addnS /= addnS {2}addnn; elim: {1 3}n. Qed. -Lemma nat_of_succ_gt0 p : Pos.succ p = p.+1 :> nat. +Lemma nat_of_succ_pos p : Pos.succ p = p.+1 :> nat. Proof. by elim: p => //= p ->; rewrite !natTrecE. Qed. -Lemma nat_of_addn_gt0 p q : (p + q)%positive = p + q :> nat. +Lemma nat_of_add_pos p q : (p + q)%positive = p + q :> nat. Proof. apply: @fst _ (Pplus_carry p q = (p + q).+1 :> nat) _. elim: p q => [p IHp|p IHp|] [q|q|] //=; rewrite !natTrecE //; - by rewrite ?IHp ?nat_of_succ_gt0 ?(doubleS, doubleD, addn1, addnS). + by rewrite ?IHp ?nat_of_succ_pos ?(doubleS, doubleD, addn1, addnS). +Qed. + +Lemma nat_of_mul_pos p q : (p * q)%positive = p * q :> nat. +Proof. +elim: p => [p IHp|p IHp|] /=; rewrite ?mul1n //; + by rewrite ?nat_of_add_pos /= !natTrecE IHp doubleMl. Qed. Lemma nat_of_add_bin b1 b2 : (b1 + b2)%num = b1 + b2 :> nat. -Proof. by case: b1 b2 => [|p] [|q] //=; apply: nat_of_addn_gt0. Qed. +Proof. by case: b1 b2 => [|p] [|q]; rewrite ?addn0 //= nat_of_add_pos. Qed. Lemma nat_of_mul_bin b1 b2 : (b1 * b2)%num = b1 * b2 :> nat. -Proof. -case: b1 b2 => [|p] [|q] //=; elim: p => [p IHp|p IHp|] /=; - by rewrite ?(mul1n, nat_of_addn_gt0, mulSn) //= !natTrecE IHp doubleMl. -Qed. +Proof. by case: b1 b2 => [|p] [|q]; rewrite ?muln0 //= nat_of_mul_pos. Qed. Lemma nat_of_exp_bin n (b : N) : n ^ b = pow_N 1 muln n b. Proof. |