I have just started using coq and couldn’t find a solution to this Problem.
How can I use the
apply .. in tactic, when the desired conclusion begins with ∀?
I am trying to prove the following theorem:
Theorem noworks : forall (X : Type) (P : X -> Prop) (A : Prop) (x' : X), A -> (A -> (forall x, P x)) -> P x'.
This proof attempt where I try using the premises to arrive at ∀x P x fails.
Proof. intros X P A x HA Himp. apply Himp in HA. > Output: Unable to find an instance for the variable x.
If however I replace the ∀x P x in the theorem by a helper definition, the Proof works the intended way.
Definition helper (X : Type) (P : X -> Prop) : Prop := forall x, P x. Theorem works : forall (X : Type) (P : X -> Prop) (A : Prop) (x' : X), A -> (A -> helper X P) -> P x'. (* ^^^^^^^^^^ *) Proof. intros X P A x HA Himp. apply Himp in HA. unfold helper in HA. apply HA. Qed.
I’d also appreciate any tips on how to troubleshoot these kinds of issues (e.g. using the documentation).
Thanks for your help!