Как доказать (forall x, P x/\Q x)-> (forall x, P x)

Как каждый доказывает (forall x, P x/\Q x)-> (forall x, P x) в Coq? Попытка в течение многих часов и не может выяснить, как сломать антецедент к чему-то, что может переварить Coq. (Я - newb, очевидно :)

7
задан Stefan 27 October 2019 в 20:59
поделиться

2 ответа

Попробуйте

elim (H x).
2
ответ дан 6 December 2019 в 23:13
поделиться

На самом деле, я понял это, когда обнаружил это:

Математика для компьютерных ученых 2

В уроке 5 он решает ту же задачу и использует команду «вырезать (P x / \ Q x)», которая переписывает цель с «P x» на «P x / \ Q x -> P x ". Оттуда вы можете выполнить некоторые манипуляции, а когда цель - просто «P x / \ Q x», вы можете применить «forall x: P x / \ Q x», а остальное просто.

2
ответ дан 6 December 2019 в 23:13
поделиться
Другие вопросы по тегам:

Похожие вопросы: