factoring out in_sig

1 files changed, 42 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v
index 48f0262..1864b53 100644
--- a/mathcomp/ssreflect/ssrbool.v
+++ b/mathcomp/ssreflect/ssrbool.v
@@ -349,3 +349,45 @@ Proof. by case: b => // /(_ isT). Qed.
 Lemma contra_notF P b : (b -> P) -> ~ P -> b = false.
 Proof. by case: b => // /(_ isT). Qed.
 End Contra.
+
+(******************)
+(* v8.14 addtions *)
+(******************)
+
+Section in_sig.
+Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0).
+Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0).
+Local Notation "{ 'all3' P }" := (forall x y z, P x y z : Prop) (at level 0).
+
+Variables T1 T2 T3 : Type.
+Variables (D1 : {pred T1}) (D2 : {pred T2})  (D3 : {pred T3}).
+Variable P1 : T1 -> Prop.
+Variable P11 : T1 -> T2 -> Prop.
+Variable P111 : T1 -> T2 -> T3 -> Prop.
+Variable P2 :  T1 -> T1 -> Prop.
+Variable P3 :  T1 -> T1 -> T1 -> Prop.
+
+Lemma in1_sig : {in D1, {all1 P1}} -> forall x : sig D1, P1 (sval x).
+Proof. by move=> DP [x Dx]; have := DP _ Dx. Qed.
+
+Lemma in11_sig : {in D1 & D2, {all2 P11}} ->
+  forall (x : sig D1) (y : sig D2), P11 (sval x) (sval y).
+Proof. by move=> DP [x Dx] [y Dy]; have := DP _ _ Dx Dy. Qed.
+
+Lemma in111_sig : {in D1 & D2 & D3, {all3 P111}} ->
+  forall (x : sig D1) (y : sig D2) (z : sig D3), P111 (sval x) (sval y) (sval z).
+Proof. by move=> DP [x Dx] [y Dy] [z Dz]; have := DP _ _ _ Dx Dy Dz. Qed.
+
+Lemma in2_sig : {in D1 &, {all2 P2}} -> forall x y : sig D1, P2 (sval x) (sval y).
+Proof. by move=> DP [x Dx] [y Dy]; have := DP _ _ Dx Dy. Qed.
+
+Lemma in3_sig : {in D1 & &, {all3 P3}} ->
+   forall x y z : sig D1, P3 (sval x) (sval y) (sval z).
+Proof. by move=> DP [x Dx] [y Dy] [z Dz]; have := DP _ _ _ Dx Dy Dz. Qed.
+
+End in_sig.
+Arguments in1_sig {T1 D1 P1}.
+Arguments in11_sig {T1 T2 D1 D2 P11}.
+Arguments in111_sig {T1 T2 T3 D1 D2 D3 P111}.
+Arguments in2_sig {T1 D1 P2}.
+Arguments in3_sig {T1 D1 P3}.