Taxonomy

Stream: new members

[rzeta0]

Following a good but long discussion in another thread, I've written up a blog to briefly explain just enough (for beginners) about:

• universe, types and terms
• the initially odd idea that proofs are elements of propositions
• explaining how using hypotheses in proofs is actually using proofs of propositions

I'd welcome feedback / corrections: https://leanfirststeps.blogspot.com/2024/10/appendix-taxonomy.html

app_taxonomy.png

[Kyle Miller]

13 = 2*6+1 is a proposition, not a proof. rfl is an example of a proof.

[Arthur Paulino]

Maybe this clarifies:

#check Eq 13 (2 * 6 + 1) -- 13 = 2 * 6 + 1 : Prop

[Arthur Paulino]

If you perform a "go to definition" on =, it should take you to Notation.lean from core, highlighting the following line:

macro_rules | `($x = $y)  => `(binrel% Eq $x $y)

That is, a = b is syntax sugar for Eq a b

For further investigation, it might be worth checking the definition of Eq. The docstring is quite rich

[Arthur Paulino]

And this is a very raw example:

example : Eq 3 3 := Eq.refl 3

[rzeta0]

I think this has made realise I don't actually know what a proof is, despite having written many of them in lean exercises!

Consider Odd 13. This is a proposition, I think we can agree on this.

The following is a lean proof if this proposition:

import Mathlib.Tactic

example : Odd (13: ℤ)  := by
  use 6
  norm_num

So my understanding that example is the proof of the proposition Odd (13:ℤ), but example is a special case where the name of the proof is discarded and cannot be referred to later.

In any case, the code after := is equivalent to the proof, so the proof is all the code use 6; norm_num.

---

Here is another example:

import Mathlib.Tactic

example : IsSquare 9 := by
  use 3

Here the proposition is IsSquare 9, and the proof is use 3. Is that a better simpler example of a proof?

---

So is it the case that many proofs are actually tactics?

I guess the core question I'm asking is "what are examples of proofs?" - and I realise this is an odd question to ask given I've been writing dozens of lean proofs as I do the Mechanics of Proof course.

[Yakov Pechersky]

So is it the case that many proofs are actually tactics?

No, tactics construct the term that is the "proof term". No, example is not the proof of the proposition. Instead, example : T := term is the command that tells Lean "I am about to provide a term of type T, please check that for me, and don't worry about remembering this fact"

[Kyle Miller]

The entire expression

by
  use 6
  norm_num

evaluates to a proof.

You can use by? to see what proof it evaluates to. Don't expect to understand it! It's like trying to read assembly code from compiler output.

[Yakov Pechersky]

and it just so happens that one can construct a term using tactics because the by keyword means "I am about to give you a term through constructing it using tactics".

You might be familiar with exact. That is a keyword that says "I am about to give you a tactic that provides precisely the term to follow".

[Yakov Pechersky]

Note the dual nature between by and exact

[Kyle Miller]

You can wonder philosophically about whether by use 6; norm_num is the proof itself, but in any case, that (or what it evaluates to) is the proof, whose type is Odd (13: ℤ).

[Kyle Miller]

rzeta0 said:

"what are examples of proofs?"

Arthur has already given you an example of Eq.refl 3 as a proof.

[Edward van de Meent]

if you want to write it without tactics:

example : Odd (13: ℤ) :=
  ⟨6,rfl⟩
example : IsSquare 9 :=
  ⟨3,rfl⟩

(still cheating a bit rfl is in this case not a tactic afaik, but in spirit it is)

[Kyle Miller]

What do you mean? rfl-the-term is a theorem: https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L294

[Edward van de Meent]

huh... i didn't know that...

[Kyle Miller]

(You can "go to definition" to be sure :-))

[Kyle Miller]

You might say there's some magic to rfl though because the elaborator fills in the a argument from the expected type, though that's not magic specific to rfl.

[Edward van de Meent]

i was under the impression that there was more magic to it, i guess...

[Yakov Pechersky]

I think to be most explicit, one would use Exists.intro explicitly

[Damiano Testa]

Honestly, I find proof terms that involve rfl to be the hardest to parse. I would probably start by looking at a "chaining" proof, something like a < b -> b < c -> a < c.

[Kyle Miller]

Yeah, rfl can be a bit subtle. Anyway, @Exists.intro Nat (fun r : Nat => 9 = r * r) 3 (@Eq.refl Nat 9 : 9 = 3 * 3) is a proof of IsSquare 9, written out in detail.

example : IsSquare 9 :=
  @Exists.intro Nat (fun r : Nat => 9 = r * r) 3 (@Eq.refl Nat 9 : 9 = 3 * 3)

[Derek Rhodes]

@rzeta0 (if I may interject, the book "theorem proving in lean" starts off without tactics and immediately gets down to the nitty gritty about what proofs are and then later shows how tactics fit in starting in chapter 5)

[rzeta0]

Kyle Miller said:

The entire expression

by
  use 6
  norm_num

evaluates to a proof.

This is helpful.

I don't know what rfl or reflis so will have to appreciate those later on my journey.

[Kyle Miller]

Why wait? Here: Eq.refl a is the proof that a = a

[Arthur Paulino]

@rzeta0 I can provide the explanation I believe I would need if I were trying to understand this a while ago.

It would be simpler if I could just say that a proof is a term of a type, but it sounds strange when I say that 3 is a proof of Nat. So a more conservative approach is to say that a proof is a term of a type when this type inhabits Prop. It may still be debatable, but definitely workable. So let's take it from there.

The community has absorbed the terminology "term mode" and "tactic mode" to differentiate whether you're using the tactic DSL or not.

For example, when I say example : Eq 3 3 := Eq.refl 3, I'm literally calling the (only) constructor of the Eq type. In a way, it's similar to example : Nat := Nat.zero, but the Nat type is not parametric.

If you choose to "enter tactic mode" by starting your proof with by, it will tell Lean to spin a specific elaboration process, which is ultimately meant to produce a term of the type you're intending to inhabit. Or in other words, the type you're trying to come up with a term for.

This is not common, but take a look nevertheless because it may be strangely insightful:

def three : Nat := 3
def three' : Nat := by exact 3

[Arthur Paulino]

It may be the case that the way Lean 4 code is generally written is a bit overpowered when we're trying to get to a very detailed understanding of how things work.

One path is to just go with it, start your proof with by, live in tactic mode and get your goals closed. This is definitely a valid path for math students whose job is to actually learn and practice mathematics. But once you write that by, you're summoning a very powerful system. And at that point it's harder to point your finger at what is what.

[rzeta0]

Two last questions on this.

Question 1

Consider h: Odd 13.

I was told in the other thread that h is a proof. So why is h a proof but example not?

Question 2

What's the difference between "is a proof" and "evaluates to a proof" ?

[rzeta0]

---

@Arthur Paulino - thanks for trying hard to help. Sadly I'm still a beginner and so I didn't fully understand your examples. Maybe I will in a few weeks/months time.

In particular I wanted to understand your three and three' examples but I am not seeing the key lesson. Is the idea that by exact will eventual return something that is equivalent to 3 ?

[Ruben Van de Velde]

So, if you have

example : IsSquare 9 :=
  @Exists.intro Nat (fun r : Nat => 9 = r * r) 3 (@Eq.refl Nat 9 : 9 = 3 * 3)

then probably one would not say that the example is a proof, but @Exists.intro Nat (fun r : Nat => 9 = r * r) 3 (@Eq.refl Nat 9 : 9 = 3 * 3) is.

Say you are in the middle of a proof, and you need this fact, you can write

have H : IsSquare 9 := [... proof ...]

At this point, if you have a hypothesis h : IsSquare 9, you could write in particular

have H : IsSquare 9 := h

or you could reuse the proof of the example:

have H : IsSquare 9 := @Exists.intro Nat (fun r : Nat => 9 = r * r) 3 (@Eq.refl Nat 9 : 9 = 3 * 3)

but you could not write

have H : IsSquare 9 := example ...

[Ruben Van de Velde]

Does any of that make sense?

[Arthur Paulino]

To the question you asked me, yes. That's the idea. by exact 3 is taking a slightly longer path but it gets elaborated to 3 in the end.

[Ruben Van de Velde]

Re three and three' - at a basic level, lean deals in terms of types. 3 is a term of type Nat. Tactics - that is, everything after by- are simply a way to build terms. In particular, the exact tactic just creates the term that you write after exact.

Maybe this can help:

def f (x : Nat) : Nat := x + 1

def g (x : Nat) : Nat := f (f x)
#print g
-- def g : Nat → Nat :=
-- fun x => f (f x)

def g' (x : Nat) : Nat := by
  apply f
  apply f
  exact x
#print g'
-- def g' : Nat → Nat :=
-- fun x => f (f x)

This shows two ways of defining a function - the first (g) just has a term after the :=; the second (g') has a sequence of tactics which build up the function step by step - but in the end the two functions are exactly the same, as the #print command shows

[rzeta0]

@Ruben Van de Velde so in

have H : IsSquare 9 := h

h is a proof. Not just because it looks and acts like one, but also because it is a term of the type proposition IsSquare 9.

Am i correct up to this point.

If yes, then let's compare:

h : IsSquare 9
example : IsSquare 9
my_lemma : IsSquare 9

Why is h not like my_lemma ?

[Arthur Paulino]

Oh, that's an interesting confusion. "example" is more like "def" or "theorem". It's syntax for a different purpose

[Ruben Van de Velde]

Well, each of those are a snippet of lean code. It might help to write them out:

import Mathlib

theorem x (h : IsSquare 9) : True := by
-----------^ this is the term
  #check h
  trivial

example : IsSquare 9 := ⟨3, rfl⟩
------------------------^^^^^^^^ this is the term

theorem isSquare_nine : IsSquare 9 := ⟨3, rfl⟩
--------------------------------------^^^^^^^^ this is the term
--------^^^^^^^^^^^^^ and now this is also a term of the same type:
#check isSquare_nine

[Kyle Miller]

Mario explained example here for what it's worth.

[rzeta0]

@Ruben Van de Velde thank you, your examples have helped a lot.

Thanks also @Kyle Miller a re-reading of Mario's replies helped.

[Damiano Testa]

import Mathlib

example : IsSquare 9 := ⟨3, rfl⟩
------------------------^^^^^^^^ this is the term
-------^ the margin of the syntax is too small to store the proof

[rzeta0]

I've updated the blog to reflect the feedback here.

The only thing niggling at the back of my mind is the distinction between:

• h and by use 6; norm_num are proofs of Odd 13
• h and by use 6; norm_num evaluate to proofs of Odd 13

Is this a bigger issue than I think it is? Should I be making a distinction?

[Arthur Paulino]

If we go by what I said above:

So a more conservative approach is to say that a proof is a term of a type when this type inhabits Prop.

Then I would say that h is a proof and by use 6; norm_num evaluates to a proof.

Note that elaboration is not context-free so something you write with the tactics DSL may or may not prove a theorem.

def forty_two := 42
example : forty_two = 42 := by simp -- simp made no progress

@[simp] def forty_two' := 42
theorem foo : forty_two' = 42 := by simp -- success
#print foo -- theorem foo : forty_two' = 42 := of_eq_true (eq_self 42)
example : forty_two = 42 := of_eq_true (eq_self 42) -- success

We can't just say that by simp is a proof of forty_two = 42. But when I tagged the definition of forty_two' with @[simp], it was added to the search space of the simp tactic, allowing it to produce a proof of forty_two' = 42 for me.

And notably, the same proof worked for forty_two = 42.

[Arthur Paulino]

But look, the term "proof" can be highly conflating, as it would be annoying and unnecessarily pedantic to fight the natural use of the word.

If a professor tells the students to write a proof of a theorem and they use the tactics DSL, everyone will be happy and that's totally fine. Although you can argue that Lean 4 was probably the one putting the pieces together and creating the proof term.

[Arthur Paulino]

If you can't make peace with imprecision, then you can just use the verb "prove the following theorem(s)" and the students will join forces with Lean 4 to produce the proof(s)