Recursive definition of a sum of squares

Question

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

Answer 1

Is there some reason you don't like the straightforward definition?

def sum_list_squares : List Nat → Nat
  | [] => 0
  | a :: lst => a * a + sum_list_squares lst

This is easily generalized to replace Nat with an arbitrary A that has addition.