Functions on an inductive type

Stream: Type theory

[Flo (Florent Schaffhauser)]

If I is an inductive type and T is a type, can functions from I to T be used to define an inductive type?

For instance, if I = nat and T is a type, is there an inductive type with terms indexed by the integers and whose terms indexed by n are exactly the n-tuples of terms of type T?

In the context of Lean, I have been thinking about this in order to define the sum of $n$ terms in a monoid $M$ recursively:

$$\sum_{ k=1 }^{ n } a_k := \left( \sum_{ k=1 }^{ n-1 } a_k \right) + a_n$$

where by definition $\sum_{k=1}^0 a_k := 0_M$.

I know that such sums are defined in mathlibbut I am thinking about this for teaching purposes.

[Johan Commelin]

It might be easier to use list M... but if you are willing to consider infinite sequences $(a_n)_n$ for $n = 0, \dots, ∞$ then you can do what you want.

[Johan Commelin]

However, it would be a lot more convenient to define

$$\sum_{k=0}^{n+1} a_k = \left( \sum_{k=0}^{n} a_{k+1} \right) + a_0$$

[Johan Commelin]

Actually, I guess your version is also fine.

[Flo (Florent Schaffhauser)]

Johan Commelin said:

It might be easier to use list M... but if you are willing to consider infinite sequences $(a_n)_n$ for $n = 0, \dots, ∞$ then you can do what you want.

Yes, I forgot to say it but with infinite sequences I can implement what I want in Lean. That's why I am now wondering about $n$-tuples. I will look into list Mmore, thanks for the tip :+1:

[Johan Commelin]

Yeah, you'll have to decide what you mean by n-tuple before you can sum them. list M is one option. There is also vector n M, but it has very little API. Yet another option is maps fin n → M.

[Kevin Buzzard]

You can make the definition recursively -- surely this is what you want? Why do you want the type itself to be inductive?

import Mathlib

/-- `sum f n` is `f(0)+f(1)+...+f(n-1)` -/
def sum {M : Type} [AddMonoid M] (f : ℕ → M) : ℕ → M
| 0 => 0
| (n + 1) => sum f n + f n

[Flo (Florent Schaffhauser)]

Kevin Buzzard said:

You can make the definition recursively -- surely this is what you want? Why do you want the type itself to be inductive?

import Mathlib

/-- `sum f n` is `f(0)+f(1)+...+f(n-1)` -/
def sum {M : Type} [AddMonoid M] (f : ℕ → M) : ℕ → M
| 0 => 0
| (n + 1) => sum f n + f n

Yes, that is indeed what I want!

And I wrote something similar to what you did here but then I started thinking about a definition that would start like this

def sum {M : Type} [AddMonoid M] (n : ℕ) (f : fin n → M) : M

and with this formalism I have not been able to make it work.

So now I am wondering if there is an inductive type of $n$-tuples of elements of $M$, that I can use to write a recursive definition. And that's why I got interested in the type-theoretic aspects :sweat_smile:

[Eric Wieser]

You can write a recursive definition using docs#fin.cons_induction / docs4#Fin.consInduction

[Flo (Florent Schaffhauser)]

Fantastic, thanks!!!

[Eric Wieser]

def sum {M : Type} [AddMonoid M] (n : ℕ) (f : Fin n → M) : M := by
  induction f using Fin.consInduction with
  | h0 => exact 0
  | h x₀ _xs ih => exact x₀ + ih

[Eric Wieser]

Another option is to use the poorly-named docs#vector3, though I don't know what Lean 4 calls it

[Kevin Buzzard]

Hopefully vector4

[Alex Keizer]

Maybe to answer the question as originally stated, functions are generally coinductive, rather than inductive, so, no, a function Nat -> M cannot be used to define an inductive type (what would it's recursion/induction principle be), but it could define a coinductive type.