Coq证明阶乘N /（阶乘k *阶乘（N-k））是整数

Question

我找不到N choose k在Coq标准库中不可或缺的证据。什么是这个引理的简短自足证明？

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!来回避整个问题。

但是，如果不采用pascal的三角形，也可以直接证明上述情况。当我在Stack上搜索它时出现的许多“非正式”证据。*隐含地使用有代数的代数步骤，并且他们不打算证明它适用于严格的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的独立，不那么短的证据。你可以尝试运行它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.