fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interface

** Changed definition of `simpl_rel` to `T -> `simpl_pred T`, so that
`inE` will now expand `a \in r b`, when `r := [rel x y | R]` to `R{b/x,
a/y}`, as the expanding coercion is now only inserted in the _last_
application.
The old definition made it possible to have a `simpl_rel >-> rel`
coercion that does not block expansion, but this can now be achieved
more economically with the `Arguments … /.` annotation.
**  Deleted the `[rel of P]` notation which is no longer needed with
the new `simpl_rel` definition, and was broken anyway.
** Added `relpre f R` definition of functional preimage of a notation.
** `comp` and `idfun` are now proper definitions, using the `Arguments
… /.` annotation to specify simplification on application.
** Added `{pred T}` syntax for the alias of `pred T` in the `pred_sort`
coercion class; deleted the `pred_class` alias: one should either
use `pred_sort` in `Coercion` declarations, or `{pred T}` in type casts.
Used `{pred T}` as appropriate in localised predicate (`{in …, …}`) theory.
Extended and corrected `pred` coercion internal documentation.
** Simplified the `predType` structure by removing the redundant
explicit `mem_pred` subfield, and replacing it with an interlocked
projection; deleted `mkPredType`, now replaced by `PredType`.
** Added (and extensively documented) a `nonPropType` interface
matching types that do _not_ have sort `Prop`, and used it to remove
the non-standard maximal implicits annotation on `Some_inj` introduced
in #6911 by @anton-trumov; included `test-suite` entry for `nonPropType`.
** Documented the design of the four structures used to control the
matching of `inE` and related predicate rewriting lemmas; added `test-suite`
entry covering the `pred` rewriting control idioms.
** Used `only printing` annotations to get rid of token concatenation
hacks.
** Fixed boolean and general `if b return t then …` notation so that
`b` is bound in `t`. This is a minor source of incompatibility for
misuses of this syntax when `b` is _not_ bound in `t`, and `(if b then
…) : t` should have been used instead.
** Reserved all `ssreflect`, `ssrfun` and `ssrbool` notation at the top
of the file, adding some printing boxes, and removing some spurious
`[pred .. => ..]` reserved notation.
** Fixed parsing precedence and format of `<hidden n>` notation, and
declared and put it in an explicit `ssr_scope`.
** Used module-and-functor idiom to ensure that the `simpl_pred T >-
pred T` _and_ `simpl_pred T >-> {pred T}` coercions are realised by the
_same_ Gallina constant.
** Updated `CREDITS`.
The policy implied by this PR: that `{pred T}` should systematically
be used as the generic collective predicate type, was implemented in MathComp
math-comp/math-comp#237. As a result  `simpl_pred >-> pred_sort` coercions
became more frequent, as it turned out they were not, as incorrectly stated
in `ssrbool` internal comments, impossible: while the `simplPredType`
canonical instance does solve all `simpl_pred T =~= pred_sort ?pT`
instances, it does _not_ solve `simpl_pred T =~= {pred T}`, and so the
coercion will be used in that case. However it appeared that having two
different coercion constants confused the SSReflect keyed matching
heuristic, hence the fix introduced here. This has entailed some
rearrangement of `ssrbool`: the large  `Predicates` section had to be
broken up as the module-functor idiom for aliasing coercions cannot be
used inside a section.

3 files changed, 53 insertions, 2 deletions

diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v
index ca360f65a7..6fc630056c 100644
--- a/test-suite/prerequisite/ssr_mini_mathcomp.v
+++ b/test-suite/prerequisite/ssr_mini_mathcomp.v
@@ -634,9 +634,9 @@ Fixpoint mem_seq (s : seq T) :=
 
 Definition eqseq_class := seq T.
 Identity Coercion seq_of_eqseq : eqseq_class >-> seq.
-Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s].
+Coercion pred_of_eq_seq (s : eqseq_class) : {pred T} := [eta mem_seq s].
 
-Canonical seq_predType := @mkPredType T (seq T) pred_of_eq_seq.
+Canonical seq_predType := @PredType T (seq T) pred_of_eq_seq.
 
 Fixpoint uniq s := if s is x :: s' then (x \notin s') && uniq s' else true.
 
diff --git a/test-suite/ssr/nonPropType.v b/test-suite/ssr/nonPropType.v
new file mode 100644
index 0000000000..bcdc907b38
--- /dev/null
+++ b/test-suite/ssr/nonPropType.v
@@ -0,0 +1,23 @@
+Require Import ssreflect.
+
+(** Test the nonPropType interface and its application to prevent unwanted
+    instantiations in views. **)
+
+Lemma raw_flip {T} (x y : T) : x = y -> y = x. Proof. by []. Qed.
+Lemma flip {T : nonPropType} (x y : T) : x = y -> y = x. Proof. by []. Qed.
+
+Lemma testSet : true = false -> True.
+Proof.
+Fail move/raw_flip.
+have flip_true := @flip _ true.
+(* flip_true : forall y : notProp bool, x = y -> y = x *)
+simpl in flip_true.
+(* flip_true : forall y : bool, x = y -> y = x *)
+by move/flip.
+Qed.
+
+Lemma override (t1 t2 : True) : t1 = t2 -> True.
+Proof.
+Fail move/flip.
+by move/(@flip (notProp True)).
+Qed.
diff --git a/test-suite/ssr/predRewrite.v b/test-suite/ssr/predRewrite.v
new file mode 100644
index 0000000000..2ad762ccf1
--- /dev/null
+++ b/test-suite/ssr/predRewrite.v
@@ -0,0 +1,28 @@
+Require Import ssreflect ssrfun ssrbool.
+
+(** Test the various idioms that control rewriting in boolean predicate. **)
+
+Definition simpl_P := [pred a | ~~ a].
+Definition nosimpl_P : pred bool := [pred a | ~~ a].
+Definition coll_P : collective_pred bool := [pred a | ~~ a].
+Definition appl_P : applicative_pred bool := [pred a | ~~ a].
+Definition can_appl_P : pred bool := [pred a | ~~ a].
+Canonical register_can_appl_P := ApplicativePred can_appl_P.
+Ltac see_neg := (let x := fresh "x" in set x := {-}(~~ _); clear x).
+
+Lemma test_pred_rewrite (f := false) : True.
+Proof.
+have _: f \in simpl_P by rewrite inE; see_neg.
+have _ a: simpl_P (a && f) by simpl; see_neg; rewrite andbF.
+have _ a: simpl_P (a && f) by rewrite inE; see_neg; rewrite andbF.
+have _: f \in nosimpl_P by rewrite inE; see_neg.
+have _: nosimpl_P f. simpl. Fail see_neg. Fail rewrite inE. done.
+have _: f \in coll_P. Fail rewrite inE. by rewrite in_collective; see_neg.
+have _: f \in appl_P.
+  rewrite inE. Fail see_neg. Fail rewrite inE. simpl. Fail see_neg.
+  Fail rewrite app_predE. done.
+have _: f \in can_appl_P.
+  rewrite inE. Fail see_neg. Fail rewrite inE. simpl. Fail see_neg.
+  by rewrite app_predE in_simpl; see_neg.
+done.
+Qed.