Ssreflect Users Discussion List

[Yves Bertot <>]

I made a mistake in my previous answer.  The right way to write the inverse of a number is ^-1.  Also, an integer, viewed as a member as an arbitrary ring is written as : n%:R.  So the definition of the average and the lemma statement
should be written as follows:

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

Lemma Koenig_Huygens n (X : R ^ n) : n != 0%N ->
  n%:R ^-1 * (\sum_(i < n) (X i - E X) ^+ 2) =
  n%:R ^-1 * (\sum_(i < n) X i ^+ 2) - E X ^+ 2.
Proof.

If you work with row vectors instead to describe vectors of values, you can write it as follows:

Definition E (n : nat) (X : 'rV[R]_n) :=
  n%:R ^-1 * \sum_(i < n) X 0 i.

Lemma Koenig_Huygens n (X : 'rV[R]_n) : n != 0%N ->
  n%:R ^-1 * (\sum_(i < n) (X 0 i - E X) ^+ 2) =
  n%:R ^-1 * (\sum_(i < n) X 0 i ^+ 2) - E X ^+ 2.
Proof.
move=> nn0.
  rewrite (eq_bigr (fun i : 'I_n => X i ^+ 2 + X i * E X * (-2%:R) + E X ^+ 2));
  last first.
  by move => i _;rewrite sqrrD !mulrN -mulr_natr sqrrN mulNr.
rewrite 2!big_split /= 2!mulrDr -addrA.
rewrite -2!big_distrl /= (mulrA _ _ (1 *- 2)) (mulrA _ _ (E X)).
rewrite -/(E X) -expr2 -mulNrn -(mulr_natr (-1)) mulNr mulrN mul1r.
rewrite sumr_const card_ord -(mulr_natr (E X ^+ 2)) -(mulrC n%:R).
rewrite (mulrA _^-1) mulVf ?pnatr_eq0 // mul1r mulr_natr mulr2n opprD.
by rewrite subrK.
Qed.

Note that, while doing the proof, I found out that the condition that  n is not 0 is relevant.  If you want the proof, I will
send it to you.

Yves

On 12/21/2017 03:08 PM, Yves Bertot wrote:

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