Модус Поненс и Модус Толленс в Кок - PullRequest
Новая
       112

Модус Поненс и Модус Толленс в Кок

0 голосов
/ 22 октября 2018

Я бы хотел использовать тактику Ltac для этих простых правил вывода.

В Modus Ponens, если у меня есть H:P->Q и H1:P, Ltac mp H H1 добавит Q к контексту как H2 : Q.

В Модус Толленс, если у меня есть H:P->Q и H1:~Q, то Ltac mt H H1 добавит H2:~P к контексту.

Я написал один для модусаponens, но это не работает в сложных случаях, когда прецедент также является следствием.

Ltac mp H0 H1 := let H := fresh "H" in apply H0 in H1 as H.

Редактировать: я нашел ответ на Modus Ponens в другом, казалось бы, не связанном вопросе ( Перепишите гипотезу в Coq, сохраняя смысл ), где "10" * "10"

. *1025*

Ltac mp H H0 := let H1 := fresh "H" in generalize (H H0); intros H1.

Iвсе равно буду благодарен за ответ Модуса Толленса.

1 Ответ

0 голосов
/ 22 октября 2018

Вот одно из решений: 

Ltac mt PtoQ notQ notP :=
  match type of PtoQ with
  | ?P -> _ => pose proof ((fun p => notQ (PtoQ p)) : ~ P) as notP
  end.

Эта тактика запрашивает у пользователя две входные гипотезы и явное имя выходной гипотезы.Я использую конструкцию type of PtoQ для извлечения типа P из входного значения, а затем предоставляю явный термин (fun p => notQ (PtoQ p) типа P -> False, который по определению равен ~ P.Явный тип ascription : ~ P используется для того, чтобы сделать контекст более красивым, без него Coq покажет тип выходной гипотезы как P -> False.

Кстати, я бы использовал что-то подобное для реализации тактики modus ponens: 

Ltac mp PtoQ P Q := 
  pose proof (PtoQ P) as Q.

Здесь снова параметры PtoQ и P являются именами входных гипотез, а Q - это имя, которое будет добавлено в контекст.

...