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

Link:: https://stackoverflow.com/q/33140390

Display all goals and responses

Question

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

I have the following intermediate proof state:

1 subgoal

  X : Type
  P : X -> Prop
  x : X
  H0 : P x -> False
  H : (exists x : X, P x -> False) -> False
  ============================
  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 (H (ex_intro (fun x => P x -> False) x H0)).H (ex_intro (fun x : X => P x -> False) x H0)
     : False
X: Type
P: X -> Prop
x: X
H0: P x -> False
H: (exists x : X, P x -> False) -> False
P x

gives False.

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

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).excluded_middle ->
forall (X : Type) (P : X -> Prop),
~ (exists x : X, ~ P x) -> forall x : X, P x
Proof.excluded_middle ->
forall (X : Type) (P : X -> Prop),
~ (exists x : X, ~ P x) -> forall x : X, P x
  unfold excluded_middle, not.(forall A : Prop, A \/ (A -> False)) ->
forall (X : Type) (P : X -> Prop),
((exists x : X, P x -> False) -> False) ->
forall x : X, P x
  intros exm X P H x.exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
P x
  destruct (exm (P x)).exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
H0: P x
P x
exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
H0: P x -> False
P x
  -exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
H0: P x
P x apply H0.
  -exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
H0: P x -> False
P x Check (H (ex_intro (fun x => P x -> False)  x H0)).H (ex_intro (fun x : X => P x -> False) x H0)
     : False
exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
H0: P x -> False
P x

A: Note that it is not necessary to unfold excluded_middle or not to use them.

Answer (eponier)

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)).exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
H0: P x -> False
H1: False
P x

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.exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
H0: P x -> False
False apply H. (* or directly, contradiction H *)exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
H0: P x -> False
exists x : X, P x -> False
    exists x.exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
H0: P x -> False
P x -> False assumption.

Q: Thanks. It's interesting because I tried

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

but it didn't work. Could you explain why destruct worked here instead?

A: Actually, it works for me. Maybe it is due to the underscore you are using. ex_intro expects 4 parameters, but the first one is implicit, so it is not needed to specify it. I will edit my answer. But I do not understand why it passes type-checking for you.

Q: My fault, I tried inversion (not induction) trying to inversion the False. But it didn't work. Do you know why destruct/induction works while inversion doesn't?

A: It also works for me. After

    pose proof (H (ex_intro (fun x => P x -> False) x H0)).exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
H0: P x -> False
H1: False
P x
    inversion H1.

solves the goal. What did you try to inverse? Note that you must invert the hypothesis of type False, not False itself.

Answer (Vinz)

You could use the assert tactic:

assert (w: exists x, P x -> False).exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
H0: P x -> False
H1: False
exists x : X, P x -> False
exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
H0: P x -> False
H1: False
w: exists x : X, P x -> False
P x

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).exm: forall A : Prop, A \/ (A -> False)
X: Type
P: X -> Prop
H: (exists x : X, P x -> False) -> False
x: X
H0: P x -> False
H1: False
w: exists x : X, P x -> False
P x