互感类型解决方法答案

【问题标题】：mutually inductive types workaround互感类型解决方法
【发布时间】：2018-04-05 01:29:20
【问题描述】：

考虑一种简单的语言，它具有自然数、自然数向量、变量和一些操作，例如 +、- 和 nth。天真地，我会像这样在 Coq 中对其进行编码：

Require Import Coq.Vectors.Vector.

Inductive NExpr: Type :=
| NVarValue: nat -> NExpr
| NConst: nat -> NExpr
| NPlus : NExpr -> NExpr -> NExpr
| NMinus: NExpr -> NExpr -> NExpr
| NNth  : forall n, VExpr n -> NExpr -> NExpr
with
VExpr (n:nat): Type :=
| VVarValue: nat -> VExpr n
| VConst: Vector.t nat n -> VExpr n.

当然，由于已知限制会产生错误，这不起作用：“错误：每个归纳类型的参数在语法上应该相同。”

在 Coq 中编码这种语言的正确方法是什么？。当然，我应该可以编写一个eval 函数，按照https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html 的行评估这些表达式

在求值时，向量的维数使用如下：

match e with
  ...
  | @NNth v i => match Compare_dec.lt_dec (evalNexp st i) n with
                | left p => Vnth (evalNexp st v) p
                | right _ => 0
                end

注意在这个例子中，VExpr 不依赖于 NExpr，但将来它可以，通过添加构造函数，其中一些可能使用NExpr。另外，我可能需要添加更多类型，例如，ZExpr 表示整数。

【问题讨论】：

您举个例子，VExpr 将依赖于NExpr？我对你的评估 sn-p 理解正确吗，那么VExpr 用于表示值，NExpr 表示抽象语法？
我不明白NVarValue 和VVarValue 之间的区别，它们似乎都是自然数常数的模型。
@eponier NVarValue 和 VVarValue 是查找函数，它们采用变量名（表示为自然数）并分别返回自然数或向量。
@nesreka 它们都是表达式的句法表示，分别表示自然数和向量。 NExpr 的示例是 1+2*3，VExpr 的示例是 [1,2,3]，使用更传统的语法。依赖于NExpr 的VExpr 的一个示例是，如果我们向VExpr 添加一个新的构造函数，比如VZeroElement: VExpr n -> NExpr -> VExpr n，它将表示一个假设函数，该函数接受一个向量并将具有给定索引的元素替换为0。
@krokodil 谢谢。从第二个归纳中删除n:nat参数是否可行？您可以将 is 作为参数添加到需要的构造函数并对其进行模式匹配。您还可以将forall n:nat, ... 移动到constructor n : ...

标签： coq

【解决方案1】：

您可以更改第二个归纳法，使其使用索引而不是参数。

Require Import Coq.Vectors.Vector.

Inductive NExpr: Type :=
| NVarValue: nat -> NExpr
| NConst: nat -> NExpr
| NPlus : NExpr -> NExpr -> NExpr
| NMinus: NExpr -> NExpr -> NExpr
| NNth  : forall n, VExpr n -> NExpr -> NExpr
with
VExpr : nat -> Type :=
| VVarValue: forall n, nat -> VExpr n
| VConst: forall n, Vector.t nat n -> VExpr n.

【讨论】：