actual meaning of `:=`

Stream: new members

[rzeta0]

This is a question about the := symbol in Lean.

As I haven't ever come across official documentation or explanation about what it means, I have - I suspect like most people - worked out what it means by seeing examples of how it is used.

So I want to check my understanding.

Consider

S := P

Here S and P are Lean code. I expect we can be more specific and say S and P are expressions.

We then say that whenever we see a S := P, we can read it as S is justified (proven) by P.

Question 1: Must S and P be expressions? Are they always expressions?

Question 2: Is the only use of := of the form S := P which is S justified by P.

[Mark Fischer]

I don't really know the answer, though I think a first approximation is perhaps better worded as "S is defined as P"

If S has some type T, then you can say something like "S : T := P" means P is a justification that T is inhabited. Which if T is a proposition, is the same thing as a proof of T.

If something is definitionally true, it's typically easy to prove an equality:

def foo: S = P := rfl

In this case, we know the proposition S = P is true, because rfl is an acceptable as a definition for foo. I think.

[Jireh Loreaux]

S := P indeed means "S is defined as P". You can think of this as saying the named constant S is an abbreviation (although not in the technical sense I will describe in a moment) for the term P.

Although this is a definitional equality, it turns out that there are different transparency settings for definitional equality. S := P uses the default transparency, however, there also exist reducible and irreducible transparencies (as well as reducible and instances). In order from most to least transparent, these are:

• reducible
• reducible and instances
• default
• irreducible

Note that when you write abbrev S := P, this means S := P at reducible transparency (this is the technical sense of abbreviation that I mentioned above). You can also write irreducible_def S := P to get a definition at irreducible transparency.

[Jireh Loreaux]

For more information, you can see this post which may provide some more detail. (there, Mario also discusses syntactic equality via notation, which is even more transparent than reducible definitional equality, and wrapping things in a structure, which is even less transparent than irreducible equality; it is no longer definitional. Although he does not mention the "reducible and instances" setting, which is a bit technical anyway)