在coq中，如何做涉及求和和均值的证明？

Question

例如，如何在 coq 中证明：

或者那个：

Answer 1

您可以通过多种方式来陈述您的引理和定义，尤其是这取决于您对数据类型的假设。我建议使用 Mathematical Components Coq 包中的 bigop 库。有了它，你可以很容易地证明你的第二个引理：

From mathcomp Require Import all_ssreflect all_algebra.

Section Avg.

Open Scope ring_scope.
Import GRing.Theory.

Variables (N : fieldType) (n : nat) (n_pos : n%:R != 0 :> N) (X : n.-tuple N).

Definition avg := (\sum_(x <- X) x) / n%:R.

Lemma avgP : \sum_(x <- X) (x - avg) = 0.
Proof.
rewrite sumrB !big_tuple sumr_const card_ord -mulr_natr divfK //.
by rewrite big_tuple subrr.
Qed.

End Avg.

注意上面的代码只是一个例子，让大家感受一下简单的证明；正确地发展关于统计的理论需要更多的方式，并且可能需要 avg.

的不同编码