Транзитивность -> в Coq - PullRequest
Новая
       47

Транзитивность -> в Coq

2 голосов
/ 22 марта 2019

Я пытаюсь доказать транзитивность -> в предложениях Кока: 

Theorem implies_trans : forall P Q R : Prop,
  (P -> Q) -> (Q -> R) -> (P -> R).
Proof.

Я хотел уничтожить все предложения и просто обработать все 8 возможностей с рефлексивностью.Видимо, не все так просто.Вот что я попробовал: 

Theorem implies_trans : forall P Q R : Prop,
  (P -> Q) -> (Q -> R) -> (P -> R).
Proof.
  intros P Q R H1 H2.
  destruct P. (** Hmmm ... this doesn't work *)
Admitted.

И вот что я получаю: 

1 subgoal
P, Q, R : Prop
H1 : P -> Q
H2 : Q -> R
______________________________________(1/1)
P -> R

с этой ошибкой: 

Error: Not an inductive product.

Любая помощь очень ценится, спасибо!

1 Ответ

5 голосов
/ 22 марта 2019

Логика Coq не является классической логикой, где суждения являются истинными или ложными. Вместо этого он основан на теории типов и по умолчанию имеет интуитивистский оттенок. 1 В теории типов вы должны думать, что P -> Q является функцией от "вещей типа P" до "вещей типа Q». 2

Обычный способ доказать цель типа P -> Q состоит в том, чтобы использовать intro или intros, чтобы ввести гипотезу типа P, а затем использовать эту гипотезу, чтобы каким-то образом создать элемент типа Q.

Например, мы можем доказать, что (P -> Q -> R) -> (Q -> P -> R). В интерпретации «импликация - это функция» это может быть истолковано как выражение, что если у нас есть функция, которая принимает P и Q и производит R, то мы можем определить функцию, которая принимает Q и P и производит R. Это та же функция, но с замененными аргументами. 

Definition ArgSwap_1 {P Q R: Prop}: (P -> Q -> R) -> (Q -> P -> R) :=
  fun f q p => f p q.

Используя тактику, мы можем видеть типы отдельных элементов. 

Lemma ArgSwap_2 {P Q R: Prop}: (P -> Q -> R) -> (Q -> P -> R).
Proof.
  intro f.
  intros q p.
  exact (f p q).
Qed.

После intro мы видим, что f: P -> Q -> R, поэтому f - наша функция, которая принимает P с и Q с и производит R с. После intros (который вводит несколько терминов) мы видим, что q: Q и p: P. Последняя строка (перед Qed.) просто применяет функцию f к p и q, чтобы получить что-то в R.

Для вашей проблемы intros вводит предложения P, Q и R, а также H1: P -> Q и H2: Q -> R. Тем не менее, мы можем ввести еще один термин типа P, поскольку цель - P -> R. Вы видите, как использовать H1 и H2 и элемент P для получения элемента R? Подсказка: вы пройдете через Q. Также помните, что H1 и H2 являются функциями.

1 Вы можете добавить в качестве аксиомы закон исключенного среднего, который позволил бы анализ того типа, который вы хотите, но я думаю, что он пропускает точку Coq.

2 Если вам интересно, элементы Prop все еще являются типами и имеют поведение, очень похожее на элементы Set или Type. Единственное отличие состоит в том, что Prop является «непредсказуемым», что позволяет количественно оценивать предложения по всем предложениям. Например, forall P: Prop, P -> P - это элемент Prop, но forall A: Type, A -> A - это элемент следующего уровня до Type (Type на самом деле является бесконечной иерархией).

...