Rel: le_antisymmetric понимание - PullRequest
Новая
       58

Rel: le_antisymmetric понимание

0 голосов
/ 21 октября 2019

Относительная глава из Логических основ. Мне дали решение для упражнения, которое я пытаюсь понять: 

Definition antisymmetric {X: Type} (R: relation X) :=
  forall a b : X, (R a b) -> (R b a) -> a = b.

Theorem le_antisymmetric :
  antisymmetric le.
Proof.
  unfold antisymmetric. intros a b [| b' H1] H2.
  - reflexivity.
  - absurd (S b' <= b').
    + apply le_Sn_n.
    + etransitivity ; eassumption.

Я не понимаю, как работает шаблон ввода [| b' H1]? После вступления он показывает: 

2 subgoals (ID 43)

  a, b : nat
  H2 : a <= a
  ============================
  a = a

subgoal 2 (ID 46) is:
 a = S b'

2-ая подцель: 

a, b, b' : nat
H1 : a <= b'
H2 : S b' <= a
============================
a = S b'

Я понимаю, что это эквивалентно разрушению, но что за разрушение? Это определенно не просто destruct b.

Также я пытаюсь понять логику использования тактики absurd (S b' <= b'). Означает ли это, что если мы докажем, что a = S b' в этом контексте, это будет означать, что после того, как мы переписываем a в S b' в H1, мы получим: S b' <= b', что является универсально ложным утверждением (абсурдным)?

1 Ответ

2 голосов
/ 21 октября 2019

intros a b [| b' H1] H2 эквивалентно шаблонам 

intros a b H H2.
destruct H as [| b' H1].

destruct, как правило, соответствуют правилам, согласно которым если индуктивный тип имеет один конструктор (например, продукты), то для x в этом индуктивном типе destruct x as [a b c...] выполняет (нерекурсивную) индукцию и переименовывает новые переменные в a, b, c и т. Д. Когда индуктивный тип имеет более одного конструктора, существует несколько случаев. Для этого вы используете destruct x as [a b c ... | d e f ... | ...]. Эти шаблоны разрушения могут быть вложены в случае необходимости, например destruct x as [[a b] | [c [d | e]]]. Обратите внимание, что если конструктор не принимает аргументов, переименовать нечего, поэтому вы можете оставить шаблон пустым.

В частности, что-то вроде натурального числа может быть уничтожено с помощью destruct n as [ | n']. Это делится на случаи, когда n равен нулю (а конструктор не имеет аргументов, поэтому слева от | ничего нет) или n является преемником n'. Точно так же список может быть уничтожен как destruct li as [ | a li'], чтобы разделить его на случаи, когда список равен nil и где он равен cons a li'. Пробел слева от | не нужен, так что вы можете сделать destruct li as [| a li'].

В вашем случае, в частности, происходит то, что le определяется как индуктивный тип, что-то вроде 

Inductive le (n : nat) : nat -> Prop :=
| le_n : le n n
| le_S : forall m : nat, le n m -> le n (S m).

Таким образом, есть два случая: один без аргументов и случай преемника, где аргументами являются m: nat и H: le n m. Следовательно, шаблон разрушения - [| m H].

Чтобы ответить на ваш второй вопрос, absurd (S b' <= b'). означает, что (мы думаем) мы можем доказать S b' <= b' в текущем контексте. Мы также можем доказать (в том же контексте), что S b' <= b' абсурдно, то есть приводит к свидетельству False (точнее, S b' <= b' -> False). Используя принцип индукции для False, это позволяет нам генерировать свидетеля для любого типа, и в частности для a = S b'.

. Вы можете увидеть, какой вид доказательства absurd производит с минимальным экспериментом. . 

Goal forall A B: Type, A.
Proof.
  intros A B.
  absurd B.
  Show Proof.

Это должно вывести (fun A B : Type => False_rect A (?Goal ?Goal0)). Первая цель (?Goal) имеет тип ~B (то есть B -> False). Второй гол (?Goal0) имеет тип B. Если мы можем предоставить и то и другое, то ?Goal ?Goal0 имеет тип False, поэтому False_rect A (?Goal ?Goal0) выдает свидетель типа A.

...