主页 / coding / 问题 / 79368036
Accepted
radrow
Asked: 2025-01-19 06:04:02 +0800 CST

Coq 定理中的“参数”和“指标”之间有什么区别？

  • 772

我非常熟悉在声明归纳类型时区分参数和索引。我不确定的是，在声明定理时，将内容放在冒号前和冒号后是否有区别。具体来说

Lemma par (n : nat) : n < 1 -> n = 0.

Lemma ind : forall (n : nat), n < 1 -> n = 0.

我发现的一个区别是，在证明 时par，冒号右侧的所有内容最初都在上下文中，而在 中则ind必须如此intro。您知道这两者之间还有其他区别吗？您能举一个例子来说明这不仅仅是一堆intro/revert吗？

我担心的问题之一是自动化可能会更喜欢其中一个，例如autorewrite或auto，尽管我找不到会产生影响的例子。

coq

2 个回答

  1. Best Answer

    参见文档：

    该形式Definition ident binders : type := term相当于Definition ident : forall binders, type := fun binders => term。

    • 3

  2. 对于归纳数据类型，所有构造函数的参数都是固定的，并且它们之间不会发生变化。

    索引根据构造函数而变化，并反映在类型中。

    Inductive vector (A : Type) : nat -> Type :=
| vnil : vector A 0
| vcons : A -> forall n, vector A n -> vector A (S n).

    这里，A 是一个参数，对于所有构造函数都是固定的。的第二个参数vector是一个索引，用于表示向量的长度。请注意索引如何根据特定的构造函数（0for vnil，S nfor vcons）而变化。

    • 1

相关问题