我想了解下面证明中的语法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]？
你是对的。 您在此处使用的称为介绍模式。
intros [|n].
相当于
intro n. destruct n as [|n].
你基本上是给构造函数的不同参数命名，使用|来分隔所述构造函数。 对于自然数，您有构造函数O和S。第一个没有参数，而第二个有一个，我们称之为n.
如果你有一个布尔值，你可以使用[|]因为true和false都不接受论证。 请注意，intros []也是可能的，并且对应于intro h. destruct h.而不命名变量。 更一般地说，您不必详尽无遗地命名变量。intros [|].，intros []或intros [|?]对自然数同样有效(?允许你声明有一个你不会命名的变量，coq会自动给它一个(。