时间戳

首页 > 解决方案 > 当您有多行定义归纳构造函数的操作时，这意味着什么？

coq - 当您有多行定义归纳构造函数的操作时，这意味着什么？

问题描述

我在看：

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum  : forall (n: nat),
      aevalR (ANum n) n
  | E_APlus : forall (e1 e2: aexp) (n1 n2: nat),
      aevalR e1 n1 ->
      aevalR e2 n2 ->
      aevalR (APlus e1 e2) (n1 + n2)
  | E_AMinus: forall (e1 e2: aexp) (n1 n2: nat),
      aevalR e1 n1 ->
      aevalR e2 n2 ->
      aevalR (AMinus e1 e2) (n1 - n2)
  | E_AMult : forall (e1 e2: aexp) (n1 n2: nat),
      aevalR e1 n1 ->
      aevalR e2 n2 ->
      aevalR (AMult e1 e2) (n1 * n2).

并试图理解它的含义。我知道这需要算术exp。将其映射到映射到 nat 的函数，该 nat 映射到 prop。但令我困惑的是| A_AOp条款中的内容。它们末尾没有句点，加号和减号有一个指向另一个箭头的箭头。

这是什么类型的语法，它应该说什么？这种感应类型的输入是什么？就像我通常在 python 中看到的那样：

def f(a,b,*args):

所以我知道我应该提供什么作为输入（或多或少）。但这让我很困惑。我该如何使用它，定义是什么意思？

idk 是否应该是一个简单的函数式编程问题，因为我只是在学习 Coq 和函数式编程，而这部分不在我正在查看的课程的函数式编程介绍中：

https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html

标签： coq

解决方案

aevalR这个片段归纳地定义了一个谓词。e : aexp谓词是表达式和​​数字之间的关系n : nat：aevalR e n当e计算结果为时成立n。由竖线引入的每个子句都描述了评估表达式的一种可能性。例如，E_APlus说当e1评估为n1和e2评估为 时n2，我们知道APlus e1 e2评估为n1 + n2。

归纳命题是 Coq 中最常用的工具之一。Software Foundations 一书中有一章介绍了这个概念。我建议您在尝试攻击 Imp 章节之前熟悉该概念——它应该使阅读更容易。

推荐阅读