Implementation of all2 (#224)

 Added the definition of all2.

This definition of all2 has the useful computational behaviour, and all2E unfolds an equivalent one.

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.