Merge PR #9995: fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interface

Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: ggonthier

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.