existential quantifier in a goal

Stream: new members

[Claus-Peter Becke]

I stick to the problem of removing an existential quantifier from a goal. The situation is the following one:

example : r → (∃ x : α , r) :=
begin
    intro h1,
end

This is what follows:

tactic failed, there are unsolved goals
state:
α : Type u_1,
r : Prop,
h1 : r
⊢ ∃ (x : α), r

The first thing I don't really understand is the relationship between the bound variable x of type alpha and the proposition r. As far as I see doesn't exist a relationship between them. It is asserted that there is an x of type alpha and a proposition r. The variable x doesn't belong to that proposition.
If the bound variable were part of a hypothesis I could choose an x_0 as a value for x. But in the actual context that doesn't work. If there were an arithmetic expression inside the goal I could apply the use-tactic to supply x with a value. But that doesn't work here neither. Which other possibilities to solve this problem are suitable?

[Ruben Van de Velde]

So this is false, is it not?

[Ruben Van de Velde]

You need to know that there exists a value of type alpha in the first place

[Bryan Gin-ge Chen]

You haven't given a #mwe. Do you have some variables declarations above which you didn't include in your message?

[Claus-Peter Becke]

I'm sorry. Yes, I had declared the variable r the following way:

variable r : Prop

[Bryan Gin-ge Chen]

Presumably you also have variable α : Type* as well. But in any case, as Ruben says, if you don't know anything else about α then your example is unprovable.

[Claus-Peter Becke]

This example is part of the descriptions in "Theorem Proving in Lean", Release 3.18.4, p. 46.
These declarations are given with respect to alpha.

[Claus-Peter Becke]

variables (α: Type*) (p q : α → Prop)

[Bryan Gin-ge Chen]

Ah, I see. More importantly, there's a variable a : α which makes the example provable again.

[Bryan Gin-ge Chen]

By the way, in this part of the book I think you're meant to be trying to write proofs in "term mode" (without use of tactics).

[Claus-Peter Becke]

Ok, thank you for your hints. Then I will try that way.