CODEWITHSUNDEEP
coqcoq-tactic
thor
thor

Reputation: 22530

How to introduce a new existential condition from a witness in Coq?

My question relates to how to construct an exist term in the set of conditions/hypotheses.

I have the following intermediate proof state:

X : Type
P : X -> Prop
H : (exists x : X, P x -> False) -> False
x : X
H0 : P x -> False
______________________________________(1/1)
P x

In my mind, I know that because of H0, x is a witness for (exists x : X, P x -> False), and I want to introduce a name:

w: (exists x : X, P x -> False)

based on the above reasoning and then use it with apply H in w to generate a False in the hypothesis, and finally inversion the False.

But I don't know what tactic/syntax to use to introduce the witness w above. The best I can reach so far is that Check (ex_intro _ (fun x => P x -> False) x H0)). gives False.

Can someone explain how to introduce the existential condition, or an alternative way to finish the proof?

Thanks.

P.S. What I have for the whole theorem to prove is:

Theorem not_exists_dist :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~ (exists x, ~ P x) -> (forall x, P x).
Proof.
  unfold excluded_middle. unfold not. 
  intros exm X P H x.

  destruct (exm (P x)).
    apply H0.
    Check (H (ex_intro _ (fun x => P x -> False)  x H0)).

Upvotes: 2

Views: 1614

Answers (2)

eponier
eponier

Reputation: 3122

Here, since you already know how to construct a term of type False, you can add it to the context using pose proof. This gives:

pose proof (H (ex_intro (fun x => P x -> False)  x H0))

You can even directly destruct the term, which solves the goal.

destruct (H (ex_intro (fun x => P x -> False)  x H0))

Another way to finish your proof is to prove False. You can change the goal to False with tactics like exfalso or contradiction. With this approach, you can use hypotheses of the form _ -> False that are otherwise difficult to manipulate. For your proof, you can write:

exfalso. apply H. (* or directly, contradiction H *)
exists x. assumption.

Upvotes: 2

Vinz
Vinz

Reputation: 6047

You could use the assert tactic:

assert(w: exists x, P x -> False).

It will ask you to prove this statement in a new sub-goal, and will add w to your existing goal. For this kind of trivial proof, you can inline the proof directly:

assert(w: exists x, P x -> False) by (exists x; exact H0).

Upvotes: 2

Related Questions