Есть ли какая-то тактика для работы с предусловиями с «и»?

Question

Моя цель как ниже. Есть ли какая-то тактика для решения этих тривиальных целей?

Goal forall A (x : A) P Q,
  (forall y, P y /\ Q y) ->
  Q x.
Proof.
  intros. intuition. auto.
Abort.

(* a more complex version *)
Goal forall A (x : A) P Q R,
  (forall y, R -> P y /\ Q y) ->
  R ->
  Q x.
Proof.
  intros. intuition. auto.
Abort.

Answer 1

Тактика intuition не работает, потому что эта тактика разработана для логики высказываний (т. Е. Она не является квантификатором в forall y, R -> .... Существует другая тактика для этого, она называется firstorder. Попробуйте!