Início / coding / Perguntas / 77876003
Accepted
lukmik
Asked: 2024-01-25 04:23:07 +0800 CST

Como provar isso no 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).

Tento fazer isso de muitas maneiras diferentes e não sei o que há de errado. Esta é minha última tentativa:

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.

mas produz este erro: No ambiente P, Q: Set -> Prop f: Set -> Set x: Set H1: P x -> Q (fx) x0: Set H2: P x0 Incapaz de unificar "Q (fx) " com "Q (f x0)".

coq

1 respostas

  1. Best Answer

    Seu lema é realmente falso. Aqui está uma prova de que é falso:

    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.

    No entanto, é provável que o lema que você está tentando provar não seja aquele que você deseja provar. É possível que você quisesse provar esse lema aqui?

    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.

    A diferença é que a suposição é forall x, P x -> Q (f x), em vez de ser apenas P x -> Q (f x)para um específico xque não é mencionado de outra forma em seu objetivo (uma vez que é obscurecido por ambos exists x, P/Q x).

    • 1

relate perguntas