diff options
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 51 | ||||
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 10 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finfun.v | 447 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fingraph.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 34 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 171 | ||||
| -rw-r--r-- | mathcomp/ssreflect/tuple.v | 6 |
7 files changed, 502 insertions, 219 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index f108ff9..a3dd0be 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -786,6 +786,9 @@ Section SeqExtension. Variable I : Type. +Lemma foldrE r : foldr op idx r = \big[op/idx]_(x <- r) x. +Proof. by rewrite unlock. Qed. + Lemma big_filter r (P : pred I) F : \big[op/idx]_(i <- filter P r) F i = \big[op/idx]_(i <- r | P i) F i. Proof. by rewrite unlock; elim: r => //= i r <-; case (P i). Qed. @@ -878,6 +881,11 @@ Proof. by rewrite unlock; elim: r => //= i r ->; case: (P i). Qed. End SeqExtension. +Lemma big_map_id J (h : J -> R) r (P : pred R) : + \big[op/idx]_(i <- map h r | P i) i + = \big[op/idx]_(j <- r | P (h j)) h j. +Proof. exact: big_map. Qed. + (* The following lemmas can be used to localise extensionality to a specific *) (* index sequence. This is done by ssreflect rewriting, before applying *) (* congruence or induction lemmas. *) @@ -1085,6 +1093,24 @@ Lemma big_nseq I n a (F : I -> R): \big[op/idx]_(i <- nseq n a) F i = iter n (op (F a)) idx. Proof. exact: big_nseq_cond. Qed. +Lemma big_image_cond I (J : finType) (h : J -> I) (A : pred J) (P : pred I) F : + \big[op/idx]_(i <- [seq h j | j in A] | P i) F i + = \big[op/idx]_(j in A | P (h j)) F (h j). +Proof. by rewrite big_map big_filter_cond. Qed. + +Lemma big_image I (J : finType) (h : J -> I) (A : pred J) F : + \big[op/idx]_(i <- [seq h j | j in A]) F i = \big[op/idx]_(j in A) F (h j). +Proof. by rewrite big_map big_filter. Qed. + +Lemma big_image_cond_id (J : finType) (h : J -> R) (A : pred J) (P : pred R) : + \big[op/idx]_(i <- [seq h j | j in A] | P i) i + = \big[op/idx]_(j in A | P (h j)) h j. +Proof. exact: big_image_cond. Qed. + +Lemma big_image_id (J : finType) (h : J -> R) (A : pred J) : + \big[op/idx]_(i <- [seq h j | j in A]) i = \big[op/idx]_(j in A) h j. +Proof. exact: big_image. Qed. + End Extensionality. Section MonoidProperties. @@ -1103,6 +1129,14 @@ Variable op : Monoid.law 1. Local Notation "*%M" := op (at level 0). Local Notation "x * y" := (op x y). +Lemma foldlE x r : foldl *%M x r = \big[*%M/1]_(y <- x :: r) y. +Proof. +by rewrite -foldrE; elim: r => [|y r IHr]/= in x *; rewrite ?mulm1 ?mulmA ?IHr. +Qed. + +Lemma foldl_idx r : foldl *%M 1 r = \big[*%M/1]_(x <- r) x. +Proof. by rewrite foldlE big_cons mul1m. Qed. + Lemma eq_big_idx_seq idx' I r (P : pred I) F : right_id idx' *%M -> has P r -> \big[*%M/idx']_(i <- r | P i) F i =\big[*%M/1]_(i <- r | P i) F i. @@ -1159,14 +1193,20 @@ rewrite !(big_mkcond _ P) unlock. by elim: r1 => /= [|i r1 ->]; rewrite (mul1m, mulmA). Qed. -Lemma big_allpairs I1 I2 (r1 : seq I1) (r2 : seq I2) F : - \big[*%M/1]_(i <- [seq (i1, i2) | i1 <- r1, i2 <- r2]) F i = - \big[*%M/1]_(i1 <- r1) \big[op/idx]_(i2 <- r2) F (i1, i2). +Lemma big_allpairs_dep I1 (I2 : I1 -> Type) J (h : forall i1, I2 i1 -> J) + (r1 : seq I1) (r2 : forall i1, seq (I2 i1)) (F : J -> R) : + \big[*%M/1]_(i <- [seq h i1 i2 | i1 <- r1, i2 <- r2 i1]) F i = + \big[*%M/1]_(i1 <- r1) \big[*%M/1]_(i2 <- r2 i1) F (h i1 i2). Proof. elim: r1 => [|i1 r1 IHr1]; first by rewrite !big_nil. by rewrite big_cat IHr1 big_cons big_map. Qed. +Lemma big_allpairs I1 I2 (r1 : seq I1) (r2 : seq I2) F : + \big[*%M/1]_(i <- [seq (i1, i2) | i1 <- r1, i2 <- r2]) F i = + \big[*%M/1]_(i1 <- r1) \big[op/idx]_(i2 <- r2) F (i1, i2). +Proof. exact: big_allpairs_dep. Qed. + Lemma big_pred1_eq (I : finType) (i : I) F : \big[*%M/1]_(j | j == i) F j = F i. Proof. by rewrite -big_filter filter_index_enum enum1 big_seq1. Qed. @@ -1327,7 +1367,7 @@ by apply: big_pred1 => i; rewrite /= andbC; case: eqP => // ->. Qed. Arguments bigD1 [I] j [P F]. -Lemma bigD1_seq (I : eqType) (r : seq I) j F : +Lemma bigD1_seq (I : eqType) (r : seq I) j F : j \in r -> uniq r -> \big[*%M/1]_(i <- r) F i = F j * \big[*%M/1]_(i <- r | i != j) F i. Proof. by move=> /big_rem-> /rem_filter->; rewrite big_filter. Qed. @@ -1512,6 +1552,7 @@ Arguments reindex [R idx op I J] h [P F]. Arguments reindex_inj [R idx op I h P F]. Arguments pair_big_dep [R idx op I J]. Arguments pair_big [R idx op I J]. +Arguments big_allpairs_dep [R idx op I1 I2 J h r1 r2 F]. Arguments big_allpairs [R idx op I1 I2 r1 r2 F]. Arguments exchange_big_dep [R idx op I J rI rJ P Q] xQ [F]. Arguments exchange_big_dep_nat [R idx op m1 n1 m2 n2 P Q] xQ [F]. @@ -1687,6 +1728,8 @@ Proof. by rewrite big_const_nat -Monoid.iteropE. Qed. End NatConst. +Lemma sumnE r : sumn r = \sum_(i <- r) i. Proof. exact: foldrE. Qed. + Lemma leqif_sum (I : finType) (P C : pred I) (E1 E2 : I -> nat) : (forall i, P i -> E1 i <= E2 i ?= iff C i) -> \sum_(i | P i) E1 i <= \sum_(i | P i) E2 i ?= iff [forall (i | P i), C i]. diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 98ee64e..c99e296 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -365,10 +365,10 @@ Lemma card_inj_ffuns_on D T (R : pred T) : Proof. rewrite -card_uniq_tuples. have bijFF: {on (_ : pred _), bijective (@Finfun D T)}. - by exists val => // x _; apply: val_inj. -rewrite -(on_card_preimset (bijFF _)); apply: eq_card => t. -rewrite !inE -(codom_ffun (Finfun t)); congr (_ && _); apply: negb_inj. -by rewrite -has_predC has_map enumT has_filter -size_eq0 -cardE. + by exists fgraph => x _; [apply: FinfunK | apply: fgraphK]. +rewrite -(on_card_preimset (bijFF _)); apply: eq_card => /= t. +rewrite !inE -(big_andE predT) -big_filter big_all -all_map. +by rewrite -[injectiveb _]/(uniq _) [map _ _]codom_ffun FinfunK. Qed. Lemma card_inj_ffuns D T : @@ -387,7 +387,7 @@ have [ltTk | lekT] := ltnP #|B| k. have [AsubB /=|//] := boolP (A \subset B). by rewrite (leq_ltn_trans (subset_leq_card AsubB)) ?andbF. apply/eqP; rewrite -(eqn_pmul2r (fact_gt0 k)) bin_ffact // eq_sym. -rewrite -sum_nat_dep_const -{1 3}(card_ord k). +rewrite -sum_nat_cond_const -{1 3}(card_ord k). rewrite -card_inj_ffuns_on -sum1dep_card. pose imIk (f : {ffun 'I_k -> T}) := f @: 'I_k. rewrite (partition_big imIk (fun A => (A \subset B) && (#|A| == k))) /= diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index db1a8e7..db03671 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -6,21 +6,51 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype tuple. (******************************************************************************) (* This file implements a type for functions with a finite domain: *) -(* {ffun aT -> rT} where aT should have a finType structure. *) +(* {ffun aT -> rT} where aT should have a finType structure, *) +(* {ffun forall x : aT, rT} for dependent functions over a finType aT, *) +(* and {ffun funT} where funT expands to a product over a finType. *) (* Any eqType, choiceType, countType and finType structures on rT extend to *) (* {ffun aT -> rT} as Leibnitz equality and extensional equalities coincide. *) (* (T ^ n)%type is notation for {ffun 'I_n -> T}, which is isomorphic *) -(* to n.-tuple T. *) -(* For f : {ffun aT -> rT}, we define *) +(* to n.-tuple T, but is structurally positive and thus can be used to *) +(* define inductive types, e.g., Inductive tree := node n of tree ^ n (see *) +(* mid-file for an expanded example). *) +(* --> More generally, {ffun fT} is always structurally positive. *) +(* {ffun fT} inherits combinatorial structures of rT, i.e., eqType, *) +(* choiceType, countType, and finType. However, due to some limitations of *) +(* the Coq 8.9 unification code the structures are only inherited in the *) +(* NON dependent case, when rT does not depend on x. *) +(* For f : {ffun fT} with fT := forall x : aT, rT we define *) (* f x == the image of x under f (f coerces to a CiC function) *) -(* fgraph f == the graph of f, i.e., the #|aT|.-tuple rT of the *) -(* values of f over enum aT. *) -(* finfun lam == the f such that f =1 lam; this is the RECOMMENDED *) -(* interface to build an element of {ffun aT -> rT}. *) -(* [ffun x => expr] == finfun (fun x => expr) *) -(* [ffun => expr] == finfun (fun _ => expr) *) -(* f \in ffun_on R == the range of f is a subset of R *) +(* --> The coercion is structurally decreasing, e.g., Coq will accept *) +(* Fixpoint size t := let: node n f := t in sumn (codom (size \o f)) + 1. *) +(* as structurally decreasing on t of the inductive tree type above. *) +(* {dffun fT} == alias for {ffun fT} that inherits combinatorial *) +(* structures on rT, when rT DOES depend on x. *) +(* total_fun g == the function induced by a dependent function g of type *) +(* forall x, rT on the total space {x : aT & rT}. *) +(* := fun x => Tagged (fun x => rT) (g x). *) +(* tfgraph f == the total function graph of f, i.e., the #|aT|.-tuple *) +(* of all the (dependent pair) values of total_fun f. *) +(* finfun g == the f extensionally equal to g, and the RECOMMENDED *) +(* interface for building elements of {ffun fT}. *) +(* [ffun x : aT => E] := finfun (fun x : aT => E). *) +(* There should be an explicit type constraint on E if *) +(* type does not depend on x, due to the Coq unification *) +(* limitations referred to above. *) +(* ffun0 aT0 == the trivial finfun, from a proof aT0 that #|aT| = 0. *) (* f \in family F == f belongs to the family F (f x \in F x for all x) *) +(* There are addidional operations for non-dependent finite functions, *) +(* i.e., f in {ffun aT -> rT}. *) +(* [ffun x => E] := finfun (fun x => E). *) +(* The type of E must not depend on x; this restriction *) +(* is a mitigation of the aforementioned Coq unification *) +(* limitations. *) +(* [ffun=> E] := [ffun _ => E] (E should not have a dependent type). *) +(* fgraph f == the function graph of f, i.e., the #|aT|.-tuple *) +(* listing the values of f x, for x ranging over enum aT. *) +(* Finfun G == the finfun f whose (simple) function graph is G. *) +(* f \in ffun_on R == the range of f is a subset of R. *) (* y.-support f == the y-support of f, i.e., [pred x | f x != y]. *) (* Thus, y.-support f \subset D means f has y-support D. *) (* We will put Notation support := 0.-support in ssralg. *) @@ -36,128 +66,272 @@ Unset Printing Implicit Defensive. Section Def. -Variables (aT : finType) (rT : Type). +Variables (aT : finType) (rT : aT -> Type). + +Inductive finfun_on : seq aT -> Type := +| finfun_nil : finfun_on [::] +| finfun_cons x s of rT x & finfun_on s : finfun_on (x :: s). -Inductive finfun_type : predArgType := Finfun of #|aT|.-tuple rT. +Local Fixpoint finfun_rec (g : forall x, rT x) s : finfun_on s := + if s is x1 :: s1 then finfun_cons (g x1) (finfun_rec g s1) else finfun_nil. -Definition finfun_of of phant (aT -> rT) := finfun_type. +Local Fixpoint fun_of_fin_rec x s (f_s : finfun_on s) : x \in s -> rT x := + if f_s is finfun_cons x1 s1 y1 f_s1 then + if eqP is ReflectT Dx in reflect _ Dxb return Dxb || (x \in s1) -> rT x then + fun=> ecast x (rT x) (esym Dx) y1 + else fun_of_fin_rec f_s1 + else fun isF => False_rect (rT x) (notF isF). -Identity Coercion type_of_finfun : finfun_of >-> finfun_type. +Variant finfun_of (ph : phant (forall x, rT x)) : predArgType := + FinfunOf of finfun_on (enum aT). -Definition fgraph f := let: Finfun t := f in t. +Definition dfinfun_of ph := finfun_of ph. -Canonical finfun_subType := Eval hnf in [newType for fgraph]. +Definition fun_of_fin ph (f : finfun_of ph) x := + let: FinfunOf f_aT := f in fun_of_fin_rec f_aT (mem_enum aT x). End Def. +Coercion fun_of_fin : finfun_of >-> Funclass. +Identity Coercion unfold_dfinfun_of : dfinfun_of >-> finfun_of. +Arguments fun_of_fin {aT rT ph} f x. + Notation "{ 'ffun' fT }" := (finfun_of (Phant fT)) (at level 0, format "{ 'ffun' '[hv' fT ']' }") : type_scope. -Definition exp_finIndexType n := ordinal_finType n. -Notation "T ^ n" := (@finfun_of (exp_finIndexType n) T (Phant _)) : type_scope. -Local Notation fun_of_fin_def := - (fun aT rT f x => tnth (@fgraph aT rT f) (enum_rank x)). +Notation "{ 'dffun' fT }" := (dfinfun_of (Phant fT)) + (at level 0, format "{ 'dffun' '[hv' fT ']' }") : type_scope. -Local Notation finfun_def := (fun aT rT f => @Finfun aT rT (codom_tuple f)). +Definition exp_finIndexType := ordinal_finType. +Notation "T ^ n" := + (@finfun_of (exp_finIndexType n) (fun=> T) (Phant _)) : type_scope. -Module Type FunFinfunSig. -Parameter fun_of_fin : forall aT rT, finfun_type aT rT -> aT -> rT. -Parameter finfun : forall (aT : finType) rT, (aT -> rT) -> {ffun aT -> rT}. -Axiom fun_of_finE : fun_of_fin = fun_of_fin_def. +Local Notation finPi aT rT := (forall x : Finite.sort aT, rT x) (only parsing). +Local Notation finfun_def := + (fun aT rT g => FinfunOf (Phant (finPi aT rT)) (finfun_rec g (enum aT))). + +Module Type FinfunDefSig. +Parameter finfun : forall aT rT, finPi aT rT -> {ffun finPi aT rT}. Axiom finfunE : finfun = finfun_def. -End FunFinfunSig. +End FinfunDefSig. -Module FunFinfun : FunFinfunSig. -Definition fun_of_fin := fun_of_fin_def. +Module FinfunDef : FinfunDefSig. Definition finfun := finfun_def. -Lemma fun_of_finE : fun_of_fin = fun_of_fin_def. Proof. by []. Qed. Lemma finfunE : finfun = finfun_def. Proof. by []. Qed. -End FunFinfun. +End FinfunDef. + +Notation finfun := FinfunDef.finfun. +Canonical finfun_unlock := Unlockable FinfunDef.finfunE. +Arguments finfun {aT rT} g. + +Notation "[ 'ffun' x : aT => E ]" := (finfun (fun x : aT => E)) + (at level 0, x ident) : fun_scope. + +Notation "[ 'ffun' x => E ]" := (@finfun _ (fun=> _) (fun x => E)) + (at level 0, x ident, format "[ 'ffun' x => E ]") : fun_scope. + +Notation "[ 'ffun' => E ]" := [ffun _ => E] + (at level 0, format "[ 'ffun' => E ]") : fun_scope. + +(* Example outcommented. +(* Examples of using finite functions as containers in recursive inductive *) +(* types, and making use of the fact that the type and accessor are *) +(* structurally positive and decreasing, respectively. *) +Unset Elimination Schemes. +Inductive tree := node n of tree ^ n. +Fixpoint size t := let: node n f := t in sumn (codom (size \o f)) + 1. +Example tree_step (K : tree -> Type) := + forall n st (t := node st) & forall i : 'I_n, K (st i), K t. +Example tree_rect K (Kstep : tree_step K) : forall t, K t. +Proof. by fix IHt 1 => -[n st]; apply/Kstep=> i; apply: IHt. Defined. + +(* An artificial example use of dependent functions. *) +Inductive tri_tree n := tri_row of {ffun forall i : 'I_n, tri_tree i}. +Fixpoint tri_size n (t : tri_tree n) := + let: tri_row f := t in sumn [seq tri_size (f i) | i : 'I_n] + 1. +Example tri_tree_step (K : forall n, tri_tree n -> Type) := + forall n st (t := tri_row st) & forall i : 'I_n, K i (st i), K n t. +Example tri_tree_rect K (Kstep : tri_tree_step K) : forall n t, K n t. +Proof. by fix IHt 2 => n [st]; apply/Kstep=> i; apply: IHt. Defined. +Set Elimination Schemes. +(* End example. *) *) + +(* The correspondance between finfun_of and CiC dependent functions. *) +Section DepPlainTheory. +Variables (aT : finType) (rT : aT -> Type). +Notation fT := {ffun finPi aT rT}. +Implicit Type f : fT. + +Fact ffun0 (aT0 : #|aT| = 0) : fT. +Proof. by apply/finfun=> x; have:= card0_eq aT0 x. Qed. + +Lemma ffunE g x : (finfun g : fT) x = g x. +Proof. +rewrite unlock /=; set s := enum aT; set s_x : mem_seq s x := mem_enum _ _. +by elim: s s_x => //= x1 s IHs; case: eqP => [|_]; [case: x1 / | apply: IHs]. +Qed. + +Lemma ffunP (f1 f2 : fT) : (forall x, f1 x = f2 x) <-> f1 = f2. +Proof. +suffices ffunK f g: (forall x, f x = g x) -> f = finfun g. + by split=> [/ffunK|] -> //; apply/esym/ffunK. +case: f => f Dg; rewrite unlock; congr FinfunOf. +have{Dg} Dg x (aTx : mem_seq (enum aT) x): g x = fun_of_fin_rec f aTx. + by rewrite -Dg /= (bool_irrelevance (mem_enum _ _) aTx). +elim: (enum aT) / f (enum_uniq aT) => //= x1 s y f IHf /andP[s'x1 Us] in Dg *. +rewrite Dg ?eqxx //=; case: eqP => // /eq_axiomK-> /= _. +rewrite {}IHf // => x s_x; rewrite Dg ?s_x ?orbT //. +by case: eqP (memPn s'x1 x s_x) => // _ _ /(bool_irrelevance s_x) <-. +Qed. -Notation fun_of_fin := FunFinfun.fun_of_fin. -Notation finfun := FunFinfun.finfun. -Coercion fun_of_fin : finfun_type >-> Funclass. -Canonical fun_of_fin_unlock := Unlockable FunFinfun.fun_of_finE. -Canonical finfun_unlock := Unlockable FunFinfun.finfunE. +Lemma ffunK : @cancel (finPi aT rT) fT fun_of_fin finfun. +Proof. by move=> f; apply/ffunP=> x; rewrite ffunE. Qed. -Notation "[ 'ffun' x : aT => F ]" := (finfun (fun x : aT => F)) - (at level 0, x ident, only parsing) : fun_scope. +Lemma eq_dffun (g1 g2 : forall x, rT x) : + (forall x, g1 x = g2 x) -> finfun g1 = finfun g2. +Proof. by move=> eq_g; apply/ffunP => x; rewrite !ffunE eq_g. Qed. -Notation "[ 'ffun' : aT => F ]" := (finfun (fun _ : aT => F)) - (at level 0, only parsing) : fun_scope. +Definition total_fun g x := Tagged rT (g x : rT x). -Notation "[ 'ffun' x => F ]" := [ffun x : _ => F] - (at level 0, x ident, format "[ 'ffun' x => F ]") : fun_scope. +Definition tfgraph f := codom_tuple (total_fun f). + +Lemma codom_tffun f : codom (total_fun f) = tfgraph f. Proof. by []. Qed. + +Local Definition tfgraph_inv (G : #|aT|.-tuple {x : aT & rT x}) : option fT := + if eqfunP isn't ReflectT Dtg then None else + Some [ffun x => ecast x (rT x) (Dtg x) (tagged (tnth G (enum_rank x)))]. + +Local Lemma tfgraphK : pcancel tfgraph tfgraph_inv. +Proof. +move=> f; have Dg x: tnth (tfgraph f) (enum_rank x) = total_fun f x. + by rewrite tnth_map -[tnth _ _]enum_val_nth enum_rankK. +rewrite /tfgraph_inv; case: eqfunP => /= [Dtg | [] x]; last by rewrite Dg. +congr (Some _); apply/ffunP=> x; rewrite ffunE. +by rewrite Dg in (Dx := Dtg x) *; rewrite eq_axiomK. +Qed. + +Lemma tfgraph_inj : injective tfgraph. Proof. exact: pcan_inj tfgraphK. Qed. + +Definition family_mem mF := [pred f : fT | [forall x, in_mem (f x) (mF x)]]. -Notation "[ 'ffun' => F ]" := [ffun : _ => F] - (at level 0, format "[ 'ffun' => F ]") : fun_scope. +Variables (pT : forall x, predType (rT x)) (F : forall x, pT x). (* Helper for defining notation for function families. *) -Definition fmem aT rT (pT : predType rT) (f : aT -> pT) := [fun x => mem (f x)]. +Local Definition fmem F x := mem (F x : pT x). -(* Lemmas on the correspondance between finfun_type and CiC functions. *) -Section PlainTheory. +Lemma familyP f : reflect (forall x, f x \in F x) (f \in family_mem (fmem F)). +Proof. exact: forallP. Qed. + +End DepPlainTheory. + +Arguments ffunK {aT rT} f : rename. +Arguments ffun0 {aT rT} aT0. +Arguments eq_dffun {aT rT} [g1] g2 eq_g12. +Arguments total_fun {aT rT} g x. +Arguments tfgraph {aT rT} f. +Arguments tfgraphK {aT rT} f : rename. +Arguments tfgraph_inj {aT rT} [f1 f2] : rename. + +Arguments fmem {aT rT pT} F x /. +Arguments familyP {aT rT pT F f}. +Notation family F := (family_mem (fmem F)). + +Section InheritedStructures. + +Variable aT : finType. +Notation dffun_aT rT rS := {dffun forall x : aT, rT x : rS}. + +Local Remark eqMixin rT : Equality.mixin_of (dffun_aT rT eqType). +Proof. exact: PcanEqMixin tfgraphK. Qed. +Canonical finfun_eqType (rT : eqType) := + EqType {ffun aT -> rT} (eqMixin (fun=> rT)). +Canonical dfinfun_eqType rT := + EqType (dffun_aT rT eqType) (eqMixin rT). + +Local Remark choiceMixin rT : Choice.mixin_of (dffun_aT rT choiceType). +Proof. exact: PcanChoiceMixin tfgraphK. Qed. +Canonical finfun_choiceType (rT : choiceType) := + ChoiceType {ffun aT -> rT} (choiceMixin (fun=> rT)). +Canonical dfinfun_choiceType rT := + ChoiceType (dffun_aT rT choiceType) (choiceMixin rT). + +Local Remark countMixin rT : Countable.mixin_of (dffun_aT rT countType). +Proof. exact: PcanCountMixin tfgraphK. Qed. +Canonical finfun_countType (rT : countType) := + CountType {ffun aT -> rT} (countMixin (fun => rT)). +Canonical dfinfun_countType rT := + CountType (dffun_aT rT countType) (countMixin rT). + +Local Definition finMixin rT := + PcanFinMixin (tfgraphK : @pcancel _ (dffun_aT rT finType) _ _). +Canonical finfun_finType (rT : finType) := + FinType {ffun aT -> rT} (finMixin (fun=> rT)). +Canonical dfinfun_finType rT := + FinType (dffun_aT rT finType) (finMixin rT). + +End InheritedStructures. + +Section FunPlainTheory. Variables (aT : finType) (rT : Type). Notation fT := {ffun aT -> rT}. Implicit Types (f : fT) (R : pred rT). -Canonical finfun_of_subType := Eval hnf in [subType of fT]. +Definition fgraph f := codom_tuple f. + +Definition Finfun (G : #|aT|.-tuple rT) := [ffun x => tnth G (enum_rank x)]. Lemma tnth_fgraph f i : tnth (fgraph f) i = f (enum_val i). -Proof. by rewrite [@fun_of_fin]unlock enum_valK. Qed. +Proof. by rewrite tnth_map /tnth -enum_val_nth. Qed. -Lemma ffunE (g : aT -> rT) : finfun g =1 g. +Lemma FinfunK : cancel Finfun fgraph. Proof. -move=> x; rewrite [@finfun]unlock unlock tnth_map. -by rewrite -[tnth _ _]enum_val_nth enum_rankK. +by move=> G; apply/eq_from_tnth=> i; rewrite tnth_fgraph ffunE enum_valK. Qed. -Lemma fgraph_codom f : fgraph f = codom_tuple f. -Proof. -apply: eq_from_tnth => i; rewrite [@fun_of_fin]unlock tnth_map. -by congr tnth; rewrite -[tnth _ _]enum_val_nth enum_valK. -Qed. +Lemma fgraphK : cancel fgraph Finfun. +Proof. by move=> f; apply/ffunP=> x; rewrite ffunE tnth_fgraph enum_rankK. Qed. -Lemma codom_ffun f : codom f = val f. -Proof. by rewrite /= fgraph_codom. Qed. +Lemma fgraph_ffun0 aT0 : fgraph (ffun0 aT0) = nil :> seq rT. +Proof. by apply/nilP/eqP; rewrite size_tuple. Qed. -Lemma ffunP f1 f2 : f1 =1 f2 <-> f1 = f2. -Proof. -split=> [eq_f12 | -> //]; do 2!apply: val_inj => /=. -by rewrite !fgraph_codom /= (eq_codom eq_f12). -Qed. +Lemma codom_ffun f : codom f = fgraph f. Proof. by []. Qed. -Lemma ffunK : cancel (@fun_of_fin aT rT) (@finfun aT rT). -Proof. by move=> f; apply/ffunP/ffunE. Qed. +Lemma tagged_tfgraph f : @map _ rT tagged (tfgraph f) = fgraph f. +Proof. by rewrite -map_comp. Qed. -Definition family_mem mF := [pred f : fT | [forall x, in_mem (f x) (mF x)]]. +Lemma eq_ffun (g1 g2 : aT -> rT) : g1 =1 g2 -> finfun g1 = finfun g2. +Proof. exact: eq_dffun. Qed. -Lemma familyP (pT : predType rT) (F : aT -> pT) f : - reflect (forall x, f x \in F x) (f \in family_mem (fmem F)). -Proof. exact: forallP. Qed. +Lemma fgraph_codom f : fgraph f = codom_tuple f. +Proof. exact/esym/val_inj/codom_ffun. Qed. -Definition ffun_on_mem mR := family_mem (fun _ => mR). +Definition ffun_on_mem (mR : mem_pred rT) := family_mem (fun _ : aT => mR). Lemma ffun_onP R f : reflect (forall x, f x \in R) (f \in ffun_on_mem (mem R)). Proof. exact: forallP. Qed. -End PlainTheory. - -Notation family F := (family_mem (fun_of_simpl (fmem F))). -Notation ffun_on R := (ffun_on_mem _ (mem R)). +End FunPlainTheory. -Arguments ffunK {aT rT}. -Arguments familyP {aT rT pT F f}. +Arguments Finfun {aT rT} G. +Arguments fgraph {aT rT} f. +Arguments FinfunK {aT rT} G : rename. +Arguments fgraphK {aT rT} f : rename. +Arguments eq_ffun {aT rT} [g1] g2 eq_g12. Arguments ffun_onP {aT rT R f}. -(*****************************************************************************) +Notation ffun_on R := (ffun_on_mem _ (mem R)). +Notation "@ 'ffun_on' aT R" := + (ffun_on R : simpl_pred (finfun_of (Phant (aT -> id _)))) + (at level 10, aT, R at level 9). Lemma nth_fgraph_ord T n (x0 : T) (i : 'I_n) f : nth x0 (fgraph f) i = f i. Proof. -by rewrite -{2}(enum_rankK i) -tnth_fgraph (tnth_nth x0) enum_rank_ord. +by rewrite -[i in RHS]enum_rankK -tnth_fgraph (tnth_nth x0) enum_rank_ord. Qed. +(*****************************************************************************) + Section Support. Variables (aT : Type) (rT : eqType). @@ -183,11 +357,6 @@ Proof. by apply: (iffP subsetP) => Dg x; [apply: contraNeq | apply: contraR] => /Dg->. Qed. -Definition finfun_eqMixin := - Eval hnf in [eqMixin of finfun_type aT rT by <:]. -Canonical finfun_eqType := Eval hnf in EqType _ finfun_eqMixin. -Canonical finfun_of_eqType := Eval hnf in [eqType of fT]. - Definition pfamily_mem y mD (mF : aT -> mem_pred rT) := family (fun i : aT => if in_mem i mD then pred_of_simpl (mF i) else pred1 y). @@ -215,73 +384,70 @@ Qed. End EqTheory. Arguments supportP {aT rT y D g}. -Notation pfamily y D F := (pfamily_mem y (mem D) (fun_of_simpl (fmem F))). -Notation pffun_on y D R := (pffun_on_mem y (mem D) (mem R)). +Arguments pfamilyP {aT rT pT y D F f}. +Arguments pffun_onP {aT rT y D R f}. -Definition finfun_choiceMixin aT (rT : choiceType) := - [choiceMixin of finfun_type aT rT by <:]. -Canonical finfun_choiceType aT rT := - Eval hnf in ChoiceType _ (finfun_choiceMixin aT rT). -Canonical finfun_of_choiceType (aT : finType) (rT : choiceType) := - Eval hnf in [choiceType of {ffun aT -> rT}]. - -Definition finfun_countMixin aT (rT : countType) := - [countMixin of finfun_type aT rT by <:]. -Canonical finfun_countType aT (rT : countType) := - Eval hnf in CountType _ (finfun_countMixin aT rT). -Canonical finfun_of_countType (aT : finType) (rT : countType) := - Eval hnf in [countType of {ffun aT -> rT}]. -Canonical finfun_subCountType aT (rT : countType) := - Eval hnf in [subCountType of finfun_type aT rT]. -Canonical finfun_of_subCountType (aT : finType) (rT : countType) := - Eval hnf in [subCountType of {ffun aT -> rT}]. +Notation pfamily y D F := (pfamily_mem y (mem D) (fmem F)). +Notation pffun_on y D R := (pffun_on_mem y (mem D) (mem R)). (*****************************************************************************) -Section FinTheory. +Section FinDepTheory. -Variables aT rT : finType. -Notation fT := {ffun aT -> rT}. -Notation ffT := (finfun_type aT rT). -Implicit Types (D : pred aT) (R : pred rT) (F : aT -> pred rT). - -Definition finfun_finMixin := [finMixin of ffT by <:]. -Canonical finfun_finType := Eval hnf in FinType ffT finfun_finMixin. -Canonical finfun_subFinType := Eval hnf in [subFinType of ffT]. -Canonical finfun_of_finType := Eval hnf in [finType of fT for finfun_finType]. -Canonical finfun_of_subFinType := Eval hnf in [subFinType of fT]. +Variables (aT : finType) (rT : aT -> finType). +Notation fT := {dffun forall x : aT, rT x}. -Lemma card_pfamily y0 D F : - #|pfamily y0 D F| = foldr muln 1 [seq #|F x| | x in D]. +Lemma card_family (F : forall x, pred (rT x)) : + #|(family F : simpl_pred fT)| = foldr muln 1 [seq #|F x| | x : aT]. Proof. -rewrite /image_mem; transitivity #|pfamily y0 (enum D) F|. - by apply/eq_card=> f; apply/eq_forallb=> x /=; rewrite mem_enum. -elim: {D}(enum D) (enum_uniq D) => /= [_|x0 s IHs /andP[s'x0 /IHs<-{IHs}]]. - apply: eq_card1 [ffun=> y0] _ _ => f. - apply/familyP/eqP=> [y0_f|-> x]; last by rewrite ffunE inE. - by apply/ffunP=> x; rewrite ffunE (eqP (y0_f x)). -pose g (xf : rT * fT) := finfun [eta xf.2 with x0 |-> xf.1]. +rewrite /image_mem; set E := enum aT in (uniqE := enum_uniq aT) *. +have trivF x: x \notin E -> #|F x| = 1 by rewrite mem_enum. +elim: E uniqE => /= [_ | x0 E IH_E /andP[E'x0 uniqE]] in F trivF *. + have /fin_all_exists[f0 Ff0] x: exists y0, F x =i pred1 y0. + have /pred0Pn[y Fy]: #|F x| != 0 by rewrite trivF. + by exists y; apply/fsym/subset_cardP; rewrite ?subset_pred1 // card1 trivF. + apply: eq_card1 (finfun f0 : fT) _ _ => f; apply/familyP/eqP=> [Ff | {f}-> x]. + by apply/ffunP=> x; have:= Ff x; rewrite Ff0 ffunE => /eqP. + by rewrite ffunE Ff0 inE /=. +have [y0 Fxy0 | Fx00] := pickP (F x0); last first. + by rewrite !eq_card0 // => f; apply: contraFF (Fx00 (f x0))=> /familyP; apply. +pose F1 x := if eqP is ReflectT Dx then xpred1 (ecast x (rT x) Dx y0) else F x. +transitivity (#|[predX F x0 & family F1 : pred fT]|); last first. + rewrite cardX {}IH_E {uniqE}// => [|x E'x]; last first. + rewrite /F1; case: eqP => [Dx | /nesym/eqP-x0'x]; first exact: card1. + by rewrite trivF // negb_or x0'x. + congr (_ * foldr _ _ _); apply/eq_in_map=> x Ex. + by rewrite /F1; case: eqP => // Dx0; rewrite Dx0 Ex in E'x0. +pose g yf : fT := let: (y, f) := yf : rT x0 * fT in + [ffun x => if eqP is ReflectT Dx then ecast x (rT x) Dx y else f x]. have gK: cancel (fun f : fT => (f x0, g (y0, f))) g. - by move=> f; apply/ffunP=> x; do !rewrite ffunE /=; case: eqP => // ->. -rewrite -cardX -(card_image (can_inj gK)); apply: eq_card => [] [y f] /=. -apply/imageP/andP=> [[f0 /familyP/=Ff0] [{f}-> ->]| [Fy /familyP/=Ff]]. - split; first by have:= Ff0 x0; rewrite /= mem_head. - apply/familyP=> x; have:= Ff0 x; rewrite ffunE inE /=. - by case: eqP => //= -> _; rewrite ifN ?inE. + by move=> f; apply/ffunP=> x; rewrite !ffunE; case: eqP => //; case: x /. +rewrite -(card_image (can_inj gK)); apply: eq_card => [] [y f] /=. +apply/imageP/andP=> [[f1 /familyP/=Ff1] [-> ->]| [/=Fx0y /familyP/=Ff]]. + split=> //; apply/familyP=> x; rewrite ffunE /F1 /=. + by case: eqP => // Dx; apply: eqxx. exists (g (y, f)). - by apply/familyP=> x; have:= Ff x; rewrite ffunE /= inE; case: eqP => // ->. -congr (_, _); last apply/ffunP=> x; do !rewrite ffunE /= ?eqxx //. -by case: eqP => // ->{x}; apply/eqP; have:= Ff x0; rewrite ifN. + by apply/familyP=> x; have:= Ff x; rewrite ffunE /F1; case: eqP; [case: x /|]. +congr (_, _); first by rewrite /= ffunE; case: eqP => // Dx; rewrite eq_axiomK. +by apply/ffunP=> x; have:= Ff x; rewrite !ffunE /F1; case: eqP => // Dx /eqP. Qed. -Lemma card_family F : #|family F| = foldr muln 1 [seq #|F x| | x : aT]. +Lemma card_dep_ffun : #|fT| = foldr muln 1 [seq #|rT x| | x : aT]. +Proof. by rewrite -card_family; apply/esym/eq_card=> f; apply/familyP. Qed. + +End FinDepTheory. + +Section FinFunTheory. + +Variables aT rT : finType. +Notation fT := {ffun aT -> rT}. +Implicit Types (D : pred aT) (R : pred rT) (F : aT -> pred rT). + +Lemma card_pfamily y0 D F : + #|pfamily y0 D F| = foldr muln 1 [seq #|F x| | x in D]. Proof. -have [y0 _ | rT0] := pickP rT; first exact: (card_pfamily y0 aT). -rewrite /image_mem; case DaT: (enum aT) => [{rT0}|x0 e] /=; last first. - by rewrite !eq_card0 // => [f | y]; [have:= rT0 (f x0) | have:= rT0 y]. -have{DaT} no_aT P (x : aT) : P by have:= mem_enum aT x; rewrite DaT. -apply: eq_card1 [ffun x => no_aT rT x] _ _ => f. -by apply/familyP/eqP=> _; [apply/ffunP | ] => x; apply: no_aT. +rewrite card_family !/(image _ _) /(enum D) -enumT /=. +by elim: (enum aT) => //= x E ->; have [// | D'x] := ifP; rewrite card1 mul1n. Qed. Lemma card_pffun_on y0 D R : #|pffun_on y0 D R| = #|R| ^ #|D|. @@ -290,7 +456,7 @@ rewrite (cardE D) card_pfamily /image_mem. by elim: (enum D) => //= _ e ->; rewrite expnS. Qed. -Lemma card_ffun_on R : #|ffun_on R| = #|R| ^ #|aT|. +Lemma card_ffun_on R : #|@ffun_on aT R| = #|R| ^ #|aT|. Proof. rewrite card_family /image_mem cardT. by elim: (enum aT) => //= _ e ->; rewrite expnS. @@ -299,5 +465,4 @@ Qed. Lemma card_ffun : #|fT| = #|rT| ^ #|aT|. Proof. by rewrite -card_ffun_on; apply/esym/eq_card=> f; apply/forallP. Qed. -End FinTheory. - +End FinFunTheory. diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index 5358dc7..1a0f25f 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -14,7 +14,7 @@ Require Import ssrbool ssrfun eqtype ssrnat seq path fintype. (* dfs g n v x == the list of points traversed by a depth-first search of *) (* the g, at depth n, starting from x, and avoiding v. *) (* dfs_path g v x y <-> there is a path from x to y in g \ v. *) -(* connect e == the transitive closure of e (computed by dfs). *) +(* connect e == the reflexive transitive closure of e (computed by dfs). *) (* connect_sym e <-> connect e is symmetric, hence an equivalence relation. *) (* root e x == a representative of connect e x, which is the component *) (* of x in the transitive closure of e. *) diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 87d5da4..72bfe74 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -239,11 +239,15 @@ Proof. by rewrite in_set. Qed. Lemma eqsVneq A B : {A = B} + {A != B}. Proof. exact: eqVneq. Qed. +Lemma eq_finset (pA pB : pred T) : pA =1 pB -> finset pA = finset pB. +Proof. by move=> eq_p; apply/setP => x; rewrite !(in_set, inE) eq_p. Qed. + End BasicSetTheory. Definition inE := (in_set, inE). Arguments set0 {T}. +Arguments eq_finset {T} [pA] pB eq_pAB. Hint Resolve in_setT : core. Notation "[ 'set' : T ]" := (setTfor (Phant T)) @@ -717,7 +721,7 @@ Proof. exact/eq_card/in_set. Qed. Lemma sum1dep_card pA : \sum_(x | pA x) 1 = #|[set x | pA x]|. Proof. by rewrite sum1_card cardsE. Qed. -Lemma sum_nat_dep_const pA n : \sum_(x | pA x) n = #|[set x | pA x]| * n. +Lemma sum_nat_cond_const pA n : \sum_(x | pA x) n = #|[set x | pA x]| * n. Proof. by rewrite sum_nat_const cardsE. Qed. Lemma cards0 : #|@set0 T| = 0. @@ -1380,24 +1384,21 @@ Proof. by apply: big_pred0 => i; rewrite inE. Qed. Lemma big_set1 a F : \big[op/idx]_(i in [set a]) F i = F a. Proof. by apply: big_pred1 => i; rewrite !inE. Qed. -Lemma big_setIDdep A B P F : - \big[aop/idx]_(i in A | P i) F i = - aop (\big[aop/idx]_(i in A :&: B | P i) F i) - (\big[aop/idx]_(i in A :\: B | P i) F i). -Proof. -rewrite (bigID (mem B)) setDE. -by congr (aop _ _); apply: eq_bigl => i; rewrite !inE andbAC. -Qed. - Lemma big_setID A B F : \big[aop/idx]_(i in A) F i = aop (\big[aop/idx]_(i in A :&: B) F i) (\big[aop/idx]_(i in A :\: B) F i). Proof. -rewrite (bigID (mem B)) !(eq_bigl _ _ (in_set _)) //=. -by congr (aop _); apply: eq_bigl => i; rewrite andbC. +rewrite (bigID (mem B)) setDE. +by congr (aop _ _); apply: eq_bigl => i; rewrite !inE. Qed. +Lemma big_setIDcond A B P F : + \big[aop/idx]_(i in A | P i) F i = + aop (\big[aop/idx]_(i in A :&: B | P i) F i) + (\big[aop/idx]_(i in A :\: B | P i) F i). +Proof. by rewrite !big_mkcondr; apply: big_setID. Qed. + Lemma big_setD1 a A F : a \in A -> \big[aop/idx]_(i in A) F i = aop (F a) (\big[aop/idx]_(i in A :\ a) F i). Proof. @@ -1409,8 +1410,7 @@ Lemma big_setU1 a A F : a \notin A -> \big[aop/idx]_(i in a |: A) F i = aop (F a) (\big[aop/idx]_(i in A) F i). Proof. by move=> notAa; rewrite (@big_setD1 a) ?setU11 //= setU1K. Qed. -Lemma big_imset h (A : pred I) G : - {in A &, injective h} -> +Lemma big_imset h (A : pred I) G : {in A &, injective h} -> \big[aop/idx]_(j in h @: A) G j = \big[aop/idx]_(i in A) G (h i). Proof. move=> injh; pose hA := mem (image h A). @@ -1427,6 +1427,11 @@ symmetry; rewrite (negbTE nhAhi); apply/idP=> Ai. by case/imageP: nhAhi; exists i. Qed. +Lemma big_imset_cond h (A : pred I) (P : pred J) G : {in A &, injective h} -> + \big[aop/idx]_(j in h @: A | P j) G j = + \big[aop/idx]_(i in A | P (h i)) G (h i). +Proof. by move=> h_inj; rewrite 2!big_mkcondr big_imset. Qed. + Lemma partition_big_imset h (A : pred I) F : \big[aop/idx]_(i in A) F i = \big[aop/idx]_(j in h @: A) \big[aop/idx]_(i in A | h i == j) F i. @@ -2210,4 +2215,3 @@ Arguments setCK {T}. Arguments minsetP {T P A}. Arguments maxsetP {T P A}. Prenex Implicits minset maxset. - diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index f503613..afc571a 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -106,11 +106,19 @@ Require Import ssrfun ssrbool eqtype ssrnat. (* rev s == the (linear time) reversal of s. *) (* catrev s1 s2 == the reversal of s1 followed by s2 (this is the *) (* recursive form of rev). *) +(* ** Dependent iterator: for s : seq S and t : S -> seq T *) +(* [seq E | x <- s, y <- t] := flatten [seq [seq E | x <- t] | y <- s] *) +(* == the sequence of all the f x y, with x and y drawn from *) +(* s and t, respectively, in row-major order, *) +(* and where t is possibly dependent in elements of s *) +(* allpairs_dep f s t := self expanding definition for *) +(* [seq f x y | x <- s, y <- t i] *) (* ** Iterators: for s == [:: x_1, ..., x_n], t == [:: y_1, ..., y_m], *) -(* map f s == the sequence [:: f x_1, ..., f x_n]. *) -(* allpairs f s t == the sequence of all the f x y, with x and y drawn from *) -(* s and t, respectively, in row-major order. *) +(* allpairs f s t := same as allpairs_dep but where t is non dependent, *) +(* 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] *) +(* 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 *) (* {i1, ..., ik}. *) @@ -144,7 +152,6 @@ Require Import ssrfun ssrbool eqtype ssrnat. (* ** Notation for manifest comprehensions: *) (* [seq x <- s | C] := filter (fun x => C) s. *) (* [seq E | x <- s] := map (fun x => E) s. *) -(* [seq E | x <- s, y <- t] := allpairs (fun x y => E) s t. *) (* [seq x <- s | C1 & C2] := [seq x <- s | C1 && C2]. *) (* [seq E | x <- s & C] := [seq E | x <- [seq x | C]]. *) (* --> The above allow optional type casts on the eigenvariables, as in *) @@ -1926,6 +1933,9 @@ Qed. Lemma mem_rem_uniq s : uniq s -> rem s =i [predD1 s & x]. 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. + End Rem. Section Map. @@ -2733,31 +2743,106 @@ rewrite /N /= count_cat -/(N x _) Nx0 ?mem_rem_uniq ?undup_uniq ?inE ?eqxx //. by rewrite addn0 -{2}(size_nseq (_ s) x) -all_count all_pred1_nseq. Qed. -Section AllPairs. +Notation "[ 'seq' E | x <- s , y <- t ]" := + (flatten [seq [seq E | y <- t] | x <- s]) + (at level 0, E at level 99, x ident, y ident, + format "[ '[hv' 'seq' E '/ ' | x <- s , '/ ' y <- t ] ']'") + : seq_scope. +Notation "[ 'seq' E | x : S <- s , y : T <- t ]" := + (flatten [seq [seq E | y : T <- t] | x : S <- s]) + (at level 0, E at level 99, x ident, y ident, only parsing) : seq_scope. + +Section AllPairsDep. + +Variables (S : Type) (T : S -> Type) (R : Type) (f : forall x, T x -> R). +Implicit Types (s : seq S) (t : forall x, seq (T x)). + +Definition allpairs_dep s t := [seq f y | x <- s, y <- t x]. + +Lemma size_allpairs_dep s t : + size [seq f 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 allpairs_cat s1 s2 t : + [seq f y | x <- s1 ++ s2, y <- t x] = + [seq f y | x <- s1, y <- t x] ++ [seq f y | x <- s2, y <- t x]. +Proof. by rewrite map_cat flatten_cat. Qed. + +Lemma allpairs_comp R' (g : R -> R') s t : + [seq g (f y) | x <- s, y <- t x] = + [seq g r | r <- [seq f y | x <- s, y <- t x]]. +Proof. by elim: s => //= x s ->; rewrite map_cat map_comp. Qed. + +End AllPairsDep. + +Arguments allpairs_dep {S T R} f s t /. + +Section AllPairsNonDep. Variables (S T R : Type) (f : S -> T -> R). Implicit Types (s : seq S) (t : seq T). -Definition allpairs s t := foldr (fun x => cat (map (f x) t)) [::] s. +Definition allpairs s t := [seq f x y | x <- s, y <- t]. -Lemma size_allpairs s t : size (allpairs s t) = size s * size t. +Lemma size_allpairs s t : size [seq f x y | x <- s, y <- t] = size s * size t. Proof. by elim: s => //= x s IHs; rewrite size_cat size_map IHs. Qed. -Lemma allpairs_cat s1 s2 t : - allpairs (s1 ++ s2) t = allpairs s1 t ++ allpairs s2 t. -Proof. by elim: s1 => //= x s1 ->; rewrite catA. Qed. +End AllPairsNonDep. -End AllPairs. +Arguments allpairs {S T R} f s t /. -Prenex Implicits allpairs. +Section EqAllPairsDep. -Notation "[ 'seq' E | i <- s , j <- t ]" := (allpairs (fun i j => E) s t) - (at level 0, E at level 99, i ident, j ident, - format "[ '[hv' 'seq' E '/ ' | i <- s , '/ ' j <- t ] ']'") - : seq_scope. -Notation "[ 'seq' E | i : T <- s , j : U <- t ]" := - (allpairs (fun (i : T) (j : U) => E) s t) - (at level 0, E at level 99, i ident, j ident, only parsing) : seq_scope. +Variables (S : eqType) (T : S -> eqType). +Implicit Types (R : eqType) (s : seq S) (t : forall x, seq (T x)). + +Lemma allpairsPdep R f s t (z : R) : + reflect (exists x y, [/\ x \in s, y \in t x & z = f x y]) + (z \in [seq f x y | x <- s, y <- t x]). +Proof. +apply: (iffP flatten_mapP); first by case=> x ? /mapP[y ? ->]; exists x, y. +by move=> [x [y [xs yt ->]]]; exists x => //; apply: map_f. +Qed. + +Lemma allpairs_f_dep R (f : forall x, T x -> R) s t x y : + x \in s -> y \in t x -> f x y \in [seq f x y | x <- s, y <- t x]. +Proof. by move=> xs yt; apply/allpairsPdep; exists x, y. Qed. + +Lemma mem_allpairs_dep R (f : forall x, T x -> R) s1 t1 s2 t2 : + s1 =i s2 -> (forall x, x \in s1 -> t1 x =i t2 x) -> + [seq f x y | x <- s1, y <- t1 x] =i [seq f x y | x <- s2, y <- t2 x]. +Proof. +move=> eq_s eq_t z; apply/allpairsPdep/allpairsPdep=> -[x [y [xs ys ->]]]; +by exists x, y; rewrite ?eq_s ?eq_t// -?eq_s -?eq_t// eq_s. +Qed. + +Lemma allpairs_catr R (f : forall x, T x -> R) 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]. +Proof. +move=> r; rewrite mem_cat; apply/allpairsPdep/orP=> [[x [y [xs]]]|]. + by rewrite mem_cat; case/orP; [left|right]; apply/allpairsPdep; exists x, y. +by case=>/allpairsPdep[x [y [? yt ->]]]; exists x, y; rewrite mem_cat yt ?orbT. +Qed. + +Lemma allpairs_uniq_dep R (f : forall x, T x -> R) s t + (g := fun p : {x : S & T x} => f _ (tagged p)) : + uniq s -> (forall x, x \in s -> uniq (t x)) -> + {in [seq Tagged T y | x <- s, y <- t x] &, injective g} -> + uniq [seq f x y | x <- s, y <- t x]. +Proof. +move=> Us Ut gI; have s_s : all (mem s) s by apply/allP. +rewrite (allpairs_comp (fun=> Tagged T) g) map_inj_in_uniq// {f g gI R}. +elim: {-1}s s_s Us => //= x s1 IHs /andP[xs s_s1] /andP[xNs1 Us1]. +rewrite cat_uniq {}IHs // andbT map_inj_in_uniq ?Ut //; last first. + by move=> y1 y2 _ _ /eqP; rewrite eq_Tagged /= => /eqP. +apply/hasPn=> _ /allpairsPdep[x1 [y1 [xs1 ys2 ->]]]. +by apply/mapP=> [[y ty [x1_eq _]]]; move: xs1 xNs1; rewrite x1_eq => ->. +Qed. + +End EqAllPairsDep. + +Arguments allpairsPdep {S T R f s t z}. Section EqAllPairs. @@ -2766,50 +2851,32 @@ Implicit Types (R : eqType) (s : seq S) (t : seq T). Lemma allpairsP R (f : S -> T -> R) s t z : reflect (exists p, [/\ p.1 \in s, p.2 \in t & z = f p.1 p.2]) - (z \in allpairs f s t). + (z \in [seq f x y | x <- s, y <- t]). Proof. -elim: s => [|x s IHs /=]; first by right=> [[p []]]. -rewrite mem_cat; have [fxt_z | not_fxt_z] := altP mapP. - by left; have [y t_y ->] := fxt_z; exists (x, y); rewrite mem_head. -apply: (iffP IHs) => [] [[x' y] /= [s_x' t_y def_z]]; exists (x', y). - by rewrite !inE predU1r. -by have [def_x' | //] := predU1P s_x'; rewrite def_z def_x' map_f in not_fxt_z. +by apply: (iffP allpairsPdep) => [[x[y]]|[[x y]]]; [exists (x, y)|exists x, y]. Qed. -Lemma mem_allpairs R (f : S -> T -> R) s1 t1 s2 t2 : - s1 =i s2 -> t1 =i t2 -> allpairs f s1 t1 =i allpairs f s2 t2. -Proof. -move=> eq_s eq_t z. -by apply/allpairsP/allpairsP=> [] [p fpz]; exists p; rewrite eq_s eq_t in fpz *. -Qed. +Lemma allpairs_f R (f : S -> T -> R) s t x y : + x \in s -> y \in t -> f x y \in [seq f x y | x <- s, y <- t]. +Proof. exact: allpairs_f_dep. Qed. -Lemma allpairs_catr R (f : S -> T -> R) s t1 t2 : - allpairs f s (t1 ++ t2) =i allpairs f s t1 ++ allpairs f s t2. -Proof. -move=> z; rewrite mem_cat. -apply/allpairsP/orP=> [[p [sP1]]|]. - by rewrite mem_cat; case/orP; [left | right]; apply/allpairsP; exists p. -by case=> /allpairsP[p [sp1 sp2 ->]]; exists p; rewrite mem_cat sp2 ?orbT. -Qed. +Lemma mem_allpairs R (f : S -> T -> R) s1 t1 s2 t2 : s1 =i s2 -> t1 =i t2 -> + [seq f x y | x <- s1, y <- t1] =i [seq f x y | x <- s2, y <- t2]. +Proof. by move=> *; apply: mem_allpairs_dep. Qed. -Lemma allpairs_uniq R (f : S -> T -> R) s t : - uniq s -> uniq t -> +Lemma allpairs_uniq R (f : S -> T -> R) s t : uniq s -> uniq t -> {in [seq (x, y) | x <- s, y <- t] &, injective (prod_curry f)} -> - uniq (allpairs f s t). + uniq [seq f x y | x <- s, y <- t]. Proof. -move=> Us Ut inj_f; have: all (mem s) s by apply/allP. -elim: {-2}s Us => //= x s1 IHs /andP[s1'x Us1] /andP[sx1 ss1]. -rewrite cat_uniq {}IHs // andbT map_inj_in_uniq ?Ut // => [|y1 y2 *]. - apply/hasPn=> _ /allpairsP[z [s1z tz ->]]; apply/mapP=> [[y ty Dy]]. - suffices [Dz1 _]: (z.1, z.2) = (x, y) by rewrite -Dz1 s1z in s1'x. - apply: inj_f => //; apply/allpairsP; last by exists (x, y). - by have:= allP ss1 _ s1z; exists z. -suffices: (x, y1) = (x, y2) by case. -by apply: inj_f => //; apply/allpairsP; [exists (x, y1) | exists (x, y2)]. +move=> Us Ut inj_f; apply: allpairs_uniq_dep => //. +move=> _ _ /allpairsPdep[x [y [xs yt ->]]] /allpairsPdep[u [v [us vt ->]]]/=. +by move=> /(inj_f (_, _) (_, _)); rewrite !allpairs_f// => /(_ isT isT)[->->]. Qed. End EqAllPairs. +Arguments allpairsP {S T R f s t z}. + Section AllIff. (* The Following Are Equivalent *) diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index 8f81155..c0ba403 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -411,10 +411,14 @@ Proof. by rewrite -tnth_nth tnth_mktuple. Qed. End MkTuple. +Lemma eq_mktuple T' (f1 f2 : 'I_n -> T') : + f1 =1 f2 -> mktuple f1 = mktuple f2. +Proof. by move=> eq_f; apply eq_from_tnth=> i; rewrite !tnth_map eq_f. Qed. + End UseFinTuple. Notation "[ 'tuple' F | i < n ]" := (mktuple (fun i : 'I_n => F)) (at level 0, i at level 0, format "[ '[hv' 'tuple' F '/' | i < n ] ']'") : form_scope. - +Arguments eq_mktuple {n T'} [f1] f2 eq_f12. |