Zulip Chat Archive

Stream: new members

Topic: existential quantifier in a goal


view this post on Zulip Claus-Peter Becke (Sep 09 2020 at 15:05):

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?

view this post on Zulip Ruben Van de Velde (Sep 09 2020 at 15:14):

So this is false, is it not?

view this post on Zulip Ruben Van de Velde (Sep 09 2020 at 15:15):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 09 2020 at 15:15):

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

view this post on Zulip Claus-Peter Becke (Sep 09 2020 at 15:18):

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

variable r : Prop

view this post on Zulip Bryan Gin-ge Chen (Sep 09 2020 at 15:20):

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.

view this post on Zulip Claus-Peter Becke (Sep 09 2020 at 15:24):

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.


view this post on Zulip Claus-Peter Becke (Sep 09 2020 at 15:24):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 09 2020 at 15:27):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 09 2020 at 15:28):

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).

view this post on Zulip Claus-Peter Becke (Sep 09 2020 at 15:29):

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


Last updated: May 11 2021 at 21:10 UTC