Логика: In_example_2

Question

Вот код из книги:

Example In_example_2 :
  forall n, In n [2; 4] ->
  exists n', n = 2 * n'.
Proof.
  (* WORKED IN CLASS *)
  simpl.
  intros n [H | [H | []]].
  - exists 1. rewrite <- H. reflexivity.
  - exists 2. rewrite <- H. reflexivity.
Qed.

После simpl.In превращается в дизъюнкцию из 3 элементов:

============================
forall n : nat, 2 = n \/ 4 = n \/ False -> exists n' : nat, n = n' + (n' + 0)

Но я совершенно не понимаю, как это читать:

intros n [H | [H | []]].

Это произвело это:

n : nat
H : 2 = n
============================
exists n' : nat, n = n' + (n' + 0)

subgoal 2 (ID 229) is:
 exists n' : nat, n = n' + (n' + 0)

То, что я понял:

1. Это поставил из forall в контекст.
2. Он разделил дизъюнкцию 3 элементов на 2 подцела, игнорируя False:
3. Создано 2 подзадачи в зависимости от количества расколов.

Внизу также есть надпись:

(** (Notice the use of the empty pattern to discharge the last case
    _en passant_.) *)

"En passant" (по-французски "[ɑ̃ paˈs lit]", буквально "мимоходом") - ход в шахматах Это специальный захват пешки, который может происходить только сразу после того, как пешка делает ход на два квадрата от ее стартового квадрата, и когда она могла быть захвачена вражеской пешкой, если она продвинулась только на один квадрат.

Глядя на это:

intros n [H | [H | []]].

Может кто-нибудь объяснить мне:

1. Должна ли команда этой формы использоваться для разрушения? Есть ли что-то еще для этой задачи?
2. Как читать эту команду на английском?
3. Зачем [H | []] был помещен в другую пару скобок?
4. Как [] сказал coq игнорировать ложное утверждение?
5. Когда эту команду следует использовать вообще?

Answer 1

intros n [H | [H | []]] форма является сокращением для

intros n H. destruct H as [H | [H | []]].

Вы можете в дальнейшем переписать доказательство как

intros n H. destruct H as [H2 | H4F].
- (* H2 : 2 = n *)
  exists 1. rewrite <- H2. reflexivity.
- (* H4F : 4 = n \/ False *)
  destruct H4F as [H4 | HF].
  + (* H4 : 4 = n *)
    exists 2. rewrite <- H4. reflexivity.
  + (* HF : False *)
    destruct HF. (* No more subgoals here *)

Два доказательства логически эквивалентны, но первое из них короче (и легче для чтения, когда вы привыкнете к синтаксису).

Вообще говоря, тактика destruct x as [...] принимает выражение x и генерирует одну подцель для каждого конструктора, который мог бы быть использован для создания x, Аргументы для конструкторов названы в соответствии с шаблоном [...]и части, соответствующие различным конструкторам, разделены вертикальными чертами.

Предложение в форме A \/ B \/ C следует читать как A \/ (B \/ C), Таким образом, когда вы звоните destruct впервые в расширенной форме выше, вы получаете два случая: когда для когда A держит, другой, когда B \/ C держит. Вам нужно позвонить destruct во второй раз проанализировать внутреннюю или, поэтому у вас были вложенные скобки в исходном выражении. Что касается последней ветки, False определяется как предложение без конструкторов, поэтому, как только вы разрушите гипотезу HF : Falseдоказательство завершено.

(Здесь "en passant" эквивалентно английскому "попутно", что примерно означает "случайно". Это относится к тому факту, что мы выписываем последний случай как побочный продукт выполнения анализа случая или гипотезы).)