diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/path.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrbool.v | 35 |
2 files changed, 18 insertions, 21 deletions
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index f4ecfbb..d99dedf 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -882,7 +882,7 @@ Arguments sort_map {T T' f leT}. Section SortSeq_in. Variables (T : Type) (P : {pred T}) (leT : rel T). -Notation le_sT := (relpre (val : sig P -> _) leT). +Let le_sT := relpre (val : sig P -> _) leT. Hypothesis leT_total : {in P &, total leT}. Let le_sT_total : total le_sT := in2_sig leT_total. @@ -1138,7 +1138,7 @@ Variables (T : Type) (P : {pred T}) (leT : rel T). Hypothesis leT_total : {in P &, total leT}. Hypothesis leT_tr : {in P & &, transitive leT}. -Notation le_sT := (relpre (val : sig P -> _) leT). +Let le_sT := relpre (val : sig P -> _) leT. Let le_sT_total : total le_sT := in2_sig leT_total. Let le_sT_tr : transitive le_sT := in3_sig leT_tr. diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v index 1864b53..49be7b0 100644 --- a/mathcomp/ssreflect/ssrbool.v +++ b/mathcomp/ssreflect/ssrbool.v @@ -102,6 +102,10 @@ Arguments mono_sym_in {aT rT} [aR rR f aD]. Arguments homo_sym_in11 {aT rT} [aR rR f aD aD']. Arguments mono_sym_in11 {aT rT} [aR rR f aD aD']. +(******************) +(* v8.14 addtions *) +(******************) + Section LocalGlobal. Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). @@ -209,6 +213,10 @@ Arguments in_on1S {T1 T2} D2 {f Q1}. Arguments in_on1lS {T1 T2 T3} D2 {f h Q1l}. Arguments in_on2S {T1 T2} D2 {f Q2}. +(******************) +(* v8.13 addtions *) +(******************) + Section CancelOn. Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}). @@ -362,32 +370,21 @@ 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. +Variable P2 : T1 -> T2 -> Prop. +Variable P3 : T1 -> T2 -> T3 -> 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). +Lemma in2_sig : {in D1 & D2, {all2 P2}} -> + forall (x : sig D1) (y : sig D2), 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). +Lemma in3_sig : {in D1 & D2 & D3, {all3 P3}} -> + forall (x : sig D1) (y : sig D2) (z : sig D3), 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}. +Arguments in2_sig {T1 T2 D1 D2 P2}. +Arguments in3_sig {T1 T2 T3 D1 D2 D3 P3}. |