有没有什么策略可以和"and“一起使用前提条件？

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。试试看！