Merge pull request #342 from math-comp/deprecation

add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma names

6 files changed, 89 insertions, 11 deletions

diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 468aa66..65167b5 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -2412,7 +2412,7 @@ Proof.
 set Su := map _ S => sSuS freeS; have uniqS := free_uniq freeS.
 have uniqSu: uniq Su by rewrite (map_inj_uniq cfAut_inj).
 have{sSuS} sSuS: {subset Su <= S} by move=> _ /mapP[phi Sphi ->]; apply: sSuS.
-have [|eqSuS _] := leq_size_perm uniqSu sSuS; first by rewrite size_map.
+have [|_ eqSuS] := uniq_min_size uniqSu sSuS; first by rewrite size_map.
 by rewrite (perm_free (uniq_perm_eq uniqSu uniqS eqSuS)).
 Qed.
 
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index 459250f..ae54fa1 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -1332,9 +1332,9 @@ rewrite -coef_map rmorph_prod; congr (_ : {poly _})`_i.
 symmetry; rewrite (eq_big_perm (map x r)) /= ?(big_map x).
   by apply: eq_bigr => b _; rewrite rmorphB /= map_polyX map_polyC.
 have Uxr: uniq (map x r) by rewrite map_inj_uniq //; apply: fmorph_inj.
-have /leq_size_perm: {subset map x r <= r}.
+have /uniq_min_size: {subset map x r <= r}.
   by rewrite -map_comp => _ /codomP[b ->] /=; rewrite -galM // r_xa ?groupM.
-by rewrite (size_map x) perm_eq_sym; case=> // /uniq_perm_eq->.
+by rewrite (size_map x) perm_eq_sym; case=> // _ /uniq_perm_eq->.
 Qed.
 
 Lemma mem_galTrace K E a : galois K E -> a \in E -> galTrace K E a \in K.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 5576355..3685c23 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1516,26 +1516,26 @@ move=> Us1 eqs12; apply/idP/idP=> [Us2 | /eqP eq_sz12].
 by apply: (leq_size_uniq Us1) => [y|]; rewrite (eqs12, eq_sz12).
 Qed.
 
-Lemma leq_size_perm s1 s2 :
+Lemma uniq_min_size s1 s2 :
     uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 ->
-  s1 =i s2 /\ size s1 = size s2.
+  (size s1 = size s2) * (s1 =i s2).
 Proof.
 move=> Us1 ss12 le_s21; have Us2: uniq s2 := leq_size_uniq Us1 ss12 le_s21.
-suffices: s1 =i s2 by split; last by apply/eqP; rewrite -uniq_size_uniq.
+suffices: s1 =i s2 by split; first by apply/eqP; rewrite -uniq_size_uniq.
 move=> x; apply/idP/idP=> [/ss12// | s2x]; apply: contraLR le_s21 => not_s1x.
 rewrite -ltnNge (@uniq_leq_size (x :: s1)) /= ?not_s1x //.
 by apply/allP; rewrite /= s2x; apply/allP.
 Qed.
 
-Lemma perm_uniq s1 s2 : s1 =i s2 -> size s1 = size s2 -> uniq s1 = uniq s2.
+Lemma eq_uniq s1 s2 : size s1 = size s2 -> s1 =i s2 -> uniq s1 = uniq s2.
 Proof.
-move=> Es12 Esz12.
-by apply/idP/idP=> Us; rewrite (uniq_size_uniq Us) ?Esz12 ?eqxx.
+move=> eq_sz12 eq_s12.
+by apply/idP/idP=> Us; rewrite (uniq_size_uniq Us) ?eq_sz12 ?eqxx.
 Qed.
 
 Lemma perm_eq_uniq s1 s2 : perm_eq s1 s2 -> uniq s1 = uniq s2.
 Proof.
-by move=> eq_s12; apply: perm_uniq; [apply: perm_eq_mem | apply: perm_eq_size].
+by move=> eq_s12; apply/eq_uniq; [apply: perm_eq_size | apply: perm_eq_mem].
 Qed.
 
 Lemma uniq_perm_eq s1 s2 : uniq s1 -> uniq s2 -> s1 =i s2 -> perm_eq s1 s2.
@@ -3056,3 +3056,16 @@ Coercion all_iffP : all_iff >-> Funclass.
 Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := (all_iff P0 (P1 :: .. [:: Pn] ..))
   (at level 0, format "[ '<->' '['  P0 ;  '/' P1 ;  '/'  .. ;  '/'  Pn ']' ]")
   : form_scope.
+
+Notation leq_size_perm :=
+  ((fun T s1 s2 Us1 ss12 les21 =>
+   let: (Esz12, Es12) :=
+     deprecate leq_size_perm uniq_min_size T s1 s2 Us1 ss12 les21
+   in conj Es12 Esz12) _ _ _)
+  (only parsing).
+Notation perm_uniq :=
+  ((fun T s1 s2 eq_s12 eq_sz12 =>
+      deprecate perm_uniq eq_uniq T s1 s2 eq_sz12 eq_s12)
+    _ _ _)
+  (only parsing).
+
diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v
index 7eb7fd9..54c74dd 100644
--- a/mathcomp/ssreflect/ssrbool.v
+++ b/mathcomp/ssreflect/ssrbool.v
@@ -1,6 +1,18 @@
 From mathcomp Require Import ssreflect ssrfun.
 From Coq Require Export ssrbool.
 
+(******************************************************************************)
+(* Local additions:                                                           *)
+(*      {pred T} == a type convertible to pred T but that presents the        *)
+(*                  pred_sort coercion class.                                 *)
+(*  PredType toP == the predType structure for toP : A -> pred T.             *)
+(*    relpre f r == the preimage of r by f, simplifying to r (f x) (f y).     *)
+(* --> These will become part of the core SSReflect library with Coq 8.11.    *)
+(* This file also anticipates a v8.11 change in the definition of simpl_pred  *)
+(* to T -> simpl_pred T. This change ensures that inE expands the definition  *)
+(* of r : simpl_rel along with the \in, when rewriting in y \in r x.          *)
+(******************************************************************************)
+
 Notation "{ 'pred' T }" := (pred_sort (predPredType T)) (at level 0,
   format "{ 'pred'  T }") : type_scope.
 
@@ -37,4 +49,3 @@ Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] (at level 0,
 Notation xrelpre := (fun f (r : rel _) x y => r (f x) (f y)).
 Definition relpre {T rT} (f : T -> rT)  (r : rel rT) :=
   [rel x y | r (f x) (f y)].
-
diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index fe06c0d..95da9cd 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -5,6 +5,22 @@ Global Set SsrOldRewriteGoalsOrder.
 Global Set Asymmetric Patterns.
 Global Set Bullet Behavior "None".
 
+(******************************************************************************)
+(* Local additions:                                                           *)
+(*   nonPropType == an interface for non-Prop Types: a nonPropType coerces    *)
+(*                  to a Type, and only types that do _not_ have sort         *)
+(*                  Prop are canonical nonPropType instances. This is         *)
+(*                  useful for applied views.                                 *)
+(*   --> This will become standard with the Coq v8.11 SSReflect core library. *)
+(*  deprecate old new == new, but warning that old is deprecated and new      *)
+(*                       should be used instead.                              *)
+(*    --> Usage: Notation old := (deprecate old new) (only parsing).          *)
+(*    --> Caveat: deprecate old new only inherits new's maximal implicits;    *)
+(*        on-demand implicits should be added after : (deprecate old new _).  *)
+(*  Import Deprecation.Silent :: turn off deprecation warning messages.       *)
+(*  Import Deprecation.Reject :: raise an error instead of only warning.      *)
+(******************************************************************************)
+
 Module NonPropType.
 
 Structure call_of (condition : unit) (result : bool) := Call {callee : Type}.
@@ -33,3 +49,39 @@ End Exports.
 End NonPropType.
 Export NonPropType.Exports.
 
+Module Deprecation.
+
+Definition hidden (T : Type) := T.
+Definition exposed (T : Type) & unit -> unit -> unit := T.
+Definition hide T u (v : exposed T u) : hidden T := v.
+
+Ltac warn old_id new_id :=
+  idtac "Warning:" old_id "is deprecated; use" new_id "instead".
+
+Ltac stop old_id new_id :=
+  fail 1 "Error:" old_id "is deprecated; use" new_id "instead".
+
+Structure hinted := Hint {statement; hint : statement}.
+Ltac check cond := let test := constr:(hint _ : cond) in idtac.
+
+Variant reject := Reject.
+Definition reject_hint := Hint reject Reject.
+Module Reject. Canonical reject_hint. End Reject.
+
+Variant silent := Silent.
+Definition silent_hint := Hint silent Silent.
+Module Silent. Canonical silent_hint. End Silent.
+
+Ltac flag old_id new_id :=
+  first [check reject; stop old_id new_id | check silent | warn old_id new_id].
+
+Module Exports.
+Arguments hide {T} u v /.
+Coercion hide : exposed >-> hidden.
+Notation deprecate old_id new_id :=
+  (hide (fun old_id new_id => ltac:(flag old_id new_id; exact tt)) new_id)
+  (only parsing).
+End Exports.
+
+End Deprecation.
+Export Deprecation.Exports.
diff --git a/mathcomp/ssreflect/ssrnotations.v b/mathcomp/ssreflect/ssrnotations.v
index 4c55514..dbc7f3d 100644
--- a/mathcomp/ssreflect/ssrnotations.v
+++ b/mathcomp/ssreflect/ssrnotations.v
@@ -1,6 +1,7 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 
+(******************************************************************************)
 (* - Reserved notation for various arithmetic and algebraic operations:       *)
 (*     e.[a1, ..., a_n] evaluation (e.g., polynomials).                       *)
 (*                 e`_i indexing (number list, integer pi-part).              *)
@@ -27,6 +28,7 @@
 (*    [rec a1, ..., an] standard shorthand for hidden recursor (see prime.v). *)
 (*   The interpretation of these notations is not defined here, but the       *)
 (*   declarations help maintain consistency across the library.               *)
+(******************************************************************************)
 
 (* Reserved notation for evaluation *)
 Reserved Notation "e .[ x ]"