Transport along a type equality, then small facts about stdpp's own datatypes: options, lists, lists read as finite maps and sets, strings and their renderings, and stdpp's fresh-string generator.

Type Casts

Two types that are provably equal are not thereby definitionally equal, so a value of one is not accepted where the other is expected until it is transported across the proof. cast transports forwards along such an equality and cast_sym backwards; the facts below are what lets a proof move a goal between the two sides. The caller this exists for is a record field of the form f x = T, which fixes a type propositionally rather than by definition and leaves every use of that type owing a transport.

Heterogeneous Equality

Two elements of a family at two indices, equal in the sense that carries the two indices. JMeq states the same thing about their two *types* and forgets the indices, so recovering an equation from it is UIP at Type, which is an axiom; eq_dep keeps them, and eq_of_heq below recovers an equation whenever the index type has decidable equality — which it does everywhere here, the indices being sorts. An equation between dependent pairs would say the same thing again, but it is an eq, so simplify_eq takes it apart and, with an equation between the two indices also in context, loops; set_solver is then unusable in any proof that carries one.

Transport along an equation of indices is heterogeneously the identity.

At one index, a heterogeneous equation is an equation. eq_dep_sym and eq_dep_trans are the other two steps; reflexivity already closes a ≅ goal, but symmetry and etransitivity do not, the relation not being homogeneous.

The same for an equation of dependent pairs at one index, which is how a finite map of sort-tagged values hands back what it stores.

Options

For the general characterisation of option_Forall, see stdpp's option_Forall_from_option.

Lists

omap never grows a list.

An element omap drops makes the shrinkage strict.

Mapping over the second component of a list of pairs leaves the first projections alone.

Contiguous Sublists

l1 occurs in l2 as one unbroken run. stdpp's sublist_of allows gaps, and stdpp has prefix_of and suffix_of but nothing between them.

Type-Valued "Every Element"

stdpp's Forall is Prop-valued, so it cannot carry the induction hypotheses of a recursor whose motive is in Type. This is the Type analogue, a nested tuple, matching hlist_ForallT in SMTLIB.Theory.

The payload wants to be read positionally in a proof, as hlist_ForallT's does.

Decidable List Equality

Boolean equality on lists, from a boolean equality on elements.

list_eqb decides equality exactly when the element test does.

Decide list equality from a decision that holds only at the elements the two lists actually contain. list_eq_dec asks for a decision at every element of the type, which a nested inductive cannot supply: its induction hypothesis reaches its own subterms and nothing else.

Deciding Forall From Elementwise Decisions

stdpp's Forall_dec wants a decision at *every* element of the carrier, which a recursion over a nested inductive cannot supply: sort_rect's induction hypothesis decides only the immediate arguments. This is the version that asks no more than that.

Projecting Forall

Forall's two projections at a cons, as transparent terms. Stdlib's Forall_inv and Forall_inv_tail are opaque, which matters to a Type-valued recursion that threads a Forall through: a cbn that cannot step the projection stops with the premise unread, and a proof that passed a particular premise in cannot see it come back out.

Lists into Finite Maps and Sets

A key outside the key list is absent from the map the list zips into. Stated one-directionally: the converse needs length ks = length vs, since a key can otherwise sit in ks beyond the point where zip truncates.

Mapping over the values of a zipped map is mapping over the value list.

A one-binder list extension is an insertion.

Two maps agreeing at j away from a common extension still agree at j once both are extended the same way: an insert at i decides j = i, a common left operand of ∪ decides every key it defines.

list_to_set can only lose elements, never gain them. stdpp's size_list_to_set gives the exact size but assumes NoDup; this bound holds unconditionally.

Looking a key up by its first position in the key list agrees with looking it up in the map the keys zip into.

Strings

stdpp's String.app_inj cancels a common prefix; this cancels a common suffix.

Reading Back a Rendering

A symbol that carries a number carries it as text, through stdpp's pretty. Deciding whether a symbol is one of those, or recovering the number it carries, therefore needs a partial inverse: a parse that agrees with pretty on pretty's image. Soundness on the rest of the strings is not needed and is not claimed — a caller that wants it checks the candidate by rendering it again.

Read the digits of s onto acc, left to right.

k is the power of ten x was rendered at; the digit count is not needed anywhere else, so it stays existential.

A leading minus is what pretty puts on a negative, and it is not a digit, so the unsigned read fails on exactly those.

Taking a Rendering Apart

Read a known prefix off the front of a string.

Split at the first occurrence of c, which is dropped.

A rendered number is digits, so a separator that is not one survives the split above.

Fresh Strings

fresh_string_of_set and fresh_strings_of_set are stdpp's, from stringmap: the second draws n names avoiding a given stringset, each draw also avoiding the ones before it. Three facts make such a list usable as a run of binder names: there are n of them, they are pairwise distinct, and they avoid the set.

The names drawn avoid the set, and so avoid any subset of it. The subset X' is what makes this usable: a caller draws against a union of several sets and then needs disjointness from one of them.