Zulip Chat Archive

Stream: new members

Topic: Proving that a type is inhabited


Rajesh Jayaprakash (Sep 27 2021 at 07:11):

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 (Sep 27 2021 at 07:19):

You should read #backticks

Patrick Massot (Sep 27 2021 at 07:20):

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

Patrick Massot (Sep 27 2021 at 07:20):

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

Patrick Massot (Sep 27 2021 at 07:21):

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 (Sep 27 2021 at 07:22):

You can fix that by writing

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

Patrick Massot (Sep 27 2021 at 07:23):

@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 (Sep 27 2021 at 08:06):

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 (Oct 02 2021 at 20:51):

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 (Oct 02 2021 at 21:29):

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


Last updated: Dec 20 2023 at 11:08 UTC