+ 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.
+
+
+
Lemma simpl_pred_sortE T (
p :
pred T) :
(SimplPred p : {pred T}) =1 p.
+
Definition inE :=
(inE, simpl_pred_sortE).
+
+
+
Definition PredType :
∀ T pT,
(pT → pred T) → predType T.
+
Defined.
+
+
+
Definition simpl_rel T :=
T → simpl_pred T.
+
Definition SimplRel {
T} (
r :
rel T) :
simpl_rel T :=
fun x ⇒
SimplPred (
r x).
+
Coercion rel_of_simpl_rel T (
sr :
simpl_rel T) :
rel T :=
sr.
+
+
+
Notation "[ 'rel' x y | E ]" := (
SimplRel (
fun x y ⇒
E%
B)) (
at level 0,
+
x ident,
y ident,
format "'[hv' [ 'rel' x y | '/ ' E ] ']'") :
fun_scope.
+
Notation "[ 'rel' x y : T | E ]" := (
SimplRel (
fun x y :
T ⇒
E%
B)) (
at level 0,
+
x ident,
y ident,
only parsing) :
fun_scope.
+
Notation "[ 'rel' x y 'in' A & B | E ]" :=
+
[rel x y | (x \in A) && (y \in B) && E] (
at level 0,
x ident,
y ident,
+
format "'[hv' [ 'rel' x y 'in' A & B | '/ ' E ] ']'") :
fun_scope.
+
Notation "[ 'rel' x y 'in' A & B ]" :=
[rel x y | (x \in A) && (y \in B)]
+ (
at level 0,
x ident,
y ident,
+
format "'[hv' [ 'rel' x y 'in' A & B ] ']'") :
fun_scope.
+
Notation "[ 'rel' x y 'in' A | E ]" :=
[rel x y in A & A | E]
+ (
at level 0,
x ident,
y ident,
+
format "'[hv' [ 'rel' x y 'in' A | '/ ' E ] ']'") :
fun_scope.
+
Notation "[ 'rel' x y 'in' A ]" :=
[rel x y in A & A] (
at level 0,
+
x ident,
y ident,
format "'[hv' [ 'rel' x y 'in' A ] ']'") :
fun_scope.
+
+
+
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)
].