Theorem Proving In Lean 4

Stream: new members

[Robert Culling]

Hello :)

I'm working my way through the Theorem Proving in Lean 4 guide. I am working in a bit of a vacuum as no one in my department (UC, New Zealand) is particularly interested in LEAN. So I was hoping to get some thoughts on my code and answers to a few questions I have.

First, how do I embed code examples nicely as in comments above?

[Bryan Gin-ge Chen]

Welcome! Check out this link: #backticks

[Robert Culling]

Thank you Bryan :)

As part of the exercises I wrote the following example.

theorem EXPAND_and_over_or {p q r : Prop} (w : p ∧ (q ∨ r)) : (p ∧ q) ∨ (p ∧ r) :=
  have wp : p := And.left w
  have wqOr : q ∨ r := And.right w
  Or.elim wqOr
    (λ wq : q =>
      have wpAq : p ∧ q := And.intro wp wq
      show (p ∧ q) ∨ (p ∧ r) from Or.intro_left (p ∧ r) wpAq)
    (λ wr : r =>
      have wpAr : p ∧ r := And.intro wp wr
      show (p ∧ q) ∨ (p ∧ r) from Or.intro_right (p ∧ q) wpAr)

#check EXPAND_and_over_or

The #check returns the following unexpected output

EXPAND_and_over_or : ?m.478 ∧ (?m.479 ∨ ?m.480) → ?m.478 ∧ ?m.479 ∨ ?m.478 ∧ ?m.480

Can someone explain what the ?m.478 etc. are? Why aren't the types p,q,r in there?

[Bryan Gin-ge Chen]

I believe the ?m are there because you used curly braces for p, q, r, so they're treated as implicit variables and Lean gives them temporary names. (I haven't read TPiL4 yet but assuming it's like the Lean 3 version they should be covered in there fairly early on...).

If you write #check @EXPAND_and_over_or, you should see p, q, and r (@ turns all implicit variables into explicit ones and should also be covered in TPiL4).

[Robert Culling]

@Bryan Gin-ge Chen thank you :) Removing the explicit typing of p q r fixed that issue.

[Kevin Buzzard]

@Robert Culling I also learnt lean in a vacuum and let me assure you that a combination of solving problems by writing code and asking questions here when you're not sure can work fine as a pathway to learning lean

[Robert Culling]

@Kevin Buzzard thanks for your message :) I'm enjoying the process. I wrote my thesis on the algebraic geometry of semirings, so I am aiming to learn what is required to formalize the statements and proofs of those theorems.