主页 / coding / 问题 / 77876003
Accepted
lukmik
Asked: 2024-01-25 04:23:07 +0800 CST

如何在 CoqIDE 中证明这一点

  • 772
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 : Set -> Prop f : Set -> Set x : Set H1 : P x -> Q (fx) x0 : Set H2 : P x0 Unable to unify "Q (fx) ”与“Q (f x0)”。

coq

1 个回答

  1. Best Answer

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

    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)一个具体情况（因为它被两者所掩盖）。xexists x, P/Q x

    • 1

相关问题