Types with a decidable equality NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. This file defines two "base" combinatorial structures: eqType == types with a decidable equality The HB class is called Equality. The equality operation on an eqType is proof-irrelevant (lemma eq_irrelevance). The main notation is the boolean equality "==", see below. subType P == types isomorphic to {x : T | P x} with P : pred T for some type T The HB class is called SubType. subEqType P == join of eqType and subType P The HB class is called SubEquality. The eqType interface supports the following operations (in bool_scope): 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 (see lemma eqE below for generic folding of equality predicates) eqP == proof of Equality.axiom eq_op behind the =P notation 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 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 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

Sub

Specific notations

[isSub of S for S_val] == subtype for S where S_val : S -> T is the first projection of a type S isomorphic to {x : T | P}; if S_val is specified, then it replaces the inferred projector. [isSub for S_val] := [isSub of _ for S_val] It clones the canonical subType structure for S. [isNew of S for S_val] == subtype for S where S_val : S -> T is the projection of a type S isomorphic to T; in this case P must be predT [isNew for S_val] := [isNew of _ for S_val] [isSub for S_val by Srect], [isNew 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). Subtypes inherit the eqType structure of their base types; the generic structure should be explicitly instantiated using the [Equality of S by <: ] construct; this pattern is repeated for all the combinatorial interfaces (Choice, Countable, Finite). List of factories with a dedicated alias (not generated automatically): inj_type injf == alias of T to copy an interface from another T' already equipped with it and injf : injective f with f : T -> T' pcan_type fK == alias of T to similarly derive an interface from f and a left inverse partial function g and fK : pcancel f g can_type fK == alias of T to similarly derive an interface from f and a left inverse function g and fK : cancel f g sub_type sT == alias of sT : subType _ comparable T <-> equality on T is decidable. := forall x y : T, decidable (x = y) comparableMixin compT == equality mixin for compT : comparable T 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 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.

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