Theorem vs definition

Stream: new members

[jsodd]

I have a strange question about the implementation of theorem and def. If I understand correctly, theorem th1 : P := x should be read as "expression th1 defined byth1 := x has type P, where P : Prop", and proving a theorem that P is true amounts to constructing any expression of type P (equivalently, there exists _ : P or P is non-empty). So the only thing that matters is that types check out, right?

Does it mean that def is technically the same as theorem and the main difference is that it admits expressions of types other than P : Prop?

[Daniel Weber]

IIRC after a theorem has been verified the proof is erased, because due to proof irrelevance it shouldn't matter, but that's it

[Kevin Buzzard]

In recent Leans you now get an error if you try and use theorem to define data. You can still use def to prove a theorem though :-) But yes they're both "we attach a name to this term of this type".

[jsodd]

And there is absolutely no difference between theorem and lemma, right?

[Damiano Testa]

"absolutely no difference" can be taken very literally: "sure there is a difference, one starts with t, the other with l". :upside_down:

In looser terms, there is indeed no difference between them!

[Kevin Buzzard]

Indeed many of the CS people argue that lemma should simply be removed because it's the same as theorem, and many of the maths people argue that the two terms play different roles psychologically. lemma isn't even a thing in Lean IIRC, it's a mathlibism.

[jsodd]

Thanks, good to know :+1:

[jsodd]

I would definitely keep lemma, and I would also add propositions to make it even closer to how I think about hierarchy of a theory. But this is a taste matter.

[Damiano Testa]

As of a few days ago, you can actually "activate" lemma in any project depending on Batteries using set_option lang.lemmaCmd true.

[Kevin Buzzard]

The CS argument (which I don't really understand) is something like: it's not good to have different ways of doing the same thing, and also something about language fragmentation or something?

[jsodd]

By the way, is there a way to hide an item (theorem, instance, class, def, ...) from the documentation?

[Julian Berman]

Kevin Buzzard said:

The CS argument (which I don't really understand) is something like: it's not good to have different ways of doing the same thing, and also something about language fragmentation or something?

(With the caveat that I'm a programmer, not a computer scientist, and that you're repeating an argument you don't agree with so clearly there could be more to the other side's argument, but "these two things have different semantic interpretations so we wish to give them separate names" is a very valid reason in a programming context to have 2 things which have the same implementation)

[Ruben Van de Velde]

(Though only, IMO, if you then actually consistently distinguish them - because otherwise you can't use the different semantic interpretation)

[Jireh Loreaux]

There was talk of requiring theorems to have docstrings (at least in Mathlib), which would provide a distinguishing element, but I don't know that we ever completely decided upon that.

[jsodd]

Regarding docstrings, I wanted to ask whether there is a way to hide some of the theorems/definitions/... from documentation