问Coq中定义与让的区别

EN

我认为您所要求的与Coq中的Definition命令和Let命令之间的区别并没有什么关系。相反，您似乎想知道Coq中的某些定义为什么包含验证脚本。

Coq的一个有趣的特性是，用于编写证明和程序的语言实际上是相同的。这种语言被称为Gallina，它是人们在使用Coq时使用的编程语言。当你写一些类似fun x => x + 5的东西时，这是一个用Gallina编写的程序。

然而，在做证明时，人们通常使用另一种语言，称为Ltac。这是出现在exp示例中的语言。这可能会让你相信Coq中的证据是用另一种语言表示的，但事实并非如此: Ltac脚本所做的就是在Gallina中实际构建验证术语。通过使用Print命令可以看到这一点。

Print exp.

即使证据和程序是用同一种语言编写的，也有一种单独的语言来编写校样，这是因为Gallina在写校样时很难直接使用。尝试在一个复杂的定理上直接使用Print命令，看看这有多难。

现在，尽管Ltac主要是用来写证明的，但是没有什么可以禁止你用它来编写正常的程序，因为最终的产品是一样的: Gallina术语。通常，人们喜欢在编写程序时使用Gallina，因为它更容易阅读。然而，当直接用Gallina编写程序时，人们可能会求助于Ltac，这太麻烦了。我个人更倾向于在示例中直接使用Gallina编写诸如exp之类的函数，尽管这可以说是一个品味问题。