Логика: In_example_2 - PullRequest
Новая
       14

Логика: In_example_2

1 голос
/ 25 апреля 2019

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

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. Он вставил n 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ɑ̃], букв. В прохождении) - движение в шахматы. Это специальный захват пешки, который может произойти только немедленно после того, как пешка делает ход на две клетки от ее стартовой площади, и когда он мог быть захвачен вражеской пешкой, если бы он только продвинулся один квадрат.

Глядя на это: 

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

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

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

1 Ответ

3 голосов
/ 26 апреля 2019

Форма 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 * 1027"* " эквивалентно английскому" попутно ", что примерно означает" случайно ". Это относится к тому факту, что мы выписываем последний случай как побочный продукт проведения анализа случая по гипотезе или.)

...