Coq 证明阶乘 N / (阶乘 k * 阶乘 (N-k)) 是整数

Question

我无法在 Coq 标准库中找到 N choose k 是积分的证据。这个引理的 简短的自包含 证明是什么？

Lemma fact_divides N k: k <= N -> Nat.divide (fact k * fact (N - k)) (fact N).

我看到在 ssreflect.binomial.v 中他们通过递归定义 choose 回避了整个问题，choose(N,k) = choose(N-1,k) + choose(N-1,k-1)，然后显示 choose(N,k) * k! * (N-k)! = N!.

但是，最好也能直接证明上述内容，而无需求助于帕斯卡三角形。当我在 Stack 上搜索它时出现的许多 "informal" 证明。* 隐含地使用有理数的代数步骤，并且他们不费心证明它适用于严格的 nat 除法。

编辑：感谢@Bubbler 下面的回答（基于 this math），证明只是

intros. destruct (fact_div_fact_fact k (N - k)) as [d Hd]. exists d. rewrite <- Hd. apply f_equal. omega.

Answer 1

而不是笨拙的减号，我会这样说：

Theorem fact_div_fact_fact : forall x y, exists e, fact (x + y) = e * (fact x * fact y).

结合 Coq 标准库中关于 <= 和 - 的事实，我相信您可以从中得出自己的引理。

这是使用 pure algebraic approach. You can try running it here online 的独立的、不那么简短的证明。

From Coq Require Import Arith.

(* Let's prove that (n+m)! is divisible by n! * m!. *)

(* fact2 x y = (x+1) * (x+2) * .. * (x+y) *)

Fixpoint fact2 x y := match y with
  | O => 1
  | S y' => (x + y) * fact2 x y'
end.

Lemma fact2_0 : forall x, fact2 0 x = fact x.
Proof.
  induction x.
  - auto.
  - simpl. rewrite IHx. auto. Qed.

Lemma fact_fact2 : forall x y, fact x * fact2 x y = fact (x + y).
Proof.
  induction x.
  - intros. simpl. rewrite fact2_0. ring.
  - induction y.
    + simpl. replace (x + 0) with x by ring. ring.
    + simpl. replace (x + S y) with (S x + y) by ring. rewrite <- IHy. simpl. ring. Qed.

Lemma fact2_left : forall x y, fact2 x (S y) = S x * fact2 (S x) y.
Proof. intros x y. generalize dependent x. induction y.
  - intros. simpl. ring.
  - intros. unfold fact2. fold (fact2 x (S y)). fold (fact2 (S x) y).
    rewrite IHy. ring. Qed.

Lemma fact_div_fact2 : forall x y, exists e, fact2 x y = e * fact y.
Proof. intros x y. generalize dependent x. induction y.
  - intros. simpl. exists 1. auto.
  - induction x.
    + unfold fact2. fold (fact2 0 y). unfold fact. fold (fact y). destruct (IHy 0). rewrite H.
      exists x. ring.
    + unfold fact2. fold (fact2 (S x) y).
      destruct (IHy (S x)). destruct IHx. exists (x0 + x1).
      replace ((S x + S y) * fact2 (S x) y) with (S x * fact2 (S x) y + S y * fact2 (S x) y) by ring.
      rewrite <- fact2_left. rewrite H0. rewrite H.
      replace (S y * (x0 * fact y)) with (x0 * (S y * fact y)) by ring.
      unfold fact. fold (fact y). ring. Qed.

Theorem fact_div_fact_fact : forall x y, exists e, fact (x + y) = e * (fact x * fact y).
Proof. intros x y. destruct (fact_div_fact2 x y). exists x0.
  rewrite <- fact_fact2. rewrite H. ring. Qed.

Coq 证明阶乘 N / (阶乘 k * 阶乘 (N-k)) 是整数

Coq proof that factorial N / (factorial k * factorial (N-k)) is integer

factorial

coq