Ssreflect Users Discussion List

[Yves Bertot <>]

On 12/15/2017 01:40 PM, Edouard KLEIN wrote:

Hi all !

I'm completely new to Coq and I'm trying to use the Koenig-Huygens Theorem in a proof (more specifically, this form:  (https://i.imgur.com/3RTWgwQ.gif)).

From the book I see that I can make sets of finite types, but is it possible to express a set of reals ?

Thanks in advance,

Edouard.

If X is a finite collection of real numbers, then there are several ways to express what you want.  You don't need the field in which you work to be finite, you can easily consider finite collections of numbers taken from an infinite type.

The Koenig-Huygens theorem is probably valid in any real-closed field, so that you can actually express it using
the background provided by the rcfType structure, as given in num.v

Then, if R is a suitable field, you can describe the collection X either as sequence of numbers, as a row vector of size n, or as a finite function of from 'I_n to R, where 'I_n is the initial segment of the natural numbers with n elements.

In the latter case, you just have to write:

Definition E (n : nat) (X : R ^ n) := / n * \sum_(i < n) X i.

Lemma Koenig_Huygens n (X : R ^n) : /n * \sum_(i < n) (X i - E X) ^2 = /n * \sum_(i < n) X i ^2 - E X ^2.

Yves