diff options
Diffstat (limited to 'mathcomp/ssreflect/seq.v')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 289 |
1 files changed, 255 insertions, 34 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 1e9e1c9..9747171 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1119,6 +1119,8 @@ Proof. by rewrite -all_predC; apply: allP. Qed. Lemma allPn a s : reflect (exists2 x, x \in s & ~~ a x) (~~ all a s). Proof. by rewrite -has_predC; apply: hasP. Qed. +Lemma allss s : all (mem s) s. Proof. exact/allP. Qed. + Lemma mem_filter a x s : (x \in filter a s) = a x && (x \in s). Proof. rewrite andbC; elim: s => //= y s IHs. @@ -1269,6 +1271,17 @@ elim: s => //= y s IHs /andP[/negbTE s'y /IHs-> {IHs}]. by rewrite in_cons; case: (eqVneq y x) => // <-; rewrite s'y. Qed. +Lemma leq_uniq_countP x s1 s2 : uniq s1 -> + reflect (x \in s1 -> x \in s2) (count_mem x s1 <= count_mem x s2). +Proof. +move/count_uniq_mem->; case: (boolP (_ \in _)) => //= _; last by constructor. +by rewrite -has_pred1 has_count; apply: (iffP idP) => //; apply. +Qed. + +Lemma leq_uniq_count s1 s2 : uniq s1 -> {subset s1 <= s2} -> + (forall x, count_mem x s1 <= count_mem x s2). +Proof. by move=> s1_uniq s1_s2 x; apply/leq_uniq_countP/s1_s2. Qed. + Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x]. Proof. move=> uniq_s s_x; rewrite (all_pred1P _ _ (filter_all _ _)). @@ -1393,6 +1406,60 @@ 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. exact/inj_eq/rot_inj. Qed. +Lemma drop_index s (n := index x0 s) : x0 \in s -> drop n s = x0 :: drop n.+1 s. +Proof. by move=> xs; rewrite (drop_nth x0) ?index_mem ?nth_index. Qed. + +(* lemmas about the pivot pattern [_ ++ _ :: _] *) + +Lemma index_pivot x s1 s2 (s := s1 ++ x :: s2) : x \notin s1 -> + index x s = size s1. +Proof. by rewrite index_cat/= eqxx addn0; case: ifPn. Qed. + +Lemma take_pivot x s2 s1 (s := s1 ++ x :: s2) : x \notin s1 -> + take (index x s) s = s1. +Proof. by move=> /index_pivot->; rewrite take_size_cat. Qed. + +Lemma rev_pivot x s1 s2 : rev (s1 ++ x :: s2) = rev s2 ++ x :: rev s1. +Proof. by rewrite rev_cat rev_cons cat_rcons. Qed. + +Lemma eqseq_pivot2l x s1 s2 s3 s4 : x \notin s1 -> x \notin s3 -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. +move=> xNs1 xNs3; apply/idP/idP => [E|/andP[/eqP-> /eqP->]//]. +suff S : size s1 = size s3 by rewrite eqseq_cat// eqseq_cons eqxx in E. +by rewrite -(index_pivot s2 xNs1) (eqP E) index_pivot. +Qed. + +Lemma eqseq_pivot2r x s1 s2 s3 s4 : x \notin s2 -> x \notin s4 -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. +move=> xNs2 xNs4; rewrite -(can_eq revK) !rev_pivot. +by rewrite eqseq_pivot2l ?mem_rev // !(can_eq revK) andbC. +Qed. + +Lemma eqseq_pivotl x s1 s2 s3 s4 : x \notin s1 -> x \notin s2 -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. +move=> xNs1 xNs2; apply/idP/idP => [E|/andP[/eqP-> /eqP->]//]. +rewrite -(@eqseq_pivot2l x)//; have /eqP/(congr1 (count_mem x)) := E. +rewrite !count_cat/= eqxx !addnS (count_memPn _ _ xNs1) (count_memPn _ _ xNs2). +by move=> -[/esym/eqP]; rewrite addn_eq0 => /andP[/eqP/count_memPn]. +Qed. + +Lemma eqseq_pivotr x s1 s2 s3 s4 : x \notin s3 -> x \notin s4 -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. by move=> *; rewrite eq_sym eqseq_pivotl//; case: eqVneq => /=. Qed. + +Lemma uniq_eqseq_pivotl x s1 s2 s3 s4 : uniq (s1 ++ x :: s2) -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. +by rewrite uniq_catC/= mem_cat => /andP[/norP[? ?] _]; rewrite eqseq_pivotl. +Qed. + +Lemma uniq_eqseq_pivotr x s1 s2 s3 s4 : uniq (s3 ++ x :: s4) -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. by move=> ?; rewrite eq_sym uniq_eqseq_pivotl//; case: eqVneq => /=. Qed. + End EqSeq. Section RotIndex. @@ -1401,9 +1468,7 @@ Implicit Types x y z : T. Lemma rot_index s x (i := index x s) : x \in s -> rot i s = x :: (drop i.+1 s ++ take i s). -Proof. -by move=> x_s; rewrite /rot (drop_nth x) ?index_mem ?nth_index// cat_cons. -Qed. +Proof. by move=> x_s; rewrite /rot drop_index. Qed. Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'. @@ -1472,7 +1537,7 @@ Definition bitseq := seq bool. Canonical bitseq_eqType := Eval hnf in [eqType of bitseq]. Canonical bitseq_predType := Eval hnf in [predType of bitseq]. -(* Generalized versions of splitP (from path.v): split_find_nth and split_find *) +(* Generalizations of splitP (from path.v): split_find_nth and split_find *) Section FindNth. Variables (T : Type). Implicit Types (x : T) (p : pred T) (s : seq T). @@ -1623,6 +1688,10 @@ Proof. by apply/permPl; rewrite -!catA perm_cat2l perm_catC. Qed. Lemma perm_catCA s1 s2 s3 : perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3). Proof. by apply/permPl; rewrite !catA perm_cat2r perm_catC. Qed. +Lemma perm_catACA s1 s2 s3 s4 : + perm_eql ((s1 ++ s2) ++ (s3 ++ s4)) ((s1 ++ s3) ++ (s2 ++ s4)). +Proof. by apply/permPl; rewrite perm_catAC !catA perm_catAC. Qed. + Lemma perm_rcons x s : perm_eql (rcons s x) (x :: s). Proof. by move=> /= s2; rewrite -cats1 perm_catC. Qed. @@ -1920,14 +1989,24 @@ Lemma mask_cat m1 m2 s1 s2 : size m1 = size s1 -> mask (m1 ++ m2) (s1 ++ s2) = mask m1 s1 ++ mask m2 s2. Proof. by move: m1 s1; apply: seq_ind2 => // -[] m1 x1 s1 /= _ ->. Qed. +Lemma mask_rcons b m x s : size m = size s -> + mask (rcons m b) (rcons s x) = mask m s ++ nseq b x. +Proof. by move=> ms; rewrite -!cats1 mask_cat//; case: b. Qed. + +Lemma all_mask a m s : all a s -> all a (mask m s). +Proof. by elim: s m => [|x s IHs] [|[] m]//= /andP[ax /IHs->]; rewrite ?ax. Qed. + Lemma has_mask_cons a b m x s : has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s). Proof. by case: b. Qed. Lemma has_mask a m s : has a (mask m s) -> has a s. +Proof. by apply/contraTT; rewrite -!all_predC; apply: all_mask. Qed. + +Lemma rev_mask m s : size m = size s -> rev (mask m s) = mask (rev m) (rev s). Proof. -elim: m s => [|b m IHm] [|x s] //; rewrite has_mask_cons /= andbC. -by case: (a x) => //= /IHm. +move: m s; apply: seq_ind2 => //= b x m s eq_size_sm IH. +by case: b; rewrite !rev_cons mask_rcons ?IH ?size_rev// (cats1, cats0). Qed. Lemma mask_rot m s : size m = size s -> @@ -2102,6 +2181,27 @@ elim: s => //= x s; case: (_ \in _); last by rewrite eqxx. by case: (undup s) => //= y u; case: (_ == _) => //=; apply: cons_subseq. Qed. +Lemma subseq_rev s1 s2 : subseq (rev s1) (rev s2) = subseq s1 s2. +Proof. +wlog suff W : s1 s2 / subseq s1 s2 -> subseq (rev s1) (rev s2). + by apply/idP/idP => /W //; rewrite !revK. +by case/subseqP => m size_m ->; rewrite rev_mask // mask_subseq. +Qed. + +Lemma subseq_cat2l s s1 s2 : subseq (s ++ s1) (s ++ s2) = subseq s1 s2. +Proof. by elim: s => // x s IHs; rewrite !cat_cons /= eqxx. Qed. + +Lemma subseq_cat2r s s1 s2 : subseq (s1 ++ s) (s2 ++ s) = subseq s1 s2. +Proof. by rewrite -subseq_rev !rev_cat subseq_cat2l subseq_rev. Qed. + +Lemma subseq_rot p s n : + subseq p s -> exists2 k, k <= n & subseq (rot k p) (rot n s). +Proof. +move=> /subseqP[m size_m ->]. +exists (count id (take n m)); last by rewrite -mask_rot // mask_subseq. +by rewrite (leq_trans (count_size _ _))// size_take; case: ltnP. +Qed. + End Subseq. Prenex Implicits subseq. @@ -2115,16 +2215,19 @@ Variables (T : eqType) (x : T). Fixpoint rem s := if s is y :: t then (if y == x then t else y :: rem t) else s. +Lemma rem_cons y s : rem (y :: s) = if y == x then s else y :: rem s. +Proof. by []. Qed. + +Lemma remE s : rem s = take (index x s) s ++ drop (index x s).+1 s. +Proof. by elim: s => //= y s ->; case: eqVneq; rewrite ?drop0. Qed. + Lemma rem_id s : x \notin s -> rem s = s. -Proof. -by elim: s => //= y s IHs /norP[neq_yx /IHs->]; rewrite eq_sym (negbTE neq_yx). -Qed. +Proof. by elim: s => //= y s IHs /norP[neq_yx /IHs->]; case: eqVneq neq_yx. Qed. Lemma perm_to_rem s : x \in s -> perm_eq s (x :: rem s). Proof. -elim: s => // y s IHs; rewrite inE /= eq_sym perm_sym. -case: eqP => [-> // | _ /IHs]. -by rewrite (perm_catCA [:: x] [:: y]) perm_cons perm_sym. +move=> xs; rewrite remE -[X in perm_eq X](cat_take_drop (index x s)). +by rewrite drop_index// -cat1s perm_catCA cat1s. Qed. Lemma size_rem s : x \in s -> size (rem s) = (size s).-1. @@ -2154,6 +2257,18 @@ Proof. by move/rem_filter=> -> y; rewrite mem_filter. Qed. Lemma mem_rem_uniqF s : uniq s -> x \in rem s = false. Proof. by move/mem_rem_uniq->; rewrite inE eqxx. Qed. +Lemma count_rem P s : count P (rem s) = count P s - (x \in s) && P x. +Proof. +have [/perm_to_rem/permP->|xNs]/= := boolP (x \in s); first by rewrite addKn. +by rewrite subn0 rem_id. +Qed. + +Lemma count_mem_rem y s : count_mem y (rem s) = count_mem y s - (x == y). +Proof. +rewrite count_rem; have []//= := boolP (x \in s). +by case: eqP => // <- /count_memPn->. +Qed. + End Rem. Section Map. @@ -2259,8 +2374,18 @@ Notation "[ 'seq' E : R | i : T <- s & C ]" := Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s. Proof. by elim: s => //= x s <-; case: (a x). Qed. -Lemma mask_filter (T : eqType) (s : seq T) (m : bitseq) : - uniq s -> mask m s = [seq i <- s | i \in mask m s]. +Section MiscMask. + +Lemma leq_count_mask T (P : {pred T}) m s : count P (mask m s) <= count P s. +Proof. +by elim: s m => [|x s IHs] [|[] m]//=; + rewrite ?leq_add2l (leq_trans (IHs _)) ?leq_addl. +Qed. + +Variable (T : eqType). +Implicit Types (s : seq T) (m : bitseq). + +Lemma mask_filter s m : uniq s -> mask m s = [seq i <- s | i \in mask m s]. Proof. elim: m s => [|[] m ih] [|x s] //=. - by move=> _; elim: s. @@ -2269,6 +2394,33 @@ elim: m s => [|[] m ih] [|x s] //=. - by case: ifP => [/mem_mask -> // | _ /andP [] _ /ih]. Qed. +Lemma leq_count_subseq P s1 s2 : subseq s1 s2 -> count P s1 <= count P s2. +Proof. by move=> /subseqP[m _ ->]; rewrite leq_count_mask. Qed. + +Lemma count_maskP s1 s2 : + (forall x, count_mem x s1 <= count_mem x s2) <-> + exists2 m : bitseq, size m = size s2 & perm_eq s1 (mask m s2). +Proof. +split=> [s1_le|[m _ /permP s1ms2 x]]; last by rewrite s1ms2 leq_count_mask. +suff [m mP]: exists m, perm_eq s1 (mask m s2). + by have [m' sm' eqm] := resize_mask m s2; exists m'; rewrite -?eqm. +elim: s2 => [|x s2 IHs]//= in s1 s1_le *. + by exists [::]; apply/allP => x _/=; rewrite eqn_leq s1_le. +have [y|m s1s2] := IHs (rem x s1); first by rewrite count_mem_rem leq_subLR. +exists ((x \in s1) :: m); have [|/rem_id<-//] := boolP (x \in s1). +by move/perm_to_rem/permPl->; rewrite perm_cons. +Qed. + +Lemma count_subseqP s1 s2 : + (forall x, count_mem x s1 <= count_mem x s2) <-> + exists2 s, subseq s s2 & perm_eq s1 s. +Proof. +rewrite count_maskP; split=> [[m _]|[_/subseqP[m sm ->]]]; last by exists m. +by exists (mask m s2); rewrite ?mask_subseq. +Qed. + +End MiscMask. + Section FilterSubseq. Variable T : eqType. @@ -2294,6 +2446,18 @@ rewrite uniq_perm ?filter_uniq ?(subseq_uniq ss12) // => x. by rewrite mem_filter; apply: andb_idr; apply: (mem_subseq ss12). Qed. +Lemma uniq_subseq_pivot x (s1 s2 s3 s4 : seq T) (s := s3 ++ x :: s4) : + uniq s -> subseq (s1 ++ x :: s2) s = (subseq s1 s3 && subseq s2 s4). +Proof. +move=> uniq_s; apply/idP/idP => [sub_s'_s|/andP[? ?]]; last first. + by rewrite cat_subseq //= eqxx. +have uniq_s' := subseq_uniq sub_s'_s uniq_s. +have/eqP {sub_s'_s uniq_s} := subseq_uniqP _ uniq_s sub_s'_s. +rewrite !filter_cat /= mem_cat inE eqxx orbT /=. +rewrite uniq_eqseq_pivotl // => /andP [/eqP -> /eqP ->]. +by rewrite !filter_subseq. +Qed. + Lemma perm_to_subseq s1 s2 : subseq s1 s2 -> {s3 | perm_eq s2 (s1 ++ s3)}. Proof. @@ -2303,15 +2467,12 @@ case: eqP => [-> | _] /IHs[s3 perm_s2] {IHs}. by exists (rcons s3 y); rewrite -cat_cons -perm_rcons -!cats1 catA perm_cat2r. Qed. -Lemma subset_maskP s1 s2 : uniq s1 -> {subset s1 <= s2} -> - exists2 m : seq bool, size m = size s2 & perm_eq s1 (mask m s2). +Lemma subseq_rem x : {homo rem x : s1 s2 / @subseq T s1 s2}. Proof. -move=> s1_uniq sub_s1_s2; pose s1' := [seq x <- undup s2 | x \in s1]. -have /subseqP[m sm s1'_eq] : subseq s1' s2. - by apply: subseq_trans (undup_subseq _); apply: filter_subseq. -exists m; rewrite // -s1'_eq; apply: uniq_perm => // [|x]. - by rewrite filter_uniq ?undup_uniq. -by rewrite mem_filter mem_undup; have [/sub_s1_s2|] := boolP (x \in s1). +move=> s1 s2; elim: s2 s1 => [|x2 s2 IHs2] [|x1 s1]; rewrite ?sub0seq //=. +have [->|_] := eqVneq x1 x2; first by case: eqP => //= _ /IHs2; rewrite eqxx. +move=> /IHs2/subseq_trans->//. +by have [->|_] := eqVneq x x2; [apply: rem_subseq|apply: subseq_cons]. Qed. End FilterSubseq. @@ -3063,16 +3224,45 @@ Lemma size_allpairs_dep f s t : size [seq f x y | x <- s, y <- t x] = sumn [seq size (t x) | x <- s]. Proof. by elim: s => //= x s IHs; rewrite size_cat size_map IHs. Qed. +Lemma allpairs0l f t : [seq f x y | x <- [::], y <- t x] = [::]. +Proof. by []. Qed. + +Lemma allpairs0r f s : [seq f x y | x <- s, y <- [::]] = [::]. +Proof. by elim: s. Qed. + +Lemma allpairs1l f x t : + [seq f x y | x <- [:: x], y <- t x] = [seq f x y | y <- t x]. +Proof. exact: cats0. Qed. + +Lemma allpairs1r f s y : + [seq f x y | x <- s, y <- [:: y x]] = [seq f x (y x) | x <- s]. +Proof. exact: flatten_map1. Qed. + +Lemma allpairs_cons f x s t : + [seq f x y | x <- x :: s, y <- t x] = + [seq f x y | y <- t x] ++ [seq f x y | x <- s, y <- t x]. +Proof. by []. Qed. + Lemma eq_allpairs (f1 f2 : forall x, T x -> R) s t : (forall x, f1 x =1 f2 x) -> [seq f1 x y | x <- s, y <- t x] = [seq f2 x y | x <- s, y <- t x]. -Proof. by move=> eq_f; rewrite (eq_map (fun x => eq_map (eq_f x) (t x))). Qed. +Proof. by move=> eq_f; rewrite (eq_map (fun x => eq_map (eq_f x) (t x))). Qed. + +Lemma eq_allpairsr (f : forall x, T x -> R) s t1 t2 : (forall x, t1 x = t2 x) -> + [seq f x y | x <- s, y <- t1 x] = [seq f x y | x <- s, y <- t2 x]. +(* From Coq 8.10 Proof. by move=> eq_t; under eq_map do rewrite eq_t. Qed. *) +Proof. by move=> eq_t; congr flatten; apply: eq_map => x; rewrite eq_t. Qed. Lemma allpairs_cat f s1 s2 t : [seq f x y | x <- s1 ++ s2, y <- t x] = [seq f x y | x <- s1, y <- t x] ++ [seq f x y | x <- s2, y <- t x]. Proof. by rewrite map_cat flatten_cat. Qed. +Lemma allpairs_rcons f x s t : + [seq f x y | x <- rcons s x, y <- t x] = + [seq f x y | x <- s, y <- t x] ++ [seq f x y | y <- t x]. +Proof. by rewrite -cats1 allpairs_cat allpairs1l. Qed. + Lemma allpairs_mapl f (g : S' -> S) s t : [seq f x y | x <- map g s, y <- t x] = [seq f (g x) y | x <- s, y <- t (g x)]. Proof. by rewrite -map_comp. Qed. @@ -3165,21 +3355,44 @@ Section MemAllPairs. Variables (S : Type) (T : S -> Type) (R : eqType). Implicit Types (f : forall x, T x -> R) (s : seq S). -Lemma allpairs_catr f s t1 t2 : - [seq f x y | x <- s, y <- t1 x ++ t2 x] =i - [seq f x y | x <- s, y <- t1 x] ++ [seq f x y | x <- s, y <- t2 x]. +Lemma perm_allpairs_catr f s t1 t2 : + perm_eql [seq f x y | x <- s, y <- t1 x ++ t2 x] + ([seq f x y | x <- s, y <- t1 x] ++ [seq f x y | x <- s, y <- t2 x]). +Proof. +apply/permPl; rewrite perm_sym; elim: s => //= x s ihs. +by rewrite perm_catACA perm_cat ?map_cat. +Qed. + +Lemma mem_allpairs_catr f s y0 t : + [seq f x y | x <- s, y <- y0 x ++ t x] =i + [seq f x y | x <- s, y <- y0 x] ++ [seq f x y | x <- s, y <- t x]. +Proof. exact/perm_mem/permPl/perm_allpairs_catr. Qed. + +Lemma perm_allpairs_consr f s y0 t : + perm_eql [seq f x y | x <- s, y <- y0 x :: t x] + ([seq f x (y0 x) | x <- s] ++ [seq f x y | x <- s, y <- t x]). Proof. -move=> z; rewrite mem_cat; elim: s => //= x s ih. -by rewrite map_cat !mem_cat ih !orbA; congr orb; rewrite orbAC. +by apply/permPl; rewrite (perm_allpairs_catr _ _ (fun=> [:: _])) allpairs1r. Qed. -Lemma allpairs_consr f s t1 t2 : - [seq f x y | x <- s, y <- t1 x :: t2 x] =i - [seq f x (t1 x) | x <- s] ++ [seq f x y | x <- s, y <- t2 x]. +Lemma mem_allpairs_consr f s t y0 : + [seq f x y | x <- s, y <- y0 x :: t x] =i + [seq f x (y0 x) | x <- s] ++ [seq f x y | x <- s, y <- t x]. +Proof. exact/perm_mem/permPl/perm_allpairs_consr. Qed. + +Lemma allpairs_rconsr f s y0 t : + perm_eql [seq f x y | x <- s, y <- rcons (t x) (y0 x)] + ([seq f x y | x <- s, y <- t x] ++ [seq f x (y0 x) | x <- s]). Proof. -by move=> z; rewrite (allpairs_catr f s (fun x => [:: t1 x])) /= flatten_map1. +apply/permPl; rewrite -(eq_allpairsr _ _ (fun=> cats1 _ _)). +by rewrite perm_allpairs_catr allpairs1r. Qed. +Lemma mem_allpairs_rconsr f s t y0 : + [seq f x y | x <- s, y <- rcons (t x) (y0 x)] =i + ([seq f x y | x <- s, y <- t x] ++ [seq f x (y0 x) | x <- s]). +Proof. exact/perm_mem/permPl/allpairs_rconsr. Qed. + End MemAllPairs. Lemma all_allpairsP @@ -3596,6 +3809,14 @@ Notation uniq_perm_eq := (deprecate uniq_perm_eq uniq_perm _ _ _) Notation perm_eq_iotaP := (deprecate perm_eq_iotaP perm_iotaP) (only parsing). Notation perm_undup_count := (deprecate perm_undup_count perm_count_undup _ _) (only parsing). - -Notation iota_add := (deprecate iota_add iotaD) (only parsing). +(* TODO: restore when Coq 8.10 is no longer supported *) +(* #[deprecated(since="mathcomp 1.13.0", note="Use iotaD instead.")] *) +Notation iota_add := iotaD (only parsing). Notation iota_addl := (deprecate iota_addl iotaDl) (only parsing). + +Notation allpairs_catr := + (deprecate allpairs_catr mem_allpairs_catr _ _ _) (only parsing). +Notation allpairs_consr := + (deprecate allpairs_consr mem_allpairs_consr _ _ _) (only parsing). +Notation perm_allpairs_rconsr := + (deprecate perm_allpairs_rconsr allpairs_rconsr _ _ _) (only parsing). |