Как смоделировать правило введения для импликации в Coq?

Я изучаю естественные дедукции и практикую Coq.

Считаем формулу:

Inductive P :=
| ...
| And: P -> P -> P
| Imp: P -> P -> P. (* implication *)

Теперь я добавляю несколько правил вывода для доказуемости:

Inductive Deriv: P -> Prop :=
| ...
| intro_and: forall p q, Deriv p -> Deriv q -> Deriv (And p q)
| elim_and1: forall p q, Deriv (And p q) -> Deriv p
| elim_and2: forall p q, Deriv (And p q) -> Deriv q
| ...

Но я застрял с правилом введения для импликации. Я пробовал это:

| intro_imp: forall p q, (Deriv p -> Deriv q) -> Deriv (Imp p q)

, что явно не работает, потому что индуктивный случай появляется в отрицательном положении.

Правило введения для импликации:

[p]
 .
 .
 q
-------
p ⊃ q

Как можно смоделировать правило введения импликации в Coq?


logic first-order-logic coq
person Alex    schedule 17.04.2015    source источник

Ответы (1)


arrow_upward
4
arrow_downward

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

Я думаю, что самое простое решение — сделать гипотезы явными в суждениях, т. е. Deriv будет иметь тип list P -> P -> Prop. Идея состоит в том, что Deriv hs p выражает, что p доказуемо при гипотезах hs. Это означает отказ от первоначальной формулировки естественного вывода в стиле Гильберта, где гипотезы неявны (см., например, статью Википедии). Оставаясь внутри фрагмента, который вы дали, это может привести к чему-то вроде этого (используя секвенцию только с одним выводом):

Inductive Deriv : list P -> P -> Prop :=
(* How to use a hypothesis *)
| premise_intro hs p : In p hs -> Deriv hs p

(* In most rules, we just maintain the list of hypotheses *)
| and_intro hs p1 p2 : Deriv hs p1 -> Deriv hs p2 -> Deriv hs (And p1 p2)
| and_elim1 hs p1 p2 : Deriv hs (And p1 p2) -> Deriv hs p1
| and_elim2 hs p1 p2 : Deriv hs (And p1 p2) -> Deriv hs p2
| imp_elim hs p1 p2 : Deriv hs (Imp p1 p2) -> Deriv hs p1 -> Deriv hs p2

(* When introducing an implication, we remove the hypothesis from our list *)
| imp_intro hs p1 p2 : Deriv (p1 :: hs) p2 -> Deriv hs (Imp p1 p2).
person Arthur Azevedo De Amorim    schedule 18.04.2015