coq - 是否有任何策略可以处理带有“和”的先决条件？

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.

标签： coqcoq-tactic

Answer 1

该策略intuition不起作用，因为该策略是为命题逻辑设计的（即，它不是量词，forall y, R -> ... 还有另一种策略，它被称为firstorder。试试吧！