Ssreflect Users Discussion List

[Cyril <>]

Hello,

The minimal assumption about your field is that the characteristic does 
not divide n. A more comfortable option is to use a numFieldType (which 
has necessarily a zero characteristic).
Then, you can use arithmetic from GRing.Theory and big operators from 
bigop.v to prove this theorem. (cf join KH.v)

As for real numbers, they are not part of the mathematical components 
library. But it is an active topic for me and a few of us to provide 
some support in a classical context, outside of mathematical components, 
but compatible with it...

Best regards,
--
Cyril Cohen


On 21/12/2017 15:08, 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: 
> > KH (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
From mathcomp Require Import all_ssreflect all_algebra.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope ring_scope.
Import GRing.Theory Num.Theory.

Section Koenig_Huygens.
Variable (R : numFieldType).

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

Lemma Koenig_Huygens n (X : 'I_n -> R) :
   E (fun i => (X i - E X)^2) = E (fun i => X i ^+ 2) - E X ^+ 2.
Proof.
case: n => [|n] in X *; first by rewrite /E invr0 !mul0r expr0n subr0.
rewrite /E (eq_bigr _ (fun _ _ => @sqrrB _ _ _)).
rewrite big_split /= sumrB mulrDr mulrBr.
rewrite sumr_const card_ord -[_ ^+ 2 *+ n.+1]mulr_natl mulKf ?pnatr_eq0 //.
by rewrite sumrMnl -!mulr_suml mulrnAr mulrA -expr2 mulr2n opprD addrA addrNK.
Qed.

End Koenig_Huygens.