How To Prove it in Lean Example_3_2_4

Stream: new members

[zigzagdoom]

Hi all,

I am new to lean and using the book here:

https://djvelleman.github.io/HTPIwL/IntroLean.html

The first example is given as follows:

theorem Example_3_2_4
    (P Q R : Prop) (h : P → (Q → R)) : ¬R → (P → ¬Q) := by
  assume h2 : ¬R
  assume h3 : P
  have h4 : Q → R := h h3
  contrapos at h4            --Now h4 : ¬R → ¬Q
  show ¬Q from h4 h2
  done

This is a very readable proof, but I cannot get it to work due to the word assume being an unknown identifier.

I am using Lean version 4.5.0-rc1, commit b614ff1d12bc, Release

Could someone please point me in the right direction so I may continue my journey?

[Mauricio Collares]

Can you double-check you followed the instructions at https://djvelleman.github.io/HTPIwL/, specifically the one paragraph starting with "You will also need the Lean package that accompanies this book"?

[Mauricio Collares]

The reason I'm asking is because the assume tactic is implemented in the book itself, and therefore will only work inside the Lean package/project you download in those instructions.

[Dan Velleman]

Right. The assume tactic is defined in the package that accompanies the book.
Note that, since the book uses some custom tactics defined in that package, what it teaches is not exactly standard Lean. There is an appendix about transitioning from the version of Lean in the book to standard Lean.
The book is primarily intended to help you learn to write proofs, especially in conjunction with the book How To Prove It. If your primary interest is learning Lean, rather than learning to write proofs, you can use the book, but you'll then have to learn how to switch to standard Lean. In that case, you might want to consider other resources.

[zigzagdoom]

Mauricio Collares said:

The reason I'm asking is because the assume tactic is implemented in the book itself, and therefore will only work inside the Lean package/project you download in those instructions.

Thanks @Mauricio Collares !

I downloaded and restarted vscode a few times and it seems it be working now (or at least building something). Didn't realise the assume tactic was implemented in the book - that is interesting indeed.

[zigzagdoom]

Dan Velleman said:

Right. The assume tactic is defined in the package that accompanies the book.
Note that, since the book uses some custom tactics defined in that package, what it teaches is not exactly standard Lean. There is an appendix about transitioning from the version of Lean in the book to standard Lean.
The book is primarily intended to help you learn to write proofs, especially in conjunction with the book How To Prove It. If your primary interest is learning Lean, rather than learning to write proofs, you can use the book, but you'll then have to learn how to switch to standard Lean. In that case, you might want to consider other resources.

Thanks @Dan Velleman - I am actually interested in learning how to prove (lean being a kind of strict tutor for now) - thanks for putting the book together

[Dan Velleman]

Sounds like the book is right for you. Good luck.
I'll be interested to hear if you run into any more problems with the installation process. I don't have much experience with the current installation process--I installed Lean a while back, but things have changed since then. The book describes my current understanding of the installation process, and links to a couple of web pages with more info. But my experience with installation was not great--there were plenty of glitches before I got things working right.
One thing you should know about the "build" process: That process used to be very slow, because Lean had to "build" not only the files in the How To Prove It package, but also files in Lean's mathematics library, Mathlib. There was an extra step you could do to speed that process up by downloading already-built files for Mathlib. But the process has been improved and that downloading should now happen automatically, so the build process shouldn't take too long--just a few minutes, I think. Let me know if you run into further problems.

[zigzagdoom]

Dan Velleman said:

Sounds like the book is right for you. Good luck.
I'll be interested to hear if you run into any more problems with the installation process. I don't have much experience with the current installation process--I installed Lean a while back, but things have changed since then. The book describes my current understanding of the installation process, and links to a couple of web pages with more info. But my experience with installation was not great--there were plenty of glitches before I got things working right.
One thing you should know about the "build" process: That process used to be very slow, because Lean had to "build" not only the files in the How To Prove It package, but also files in Lean's mathematics library, Mathlib. There was an extra step you could do to speed that process up by downloading already-built files for Mathlib. But the process has been improved and that downloading should now happen automatically, so the build process shouldn't take too long--just a few minutes, I think. Let me know if you run into further problems.

Thanks @Dan Velleman - absolutely I will in case I run into any issues.