Coq-Iris框架中InjLV与InjRV算子的含义咨询

在Iris默认语言lang.v中，val是表达式的值类型，其定义如下：

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

各构造子的含义：

• LitV：表示基础字面量值，比如整数、布尔值这类底层基础数据。
• RecV：表示递归表达式的值，其中f是递归变量绑定，x是参数绑定，e是递归体表达式。
• PairV：表示二元组值，用来存储两个值组成的配对结构。
• InjLV/InjRV：这是求和类型（sum type）的注入构造子，作用是将值标记为某一分支的实例：
  • InjLV v：将值v注入到求和类型的左分支。Iris中用InjLV #()来表示NONEV（无值），这里的#()是单位值，相当于用左分支包裹空值来标识“不存在有效内容”的状态。
  • InjRV v：将值v注入到求和类型的右分支。Iris中用InjRV #v来表示SOMEV v（包含某值v的可选状态），用右分支包裹实际值来标识“存在有效内容”的状态。

本质上，Iris通过这两个构造子实现了类似ML系语言中option类型的功能——用左分支对应None，右分支对应Some v，无需单独定义option类型，直接复用val的结构来承载可选值语义。

内容的提问来源于stack exchange，提问作者Huan Sun