用Coq进行前奏的案例分析

Question

我想了解以下证明中的语法intros [|n].。

Lemma zero_or_succ :
  forall n : nat, n = 0 \/ n = S (pred n).
Proof.
  intros [|n].
  - left. reflexivity.
  - right. reflexivity.
Qed.

我的理解是，它修复n，然后对其进行案例分析。但是，我习惯于使用destruct进行案例分析。这是这样做的捷径吗？我应该如何理解第一个分支为空的案例分析[H1 | H2]？

Answer 1

您是正确的。您在这里使用的称为intro模式。

intros [|n].

相当于

intro n. destruct n as [|n].

您基本上是在使用|分隔所述构造函数，为构造函数的不同参数赋予名称。对于自然数，您具有构造函数O和S。第一个没有参数，而第二个有参数，我们称之为n。

如果您有布尔值，则可以使用[|]，因为true和false都不接受参数。请注意，intros []也是可能的，并且对应于intro h. destruct h.而未命名变量。更一般而言，您不必穷尽命名变量。intros [|].，intros []或intros [|?]同样适用于自然数（?允许您声明有一个您不会命名的变量，coq会自动给它一个值。）>