What does `?M_1 xyz` mean?

Stream: new members

[Rajiv]

I am new to lean and when working on this section, https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#enumerated-types and in the following snippet, when I do #check weekday.rec and #check weekday.rec_on, I see something like ?M_1 weekday.sunday and ?M_1 n.

What does the form ?M_1 xyz mean in a type signature?

inductive weekday : Type
| sunday : weekday
| monday : weekday
| tuessday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

#check weekday.rec

#check weekday.rec_on

[Kevin Buzzard]

I agree this is confusing. Try #check @weekday.rec

[Rajiv]

Thanks a lot. That helps! :-)

[Kevin Buzzard]

"For all functions C from weekday to types, if you have a term of type C sunday and a term of type C monday and ... and a term of type C saturday, then I can give you a function which takes any weekday n, and returns a term of type C n"

[Rajiv]

Are there more examples of how to read Π type signatures somewhere? I am finding this way of reading type signatures quite useful.

[Kevin Buzzard]

I tried to read recursors when I was getting the hang of this stuff. For me when I was learning, I found it helpful to just focus on the idea that there were only two universes, Prop (the universe of types which represent true/false statements like 2+2=4 and 2+2+5) and Type (the universe of types which represent collections of stuff, like the real numbers). (This idea isn't actually true, there are infinitely many type universes because Type has to have a type, but this is just a quirk of the theory). When I see Sort u I would interpret it as meaning "Either Prop or Type". With that in mind, here is nat.rec (which is quite a difficult one):

nat.rec : Π {C : ℕ → Sort u}, C 0 → (Π (d : ℕ), C d → C d.succ) → Π (n : ℕ), C n

If we interpret Sort u as Prop, this says the principle of mathematical induction, namely that for all families C 0, C 1, C 2, ... of true-false statements, if we know C 0 is true and if we know that for all d, C d implies C (d + 1) (note that d.succ just means d + 1), then we can conclude that for all n, C n is true.

If on the other hand we interpret Sort u as Type, then this says the principle of mathematical recursion, namely that for all families C 0, C 1, ... C n, ... of types or sets or however you want to think of them, if we have an element of C 0, and if we also have a method which given d and an element of C d produces an element of C (d + 1), then we have a method to produce an element of C n for all n.

[Rajiv]

Thanks again Prof. Kevin. I really appreciate your reply and pointers.