Step-Indices In this file, we declare an interface for step-indices (see sidx). Step-indexing in Iris enables all kinds of recursive constructions such as mixed-variance recursive definitions and mixed-variance recursive types. For more information on step-indexing and how it is used in Iris, see the journal paper "Iris from the Ground Up" (which can be found at https://doi.org/10.1017/S0956796818000151) or the Iris appendix. Traditionally, step-indexing is done by using natural numbers as indices. However, it can also be generalized to richer sets of indices such as ω^2 (i.e., pairs of natural numbers with lexicographic ordering), ω^ω (i.e., lists of natural numbers with lexicographic ordering), countable ordinals, and even uncountable ordinals. Large parts of Iris are agnostic of the step-indexing type that is used, which allows us to factor out the notion of a step-index via the interface of an "index type" (see sidx and SIdxMixin) and define them generically in the index type (e.g., the algebra folder). Note that transfinite step-indexing is not a strict improvement on finite step-indexing (i.e., step-indexing with natural numbers)—they are incomparable (see the paper on "Transfinite Iris" for an explanation of the trade-offs, which can be found at https://doi.org/10.1145/3453483.3454031). Thus, to retain the benefits of both, we make definitions parametric instead of specialized to natural numbers or a particular type of ordinals. An index type I comes with

• a well-founded strict linear order sidx_lt (written i < j),
• a total linear order sidx_le (written i ≤ j),
• a zero index sidx_zero (written 0ᵢ),
• and a successor operation on indices sidx_succ (written Sᵢ).

The less-or-equal relation ≤ must be compatible with the less-than relation < (sidx_mixin_le_lteq). That is, i ≤ j iff i < j or i = j. The 0ᵢ index has to be the smallest step-index (i.e., ¬ i ≺ zero for all i) and the successor operation Sᵢ should yield for a step-index i the least index greater than i. The strict order < should be computationally decidable, and, finally, it should be computationally decidable whether a given step-index is a limit index (i.e., it cannot be reached from any predecessor by applying the successor operation). The less-or-equal operation sidx_le is not strictly necessary since i ≤ j is equivalent to i < j or i = j. We add it as an additional parameter to this interface for engineering reasons: the addition of sidx_le simplifies backwards compatibly to developments that assume step-indices are always natural numbers and (implicitly) that (i ≤ j)%sidx unifies with (i ≤ j)%nat for natural numbers.

An index is either a successor or a limit index. The second disjunct in weak_case considers 0ᵢ to be a limit index, which is often not desired. So typically, instead of weak_case you want to use Index.case which has an explicit disjunct for 0ᵢ and uses Index.limit to define limit indices, excluding 0ᵢ.

sidx is both a canonical structure and a typeclass. When working with a concrete index type, we usually fix it globally. Declaring an appropriate instance and structure enables Coq to infer the globally fixed index type automatically in almost all places. For an example of how to instantiate sidx, see stepindex_finite.v. Using both a canonical structure and a type class is not very common. In this case, it maximizes the inference that is done by Coq when we use the index type. The fact that the step-index is a type class makes sure in, for example, lemma statements that it will be inferred from the context automatically. It also means that if we work with finite step-indices then the finite step-index instance will be used by default as soon as we (or any of our dependencies) import stepindex_finite.v. The canonical structure, on the other hand, makes sure that the index type is inferred automatically as soon as we use either natural numbers or ordinals as the step-index in a concrete lemma.

We cannot overload 0 and S, so we define custom notations with an i subscript. Overloading 0 is disallowed, one should use Number Notation, but that only works for "concrete" number types defined as an Inductive (not "abstract" number types represented by a class). One also cannot overload S since it is a constructor (of nat) and not a Notation.

The remaining operations have notations in the `

Finite indices are exactly the natural numbers

Lifting of the mixin properties

Not an Instance, we get that via StrictOrder.

Limit indices

weak_case allows us to decide whether a number is a limit index. However, according to m < n → Sᵢ m < n (right disjunct), 0 is a limit index. In many definitions and proofs (e.g., case and rec), it is helpful to think of 0 as a special case rather than a degenerate limit index. We therefore exclude 0 from the notion of limit indices.

Derived properties

These instances have a very high cost, so that the default instances for nat are prefered over these ones in case of finite step indexing.

Ordinal recursion

We define the standard recursion scheme for ordinal induction (i.e., transfinite induction) rec with the right "unfolding" lemmas: P 0 → (∀ i, P i → P (Sᵢ i)) → (∀ i, limit i, (∀ j, j < i → P j) → P i) → ∀ i, P i