Coq доказательство того, что факториал N / (факториал k * факториал (N-k)) является целым числом
Я не смог найти доказательство того, что 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!.
Однако было бы неплохо иметь и прямое доказательство вышеизложенного, не прибегая к треугольнику Паскаля. Многие из «неофициальных» доказательств, которые появляются, когда я ищу его здесь, в стеке. * неявно используют шаги алгебры для рациональных чисел, и они не удосуживаются показать, что это работает для строгого деления
Обновлено: Благодаря ответу @Bubbler ниже (на основе эта математика) доказательство просто
nat
Я надеялся на доказательство, которое не требовало бы отождествления выражения с решением какого-то рекурсивного уравнения, что вообще требует некоторой божественной проницательности, а скорее на простое доказательство, которое включало бы только алгебраические манипуляции. Кажется излишним (хотя и очень красивым) приводить такие понятия, как простые числа, фундаментальную теорему алгебры или, в данном случае, придумывать choose и т. д. Неформальные доказательства требуют только, чтобы произведение к последовательных целых чисел было всегда делится на к! (помимо "обманных" рациональных делений...)
Это звучит справедливо. Я думаю, что вся трудность доказательства заключается именно в том последнем факте, который вы упомянули, поскольку, в зависимости от того, как вы его формализуете, его утверждение может быть почти целью, которую вы пытаетесь доказать.
Да это правда.
Это не задача Кока, а простая математическая задача.
@Yves Это правда. Я спрашивал, как закодировать «простую математическую задачу» в формализме Кока. Выполнение этого кодирования имеет некоторые препятствия, которые карандашная математика обычно не замечает, как я уже упоминал в комментарии выше. Большая часть математики проста на бумаге (или в латексе), но когда кто-то пытается закодировать ее в Coq, возникают проблемы, в данном случае с делимостью. В сообществе Coq может быть кто-то, кто знает способ элегантный для выражения конкретной математической задачи в синтаксисе Coq. Как это делается, может быть полезно увидеть, когда вы столкнетесь с другими подобными проблемами. По крайней мере, это мое предположение
Спасибо за разъяснения. Меня давно заинтересовала эта конкретная проблема, и я всегда думал, что использование треугольника Паскаля — единственный способ доказать это. Если вам известно другое доказательство, достаточно подробное, чтобы мы могли восстановить все шаги, я буду заинтересован помочь построить формально проверенное доказательство.
@Yves, Бабблер показал, как это сделать ниже.
Ответы 1
Вместо громоздкого минуса я бы сформулировал это так:
Theorem fact_div_fact_fact : forall x y, exists e, fact (x + y) = e * (fact x * fact y).
Я считаю, что вы можете вывести из этого свою собственную лемму в сочетании с фактами о <= и - в стандартной библиотеке Coq.
А вот и автономное, не очень короткое доказательство с использованием чисто алгебраический подход. Вы можете попробовать запустить его здесь онлайн.
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.
Спасибо, это идеально!
Разве прохождение треугольника Паскаля не является «прямым доказательством»? Делимость определяется как
divides q p := (exists w, p = q * w), и в этом случае свидетелемwявляется именноchoose(n,k).