Proving that a type is inhabited

Stream: new members

[Rajesh Jayaprakash]

Apologies if I'm overlooking something (I am new to theorem-proving).

I am working through an exercise in Chapter 4 of "Theorem Proving in Lean":

open classical
variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop

example : r → (∃ x : α, r) :=
begin
  intro h,
  have y : α,
  tactic.swap,
  exact exists.intro y h,
  -- stuck here
end

I am stuck at the indicated point, where the state of the system is:

α: Type u_1
r: Prop
h: r
⊢ α

and the goal is to establish that an object of type α exists. I am not sure how to do this (investigation reveals that the use of inhabited types could be an approach, but α is not an inhabited type).

I am not even sure whether the proof approach I have taken is the right one.

Any help would be greatly appreciated. Thanks!

(Edited to add code formatting)

[Patrick Massot]

You should read #backticks

[Patrick Massot]

Next, your issue is a bit subtle. You're not trying to solve the problem that was set, for a subtle reason

[Patrick Massot]

Because you are using tactics that are introduced only in the next chapter

[Patrick Massot]

A side effect that would be a bit long to explain is that Lean doesn't know you meant to include the a variable

[Patrick Massot]

You can fix that by writing

example (a : α)  : r → (∃ x : α, r) :=
begin
-- ...
end

[Patrick Massot]

@Jeremy Avigad We've seen many beginners having this issue. I think you should put a in the example statement (or use include but that may be distracting)

[Rajesh Jayaprakash]

Thanks Patrick. The thought of changing the example to include something like (a : α) did cross my mind, but I wanted to see if I was missing something and the proof could be done without that. Re: #backticks - thanks for the suggestion, that was lazy of me :-)

[Jeremy Avigad]

Done! https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html#the-existential-quantifier
@Leonardo de Moura let me know if I can do anything to help maintain the Lean 4 version.

[Leonardo de Moura]

@Jeremy Avigad Thanks for offering. The help is very welcome. You should have write access to it too. BTW, we are using mdbook to write all Lean documentation.