diff options
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index d44bbd0..4e4c77b 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2839,3 +2839,21 @@ End AllIff. Arguments all_iffLR {P0 Ps}. Arguments all_iffP {P0 Ps}. Coercion all_iffP : all_iff >-> Funclass. + +Section All2. +Context {T U : Type} (p : T -> U -> bool). + +Fixpoint all2 s1 s2 := + match s1, s2 with + | [::], [::] => true + | x1 :: s1, x2 :: s2 => p x1 x2 && all2 s1 s2 + | _, _ => false + end. + +Lemma all2E s1 s2 : + all2 s1 s2 = (size s1 == size s2) && all [pred xy | p xy.1 xy.2] (zip s1 s2). +Proof. by elim: s1 s2 => [|x s1 ihs1] [|y s2] //=; rewrite ihs1 andbCA. Qed. + +End All2. + +Arguments all2 {T U} p !s1 !s2. |