This file defines two "base" combinatorial interfaces:
eqType == the structure for types with a decidable equality.
- Equality mixins can be made Canonical to allow generic
- folding of equality predicates.
- subType p == the structure for types isomorphic to {x : T | p x} with
- p : pred T for some type T.
- The eqType interface supports the following operations:
- x == y <=> x compares equal to y (this is a boolean test).
- x == y :> T <=> x == y at type T.
- x != y <=> x and y compare unequal.
- x != y :> T <=> " " " " at type T.
- x =P y :: a proof of reflect (x = y) (x == y); this coerces
- to x == y -> x = y.
- comparable T <-> equality on T is decidable
+ subType P == the structure for types isomorphic to {x : T | P x} with
+ P : pred T for some type T.
+ The following are used to construct eqType instances:
+ EqType T m == the packed eqType class for type T and mixin m.
+> As eqType is a root class, equality mixins and classes coincide.
+ Equality.axiom e <-> e : rel T is a valid comparison decision procedure
+ for type T: reflect (x = y) (e x y) for all x y : T.
+ EqMixin eP == the equality mixin for eP : Equality.axiom e.
+> Such manifest equality mixins should be declared Canonical to allow
+ for generic folding of equality predicates (see lemma eqE below).
+ [eqType of T for eT] == clone for T of eT, where eT is an eqType for a
+ type convertible, but usually not identical, to T.
+ [eqType of T] == clone for T of the eqType inferred for T, possibly
+ after unfolding some definitions.
+ [eqMixin of T] == mixin of the eqType inferred for T.
+ comparable T <-> equality on T is decidable.
:= forall x y : T, decidable (x = y)
- comparableClass compT == eqType mixin/class for compT : comparable T.
+ comparableMixin compT == equality mixin for compT : comparable T.
+ InjEqMixin injf == an Equality mixin for T, using an f : T -> U where
+ U has an eqType structure and injf : injective f.
+ PcanEqMixin fK == an Equality mixin similarly derived from f and a left
+ inverse partial function g and fK : pcancel f g.
+ CanEqMixin fK == an Equality mixin similarly derived from f and a left
+ inverse function g and fK : cancel f g.
+> Equality mixins derived by the above should never be made Canonical as
+ they provide only comparisons with a generic head constant.
+ The eqType interface supports the following operations:
+ x == y <=> x compares equal to y (this is a boolean test).
+ x == y :> T <=> x == y at type T.
+ x != y <=> x and y compare unequal.
+ x != y :> T <=> x and y compare unequal at type T.
+ x =P y :: a proof of reflect (x = y) (x == y); x =P y coerces
+ to x == y -> x = y.
+ eq_op == the boolean relation behing the == notation.
pred1 a == the singleton predicate [pred x | x == a].
pred2, pred3, pred4 == pair, triple, quad predicates.
predC1 a == [pred x | x != a].
@@ -90,7 +109,7 @@
a proof of x0 \in A.
insub_eq x == transparent version of insub x that expands to Some/None
when P x can evaluate.
- The subType P interface is most often implemented using one of:
+ The subType P interface is most often implemented using one of:
[subType for S_val]
where S_val : S -> T is the first projection of a type S isomorphic to
{x : T | P}.
@@ -111,16 +130,9 @@
Subtypes inherit the eqType structure of their base types; the generic
structure should be explicitly instantiated using the
[eqMixin of S by <: ]
- construct to declare the Equality mixin; this pattern is repeated for all
- the combinatorial interfaces (Choice, Countable, Finite).
- More generally, the eqType structure can be transfered by (partial)
- injections, using:
- InjEqMixin injf == an Equality mixin for T, using an f : T -> eT where
- eT has an eqType structure and injf : injective f.
- PcanEqMixin fK == an Equality mixin similarly derived from f and a left
- inverse partial function g and fK : pcancel f g.
- CanEqMixin fK == an Equality mixin similarly derived from f and a left
- inverse function g and fK : cancel f g.
+ construct to declare the equality mixin; this pattern is repeated for all
+ the combinatorial interfaces (Choice, Countable, Finite). As noted above,
+ such mixins should not be made Canonical.
We add the following to the standard suffixes documented in ssrbool.v:
1, 2, 3, 4 -- explicit enumeration predicate for 1 (singleton), 2, 3, or
4 values.
@@ -134,25 +146,24 @@
Module Equality.
-
Definition axiom T (
e :
rel T) :=
∀ x y,
reflect (
x = y) (
e x y).
+
Definition axiom T (
e :
rel T) :=
∀ x y,
reflect (
x = y) (
e x y).
-
Structure mixin_of T :=
Mixin {
op :
rel T;
_ :
axiom op}.
+
Structure mixin_of T :=
Mixin {
op :
rel T;
_ :
axiom op}.
Notation class_of :=
mixin_of (
only parsing).
Section ClassDef.
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Variables (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ :=
cT return class_of cT in c.
+
Definition class :=
let:
Pack _ c :=
cT return class_of cT in c.
-
Definition pack c := @
Pack T c T.
-
Definition clone :=
fun c &
cT → T &
phant_id (
pack c)
cT ⇒
pack c.
+
Definition clone :=
fun c &
cT → T &
phant_id (@
Pack T c)
cT ⇒
Pack c.
End ClassDef.
@@ -162,12 +173,12 @@
Coercion sort : type >-> Sortclass.
Notation eqType :=
type.
Notation EqMixin :=
Mixin.
-
Notation EqType T m := (@
pack T m).
-
Notation "[ 'eqMixin' 'of' T ]" := (
class _ : mixin_of T)
+
Notation EqType T m := (@
Pack T m).
+
Notation "[ 'eqMixin' 'of' T ]" := (
class _ : mixin_of T)
(
at level 0,
format "[ 'eqMixin' 'of' T ]") :
form_scope.
-
Notation "[ 'eqType' 'of' T 'for' C ]" := (@
clone T C _ idfun id)
+
Notation "[ 'eqType' 'of' T 'for' C ]" := (@
clone T C _ idfun id)
(
at level 0,
format "[ 'eqType' 'of' T 'for' C ]") :
form_scope.
-
Notation "[ 'eqType' 'of' T ]" := (@
clone T _ _ id id)
+
Notation "[ 'eqType' 'of' T ]" := (@
clone T _ _ id id)
(
at level 0,
format "[ 'eqType' 'of' T ]") :
form_scope.
End Exports.
@@ -179,7 +190,27 @@
Definition eq_op T :=
Equality.op (
Equality.class T).
-
Lemma eqE T x :
eq_op x = Equality.op (
Equality.class T)
x.
+
+ eqE is a generic lemma that can be used to fold back recursive comparisons
+ after using partial evaluation to simplify comparisons on concrete
+ instances. The eqE lemma can be used e.g. like so: rewrite !eqE /= -!eqE.
+ For instance, with the above rewrite, n.+1 == n.+1 gets simplified to
+ n == n. For this to work, we need to declare equality
mixins
+ as canonical. Canonical declarations remove the need for specific
+ inverses to eqE (like eqbE, eqnE, eqseqE, etc.) for new recursive
+ comparisons, but can only be used for manifest mixing with a bespoke
+ comparison function, and so is incompatible with PcanEqMixin and the like
+
+- this is why the tree_eqMixin for GenTree.tree in library choice is not
+
+
+
+ declared Canonical.
+
-
Notation xpred1 := (
fun a1 x ⇒
x == a1).
-
Notation xpred2 := (
fun a1 a2 x ⇒
(x == a1) || (x == a2)).
-
Notation xpred3 := (
fun a1 a2 a3 x ⇒
[|| x == a1, x == a2 | x == a3]).
+
Notation xpred1 := (
fun a1 x ⇒
x == a1).
+
Notation xpred2 := (
fun a1 a2 x ⇒
(x == a1) || (x == a2)).
+
Notation xpred3 := (
fun a1 a2 a3 x ⇒
[|| x == a1, x == a2 | x == a3]).
Notation xpred4 :=
- (
fun a1 a2 a3 a4 x ⇒
[|| x == a1, x == a2, x == a3 | x == a4]).
-
Notation xpredU1 := (
fun a1 (
p :
pred _)
x ⇒
(x == a1) || p x).
-
Notation xpredC1 := (
fun a1 x ⇒
x != a1).
-
Notation xpredD1 := (
fun (
p :
pred _)
a1 x ⇒
(x != a1) && p x).
+ (
fun a1 a2 a3 a4 x ⇒
[|| x == a1, x == a2, x == a3 | x == a4]).
+
Notation xpredU1 := (
fun a1 (
p :
pred _)
x ⇒
(x == a1) || p x).
+
Notation xpredC1 := (
fun a1 x ⇒
x != a1).
+
Notation xpredD1 := (
fun (
p :
pred _)
a1 x ⇒
(x != a1) && p x).
Section EqPred.
@@ -365,37 +411,37 @@
Variable T :
eqType.
-
Definition pred1 (
a1 :
T) :=
SimplPred (
xpred1 a1).
-
Definition pred2 (
a1 a2 :
T) :=
SimplPred (
xpred2 a1 a2).
-
Definition pred3 (
a1 a2 a3 :
T) :=
SimplPred (
xpred3 a1 a2 a3).
-
Definition pred4 (
a1 a2 a3 a4 :
T) :=
SimplPred (
xpred4 a1 a2 a3 a4).
-
Definition predU1 (
a1 :
T)
p :=
SimplPred (
xpredU1 a1 p).
-
Definition predC1 (
a1 :
T) :=
SimplPred (
xpredC1 a1).
-
Definition predD1 p (
a1 :
T) :=
SimplPred (
xpredD1 p a1).
+
Definition pred1 (
a1 :
T) :=
SimplPred (
xpred1 a1).
+
Definition pred2 (
a1 a2 :
T) :=
SimplPred (
xpred2 a1 a2).
+
Definition pred3 (
a1 a2 a3 :
T) :=
SimplPred (
xpred3 a1 a2 a3).
+
Definition pred4 (
a1 a2 a3 a4 :
T) :=
SimplPred (
xpred4 a1 a2 a3 a4).
+
Definition predU1 (
a1 :
T)
p :=
SimplPred (
xpredU1 a1 p).
+
Definition predC1 (
a1 :
T) :=
SimplPred (
xpredC1 a1).
+
Definition predD1 p (
a1 :
T) :=
SimplPred (
xpredD1 p a1).
-
Lemma pred1E :
pred1 =2 eq_op.
+
Lemma pred1E :
pred1 =2 eq_op.
-
Variables (
T2 :
eqType) (
x y :
T) (
z u :
T2) (
b :
bool).
+
Variables (
T2 :
eqType) (
x y :
T) (
z u :
T2) (
b :
bool).
-
Lemma predU1P :
reflect (
x = y ∨ b) (
(x == y) || b).
+
Lemma predU1P :
reflect (
x = y ∨ b) (
(x == y) || b).
-
Lemma pred2P :
reflect (
x = y ∨ z = u) (
(x == y) || (z == u)).
+
Lemma pred2P :
reflect (
x = y ∨ z = u) (
(x == y) || (z == u)).
-
Lemma predD1P :
reflect (
x ≠ y ∧ b) (
(x != y) && b).
+
Lemma predD1P :
reflect (
x ≠ y ∧ b) (
(x != y) && b).
-
Lemma predU1l :
x = y → (x == y) || b.
+
Lemma predU1l :
x = y → (x == y) || b.
-
Lemma predU1r :
b → (x == y) || b.
+
Lemma predU1r :
b → (x == y) || b.
-
Lemma eqVneq :
{x = y} + {x != y}.
+
Lemma eqVneq :
{x = y} + {x != y}.
End EqPred.
@@ -403,9 +449,9 @@
-
Notation "[ 'predU1' x & A ]" := (
predU1 x [mem A])
+
Notation "[ 'predU1' x & A ]" := (
predU1 x [mem A])
(
at level 0,
format "[ 'predU1' x & A ]") :
fun_scope.
-
Notation "[ 'predD1' A & x ]" := (
predD1 [mem A] x)
+
Notation "[ 'predD1' A & x ]" := (
predD1 [mem A] x)
(
at level 0,
format "[ 'predD1' A & x ]") :
fun_scope.
@@ -423,27 +469,27 @@
Section Exo.
-
Variables (
aT rT :
eqType) (
D :
pred aT) (
f :
aT → rT) (
g :
rT → aT).
+
Variables (
aT rT :
eqType) (
D :
pred aT) (
f :
aT → rT) (
g :
rT → aT).
-
Lemma inj_eq :
injective f → ∀ x y,
(f x == f y) = (x == y).
+
Lemma inj_eq :
injective f → ∀ x y,
(f x == f y) = (x == y).
-
Lemma can_eq :
cancel f g → ∀ x y,
(f x == f y) = (x == y).
+
Lemma can_eq :
cancel f g → ∀ x y,
(f x == f y) = (x == y).
-
Lemma bij_eq :
bijective f → ∀ x y,
(f x == f y) = (x == y).
+
Lemma bij_eq :
bijective f → ∀ x y,
(f x == f y) = (x == y).
-
Lemma can2_eq :
cancel f g → cancel g f → ∀ x y,
(f x == y) = (x == g y).
+
Lemma can2_eq :
cancel f g → cancel g f → ∀ x y,
(f x == y) = (x == g y).
Lemma inj_in_eq :
-
{in D &, injective f} → {in D &, ∀ x y,
(f x == f y) = (x == y)}.
+
{in D &, injective f} → {in D &, ∀ x y,
(f x == f y) = (x == y)}.
Lemma can_in_eq :
-
{in D, cancel f g} → {in D &, ∀ x y,
(f x == f y) = (x == y)}.
+
{in D, cancel f g} → {in D &, ∀ x y,
(f x == f y) = (x == y)}.
End Exo.
@@ -455,13 +501,13 @@
Variable T :
eqType.
-
Definition frel f :=
[rel x y : T | f x == y].
+
Definition frel f :=
[rel x y : T | f x == y].
-
Lemma inv_eq f :
involutive f → ∀ x y :
T,
(f x == y) = (x == f y).
+
Lemma inv_eq f :
involutive f → ∀ x y :
T,
(f x == y) = (x == f y).
-
Lemma eq_frel f f' :
f =1 f' → frel f =2 frel f'.
+
Lemma eq_frel f f' :
f =1 f' → frel f =2 frel f'.
End Endo.
@@ -479,17 +525,17 @@
-
Notation coerced_frel f := (
rel_of_simpl_rel (
frel f)) (
only parsing).
+
Notation coerced_frel f := (
rel_of_simpl_rel (
frel f)) (
only parsing).
Section FunWith.
@@ -512,14 +558,14 @@
Variables (
aT :
eqType) (
rT :
Type).
-
CoInductive fun_delta :
Type :=
FunDelta of aT &
rT.
+
Variant fun_delta :
Type :=
FunDelta of aT &
rT.
-
Definition fwith x y (
f :
aT → rT) :=
[fun z ⇒ if z == x then y else f z].
+
Definition fwith x y (
f :
aT → rT) :=
[fun z ⇒ if z == x then y else f z].
Definition app_fdelta df f z :=
-
let:
FunDelta x y :=
df in if z == x then y else f z.
+
let:
FunDelta x y :=
df in if z == x then y else f z.
End FunWith.
@@ -527,7 +573,7 @@
-
Notation "x |-> y" := (
FunDelta x y)
+
Notation "x |-> y" := (
FunDelta x y)
(
at level 190,
no associativity,
format "'[hv' x '/ ' |-> y ']'") :
fun_delta_scope.
@@ -535,22 +581,22 @@
Delimit Scope fun_delta_scope with FUN_DELTA.
-
Notation "[ 'fun' z : T => F 'with' d1 , .. , dn ]" :=
- (
SimplFunDelta (
fun z :
T ⇒
+
Notation "[ 'fun' z : T => F 'with' d1 , .. , dn ]" :=
+ (
SimplFunDelta (
fun z :
T ⇒
app_fdelta d1%
FUN_DELTA .. (
app_fdelta dn%
FUN_DELTA (
fun _ ⇒
F)) ..))
(
at level 0,
z ident,
only parsing) :
fun_scope.
-
Notation "[ 'fun' z => F 'with' d1 , .. , dn ]" :=
- (
SimplFunDelta (
fun z ⇒
+
Notation "[ 'fun' z => F 'with' d1 , .. , dn ]" :=
+ (
SimplFunDelta (
fun z ⇒
app_fdelta d1%
FUN_DELTA .. (
app_fdelta dn%
FUN_DELTA (
fun _ ⇒
F)) ..))
(
at level 0,
z ident,
format
"'[hv' [ '[' 'fun' z => '/ ' F ']' '/' 'with' '[' d1 , '/' .. , '/' dn ']' ] ']'"
) :
fun_scope.
-
Notation "[ 'eta' f 'with' d1 , .. , dn ]" :=
- (
SimplFunDelta (
fun _ ⇒
+
Notation "[ 'eta' f 'with' d1 , .. , dn ]" :=
+ (
SimplFunDelta (
fun _ ⇒
app_fdelta d1%
FUN_DELTA .. (
app_fdelta dn%
FUN_DELTA f) ..))
(
at level 0,
format
"'[hv' [ '[' 'eta' '/ ' f ']' '/' 'with' '[' d1 , '/' .. , '/' dn ']' ] ']'"
@@ -571,119 +617,132 @@
Variable T :
Type.
-
Definition comparable :=
∀ x y :
T,
decidable (
x = y).
+
Definition comparable :=
∀ x y :
T,
decidable (
x = y).
-
Hypothesis Hcompare :
comparable.
+
Hypothesis compare_T :
comparable.
-
Definition compareb x y :
bool :=
Hcompare x y.
+
Definition compareb x y :
bool :=
compare_T x y.
Lemma compareP :
Equality.axiom compareb.
-
Definition comparableClass :=
EqMixin compareP.
+
Definition comparableMixin :=
EqMixin compareP.
End ComparableType.
Definition eq_comparable (
T :
eqType) :
comparable T :=
-
fun x y ⇒
decP (
x =P y).
+
fun x y ⇒
decP (
x =P y).
Section SubType.
-
Variables (
T :
Type) (
P :
pred T).
+
Variables (
T :
Type) (
P :
pred T).
Structure subType :
Type :=
SubType {
sub_sort :>
Type;
-
val :
sub_sort → T;
-
Sub :
∀ x,
P x → sub_sort;
+
val :
sub_sort → T;
+
Sub :
∀ x,
P x → sub_sort;
_ :
∀ K (
_ :
∀ x Px,
K (@
Sub x Px))
u,
K u;
-
_ :
∀ x Px,
val (@
Sub x Px)
= x
+
_ :
∀ x Px,
val (@
Sub x Px)
= x
}.
-
Lemma vrefl :
∀ x,
P x → x = x.
+
+
+
+ Generic proof that the second property holds by conversion.
+ The vrefl_rect alias is used to flag generic proofs of the first property.
+
+
-
-
-
-
-
-Notation " [ 'subType' 'for' v ]" := (clone_subType _ v id idfun)
- (at level 0, format " [ 'subType' 'for' v ]") : form_scope.
-
-
-
@@ -755,20 +803,20 @@ Notation " [ 'subType' 'for' v ]" := (clone_subType _ v id idfun)
Prenex Implicits and renaming.