From d60c67b8f33f55e11ca159246d2a447102f10f20 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 30 Aug 2019 11:30:21 +0200 Subject: Change the order of arguments in `ltngtP` from `ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)` to `ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)`, to make it tries to match subterms with `m < n` first, `m <= n`, then `m == n`. --- CHANGELOG_UNRELEASED.md | 9 +++++++++ mathcomp/algebra/polydiv.v | 2 +- mathcomp/algebra/ssrint.v | 10 +++++----- mathcomp/field/algnum.v | 2 +- mathcomp/solvable/abelian.v | 4 ++-- mathcomp/solvable/burnside_app.v | 2 +- mathcomp/solvable/extremal.v | 2 +- mathcomp/ssreflect/path.v | 6 +++--- mathcomp/ssreflect/prime.v | 2 +- mathcomp/ssreflect/seq.v | 10 ++++------ mathcomp/ssreflect/ssrnat.v | 32 +++++++++++++++++++++++--------- 11 files changed, 51 insertions(+), 30 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 50ad28a..5f6914c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -93,6 +93,15 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). (which statement was modified to remove the dependency in `eqType`), and `order_path_min`. +- `compare_nat` type family and `ltngtP` comparison predicate are changed + from `compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)` + to `compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)`, + to make it tries to match subterms with `m < n` first, `m <= n`, then + `m == n`. + + The compatibility layer for the version 1.9 is provided as the + `ssrnat.mc_1_9` module. One may compile proofs compatible with the version + 1.9 in newer versions by using this module. + ### Infrastructure - `Makefile` now supports the `test-suite` and `only` targets. Currently, diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index b65742d..aa076a2 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -3243,7 +3243,7 @@ move=> hsp /=; have [->|p_neq0] := altP (p =P 0). by rewrite size_poly0 expr0 mulr1 dvd0p=> /(_ isT). have [|ncop_pq] := boolP (coprimep _ _); first by rewrite dvdp_mulr ?dvdpp. have g_gt1: (1 < size (gcdp p q))%N. - have [|//|/eqP] := ltngtP; last by rewrite -coprimep_def (negPf ncop_pq). + have [//||/esym/eqP] := ltngtP; last by rewrite -coprimep_def (negPf ncop_pq). by rewrite ltnS leqn0 size_poly_eq0 gcdp_eq0 (negPf p_neq0). have sd : (size (p %/ gcdp p q) < size p)%N. rewrite size_divp -?size_poly_eq0 -(subnKC g_gt1) // add2n /=. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index 3c4c002..2a17a4a 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -138,9 +138,9 @@ Lemma oppzK : involutive oppz. Proof. by do 2?case. Qed. Lemma oppz_add : {morph oppz : m n / m + n}. Proof. -move=> [[|n]|n] [[|m]|m] /=; rewrite ?NegzE ?oppzK ?addnS ?addn0 ?subn0 //; - rewrite ?ltnS[m <= n]leqNgt [n <= m]leqNgt; case: ltngtP=> hmn /=; - by rewrite ?hmn ?subnn // ?oppzK ?subSS ?subnS ?prednK // ?subn_gt0. +by move=> [[|n]|n] [[|m]|m] /=; rewrite ?addn0 ?subn0 ?addnS //; + rewrite !NegzE !ltnS !subSS; case: ltngtP => [?|?|->]; + rewrite ?subnn // ?oppzK ?subnS ?prednK // subn_gt0. Qed. Lemma add1Pz (n : int) : 1 + (n - 1) = n. @@ -154,9 +154,9 @@ Qed. Lemma addSnz (m : nat) (n : int) : (m.+1%N) + n = 1 + (m + n). Proof. move: m n=> [|m] [] [|n] //=; rewrite ?add1n ?subn1 // !(ltnS, subSS). -rewrite [n <= m]leqNgt; case: ltngtP=> hmn /=; rewrite ?hmn ?subnn //. +case: ltngtP=> hnm /=; rewrite ?hnm ?subnn //. by rewrite subnS add1n prednK ?subn_gt0. -by rewrite ltnS leqn0 subn_eq0 leqNgt hmn /= subnS subn1. +by rewrite ltnS leqn0 subn_eq0 leqNgt hnm /= subnS subn1. Qed. Lemma addSz (m n : int) : (1 + m) + n = 1 + (m + n). diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index 3f25ae6..f494a09 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -823,7 +823,7 @@ rewrite /orderC; case: pickP => /= [k /eqP Dp_k | no_k]; last first. rewrite mem_primes => /and3P[q_pr _ q_dv_m]. rewrite lognE q_pr m_gt0 q_dv_m /=; move: (logn q _) => k. rewrite !mulnA expnS leq_mul //. - case: (ltngtP q) => // [|q_gt2 | ->]; first by rewrite ltnNge prime_gt1. + case: (ltngtP q 2) (prime_gt1 q_pr) => // [q_gt2|->] _. rewrite mul1n mulnAC mulnn -{1}[q]muln1 leq_mul ?expn_gt0 ?prime_gt0 //. by rewrite -(subnKC q_gt2) (ltn_exp2l 1). by rewrite !muln1 -expnS (ltn_exp2l 0). diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 2e025a2..8c2badb 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -1742,8 +1742,8 @@ have cnt_b b: \big[dprod/1]_(x <- b) <[x]> = G -> count [pred x | #[x] == p ^ k.+1]%N b = cnt_p k b - cnt_p k.+1 b. - move/p_bG; elim: b => //= _ b IHb /andP[/p_natP[j ->] /IHb-> {IHb}]. rewrite eqn_leq !leq_exp2l ?prime_gt1 // -eqn_leq pfactorK //. - case: ltngtP => // _ {j}; rewrite subSn // add0n; elim: b => //= y b IHb. - by rewrite leq_add // ltn_neqAle; case: (~~ _). + case: (ltngtP k.+1) => // _ {j}; rewrite subSn // add0n. + by elim: b => //= y b IHb; rewrite leq_add // ltn_neqAle; case: (~~ _). by rewrite !cnt_b // /cnt_p !(@count_logn_dprod_cycle _ _ _ G). Qed. diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index 18c6509..efbe824 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -436,7 +436,7 @@ Qed. Lemma card_n3 : forall x y : square, x != y -> #|[set k : col_squares | k x == k y]| = (n ^ 3)%N. Proof. -move=> x y nxy; apply/eqP; case: (ltngtP n 0) => // [|n0]; last first. +move=> x y nxy; apply/eqP; case: (posnP n) => [n0|]. by rewrite n0; apply/existsP=> [] [p _]; case: (p c0) => i; rewrite n0. move/eqn_pmul2l <-; rewrite -expnS -card_Fid Fid cardsT. rewrite -{1}[n]card_ord -cardX. diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index d236575..be885b1 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -1831,7 +1831,7 @@ case/pred2P: Z_xxy => xy; last first. have n_gt3: n > 3. case: ltngtP notXy => // [|n3]; first by rewrite ltnNge n_gt2. rewrite -scXG inE Gy defX cent_cycle; case/cent1P; red. - by rewrite (conjgC x) xy /r p2 n3. + by rewrite (conjgC x) xy /r p2 -n3. exists n => //; rewrite isogEcard card_semidihedral // oG p2 leqnn andbT. rewrite Grp_semidihedral //; apply/existsP=> /=. case/pred2P: Zy2 => y2; [exists (x, y) | exists (x, x * y)]. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index f757e94..0da7a16 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -1004,7 +1004,7 @@ Proof. by elim: n x => //= n IHn x //=; rewrite IHn. Qed. Lemma nth_traject i n : i < n -> forall x, nth x (traject x n) i = iter i f x. Proof. -elim: n => // n IHn; rewrite ltnS leq_eqVlt => le_i_n x. +elim: n => // n IHn; rewrite ltnS => le_i_n x. rewrite trajectSr nth_rcons size_traject. by case: ltngtP le_i_n => [? _||->] //; apply: IHn. Qed. @@ -1086,8 +1086,8 @@ Proof. move=> x; rewrite prev_nth mem_next next_nth; case p_x: (x \in p) => //. case def_p: p Up p_x => // [y q]; rewrite -{-1}def_p => /= /andP[not_qy Uq] p_x. rewrite -{2}(nth_index y p_x); congr (nth y _ _); set i := index x p. -have: ~~ (size q < i) by rewrite -index_mem -/i def_p leqNgt in p_x. -case: ltngtP => // [lt_i_q | ->] _; first by rewrite index_uniq. +have: i <= size q by rewrite -index_mem -/i def_p in p_x. +case: ltngtP => // [lt_i_q|->] _; first by rewrite index_uniq. by apply/eqP; rewrite nth_default // eqn_leq index_size leqNgt index_mem. Qed. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 9eafea9..1185e67 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -579,7 +579,7 @@ Qed. Lemma coprime_has_primes m n : 0 < m -> 0 < n -> coprime m n = ~~ has (mem (primes m)) (primes n). Proof. -move=> m_gt0 n_gt0; apply/eqnP/hasPn=> [mn1 p | no_p_mn]. +move=> m_gt0 n_gt0; apply/eqP/hasPn=> [mn1 p | no_p_mn]. rewrite /= !mem_primes m_gt0 n_gt0 /= => /andP[pr_p p_n]. have:= prime_gt1 pr_p; rewrite pr_p ltnNge -mn1 /=; apply: contra => p_m. by rewrite dvdn_leq ?gcdn_gt0 ?m_gt0 // dvdn_gcd ?p_m. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index c45f7fc..35d9a69 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -725,16 +725,14 @@ Proof. by move <-; elim: s1 => [|x s1 IHs]; rewrite ?take0 //= IHs. Qed. Lemma takel_cat s1 s2 : n0 <= size s1 -> take n0 (s1 ++ s2) = take n0 s1. Proof. -by rewrite take_cat; case: ltngtP => // <-; rewrite subnn take0 take_size cats0. +by rewrite take_cat; case: ltngtP => // ->; rewrite subnn take0 take_size cats0. Qed. Lemma nth_drop s i : nth (drop n0 s) i = nth s (n0 + i). Proof. -have [lt_n0_s | le_s_n0] := ltnP n0 (size s). - rewrite -{2}[s]cat_take_drop nth_cat size_take lt_n0_s /= addKn. - by rewrite ltnNge leq_addr. -rewrite !nth_default //; first exact: leq_trans (leq_addr _ _). -by rewrite size_drop (eqnP le_s_n0). +rewrite -{2}[s]cat_take_drop nth_cat size_take ltnNge. +case: ltnP => [?|le_s_n0]; rewrite ?(leq_trans le_s_n0) ?leq_addr ?addKn //=. +by rewrite drop_oversize // !nth_default. Qed. Lemma nth_take i : i < n0 -> forall s, nth (take n0 s) i = nth s i. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 39131f0..f358f7b 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -446,7 +446,7 @@ Variant ltn_xor_geq m n : bool -> bool -> Set := | GeqNotLtn of n <= m : ltn_xor_geq m n true false. Lemma ltnP m n : ltn_xor_geq m n (n <= m) (m < n). -Proof. by rewrite -(ltnS n); case: leqP; constructor. Qed. +Proof. by case: leqP; constructor. Qed. Variant eqn0_xor_gt0 n : bool -> bool -> Set := | Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false @@ -457,18 +457,18 @@ Proof. by case: n; constructor. Qed. Variant compare_nat m n : bool -> bool -> bool -> bool -> bool -> bool -> Set := - | CompareNatLt of m < n : compare_nat m n true false true false false false - | CompareNatGt of m > n : compare_nat m n false true false true false false - | CompareNatEq of m = n : compare_nat m n true true false false true true. + | CompareNatLt of m < n : compare_nat m n false false false true false true + | CompareNatGt of m > n : compare_nat m n false false true false true false + | CompareNatEq of m = n : compare_nat m n true true true true false false. -Lemma ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) - (n < m) (n == m) (m == n). +Lemma ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m) + (m <= n) (n < m) (m < n). Proof. -rewrite !ltn_neqAle [_ == m]eq_sym; case: ltnP => [mn|]. +rewrite !ltn_neqAle [_ == n]eq_sym; case: ltnP => [nm|]. by rewrite ltnW // gtn_eqF //; constructor. -rewrite leq_eqVlt; case: ltnP; rewrite ?(orbT, orbF) => //= lt_nm eq_mn. +rewrite leq_eqVlt; case: ltnP; rewrite ?(orbT, orbF) => //= lt_mn eq_nm. by rewrite ltn_eqF //; constructor. -by rewrite eq_mn; constructor; apply/eqP. +by rewrite eq_nm; constructor; apply/esym/eqP. Qed. (* Monotonicity lemmas *) @@ -1795,3 +1795,17 @@ Ltac nat_congr := first apply: (congr1 (addn X1) _); symmetry end ]. + +Module mc_1_9. + +Variant compare_nat m n : + bool -> bool -> bool -> bool -> bool -> bool -> Set := + | CompareNatLt of m < n : compare_nat m n true false true false false false + | CompareNatGt of m > n : compare_nat m n false true false true false false + | CompareNatEq of m = n : compare_nat m n true true false false true true. + +Lemma ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) + (n < m) (n == m) (m == n). +Proof. by case: ltngtP; constructor. Qed. + +End mc_1_9. -- cgit v1.2.3