Как доказать (для всех x, P x /\ Q x) -> (для всех x, P x) [В Coq]

Question

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

Answer 1

Вы можете сделать это быстрее, просто применив H, но этот скрипт должно быть более понятным.

Lemma foo : forall (A:Type) (P Q: A-> Prop), (forall x, P x /\ Q x) -> (forall x, P x).
intros.
destruct (H x). 
exact H0.
Qed.

Answer 2

Попробуй

elim (H x).

Answer 3

На самом деле, я понял это, когда нашел это:

Математика для компьютерщиков 2

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

Answer 4

Assume ForAll x: P(x) /\ Q(x)
   var x; 
      P(x) //because you assumed it earlier
   ForAll x: P(x)
(ForAll x: P(x) /\ Q(x)) => (ForAll x: P(x))

Интуитивно, если для всех x выполняется P (x) И Q (x), то для всех x выполняется P (x).