Coq中intros的案例分析

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，然后对其进行了案例分析。然而，我习惯于用析构进行案例分析。这是一条捷径吗？如何理解具有第一个分支为空的案例分析[H1 | H2]？

Answer 1

你是对的。您在这里使用的是所谓的介绍模式。

intros [|n].

等于

intro n. destruct n as [|n].

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

如果有布尔值，则可以使用[|]，因为true和false都不接受参数。注意，intros []也是可能的，并且不需要命名变量就对应于intro h. destruct h.。更广泛地说，您不需要在命名变量方面做到详尽无遗。intros [|].、intros []或intros [|?]同样适用于自然数(?允许您声明有一个变量是您不愿命名的，coq将自动给它命名)。