From 35bd8708dacfb508f896d957d7b1189ca7decb3e Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 13 May 2020 13:11:14 +0900 Subject: Revise proofs in ssreflect/*.v This change reduces - use of numerical occurrence selectors (#436) and - use of non ssreflect tactics such as `auto`, and improves use of comparison predicates such as `posnP`, `leqP`, `ltnP`, `ltngtP`, and `eqVneq`. --- mathcomp/ssreflect/seq.v | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) (limited to 'mathcomp/ssreflect/seq.v') diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index aca2b77..28b80be 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -351,7 +351,7 @@ Lemma last_ind P : Proof. move=> Hnil Hlast s; rewrite -(cat0s s). elim: s [::] Hnil => [|x s2 IHs] s1 Hs1; first by rewrite cats0. -by rewrite -cat_rcons; auto. +by rewrite -cat_rcons; apply/IHs/Hlast. Qed. (* Sequence indexing. *) @@ -433,8 +433,7 @@ have [-> | ne_n12] := eqVneq. apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnA maxnn. by do 2!rewrite !nth_set_nth /=; case: eqP. apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnCA. -do 2!rewrite !nth_set_nth /=; case: eqP => // ->. -by rewrite eq_sym -if_neg ne_n12. +by do 2!rewrite !nth_set_nth /=; case: eqP => // ->; case: eqVneq ne_n12. Qed. (* find, count, has, all. *) @@ -751,7 +750,7 @@ Qed. Lemma nth_drop s i : nth (drop n0 s) i = nth s (n0 + i). Proof. -rewrite -{2}[s]cat_take_drop nth_cat size_take ltnNge. +rewrite -[s in RHS]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. @@ -759,8 +758,8 @@ Qed. Lemma nth_take i : i < n0 -> forall s, nth (take n0 s) i = nth s i. Proof. move=> lt_i_n0 s; case lt_n0_s: (n0 < size s). - by rewrite -{2}[s]cat_take_drop nth_cat size_take lt_n0_s /= lt_i_n0. -by rewrite -{1}[s]cats0 take_cat lt_n0_s /= cats0. + by rewrite -[s in RHS]cat_take_drop nth_cat size_take lt_n0_s /= lt_i_n0. +by rewrite -[s in LHS]cats0 take_cat lt_n0_s /= cats0. Qed. Lemma take_take i j : i <= j -> forall s, take i (take j s) = take i s. @@ -815,7 +814,7 @@ Lemma rot0 s : rot 0 s = s. Proof. by rewrite /rot drop0 take0 cats0. Qed. Lemma size_rot s : size (rot n0 s) = size s. -Proof. by rewrite -{2}[s]cat_take_drop /rot !size_cat addnC. Qed. +Proof. by rewrite -[s in RHS]cat_take_drop /rot !size_cat addnC. Qed. Lemma rot_oversize n s : size s <= n -> rot n s = s. Proof. by move=> le_s_n; rewrite /rot take_oversize ?drop_oversize. Qed. @@ -989,7 +988,7 @@ Fixpoint eqseq s1 s2 {struct s2} := Lemma eqseqP : Equality.axiom eqseq. Proof. move; elim=> [|x1 s1 IHs] [|x2 s2]; do [by constructor | simpl]. -case: (x1 =P x2) => [<-|neqx]; last by right; case. +have [<-|neqx] := x1 =P x2; last by right; case. by apply: (iffP (IHs s2)) => [<-|[]]. Qed. @@ -1371,7 +1370,7 @@ by rewrite !inE (ltn_trans ltij ltjs) ltn_eqF //=; case. Qed. Lemma mem_rot s : rot n0 s =i s. -Proof. by move=> x; rewrite -{2}(cat_take_drop n0 s) !mem_cat /= orbC. Qed. +Proof. by move=> x; rewrite -[s in RHS](cat_take_drop n0) !mem_cat /= orbC. Qed. Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2). Proof. by apply: inj_eq; apply: rot_inj. Qed. @@ -1442,7 +1441,7 @@ Qed. End NthTheory. Lemma set_nth_default T s (y0 x0 : T) n : n < size s -> nth x0 s n = nth y0 s n. -Proof. by elim: s n => [|y s' IHs] [|n] /=; auto. Qed. +Proof. by elim: s n => [|y s' IHs] [|n] //= /IHs. Qed. Lemma headI T s (x : T) : rcons s x = head x s :: behead (rcons s x). Proof. by case: s. Qed. @@ -1748,7 +1747,7 @@ Lemma rotrK : cancel (@rotr T n0) (rot n0). Proof. move=> s; have [lt_n0s | ge_n0s] := ltnP n0 (size s). by rewrite -{1}(subKn (ltnW lt_n0s)) -{1}[size s]size_rotr; apply: rotK. -by rewrite -{2}(rot_oversize ge_n0s) /rotr (eqnP ge_n0s) rot0. +by rewrite -[in RHS](rot_oversize ge_n0s) /rotr (eqnP ge_n0s) rot0. Qed. Lemma rotr_inj : injective (@rotr T n0). @@ -1786,7 +1785,7 @@ Implicit Type s : seq T. Lemma rotD m n s : m + n <= size s -> rot (m + n) s = rot m (rot n s). Proof. -move=> sz_s; rewrite {1}/rot -[take _ s](cat_take_drop n). +move=> sz_s; rewrite [LHS]/rot -[take _ s](cat_take_drop n). rewrite 5!(catA, =^~ rot_size_cat) !cat_take_drop. by rewrite size_drop !size_takel ?leq_addl ?addnK. Qed. @@ -1944,7 +1943,7 @@ exists (take i m ++ drop i.+1 m). rewrite size_cat size_take size_drop lt_i_m. by rewrite sz_m in lt_i_m *; rewrite subnKC. rewrite {s1 def_s1}[s1](congr1 behead def_s1). -rewrite -[s2](cat_take_drop i) -{1}[m](cat_take_drop i) {}def_m_i -cat_cons. +rewrite -[s2](cat_take_drop i) -[m in LHS](cat_take_drop i) {}def_m_i -cat_cons. have sz_i_s2: size (take i s2) = i by apply: size_takel; rewrite sz_m in lt_i_m. rewrite lastI cat_rcons !mask_cat ?size_nseq ?size_belast ?mask_false //=. by rewrite (drop_nth true) // nth_index -?index_mem. @@ -3176,7 +3175,7 @@ Lemma incr_tallyP x : {homo incr_tally^~ x : bs / bs \in wf_tally}. Proof. move=> bs /andP[]; rewrite unfold_in. elim: bs => [|[y [|n]] bs IHbs] //= /andP[bs'y Ubs]; rewrite inE /= => bs'0. -rewrite eq_sym; case: ifP => [/eqP<- | y'x] /=; first by rewrite bs'y Ubs. +have [<- | y'x] /= := eqVneq y; first by rewrite bs'y Ubs. rewrite -andbA {}IHbs {Ubs bs'0}// andbT. elim: bs bs'y => [|b bs IHbs] /=; rewrite inE ?y'x // => /norP[b'y bs'y]. by case: ifP => _; rewrite /= inE negb_or ?y'x // b'y IHbs. -- cgit v1.2.3 From 37a49513f22a3f792a1ac3241962a7d17455f7e5 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sat, 16 May 2020 09:02:13 +0900 Subject: A few more revisions --- mathcomp/ssreflect/seq.v | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) (limited to 'mathcomp/ssreflect/seq.v') diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 28b80be..920f393 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -615,14 +615,12 @@ Proof. by rewrite -size_filter filter_predT. Qed. Lemma count_predUI a1 a2 s : count (predU a1 a2) s + count (predI a1 a2) s = count a1 s + count a2 s. Proof. -elim: s => //= x s IHs; rewrite /= addnCA -addnA IHs addnA addnC. -by rewrite -!addnA; do 2 nat_congr; case (a1 x); case (a2 x). +elim: s => //= x s IHs; rewrite /= addnACA [RHS]addnACA IHs. +by case: (a1 x) => //; rewrite addn0. Qed. Lemma count_predC a s : count a s + count (predC a) s = size s. -Proof. -by elim: s => //= x s IHs; rewrite addnCA -addnA IHs addnA addn_negb. -Qed. +Proof. by elim: s => //= x s IHs; rewrite addnACA IHs; case: (a _). Qed. Lemma count_filter a1 a2 s : count a1 (filter a2 s) = count (predI a1 a2) s. Proof. by rewrite -!size_filter filter_predI. Qed. @@ -1373,7 +1371,7 @@ Lemma mem_rot s : rot n0 s =i s. Proof. by move=> x; rewrite -[s in RHS](cat_take_drop n0) !mem_cat /= orbC. Qed. Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2). -Proof. by apply: inj_eq; apply: rot_inj. Qed. +Proof. exact/inj_eq/rot_inj. Qed. End EqSeq. @@ -1967,7 +1965,7 @@ Qed. Lemma cat_subseq s1 s2 s3 s4 : subseq s1 s3 -> subseq s2 s4 -> subseq (s1 ++ s2) (s3 ++ s4). Proof. -case/subseqP=> m1 sz_m1 ->; case/subseqP=> m2 sz_m2 ->; apply/subseqP. +case/subseqP=> m1 sz_m1 -> /subseqP [m2 sz_m2 ->]; apply/subseqP. by exists (m1 ++ m2); rewrite ?size_cat ?mask_cat ?sz_m1 ?sz_m2. Qed. @@ -2132,9 +2130,7 @@ Lemma map_mask m s : map (mask m s) = mask m (map s). Proof. by elim: m s => [|[|] m IHm] [|x p] //=; rewrite IHm. Qed. Lemma inj_map : injective f -> injective map. -Proof. -by move=> injf; elim=> [|y1 s1 IHs] [|y2 s2] //= [/injf-> /IHs->]. -Qed. +Proof. by move=> injf; elim=> [|y1 s1 IHs] [|y2 s2] //= [/injf-> /IHs->]. Qed. End Map. @@ -2419,9 +2415,7 @@ Lemma size_iota m n : size (iota m n) = n. Proof. by elim: n m => //= n IHn m; rewrite IHn. Qed. Lemma iota_add m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2. -Proof. -by elim: n1 m => //= [|n1 IHn1] m; rewrite ?addn0 // -addSnnS -IHn1. -Qed. +Proof. by elim: n1 m => [|n1 IHn1] m; rewrite ?addn0 // -addSnnS /= -IHn1. Qed. Lemma iota_addl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n). Proof. by elim: n m2 => //= n IHn m2; rewrite -addnS IHn. Qed. -- cgit v1.2.3