From 783631c771ec76baa4ff9d292c1eddfb58f67f4c Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 20 Nov 2020 16:52:52 +0900 Subject: Generalize `allrel` to take two lists as arguments --- mathcomp/ssreflect/path.v | 33 +++++++------- mathcomp/ssreflect/seq.v | 110 ++++++++++++++++++++++++++++++++++------------ 2 files changed, 98 insertions(+), 45 deletions(-) (limited to 'mathcomp/ssreflect') diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index e9143fe..112f129 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -1097,24 +1097,25 @@ Hypothesis (leT_total : total leT) (leT'_tr : transitive leT'). Let leT_lex := [rel x y | leT x y && (leT y x ==> leT' x y)]. Lemma merge_stable_path x s1 s2 : - all (fun y => all (leT' y) s2) s1 -> - path leT_lex x s1 -> path leT_lex x s2 -> path leT_lex x (merge leT s1 s2). + allrel leT' s1 s2 -> path leT_lex x s1 -> path leT_lex x s2 -> + path leT_lex x (merge leT s1 s2). Proof. elim: s1 s2 x => //= x s1 ih1; elim => //= y s2 ih2 h. -rewrite all_predI -andbA => /and4P [xy' xs2 ys1 s1s2]. -case/andP => hx xs1 /andP [] hy ys2; case: ifP => xy /=; rewrite (hx, hy) /=. -- by apply: ih1; rewrite ?all_predI ?ys1 //= xy xy' implybT. -- by apply: ih2; have:= leT_total x y; rewrite ?xs2 //= xy => /= ->. +rewrite allrel_consl allrel_consr /= -andbA. +move=> /and4P [xy' xs2 ys1 s1s2] /andP [hx xs1] /andP [hy ys2]. +case: ifP => xy /=; rewrite (hx, hy) /=. +- by apply: ih1; rewrite ?allrel_consr ?ys1 //= xy xy' implybT. +- by apply: ih2; have:= leT_total x y; rewrite ?allrel_consl ?xs2 ?xy //= => ->. Qed. Lemma merge_stable_sorted s1 s2 : - all (fun x => all (leT' x) s2) s1 -> - sorted leT_lex s1 -> sorted leT_lex s2 -> sorted leT_lex (merge leT s1 s2). + allrel leT' s1 s2 -> sorted leT_lex s1 -> sorted leT_lex s2 -> + sorted leT_lex (merge leT s1 s2). Proof. -case: s1 s2 => [|x s1] [|y s2] //=; rewrite all_predI -andbA. +case: s1 s2 => [|x s1] [|y s2] //=; rewrite allrel_consl allrel_consr /= -andbA. case/and4P => [xy' xs2 ys1 s1s2] xs1 ys2; rewrite -/(merge _ (_ :: _)). by case: ifP (leT_total x y) => /= xy yx; apply/merge_stable_path; - rewrite /= ?(all_predI, xs2, ys1, xy, yx, xy', implybT). + rewrite /= ?(allrel_consl, allrel_consr, xs2, ys1, xy, yx, xy', implybT). Qed. End Stability_merge. @@ -1142,9 +1143,9 @@ Proof. elim: ss s1 => [] // [] //= m s2 ss ihss s1; rewrite -2!andbA. move=> /and5P [sorted_s1 perm_s1 sorted_s2 perm_s2 hss]; apply: ihss. rewrite hss size_merge size_cat iotaD addnC -size_cat perm_merge perm_cat //. -rewrite merge_stable_sorted // (perm_all _ perm_s2); apply/allP => n. -rewrite mem_iota (perm_all _ perm_s1) => /andP [_ n_lt]; apply/allP => p. -by rewrite mem_iota size_cat addnC => /andP [] /(leq_trans n_lt). +rewrite merge_stable_sorted //; apply/allrelP => n p. +rewrite (perm_mem perm_s1) (perm_mem perm_s2) !mem_iota size_cat addnC. +by move=> /andP [_ n_lt] /andP [] /(leq_trans n_lt). Qed. Let pop_stable s1 ss : @@ -1153,9 +1154,9 @@ Proof. elim: ss s1 => [s1 /andP [] /andP [] //|s2 ss ihss s1]; rewrite /= -2!andbA. move=> /and5P [sorted_s1 perm_s1 sorted_s2 perm_s2 hss]; apply: ihss. rewrite /= hss size_merge size_cat iotaD addnC -size_cat perm_merge perm_cat //. -rewrite merge_stable_sorted // (perm_all _ perm_s2); apply/allP => n. -rewrite mem_iota (perm_all _ perm_s1) => /andP [_ n_lt]; apply/allP => p. -by rewrite mem_iota size_cat addnC => /andP [] /(leq_trans n_lt). +rewrite merge_stable_sorted //; apply/allrelP => n p. +rewrite (perm_mem perm_s1) (perm_mem perm_s2) !mem_iota size_cat addnC. +by move=> /andP [_ n_lt] /andP [] /(leq_trans n_lt). Qed. Lemma sort_iota_stable n : sorted lt_lex (sort leN (iota 0 n)). diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 48a59ee..c3936bb 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -132,8 +132,11 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. (* i.e. self expanding definition for *) (* [seq f x y | x <- s, y <- t] *) (* := [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m] *) -(* allrel r s := all id [seq r x y | x <- xs, y <- xs] *) -(* == the proposition r x y holds for all possible x, y in xs *) +(* allrel r xs ys := all [pred x | all (r x) ys] xs *) +(* == the proposition r x y holds for all x and y respectively *) +(* in xs and ys. *) +(* all1rel r xs := allrel r xs xs *) +(* == the proposition r x y holds for all possible x, y in xs. *) (* map f s == the sequence [:: f x_1, ..., f x_n]. *) (* pmap pf s == the sequence [:: y_i1, ..., y_ik] where i1 < ... < ik, *) (* pf x_i = Some y_i, and pf x_j = None iff j is not in *) @@ -3484,45 +3487,94 @@ Arguments perm_consP {T x s t}. Section AllRel. -Definition allrel {T : Type} (r : rel T) xs := - all id [seq r x y | x <- xs, y <- xs]. +Variables (T S : Type) (r : T -> S -> bool). +Implicit Types (x : T) (y : S) (xs : seq T) (ys : seq S). -Lemma allrel0 (T : Type) (r : rel T) : allrel r [::]. -Proof. by []. Qed. +Definition allrel xs ys := all [pred x | all (r x) ys] xs. -Lemma allrel_map (T T' : Type) (f : T' -> T) (r : rel T) xs : - allrel r (map f xs) = allrel (relpre f r) xs. -Proof. by rewrite /allrel allpairs_mapl allpairs_mapr. Qed. +Lemma allrel0s ys : allrel [::] ys. Proof. by []. Qed. -Lemma allrelP {T : eqType} {r : rel T} {xs : seq T} : - reflect {in xs &, forall x y, r x y} (allrel r xs). -Proof. exact: all_allpairsP. Qed. +Lemma allrels0 xs : allrel xs [::]. Proof. by elim: xs. Qed. -Variable (T : nonPropType) (r : rel T). -Implicit Types (xs : seq T) (x y z : T). -Hypothesis (rxx : reflexive r) (rsym : symmetric r). +Lemma allrel_consl x xs ys : allrel (x :: xs) ys = all (r x) ys && allrel xs ys. +Proof. by []. Qed. + +Lemma allrel_consr xs y ys : + allrel xs (y :: ys) = all (r^~ y) xs && allrel xs ys. +Proof. exact: all_predI. Qed. + +Lemma allrel1s x ys : allrel [:: x] ys = all (r x) ys. Proof. exact: andbT. Qed. -Lemma allrel1 x : allrel r [:: x]. -Proof. by rewrite /allrel/= rxx. Qed. +Lemma allrels1 xs y : allrel xs [:: y] = all (r^~ y) xs. +Proof. by rewrite allrel_consr allrels0 andbT. Qed. -Lemma allrel2 x y : allrel r [:: x; y] = r x y. -Proof. by rewrite /allrel/= !rxx [r y x]rsym !(andbT, andbb). Qed. +Lemma allrel_catl xs xs' ys : + allrel (xs ++ xs') ys = allrel xs ys && allrel xs' ys. +Proof. exact: all_cat. Qed. -Lemma allrel_cons x xs : - allrel r (x :: xs) = all (r x) xs && allrel r xs. +Lemma allrel_catr xs ys ys' : + allrel xs (ys ++ ys') = allrel xs ys && allrel xs ys'. Proof. -case: (mkseqP x (_ :: _)) => -[//|n] f [-> ->]. -rewrite !allrel_map all_map; apply/allrelP/andP => /= [rf|]. - split; first by apply/allP => i iP /=; rewrite rf// in_cons iP orbT. - by apply/allrelP => i j iP jP /=; rewrite rf// in_cons (iP, jP) orbT. -move=> [/allP/= rf0 /allrelP/= rf] i j; rewrite !in_cons. -by move=> /predU1P[->|iP] /predU1P[->|jP]//=; rewrite 2?(rf0, rsym)//= rf. +elim: ys => /= [|y ys ihys]; first by rewrite allrels0. +by rewrite !allrel_consr ihys andbA. Qed. +Lemma allrel_allpairsE xs ys : + allrel xs ys = all id [seq r x y | x <- xs, y <- ys]. +Proof. by elim: xs => //= x xs ->; rewrite all_cat all_map. Qed. + End AllRel. -Arguments allrel {T} r xs. -Arguments allrelP {T r xs}. +Arguments allrel {T S} r xs ys : simpl never. +Arguments allrel0s {T S} r ys. +Arguments allrels0 {T S} r xs. +Arguments allrel_consl {T S} r x xs ys. +Arguments allrel_consr {T S} r xs y ys. +Arguments allrel1s {T S} r x ys. +Arguments allrels1 {T S} r xs y. +Arguments allrel_catl {T S} r xs xs' ys. +Arguments allrel_catr {T S} r xs ys ys'. +Arguments allrel_allpairsE {T S} r xs ys. + +Notation all1rel r xs := (allrel r xs xs). + +Lemma allrelC {T S : Type} (r : T -> S -> bool) xs ys : + allrel r xs ys = allrel (fun y => r^~ y) ys xs. +Proof. by elim: xs => [|x xs ih]; [elim: ys | rewrite allrel_consr -ih]. Qed. + +Lemma allrel_mapl {T T' S : Type} (f : T' -> T) (r : T -> S -> bool) xs ys : + allrel r (map f xs) ys = allrel (fun x => r (f x)) xs ys. +Proof. exact: all_map. Qed. + +Lemma allrel_mapr {T S S' : Type} (f : S' -> S) (r : T -> S -> bool) xs ys : + allrel r xs (map f ys) = allrel (fun x y => r x (f y)) xs ys. +Proof. by rewrite allrelC allrel_mapl allrelC. Qed. + +Lemma allrelP {T S : eqType} {r : T -> S -> bool} {xs ys} : + reflect {in xs & ys, forall x y, r x y} (allrel r xs ys). +Proof. by rewrite allrel_allpairsE; exact: all_allpairsP. Qed. + +Section All1Rel. + +Variable (T : nonPropType) (r : rel T). +Implicit Types (x y z : T) (xs : seq T). +Hypothesis (rsym : symmetric r). + +Lemma all1rel1 x : all1rel r [:: x] = r x x. +Proof. by rewrite /allrel /= !andbT. Qed. + +Lemma all1rel2 x y : all1rel r [:: x; y] = r x x && r y y && r x y. +Proof. by rewrite /allrel /= rsym; do 3 case: r. Qed. + +Lemma all1rel_cons x xs : + all1rel r (x :: xs) = [&& r x x, all (r x) xs & all1rel r xs]. +Proof. +rewrite allrel_consl allrel_consr /= !andbA [r x x && _]andbC -andbA andbACA. +rewrite -[RHS]andbA; congr andb; rewrite -all_predI. +by elim: xs => //= y xs ->; rewrite rsym andbb. +Qed. + +End All1Rel. Section Permutations. -- cgit v1.2.3 From c2b2ea2dce5fa7b8d428a5072f2e86979eeb1d98 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sat, 21 Nov 2020 13:30:45 +0900 Subject: Apply suggestions from code review Co-authored-by: Christian Doczkal --- mathcomp/ssreflect/seq.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'mathcomp/ssreflect') diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index c3936bb..777041f 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -133,8 +133,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. (* [seq f x y | x <- s, y <- t] *) (* := [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m] *) (* allrel r xs ys := all [pred x | all (r x) ys] xs *) -(* == the proposition r x y holds for all x and y respectively *) -(* in xs and ys. *) +(* == r x y holds whenever x is in xs and y is in ys *) (* all1rel r xs := allrel r xs xs *) (* == the proposition r x y holds for all possible x, y in xs. *) (* map f s == the sequence [:: f x_1, ..., f x_n]. *) -- cgit v1.2.3 From 43796130c3e59c0651a283e6654a7d82acbfeed3 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sat, 21 Nov 2020 13:32:03 +0900 Subject: Apply suggestions from code review Co-authored-by: Cyril Cohen --- mathcomp/ssreflect/path.v | 3 +-- mathcomp/ssreflect/seq.v | 41 +++++++++++++++++++++++++++++------------ 2 files changed, 30 insertions(+), 14 deletions(-) (limited to 'mathcomp/ssreflect') diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 112f129..8ee8bea 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -1101,8 +1101,7 @@ Lemma merge_stable_path x s1 s2 : path leT_lex x (merge leT s1 s2). Proof. elim: s1 s2 x => //= x s1 ih1; elim => //= y s2 ih2 h. -rewrite allrel_consl allrel_consr /= -andbA. -move=> /and4P [xy' xs2 ys1 s1s2] /andP [hx xs1] /andP [hy ys2]. +rewrite allrel_cons2 => /and4P [xy' xs2 ys1 s1s2] /andP [hx xs1] /andP [hy ys2]. case: ifP => xy /=; rewrite (hx, hy) /=. - by apply: ih1; rewrite ?allrel_consr ?ys1 //= xy xy' implybT. - by apply: ih2; have:= leT_total x y; rewrite ?allrel_consl ?xs2 ?xy //= => ->. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 777041f..9747f73 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -3491,9 +3491,9 @@ Implicit Types (x : T) (y : S) (xs : seq T) (ys : seq S). Definition allrel xs ys := all [pred x | all (r x) ys] xs. -Lemma allrel0s ys : allrel [::] ys. Proof. by []. Qed. +Lemma allrel0l ys : allrel [::] ys. Proof. by []. Qed. -Lemma allrels0 xs : allrel xs [::]. Proof. by elim: xs. Qed. +Lemma allrel0r xs : allrel xs [::]. Proof. by elim: xs. Qed. Lemma allrel_consl x xs ys : allrel (x :: xs) ys = all (r x) ys && allrel xs ys. Proof. by []. Qed. @@ -3502,10 +3502,15 @@ Lemma allrel_consr xs y ys : allrel xs (y :: ys) = all (r^~ y) xs && allrel xs ys. Proof. exact: all_predI. Qed. -Lemma allrel1s x ys : allrel [:: x] ys = all (r x) ys. Proof. exact: andbT. Qed. +Lemma allrel_cons2 x y xs ys : + allrel (x :: xs) (y :: ys) = + [&& r x y, all (r x) ys, all (r^~ y) xs & allrel xs ys]. +Proof. by rewrite /= allrel_consr -andbA. Qed. -Lemma allrels1 xs y : allrel xs [:: y] = all (r^~ y) xs. -Proof. by rewrite allrel_consr allrels0 andbT. Qed. +Lemma allrel1l x ys : allrel [:: x] ys = all (r x) ys. Proof. exact: andbT. Qed. + +Lemma allrel1r xs y : allrel xs [:: y] = all (r^~ y) xs. +Proof. by rewrite allrel_consr allrel0r andbT. Qed. Lemma allrel_catl xs xs' ys : allrel (xs ++ xs') ys = allrel xs ys && allrel xs' ys. @@ -3514,7 +3519,7 @@ Proof. exact: all_cat. Qed. Lemma allrel_catr xs ys ys' : allrel xs (ys ++ ys') = allrel xs ys && allrel xs ys'. Proof. -elim: ys => /= [|y ys ihys]; first by rewrite allrels0. +elim: ys => /= [|y ys ihys]; first by rewrite allrel0r. by rewrite !allrel_consr ihys andbA. Qed. @@ -3525,18 +3530,31 @@ Proof. by elim: xs => //= x xs ->; rewrite all_cat all_map. Qed. End AllRel. Arguments allrel {T S} r xs ys : simpl never. -Arguments allrel0s {T S} r ys. -Arguments allrels0 {T S} r xs. +Arguments allrel0l {T S} r ys. +Arguments allrel0r {T S} r xs. Arguments allrel_consl {T S} r x xs ys. Arguments allrel_consr {T S} r xs y ys. -Arguments allrel1s {T S} r x ys. -Arguments allrels1 {T S} r xs y. +Arguments allrel1l {T S} r x ys. +Arguments allrel1r {T S} r xs y. Arguments allrel_catl {T S} r xs xs' ys. Arguments allrel_catr {T S} r xs ys ys'. Arguments allrel_allpairsE {T S} r xs ys. Notation all1rel r xs := (allrel r xs xs). +Lemma eq_in_allrel {T S : Type} (P : {pred T}) (Q : {pred S}) r r' : + {in P & Q, r =2 r'} -> + forall xs ys, all P xs -> all Q ys -> allrel r xs ys = allrel r' xs ys. +Proof. +move=> rr' + ys; elim=> //= x xs IH /andP [Px Pxs] Qys. +congr andb => /=; last exact: IH. +by elim: ys Qys {IH} => //= y ys IH /andP [Qy Qys]; rewrite rr' // IH. +Qed. + +Lemma eq_allrel {T S : Type} (r r': T -> S -> bool) xs ys : + r =2 r' -> allrel r xs ys = allrel r' xs ys. +Proof. by move=> rr'; apply/eq_in_allrel/all_predT/all_predT. Qed. + Lemma allrelC {T S : Type} (r : T -> S -> bool) xs ys : allrel r xs ys = allrel (fun y => r^~ y) ys xs. Proof. by elim: xs => [|x xs ih]; [elim: ys | rewrite allrel_consr -ih]. Qed. @@ -3568,8 +3586,7 @@ Proof. by rewrite /allrel /= rsym; do 3 case: r. Qed. Lemma all1rel_cons x xs : all1rel r (x :: xs) = [&& r x x, all (r x) xs & all1rel r xs]. Proof. -rewrite allrel_consl allrel_consr /= !andbA [r x x && _]andbC -andbA andbACA. -rewrite -[RHS]andbA; congr andb; rewrite -all_predI. +rewrite allrel_cons2; congr andb; rewrite andbA -all_predI; congr andb. by elim: xs => //= y xs ->; rewrite rsym andbb. Qed. -- cgit v1.2.3 From d844896e6418bb00418964bb4ae4219e2bd6b69c Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 25 Nov 2020 22:14:58 +0900 Subject: Rename `all1rel` to `all2rel`, restate `eq_allrel`, and add CHANGELOG entries Co-authored-by: Cyril Cohen --- mathcomp/ssreflect/seq.v | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'mathcomp/ssreflect') diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 9747f73..abca0d9 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -134,7 +134,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. (* := [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m] *) (* allrel r xs ys := all [pred x | all (r x) ys] xs *) (* == r x y holds whenever x is in xs and y is in ys *) -(* all1rel r xs := allrel r xs xs *) +(* all2rel r xs := allrel r xs xs *) (* == the proposition r x y holds for all possible x, y in xs. *) (* map f s == the sequence [:: f x_1, ..., f x_n]. *) (* pmap pf s == the sequence [:: y_i1, ..., y_ik] where i1 < ... < ik, *) @@ -3540,7 +3540,7 @@ Arguments allrel_catl {T S} r xs xs' ys. Arguments allrel_catr {T S} r xs ys ys'. Arguments allrel_allpairsE {T S} r xs ys. -Notation all1rel r xs := (allrel r xs xs). +Notation all2rel r xs := (allrel r xs xs). Lemma eq_in_allrel {T S : Type} (P : {pred T}) (Q : {pred S}) r r' : {in P & Q, r =2 r'} -> @@ -3551,9 +3551,9 @@ congr andb => /=; last exact: IH. by elim: ys Qys {IH} => //= y ys IH /andP [Qy Qys]; rewrite rr' // IH. Qed. -Lemma eq_allrel {T S : Type} (r r': T -> S -> bool) xs ys : - r =2 r' -> allrel r xs ys = allrel r' xs ys. -Proof. by move=> rr'; apply/eq_in_allrel/all_predT/all_predT. Qed. +Lemma eq_allrel {T S : Type} (r r': T -> S -> bool) : + r =2 r' -> allrel r =2 allrel r'. +Proof. by move=> rr' xs ys; apply/eq_in_allrel/all_predT/all_predT. Qed. Lemma allrelC {T S : Type} (r : T -> S -> bool) xs ys : allrel r xs ys = allrel (fun y => r^~ y) ys xs. @@ -3571,26 +3571,26 @@ Lemma allrelP {T S : eqType} {r : T -> S -> bool} {xs ys} : reflect {in xs & ys, forall x y, r x y} (allrel r xs ys). Proof. by rewrite allrel_allpairsE; exact: all_allpairsP. Qed. -Section All1Rel. +Section All2Rel. Variable (T : nonPropType) (r : rel T). Implicit Types (x y z : T) (xs : seq T). Hypothesis (rsym : symmetric r). -Lemma all1rel1 x : all1rel r [:: x] = r x x. +Lemma all2rel1 x : all2rel r [:: x] = r x x. Proof. by rewrite /allrel /= !andbT. Qed. -Lemma all1rel2 x y : all1rel r [:: x; y] = r x x && r y y && r x y. +Lemma all2rel2 x y : all2rel r [:: x; y] = r x x && r y y && r x y. Proof. by rewrite /allrel /= rsym; do 3 case: r. Qed. -Lemma all1rel_cons x xs : - all1rel r (x :: xs) = [&& r x x, all (r x) xs & all1rel r xs]. +Lemma all2rel_cons x xs : + all2rel r (x :: xs) = [&& r x x, all (r x) xs & all2rel r xs]. Proof. rewrite allrel_cons2; congr andb; rewrite andbA -all_predI; congr andb. by elim: xs => //= y xs ->; rewrite rsym andbb. Qed. -End All1Rel. +End All2Rel. Section Permutations. -- cgit v1.2.3