Recursive definition of a sum of squares

I am trying to formalise in Lean3 the notion of sum of squares in a ring.

If $$A$$ is a ring, $$n$$ is an integer and $$f$$ is a function from $$F_n:= \{ i \in \mathbb{N} \ |\ 1 \leqslant i \leqslant n \}$$ to $$A$$, then

$$\sum_{i = 1}^n f(i)^2 := \left\{ \begin{array}{cl} 0 & \text{if } n = 0 \\ \sum_{ i = 0 }^{ k } f(i)^2 + f( k + 1 )^2 & \text{if } n = \mathrm{succ}(k) \end{array} \right.$$

according to whether $$n$$ is $$0$$ or the successor of an integer.

I am using $$f: F_n \to A$$ as a way to list $$n$$ elements $$a_i := f(i)$$ in $$A$$.

However, I have not been able to write it down properly like that. I would like to eventually reach something like this

def sum_of_squares {A : Ring} (n : nat) : (range n → A.dom) → A.dom


in which, for all $$n \in \mathbb{N}$$, sum_of_squares n is a function that takes a function $$f : F_n \to A$$ to the element $$\sum_{i=0}^n f(i)^2 \in A$$.

Here range n (defined in Leanas the set of natural numbers less than $$n$$) represents the set $$F_n$$ introduced above.

And I would like to define this recursively by using induction on $$n$$:

• If $$n = 0$$, then sum_of_squares n := λ f, 0. Or in other words, for all $$f : F_n \to A$$, sum_of_squares 0 f := 0.
• If $$n = \mathrm{succ}(k)$$, then sum_of_squares n := λ f, (sum_of_squares k f) + f(k+1)^2.

But I have not been able to do it. I wonder if this is a problem with the code or if there is a theoretical oversight on my part with this definition.

Any help with this would be greatly appreciated :-)

Edit (with code for failed attempt): My issue with the code is that I am unable to formalise the distinction between $$n = 0$$ and $$n = \mathrm{succ}(k)$$ that I introduced above. I think it should go something like this:

def sum_of_squares {A : Ring} (n : nat) : (range n → A.dom) → A.dom
| λ f, 0
| λ f, (sum_of_squares k f) + ((f (k+1) ) * (f (k+1) ))


but then Leanreturns the message invalid expression starting at 3:0. I am wondering if this is a syntax problem or is there in fact no chance of making this work.

I thought that the problem might come from my use of range n, so I tried to modify the definition to

def sum_of_squares {A : Ring} (n : nat) : (nat → A.dom) → A.dom


but I get the same error message.

In case it is useful, let me add that nat is just the usual type of natural numbers $$\mathbb{N}$$ as implemented in Lean3, and that Ring is a class that I would like to be defined like this:

class Ring := mk_Ring ::
(dom : Type)
(sum : dom → dom → dom)
(prod : dom → dom → dom)
(zero : dom)
(one : dom)
-- + axioms of a ring


In the code above, I have used + and * instead of A.sum and A.prod, for the sake of clarity.

I am preparing this for an exercise session in a formalisation seminar, in which one of the goals is to manipulate basic definitions, not necessarily use the full power of mathlib. But of course I am interested in all comment or advice that you may have 😊 Thanks!

Edit 2: The following definition seems to be accepted by Lean3:

def sum_of_squares {A : my_ring} (f : nat → A.dom) : nat → A.dom
| 0 := A.zero
| (n+1) := (sum_of_squares n) + ((f n) * (f n))


I do not know how to make this approach work for f: range n → A.dom, though.

Basically, what I want is a for loop: given a list $$(a_0, ... , a_{n-1})$$ of $$n$$ elements of $$A$$, I want to define the sum $$\sum_{i=0}^{n-1} a_i^2$$ recursively, starting from sum = 0 if $$n=0$$ and then by returning the value at the end of the following loop:

for i in range n:
sum = sum + a[i]^2,
i = i + 1


I have found the following post by Mario Carneiro about for loops in Lean, but I have not been able to use it yet:

Loops in Lean programming language

• Can you show some (possibly failed) code attempts? Otherwise we wouldn't know whether it is a problem with the code.
– Trebor
Commented Jun 3, 2023 at 4:04
• @Trebor Hi! Just added the code for my failed attempt :-) I hope that this clarifies what my issue is. Thanks! Commented Jun 3, 2023 at 6:42
• You are right to first try with nat in place of range n. You are using the wrong syntax for a recursive definition in Lean 3. I would look again at Theorem Proving in Lean for examples of the correct syntax. Commented Jun 3, 2023 at 10:34
• Also I think you need to use fin n in place of range n. The former is a type with exactly n elements. The later is (I think) just a list. Commented Jun 3, 2023 at 11:31
• Sorry for my last comment. Ignore that. range n seems fine as it returns a finsum nat. Also I dont know if you want to code this from scratch, but note this is already in mathlib. See stackoverflow.com/questions/69689347/… Commented Jun 3, 2023 at 12:01

def sum_list_squares : List Nat → Nat

This is easily generalized to replace Nat with an arbitrary A that has addition.
• That's exactly what I was hoping for but was not able to write myself, thank you so much :-) And yes, no problem generalizing it to A that is not necessarily Nat. Commented Jun 3, 2023 at 15:54