What code does a simple theorem create?

Stream: new members

[Josh]

Trying to get a better feel for how theorems are represented in Lean.
If I have a theorem like this:

theorem probably_not_useful
  {α : Type*}
  [ag: add_group α]
  {a b : α}
  (h₁ : a = 0)
  (h₂ : b = 0)
  : a + b = 0
  := begin
    rewrite h₁,
    rewrite h₂,
    simp
  end

Doing #check @probably_not_useful shows ∀ {α : Type u_1} [ag : add_group α] {a b : α}, a = 0 → b = 0 → a + b = 0. What would be the equivalent code for writing such a function 'the long way'?

def the_long_way
  {α : Type*}
  [ag: add_group α]
  {a b : α}
  (h₁ : a = 0)
  (h₂ : b = 0)
  : a + b = 0
  := sorry

[Scott Morrison]

Do you mean "in term mode"? (as opposed to tactic mode)

[Josh]

I believe so, I'm not entirely familiar with the terminology.

[Scott Morrison]

(Changing theorem to def was as mistake, I think.)

[Josh]

Alright, I thought that theorem meant the use of tactics

[Scott Morrison]

No. theorem is for propositions, def is for definitions (/constructions)

[Scott Morrison]

The difference is that theorem will be checked "in parallel", while Lean already continues on to later lines. This is possible because of proof irrelevance.

[Josh]

But doesn't the first code snippet create a function on propositions, not a proposition itself?

[Scott Morrison]

You might be confused here because often beginners are advised to not use tactics in definitions (i.e. when constructing data).

[Scott Morrison]

Hmm... an implication between propositions (which is the same thing as a function between propositions) is itself a proposition.

[Scott Morrison]

(I'm not sure if you've internalised the idea yet that when we represent propositions in type theory, implication is the same thing as a function.)

[Scott Morrison]

Also, check #mwe: you should add import algebra.group or something similar to your code snippet, so others can copy and paste directly into Lean.

[Josh]

I think I have internalized that. A theorem is the same thing as a function from the assumptions to the conclusion.

[Josh]

The code is working for me without any imports, I found add_group in the standard Lean library

[Scott Morrison]

You can always see what the term mode proof produced by tactics was using #print instead of #check. In this case it is:

theorem probably_not_useful : ∀ {α : Type u_1} [ag : add_group α] {a b : α}, a = 0 → b = 0 → a + b = 0 :=
λ {α : Type u_1} [ag : add_group α] {a b : α} (h₁ : a = 0) (h₂ : b = 0),
  (id (eq.rec (eq.refl (a + b = 0)) h₁)).mpr
    ((id (eq.rec (eq.refl (0 + b = 0)) h₂)).mpr
       ((id
           (((λ (a a_1 : α) (e_1 : a = a_1) (ᾰ ᾰ_1 : α) (e_2 : ᾰ = ᾰ_1), congr (congr_arg eq e_1) e_2)
               (0 + 0)
               0
               (add_zero 0)
               0
               0
               (eq.refl 0)).trans
              (propext (eq_self_iff_true 0)))).mpr
          trivial))

[Scott Morrison]

Oh! You may be using a really ancient version of Lean. Which Lean do you have?

[Josh]

3.4.2

[Scott Morrison]

Ah, that is ancient.

[Josh]

hm, alright.

[Josh]

But that command is super helpful, I'll play around with it to get a better understanding.

[Scott Morrison]

You likely want to throw out whatever you installed, and visit https://leanprover-community.github.io/get_started.html#regular-install

[Scott Morrison]

Have you started reading one of the tutorials?

[Scott Morrison]

#print is always going to produce disgusting term mode proofs if you're using rw and simp in your proof. Not really for human consumption. :-)

[Josh]

Yeah, I had followed that and started working with the Tutorials and Mathematics In Lean projects. Being curious about how everything works under the hood, I got stuck trying to see the connection between tactic proofs and the rest of the language.

[Bryan Gin-ge Chen]

You might enjoy #tpil then; it goes a bit more into the type theory than those tutorials.

[Josh]

Cool, I'll check it out!

[Josh]

Looks like I had installed lean awhile ago and just needed to run elan update