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

Question

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

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.

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

Answer 1

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

Обычный способ доказать цель типа 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с и производит Rs. После 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 являются функциями.

---

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

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