diff options
| author | Cyril Cohen | 2019-03-20 18:22:20 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2019-03-26 19:46:39 +0100 |
| commit | d6dbcfe8edacdf00df988843ed6b74ecfc2db744 (patch) | |
| tree | 52a40f6b29014664561f0aadad8ebd42cb20264c /mathcomp/ssreflect/bigop.v | |
| parent | 5c5455be722fe60634f511c876e05e3201091e25 (diff) | |
Refactoring allpairs to handle the dependent version as well
Diffstat (limited to 'mathcomp/ssreflect/bigop.v')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index bcc1f7e..a3dd0be 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1193,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. @@ -1546,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]. |