2
$\begingroup$

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

$\endgroup$
9
  • $\begingroup$ Can you show some (possibly failed) code attempts? Otherwise we wouldn't know whether it is a problem with the code. $\endgroup$
    – Trebor
    Jun 3, 2023 at 4:04
  • $\begingroup$ @Trebor Hi! Just added the code for my failed attempt :-) I hope that this clarifies what my issue is. Thanks! $\endgroup$ Jun 3, 2023 at 6:42
  • 1
    $\begingroup$ 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. $\endgroup$
    – Jason Rute
    Jun 3, 2023 at 10:34
  • 1
    $\begingroup$ 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. $\endgroup$
    – Jason Rute
    Jun 3, 2023 at 11:31
  • 1
    $\begingroup$ 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/… $\endgroup$
    – Jason Rute
    Jun 3, 2023 at 12:01

1 Answer 1

2
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ 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. $\endgroup$ Jun 3, 2023 at 15:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.