Анализ случая с вступлениями в 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 и затем анализирует его. Тем не менее, я привык к анализу случаев с использованием деструктора Это ярлык для этого? Как понимать анализ случая [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 выдаст ее автоматически).