如何在 Coq 中证明这一点

Question

Lemma x: forall P Q: Set -> Prop,
              forall f: Set -> Set, 
            forall x, (P x -> Q (f x)) -> 
               (exists x, P x) -> (exists x, Q x).

我尝试了很多不同的方法，但我不知道出了什么问题。这是我最近的尝试：

Lemma x: forall P Q: Set -> Prop,
              forall f: Set -> Set, 
            forall x, (P x -> Q (f x)) -> 
               (exists x, P x) -> (exists x, Q x).
Proof.
  intros P Q f x H1 [x0 H2].
  exists (f x0).
  apply H1.
  assumption.
Qed.

但它会产生此错误：在环境中 P, Q : 设置 -> 道具 f : 设置 -> 设置 x：设置 H1：P x -> Q (f x) x0：设置 H2 : P x0 无法将“Q (f x)”与“Q (f x0)”统一。

Answer 1

你的引理实际上是错误的。这是一个证明它是错误的：

Axiom x: forall P Q: Set -> Prop,
              forall f: Set -> Set, 
            forall x, (P x -> Q (f x)) -> 
               (exists x, P x) -> (exists x, Q x).


Lemma false : False.
Proof.
  destruct (x 
  (* P *) inhabited
  (* Q *) (fun _ => False)
  (* f *) (fun _ => False)
  (* x *) False ) as [y Hy].
  (* P x -> Q (f x) *) 
  - intros [[]]. (* trivially true, as False is not inhabited *)
  (* ∃ x, P x *) 
  - exists True. now apply inhabits.
  (* We get to assume that Q is satisfiable, but Q is always False *)
  - apply Hy.
Qed.

但是，您试图证明的引理很可能不是您想要证明的引理。您是否可能想在这里证明这个引理？

Lemma x_fixed: forall P Q: Set -> Prop,
               forall f: Set -> Set, 
               (forall x, P x -> Q (f x)) -> 
               (exists x, P x) -> (exists x, Q x).
Proof.
  intros P Q f H1 [x0 H2].
  exists (f x0).
  apply H1.
  assumption.
Qed.

不同之处在于，假设是

forall x, P x -> Q (f x)

，而不是仅仅针对您的目标中未提及的某个特定

P x -> Q (f x)

（因为它被两个

x

所掩盖）。