Library mathcomp.ssreflect.eqtype

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 := forall x y : T, decidable (x = y) comparableClass compT == eqType mixin/class for compT : comparable T. 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 k f == 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 infered 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 statisfying 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 [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. 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.

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 an 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.

Notation " [ 'subType' 'for' v ]" := (clone_subType _ v id idfun) (at level 0, format " [ 'subType' 'for' v ]") : form_scope.

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].