difference `let` and `have`

Stream: new members

[Filippo A. E. Nuccio]

I am struggling in understanding the sentence "The difference between let and have is that let introduces a local definition in the context, so that the definition of the local constant can be unfolded in the proof." from the Lean Book.

[Filippo A. E. Nuccio]

In practice, it seems to me that if I want to introduce an object (say, a set) and then state that it has more structure, I should type

let X := {x in Z | x is even}
let X : is a subgroup

whereas I would have expected the right tactic to be

let X := {x in Z | x is even}
have hX : X is a subgroup

I suspect that some type-business is hidden under the scene, as X cannot be a subgroup if it is a set. At any rate, my first question is about the difference between let and have and, secondly, about the "right" tactic to introduce an object, giving it a name, and then stating some properties of it.

[Reid Barton]

A bit difficult to say more than the book does without a more precise example.

[Reid Barton]

In general, for Props, use have. For data, use let v : T := e if the rest of the proof is going to need use the fact that v equals e, otherwise you can use have here as well.

[Filippo A. E. Nuccio]

Well, in my example, I have a maximal ideal $M$ in a ring $R$ and I am defining its "inverse", as fractional ideal in the fraction field $K$: the localization map is $f$. So what I did was
let M1 := {x : K | ∀ y ∈ M, f.is_integer (x * f.to_map y)}, have M1 : fractional_ideal f,
having in mind that $M1$ was the definition of a subset of $K$, and the second line was my claim that it is indeed a fractional ideal. But this creates two hypothesis called M1, whereas I got the advice of writing
let M1 := {x : K | ∀ y ∈ M, f.is_integer (x * f.to_map y)}, let M1 : fractional_ideal f,
which indeed does the job, but I am puzzled both from the fact that saying "let M1" twice sounds odd, and also in properly understanding what's the difference.

[Reid Barton]

I think you should check the definition of fractional_ideal

[Reid Barton]

I am also confused why you have two definitions both called M1

[Reid Barton]

have M1 : fractional_ideal f,
this couldn't possibly be correct, since it contains no reference to the original M1, unless there are more lines in between

[Reid Barton]

You seem to be imagining that fractional_ideal is something like "is_fractional_ideal", but it couldn't be because where is the ideal then?

[Reid Barton]

In the second one, I assume your definition of the second M1 refers to the first M1?

[Filippo A. E. Nuccio]

In the second I wanted to state "M1 belongs to the set of fractional ideals wrt f

[Reid Barton]

Oh I see, but that's not how let/have work

[Reid Barton]

(it's also not how types work)

[Filippo A. E. Nuccio]

I see. Can you explain a bit more?

[Reid Barton]

have M1 : fractional_ideal f means exactly the same as have M7 : fractional_ideal f except that the new variable is called M1 instead of M7

[Reid Barton]

if you reuse the name M1, it just means you end up with two variables with the same name (generally undesirable)

[Filippo A. E. Nuccio]

And what do they (both) mean?

[Reid Barton]

And, you can never prove a statement of the form "such-and-such expression has such-and-such type" which seems to have been what you were trying to express

[Reid Barton]

well, they both introduce a variable of type fractional_ideal f

[Filippo A. E. Nuccio]

Ah, I see.

[Filippo A. E. Nuccio]

I really need to run now, I will try to contact you later - or study more! Thanks in advance, at any rate.

[Filippo A. E. Nuccio]

Here I am again-could you speculate a bit on your sentence that " one can never prove a statement of the form such-and-such expression has such-and-such type"? Do you mean that every expression comes with its type and it won't change forever?

[Jalex Stark]

every term has a type which does not change

[Filippo A. E. Nuccio]

But do subgroups and normal subgroups have the same type?

[Jalex Stark]

i think normal is a predicate on subgroups, something like is_normal : subgroup G \to Prop

[Filippo A. E. Nuccio]

So, if submodule is a predicate on (sub)sets, I can prove something like

let M1 := {x : K | ∀ y ∈ M, f.is_integer (x * f.to_map y)},
have M1 : fractional_ideal f,

[Filippo A. E. Nuccio]

meaning, with the second line, that the first line is a fractional ideal

[Jalex Stark]

no

[Jalex Stark]

t : T only makes sense when T is the type of t

[Jalex Stark]

the type of M1 is set K

[Jalex Stark]

if you have a predicate is_fractional_ideal : set K \to Prop

[Jalex Stark]

then you could write have hM1 : is_fractional_ideal M1

[Filippo A. E. Nuccio]

ahah! That's what I was looking for, I guess.

[Jalex Stark]

then you get a goal of type is_fractional_ideal M1

[Jalex Stark]

after you prove it, you'll have a local variable called hM1 which can be thought of as storing the proof

[Filippo A. E. Nuccio]

Is the is_ construction automatically built by Lean when one defines something?

[Jalex Stark]

no

[Jalex Stark]

I was giving hypothetical names because I'm not familiar with this part of the library

[Filippo A. E. Nuccio]

Ah, ok: so, the existence of fractional_ideal (which I know to exist) does not imply the existence of is_fractional_ideal

[Jalex Stark]

let me go look at docs#fractional_ideal

[Filippo A. E. Nuccio]

(although I suspect this second to exist as well, I am trying to dig into the construction of those things)

[Filippo A. E. Nuccio]

Have you found a "predicate" that seems to do the trick? I haven't, but I might have overlooked it.

[Reid Barton]

If you click on "Equations" (or just view source) you can see the associated predicate is called is_fractional

[Reid Barton]

(Presumably, you were going to have to look at the definition of fractional_ideal next no matter what?)

[Filippo A. E. Nuccio]

OkOk, I see the problem I was facing. And going back to the first question, after having defined M1 with let, should I type

have hM1 : is_fractional M1

or

let hM1 : is_fractional M1

?

[Jalex Stark]

use have hM1 : is_fractional M1,

[Jalex Stark]

that's telling lean: I want to prove this proposition is_fractional M1 in tactic mode and then forget about the proof, but keep the statement and call it hM1

[Kevin Buzzard]

@Filippo A. E. Nuccio as a mathematician coming into this, it can be a bit confusing. There are two ways of working with mathematical objects in Lean -- a "bundled" way and an "unbundled" way. The other thing you to know is how to orientate your self in Lean's type universe -- there are universes, types and terms. In the universe Type, the types are what we think of as sets and the terms are what we think of as their elements. In the Prop universe, the types are what we think of as theorem statements, and the terms are what we think of as proofs.

So now let me tell you about groups and subgroups. For whatever reason, the way you say "let G be a group" in Lean is that you make a term G : Type (i.e. a set), and then we make a term called something silly like _inst_1 of type group G. The type group G is a type, so it's what we think of as a set, and it's the set of all group structures on the set G. So a term of type group G is the data of a multiplication, identity and inverse, plus also the proofs of all the group axioms. The reason the term of type group G has a weird name is that we users never have to say that name in our code -- you write [group G] in square brackets and that means "leave Lean's type class inference system to deal with all the group structure on G automatically" -- which means that if a b : G you can write a * b and Lean will know what you mean.

Now subgroups are dealt with in a completely different way. If G is a group then G : Type and if H is a subgroup then it turns out that H is not a type, it is a term. There is a type subgroup G, which is a type, so it's a set in our language, and it's the set of all subgroups of G. So H : subgroup G means H is a subgroup of G, and so H is actually something like a quadrauple of data under the hood, it's a subset and three proofs (that it's closed under multiplication, inverse and identity).

If you want to work with fractional ideals you really should read the docstring at the top of fractional_ideal.lean. This tells you all the names of all the important functions and definitions. Finding them in the lean file itself and hovering over them will tell you the types of all these terms, and then you have to start thinking very clearly about what is bundled and what isn't. For example, fractional_ideal f is the type of fractional ideals in P (using notation from the docstring) so a term of type fractional_ideal f is a fractional ideal, which means that it is some sort of n-tuple encoding all the things which a mathematician needs to make a fractional ideal. In particular its name will not be the same as the name of the underlying submodule, which is a different thing because it has a different type.

[Kenny Lau]

@Kevin Buzzard is this the start of a blogpost?

[Patrick Massot]

Please please stop this. Each new message or blog post where Kevin repeats that mathematicians should replace Type by "set" and set by "subset" is simply adding confusion for no good reason.

[Kevin Buzzard]

I know this winds you up Patrick, but this is how to teach a beginner with no knowledge of type theory how to think about types and terms in the context of something they already understand.

[Patrick Massot]

But you are teaching something wrong. What's the point?

[Mario Carneiro]

Why do you say it's wrong? This is literally how the model of lean in set theory works

[Mario Carneiro]

so people from a set theory background (inasmuch as this is true for traditional mathematicians) expect this kind of terminology

[Patrick Massot]

The model is not the real thing, and it comes with a lot of extra junk that encourages bad intuition.

[Mario Carneiro]

Now there is an additional bit of learning to make a new distinction in type theory that did not exist in set theory (namely the difference between a set-in-itself and a set-as-subset-of-another), but that can be taught separately

[Mario Carneiro]

if you want to draw a parallel between concepts in set theory and concepts in type theory, this is the right parallel

[Patrick Massot]

We now have a lot of data proving this parallel is harmful when learning.

[Mario Carneiro]

"the model is not the real thing" that depends on your religion

[Scott Morrison]

I think it's best to get out of the way early the explanation about types and sets, but then, as soon as possible, to stop conflating them.

[Scott Morrison]

Certainly when Kevin says "There is a type subgroup G, which is a type, so it's a set in our language." I get sad. :-)

[Scott Morrison]

If that sentence is to make any sense it should be "so it's a set in the old language"?

[Patrick Massot]

Exactly, this kind of sentence if just piling up confusion.

[Mario Carneiro]

I guess you could also use a vaguer word like "collection" there

[Mario Carneiro]

"The type subgroup G is the collection of all subgroup structures on G"

[Mario Carneiro]

but that sentence doesn't seem especially wrong to me even if you substitute the word "set" in for "collection"

[Patrick Massot]

That sentence is just wrong whatever the interpretation.

[Mario Carneiro]

it's not, that's literally what the type represents

[Patrick Massot]

Did you really intended to put those "sub" here?

[Mario Carneiro]

what sub? the one in "subgroup"?

[Patrick Massot]

yes

[Patrick Massot]

Because the sentence you get from removing both "sub" makes sense.

[Mario Carneiro]

um yes, that's the name of the mathematical concept

[Mario Carneiro]

The collection of all group structures on G is a completely different type

[Mario Carneiro]

I'm talking about subgroup G

[Mario Carneiro]

I think I see the confusion, the sentence is also true if you replace subgroup with group

[Patrick Massot]

A term with type subgroup G is not a structure on G.

[Scott Morrison]

I think Patrick's complaint in this sentence is that a "subgroup structure" is an alien concept.

[Mario Carneiro]

I could say "subgroup of G" but that just sounds circular

[Mario Carneiro]

and "subgroup structure" makes it clearer that it's more like a tuple than a set

[Patrick Massot]

Aren't we discussing how to make things clearer, not more obscure?

[Mario Carneiro]

I should hope so

[Anatole Dedecker]

If I understand correctly @Patrick Massot means that although group G designates the types group-structure on G, whereas subgroup G designates the types of subgroups of G, not a "structure of subgroup"

[Mario Carneiro]

it is the type of all subgroup structures of G

[Mario Carneiro]

as in, an element of the type is a subgroup structure

[Patrick Massot]

Mario, that's simply not what mathematicians call structures. That's the programming language notion of structure.

[Patrick Massot]

Anyway, this conversation is going nowhere.

[Mario Carneiro]

tuple?

[Patrick Massot]

I'll stop it.

[Mario Carneiro]

give me something to work with here

[Patrick Massot]

(but feel free to continue without me)

[Mario Carneiro]

you are just asserting that things aren't clear without suggesting any alternative

[Anatole Dedecker]

Maybe that's a french thing, but to me a "a group structure on a set/type G" designates the things we add to the "raw" G to make it behave like a group. That is, it corresponds to the class group of Lean, because it doesn't "includes" the set/type itself

[Anne Baanen]

It's at least also a Dutch thing. If I pretend to only be a mathematician, "a subgroup structure of G" sounds more like "an algebraic structure containing all subgroups of G" than "an object consisting of a subset of G along with a proof that this is a group".

[Anne Baanen]

It would be clearer for mathematician to say "subgroups G is the type of subgroups of G, which are represented by a subset of G along with the proofs showing it is a subgroup"

[Anne Baanen]

A word to abbreviate this further would be nice, but I think "structure" is not the best choice for that. "tuple" might work if you explain that tuples can also contain proofs in type theory. "object" would be nice if it didn't have the category theory connotations.

[Anne Baanen]

Hmm, how about borrowing the word record from Haskell/Agda? "subgroup G is the type of records representing a subgroup of G"?

[Mario Carneiro]

It's also not too hard to explain the lack of plural as a naming convention, where types in lean are named after the terminology you would use to refer to an element of that type

[Anatole Dedecker]

(deleted)

[Kevin Buzzard]

Naming conventions are interesting. About a third of the time set X is named correctly. Mathematicians have three totally interchangable ways of thinking about set X. It could be the type of subsets of X, and if you think about it this way then you wish it was called subset X. It could be the type of sets made from elements of X, and here set X is the perfect name. Or you could just observe that the set of subsets of X is the power set of X so it should be called powerset X. The issue seems to be whether the name is being used to describe the type or the terms.

An interesting example is (T : set (set X)) in the definition of a topological space. Mathematicians might say "T is a set of subsets of X (called the open sets...)" and here we're using two different words for the same thing in Lean

[Anatole Dedecker]

I'm still a beginner in mathematics so maybe what I say is irrelevant here, but don't you think you're spending too much energy on "setifying" Lean ? I mean, sure, types are not usual in maths, but why not just learn what they are once and then you can just use the exact terminology ? I don't think that's harder than some other concepts of maths

[Kevin Buzzard]

That is such a French response ;-)

[Kevin Buzzard]

Why not explain the translation? For me they are the same thing, ZFC sets and Lean types, they're just tools to set up maths

[Yakov Pechersky]

How do you explain that terms of different types can't be compared with equality? That looks different than zfc to me.

[Mario Carneiro]

I don't think this is a problem because it's not actually a thing mathematicians usually want to do, so it usually only shows up in hypothetical arguments about how weird ZFC is

[Yury G. Kudryashov]

OTOH, for many people (2 : ℝ) and (2 : ℕ) is the same number.

[Yury G. Kudryashov]

Or (2 : ℝ) and (2 : ℝ≥0)

[Adam Topaz]

What about (2 : N) and (2 : Z/7)?

[Adam Topaz]

They really aren't the same number

[Adam Topaz]

Even better, 2 :N and 2 : C_7 (the 7-adic complex numbers). Are these the same?

[Kevin Buzzard]

Mathematics is the art of giving the same name to different things

[Filippo A. E. Nuccio]

@Kevin Buzzard : after I received your first answer, I tried to digest it and did not open Zulip in the meantime. As a result, I missed most of the above conversation and most of @Patrick Massot 's complaints. They might be relevant for the following questions I had for you, but I am not sure. I'll post them as different messages so that they could be answered more easily. I will at any rate try to read, as you suggest, the intro to the file on fractional ideals to understand that file better.

[Filippo A. E. Nuccio]

1) You speak about universes and mention Prop and Type. Are there other examples of universes?

[Filippo A. E. Nuccio]

2) If I understand correctly, you are saying that to create a group one first creates a set G:Typeand then produces a term of type group G. But when has the type group G being created? What I mean to ask is that on a given set one can put a trillion of structures (group, ring, topological field, manifold, etc...) and it seems to me that what you are saying is that each of these structures is a term of the relevant type. So we should have a trillion of types from which to pick a term... Or does one first create G:Type then group G:Type and then finally pick a term of the latter type to put a structure on G? And what is the state of affairs after having put this structure, does Lean still understand by G the underlying set or since this has been upgraded to a group, G now denotes the group (so, the set plus the chosen group structure) and is there a way to recover the underlying set?

[Filippo A. E. Nuccio]

3) A similar question for the type subgroup G: was this type built automatically once a term _ inst_1: group G had been picked up? But more fundamentally, if I want to (1) construct a group $G'$ and (2) prove $G' \subset G$, it looks as a nightmare, because $G'$ will be of type G': Type with its _inst_1' but I will eventually need G': subgroup G which I won't be able to perform.

[Filippo A. E. Nuccio]

4) In the same vein, if I produce a subset A:set G (or may be A:set G.val or whatever the name of
the underlying set to G is) and want to prove that it is actually a subgroup, I will need to modify its type to A: subset G: is it doable? As a matter of fact, while I am writing this, I realize that may be the true statement is that "there exists a subgroup of $G$ whose underlying set is $A$" and this looks more doable-but how, really?

[Kevin Buzzard]

1) No, Prop and Type are the only universes, as far as normal mathematics is concerned. Computer scientists also use something called Type u but this is something which doesn't exist in mathematics unless you are doing category theory; whenever I see Type u in mathlib I just pretend it says Type. The only other "universe" is Sort u or Sort * which means "either Prop or Type".

https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/

2) Yes, groups are unbundled. A group in ZFC is a set plus a group structure (multiplication, inverse, identity, axioms). In Lean's type theory a group is a type G and a term _inst_1 : group G. To give a term of type group G is to give all the group structure on G. I don't really understand your question. "But when has the type group G being created?". The group function (which takes as input a type G and has output the type of all group structures on G) is defined in mathlib. Yes, if you have some ordered Lie group like the reals then you will have to pick lots of terms, terms giving the structures and more terms saying that the structures are compatible. I'm not sure you have a question here. In maths we say "let R be a commutative topological ring", in Lean we say variable (R : Type) [ring R] [topological_space R] [topological_ring R]. But R is still a type -- the "upgrading" you're talking about is all done by the type class inference system. In particular if a b : R then I can talk about a * b and the type class inference system finds the multiplication from the term of type ring R precisely because I use these square brackets [] -- that's the point of them.

3) I have no idea what your mental model of these things are. The subgroup function was "built automatically" the moment you imported the relevant mathlib files. So sure, that function was built before you start. But if you now "build" G, whatever that means, Lean will not "build" subgroup G until you run the subgroup function on the input G.

If you have two groups G and H and an injective group hom H -> G then you can build the term of type subgroup G; conversely given a term of type subgroup G you can build a group H and an injective hom H -> G. Mathematicians do this automatically but in Lean there is a separation between these two concepts. You say it looks like a nightmare but you're wrong. In practice you are either mostly doing groupy things with H or subgroupy things -- as a mathematician you have never really considered the difference, but Lean will make you do this. If it was a nightmare then we wouldn't have been able to make perfectoid spaces. Mathematicians do this all the time -- the natural number 37, the integer 37, the real number 37, the p-adic number 37 are all different 37's in Lean but this is not blocking progress. When you say "I will eventually need G' : subgroup G you have misunderstood the solution. You will eventually need the term of type subgroup G corresponding to G' and you are used to also calling this term G' but in Lean it is simply called f(G') for some function f with a name like to_subgroup or something. The fact that G' and f(G') are not literally equal objects in Lean doesn't matter, because you do groupy things with G', and subgroupy things with f(G'), and when you want to relate constructions in the two universes the function is there which relates them, says the diagram commutes, whatever.

https://xenaproject.wordpress.com/2020/04/30/the-invisible-map/

4) is the same question as 3 but in another domain. This phenomenon is everywhere when you do mathematics in type theory (as people have been doing for many decades) and they understand it well.

The point is that as a mathematician you just assume that this set-up will be unworkable, because you can see that in theory this leads to complications, but in practice mathematical arguments either focus on one implementation or the other, so things work out fine in practice. Lean has a very sophisticated system for moving between concepts, typically represented either by weird little up-arrows or by nothing at all (depending on which system is doing the moving) and in practice it does not get in your way (most of the time).

[Filippo A. E. Nuccio]

Thanks: one thing I had overlooked is that group and subgroup could be seen as functions producing a Type from another Type, and this makes sense and much of your answer looks much clearer. I am not assuming that this set-up is unworkable, I am just trying to understand it and to put as few things as possible (to my brain/knowledge) under the rug. Time will help...

[Kevin Buzzard]

Everything is a function in functional programming -- or a constant (like nat).

[Anatole Dedecker]

You can be even more extreme and say that a constant is just a constant function that takes no argument

[Utensil Song]

The never-ending lesson one learns from Lean is the delicacy of "is".

[Utensil Song]

First, there are different equalities noticeable in proofs: syntactic equality, definitional equality, propositional equality, and isomorphism etc. And this list can be further divided when it comes to choosing a specific tool (e.g. tactics) for the job.

[Utensil Song]

Then, there are the "is" issues in modeling mathematical structures:

In type theory, one starts with a hard type, which is a fixed and unbendable identity. This is far different from a set (in the sense of Mathematics), which is a flexible collection summoned by a certain condition (i.e. a proposition).

[Utensil Song]

This hard type will never be equal to another hard type in the sense of absolute equality. In order to make a hard type flexible enough to interact with other hard types like it "is" something (e.g. a group), one can give a mathematical structure to a type (by some proofs). If the type is G and the mathematical structure is group then it looks like group G in Lean.

[Utensil Song]

But this is not the right mental model to apply universally. One can't directly translate anything in the form of group G to "G is a group". An obvious counter-example is subgroup G, in this case, there's something new created as the subgroup "of" G. If we apply this counter-example back to group G, we will realize that group G also creates something new as the group structure "of" G that's not G itself.

[Utensil Song]

The same applies to set G. It's a set of G but G is not a set. There's no "is" here, only "of".

[Utensil Song]

These mathematical structures are all external to the type, like a role the type plays. And the role interacts with other roles of other types through all sorts of propositions about the roles, like our physical bodies are playing roles following social rules. And all these hard types, roles, propositions are all represented by types (in a general sense) in type theory to have a unified but also diverse solution.

[Utensil Song]

The situation is even more complicated for multiple parameters. A vector_space K V can be used to describe a vector space V "over" a field K, a clifford_algebra R M Q can be used to describe "the Clifford algebra of a module M over a commutative ring R, equipped with a quadratic_form Q".

[Utensil Song]

One might use "is" in the former case but "of" will be inevitable in the latter case, and both cases involve adverbs. The latter case also demonstrated that the last parameter might not be the thing we imagine to be "is" like in vector_space K V, because clifford_algebra R M Q "is" not any of R, M, Q but something new created out "of" them.

[Utensil Song]

What the typeclass mechanism does in this context is just auto-dressing , when a raw type appears in a statement or a proof, it will find a proper role for the type that makes sense in the context, this is called “type class resolution” and when it fails, it complains about “fail to synthesize” and the raw type will start to have difficulties interacting with other roles of other types. There’re little tricks to provide hints for finding the right dress(role).

[Filippo A. E. Nuccio]

@Utensil Song Thanks for the answer: do you have an accessible and structured reference to study all this?

[Patrick Massot]

Filippo, you should know that Utensil likes to approach these kinds of questions from a philosophical (or maybe even poetical) point of view. But it doesn't necessarily makes it easier for others to understand, compared to the more conventional approach based on raw facts.

[Patrick Massot]

In the case at hand, you can first type #check @group (remember the @ makes all inputs explicit) to see that group is a function with a single input which is a type and a single output which is a type (in the same universe, but let's ignore universes since they don't play any role here). So group G is meaningful if and only if G is a type. Then you can type #print group to see what would be the definition of group G (using jump to definition would be less useful here because groups are built on top of simpler stuff like monoids). After a couple of meta-data that are technical implementation details, you see

structure group : Type u → Type u
fields:
group.mul : Π {α : Type u} [c : group α], α → α → α
group.mul_assoc : ∀ {α : Type u} [c : group α] (a b c_1 : α), a * b * c_1 = a * (b * c_1)
group.one : Π {α : Type u} [c : group α], α
group.one_mul : ∀ {α : Type u} [c : group α] (a : α), 1 * a = a
group.mul_one : ∀ {α : Type u} [c : group α] (a : α), a * 1 = a
group.inv : Π {α : Type u} [c : group α], α → α
group.mul_left_inv : ∀ {α : Type u} [c : group α] (a : α), a⁻¹ * a = 1

The word structure on the first line is much closer to the C language use of this word than Bourbaki's word, it simply means a bunch of things put together. This first line also tells you again the information we got from #check. Then comes the list of things ("fields") that are put together. The capital Pi is a weird notation that is preferred to a good old forall in contexts where data is involved (as opposed to statements). For instance line 3 tells: if you give me a type α and a term c with type group α then I'll give you a multiplication map α → α → α. The next piece of data is two lines down: if you give me a type α and a term c with type group α then I'll give you a term with type α (and denote by one thanks to some trick that is irrelevant here). There is also the inversion map further down. All the other lines are axioms that multiplication and one should satisfy.

[Patrick Massot]

Fundamentally, everything we need to talk about needs to have a type. And in order to define a type from one or several existing types, you mostly need to tell how to create terms having that type and how to build a function whose domain is your new type. To make this more symmetric, you can say you need to describe how to define function into your new type, and from your new type. There are very few built-in ways to define types. Function types are built in, at the very core of everything. Almost everything else are inductive types, which are defined using the inductive keyword or, in an important special case, the structure (or class) keyword. Building terms of an inductive type is made using a constructor. Structures are inductive types with only one constructor, called mk by default. So you can learn how to build an element whose type is group G by typing #check @group.mk which indeed takes as input all the ingredients listed above. Calling this function directly is not very convenient when proofs are long so we have syntax sugar to help us (using { mul := ..., one :=...} etc. But really this is calling this constructor function. The other direction is more complicated. To build a function out of group G you use the recursor group.rec. So you can #check @group.rec. It will tell you how to define a function taking as input a type G and a term c of type group G and get some term of type C G (but we can pretend this target type does not depend on G if you are interested in a fixed G). Basically you are allowed to use all the ingredients that go into the definition of a term with type group G but nothing else.

[Patrick Massot]

All this is explained much better in TPIL.

[Filippo A. E. Nuccio]

@Patrick Massot Thanks so much! This makes many things much clearer, above others that the syntax
group.one : Π {α : Type u} [c : group α], α
means that the result is a term of type α and not α itself. I will play with #check and #print and try to develop some more intuition. Concerning TPIL, I must confess that it is not a very easy read-the examples are very much CS-oriented (at least, this is what I feel), and seldom Math-oriented. But I will try to study more before complaining...

[Kevin Buzzard]

Yes, we're writing mathematics in Lean precisely because the TPIL examples aren't mathematical enough

[Kevin Buzzard]

Which of course is perfect for some learners but not for my own target audience

[Utensil Song]

Filippo A. E. Nuccio said:

Utensil Song Thanks for the answer: do you have an accessible and structured reference to study all this?

What I shared before was merely what I made sense of my observation during breaking things and piecing things together in Lean.

Systematic learning can be reading any of #tpil , #mil , #tutorial, LFTCM 2020 Workshop or my personal first and favorite guide The Hitchhiker’s Guide to Logical Verification and doing exercises in them.

[Utensil Song]

#mil is the best source if you're looking for a math-oriented tutorial, but the Hitchhiker’s Guide has weaved a right proportion of type theory into the learning process so it's a good supplement for #mil IMHO. On the other hand, #tpil requires you to have an immersive walkthrough with it and examine the technicality carefully, it's easy to get lost in it if you don't already have a big picture.

I also invested quite some time to read related papers about Lean & Mathlib, about formalized math, about type foundations, and about the problems Lean 4 tries to solve, as well as the mathlib source and sometimes Lean source.

[Utensil Song]

_Patrick Massot|110031 said:

Filippo, you should know that Utensil likes to approach these kinds of questions from a philosophical (or maybe even poetical) point of view. But it doesn't necessarily make it easier for others to understand, compared to the more conventional approach based on raw facts.

Human's mind is a complicated machine, it never stops modeling raw facts, just as Einstein said, what you can observe depends on the theory you use. Mental models can be subconscious but it's always there, both helping you and creating obstacles for the specific job.

Besides gathering more raw facts by doing exercise, an important step for adjusting it is trying to explicitly state the inaccurate but partially working mental models. One thing that I particularly appreciate the Zulip chat is that there're the diverse (thus inspiring) metanarratives about modeling math in Lean.

[Scott Morrison]

While we're listing things to learn from, the opening chapters of the Homotopy Type Theory book are a great introduction to the basics of dependent type theory, for people with a mathematical background.