What does InjL and InjR operator means in coq-Iris?

Question

I'm trying to understand the iris, a state-of-art verification framework based on separation logic. lang.v is the default language used by Iris. Following code defines the value of the expression where LitV means the basic value, RecV means value of recursive expression and PairV is the value of pair expression. However, I have trouble understanding the last two definitions. To give more information, Iris uses InjLV #() to denote NONEV which means no value and uses InjRV #v to denote SOMEV which means some value v.

with val :=
  | LitV (l : base_lit)
  | RecV (f x : binder) (e : expr)
  | PairV (v1 v2 : val)
  | InjLV (v : val)
  | InjRV (v : val).

Answer 1

When reasoning abstractly about datatypes, there are two collections that come naturally. The first one is easily understood from a mathematical point of view, it is the notion of cartesian product. The elements of a cartesian product are pairs of objects, usually coming from two distinct datatypes. Constructing elements of a cartesian product is thus usually made by calling an operation called pair, which takes two values and puts them together in a new data object.

Another construction is often called the disjoint union, or the sum. The idea expressed in this construction is that if we have two collections of A and B, then the elements the sum of A and B are either elements of A or elements of B, a bit like a union of sets, but with a twist: an element of the sum of A and B is actually marked by whether it comes from A or if it comes from B. So, if we consider the sum of a datatype A with itself, it actually is a different datatype from A. In this case, this can also be understood as a cartesian product of A with the type of boolean values. So the analogy with a union operation on sets is not valid here: a set union of A and A would be A itself. This is why the term disjoint union is often used.

So elements of a disjoint union (or sum) type are produced by one of two constructors: either you come from the left, or you come from the right. Moreover, it is well known that dataype constructor are injective, so these constructors are called "injection from the left" or "injection from the right". So it makes sense to call these constructors InjLV and InjRV, adding the V suffix to indicate that we are really talking about constructors for the val part of the language.

In plain coq, you will find quite a few dataype constructors that have sum in the name, two constructors that have inj as radix and l or left and r or right in their constructors, defined as inductive data types, using either the Inductive keyword or the Variant keyword.