This file defines two "base" combinatorial interfaces: eqType == the structure for types with a decidable equality. subType P == the structure for types isomorphic to {x : T | P x} with P : pred T for some type T.

EqType (types with boolean equality relation)

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. List of factories (to use with HB.instance Definition _ := )

• hasDecEq.Build T eqP Declares an EqType on T from the equality axiom for some relation eqP must be an instance of Equality.axiom

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. [hasDecEq of T] == mixin of the eqType inferred for T. comparable T <-> equality on T is decidable. := forall x y : T, decidable (x = y) 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. eqbLHS := (X in (X == _))%pattern (for rewriting) eqbRHS := (X in (_ == X))%pattern (for rewriting) eq_op == the boolean relation behind the == notation. pred1 a == the singleton predicate [pred x | x == a]. pred2, pred3, pred4 == pair, triple, quad predicates. predC1 a == [pred x | x != a]. [predU1 a & A] == [pred x | (x == a) || (x \in A) ]. [predD1 A & a] == [pred x | x != a & x \in A]. predU1 a P, predD1 P a == applicative versions of the above. frel f == the relation associated with f : T -> T. := [rel x y | f x == y]. invariant f k == elements of T whose k-class is f-invariant. := [pred x | k (f x) == k x] with f : T -> T. [fun x : T => e0 with a1 |-> e1, .., a_n |-> e_n] [eta f with a1 |-> e1, .., a_n |-> e_n] == the auto-expanding function that maps x = a_i to e_i, and other values of x to e0 (resp. f x). In the first form the `: T' is optional and x can occur in a_i or e_i. Equality on an eqType is proof-irrelevant (lemma eq_irrelevance). The eqType interface is implemented for most standard datatypes: bool, unit, void, option, prod (denoted A * B), sum (denoted A + B), sig (denoted {x | P}), sigT (denoted {i : I & T}). We also define tagged_as u v == v cast as T(tag u) if tag v == tag u, else u.

• > We have u == v <=> (tag u == tag v) && (tagged u == tagged_as u v).

The subType interface supports the following operations: val == the generic injection from a subType S of T into T. For example, if u : {x : T | P}, then val u : T. val is injective because P is proof-irrelevant (P is in bool, and the is_true coercion expands to P = true). valP == the generic proof of P (val u) for u : subType P. Sub x Px == the generic constructor for a subType P; Px is a proof of P x and P should be inferred from the expected return type. insub x == the generic partial projection of T into a subType S of T. This returns an option S; if S : subType P then insub x = Some u with val u = x if P x, None if ~~ P x The insubP lemma encapsulates this dichotomy. P should be inferred from the expected return type. innew x == total (non-option) variant of insub when P = predT. {? x | P} == option {x | P} (syntax for casting insub x). insubd u0 x == the generic projection with default value u0. := odflt u0 (insub x). insigd A0 x == special case of insubd for S == {x | x \in A}, where A0 is 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: [subType for S_val] where S_val : S -> T is the first projection of a type S isomorphic to {x : T | P}. [newType for S_val] where S_val : S -> T is the projection of a type S isomorphic to wrapped T; in this case P must be predT. [subType for S_val by Srect], [newType for S_val by Srect] variants of the above where the eliminator is explicitly provided. Here S no longer needs to be syntactically identical to {x | P x} or wrapped T, but it must have a derived constructor S_Sub satisfying an eliminator Srect identical to the one the Coq Inductive command would have generated, and S_val (S_Sub x Px) (resp. S_val (S_sub x) for the newType form) must be convertible to x. variant of the above when S is a wrapper type for T (so P = predT). [subType of S], [subType of S for S_val] clones the canonical subType structure for S; if S_val is specified, then it replaces the inferred projector. Subtypes inherit the eqType structure of their base types; the generic structure should be explicitly instantiated using the [hasDecEq of S by <: ] 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.

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_hasDecEq for GenTree.tree in library choice is not

declared Canonical.

We use the module system to circumvent a silly limitation that forbids using the same constant to coerce to different targets.

Comparison for booleans. This is extensionally equal, but not convertible to Bool.eqb.

Equality-based predicates.

Lemmas for reflected equality and functions.

The invariant of a function f wrt a projection k is the pred of points that have the same projection as their image.

The coercion to rel must be explicit for derived Notations to unparse.

Various EqType constructions.

Generic proof that the second property holds by conversion. The vrefl_rect alias is used to flag generic proofs of the first property.

BUG in elim? sT could be inferred from u

Arguments val {T P sT} u : rename.

Prenex Implicits and renaming.

Shorthand for sigma types over collective predicates.

Shorthand for the return type of insub.

A variant of injection with default that infers a collective predicate from the membership proof for the default value.

There should be a rel definition for the subType equality op, but this seems to cause the simpl tactic to diverge on expressions involving == on 4+ nested subTypes in a "strict" position (e.g., after ~~). Definition feq f := [rel x y | f x == f y].