Library Algebra.binomial_compl
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Complements on the binomial coefficients (aka binomials).
The binomials are defined in the Mathematical Components library, and denoted
'C n p, a positive number iff p ≤ n.
The present module adds:
Taking 'C (m + n) m already structurally grants that m ≤ m + n, and the
variant (pbinom m n).+1 also structurally grants that it is positive.
This module may be used through the import of Algebra.Algebra, or
Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- a couple of properties about sums of binomials,
- a way to structurally grant that a binomial is positive.
Predecessor of (nonzero) binomial
Usage
From Requisite Require Import stdlib.
From Requisite Require Import ssr_wMC.
From mathcomp Require Import binomial.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets.
From Algebra Require Import Hierarchy_compl Monoid.
Section Binomial_compl.
Lemma binom_sym_alt :
∀ m n, 'C ((m + n)%coq_nat, m) = 'C ((m + n)%coq_nat, n).
Proof.
intros; rewrite plusE -bin_sub; [rewrite -addnBAC// subnn// | apply leq_addr].
Qed.
Lemma binom_rising_sum_l :
∀ m n,
sum (fun i : 'I_n.+1 ⇒ 'C ((m + i)%coq_nat, m)) =
'C ((m.+1 + n)%coq_nat, m.+1).
Proof.
intros m n; induction n as [| n Hn].
rewrite sum_1 !Nat.add_0_r !binn; easy.
rewrite sum_ind_r; unfold widenF_S; simpl; rewrite Hn.
replace (m.+1 + n)%coq_nat with (m + n.+1)%coq_nat; auto with zarith.
Qed.
Lemma binom_rising_sum_r :
∀ m n,
sum (fun i : 'I_n.+1 ⇒ 'C ((m + i)%coq_nat, i)) =
'C ((m.+1 + n)%coq_nat, n).
Proof.
intros; rewrite -binom_sym_alt -binom_rising_sum_l.
apply sum_ext; intros; apply eq_sym, binom_sym_alt.
Qed.
End Binomial_compl.
Section Pbinom_Def.
Definition pbinom (m n : nat) : nat := ('C ((m + n)%coq_nat, m)).-1.
End Pbinom_Def.
Section PbinomS_Facts.
Lemma pbinomS_eq : ∀ m n, (pbinom m n).+1 = 'C ((m + n)%coq_nat, m).
Proof.
intros; apply Nat.succ_pred, not_eq_sym, Nat.lt_neq; apply /ltP.
rewrite bin_gt0 plusE; apply leq_addr.
Qed.
Lemma pbinomS_pascal :
∀ m n, (pbinom m n.+1).+1 + (pbinom m.+1 n).+1 = (pbinom m.+1 n.+1).+1.
Proof. intros; rewrite !pbinomS_eq plusE addnC addSnnS; apply binS. Qed.
Lemma pbinomS_sym : ∀ m n, (pbinom m n).+1 = (pbinom n m).+1.
Proof.
intros; rewrite !pbinomS_eq plusE addnC -bin_sub;
[rewrite addnK; easy | apply leq_addl].
Qed.
Lemma pbinomS_0_l : ∀ n, (pbinom 0 n).+1 = 1.
Proof. intros; rewrite pbinomS_eq plusE add0n; apply bin0. Qed.
Lemma pbinomS_0_r : ∀ m, (pbinom m 0).+1 = 1.
Proof. intros; rewrite pbinomS_eq plusE addn0; apply binn. Qed.
Lemma pbinomS_1_l : ∀ n, (pbinom 1 n).+1 = n.+1.
Proof. intros; rewrite pbinomS_eq plusE add1n; apply bin1. Qed.
Lemma pbinomS_1_r : ∀ m, (pbinom m 1).+1 = m.+1.
Proof. intros; rewrite pbinomS_eq plusE addn1; apply binSn. Qed.
Lemma pbinomS_leq :
∀ m n1 n2, n1 ≤ n2 → (pbinom m n1).+1 ≤ (pbinom m n2).+1.
Proof.
intros; rewrite !pbinomS_eq plusE; apply leq_bin2l; rewrite leq_add2l; easy.
Qed.
Lemma pbinomS_monot :
∀ m n1 n2, (n1 ≤ n2)%coq_nat → (pbinom m n1).+1 ≤ (pbinom m n2).+1.
Proof. move=>> /leP H; apply pbinomS_leq; easy. Qed.
Lemma pbinomS_monot_pred : ∀ m n, (pbinom m (n.-1)).+1 ≤ (pbinom m n).+1.
Proof.
intros m [| n]; [simpl; apply ltnSn | apply pbinomS_monot, Nat.le_pred_l].
Qed.
Lemma pbinomS_le :
∀ m n1 n2,
(n1 ≤ n2)%coq_nat → ((pbinom m n1).+1 ≤ (pbinom m n2).+1)%coq_nat.
Proof. intros; apply /leP; apply pbinomS_monot; easy. Qed.
Lemma pbinomS_gt_0 : ∀ m n, (0 < (pbinom m n).+1)%coq_nat.
Proof.
intros; apply /ltP; rewrite pbinomS_eq plusE bin_gt0; apply leq_addr.
Qed.
Lemma pbinomS_rising_sum_l :
∀ m n, sum (fun i : 'I_n.+1 ⇒ (pbinom m i).+1) = (pbinom m.+1 n).+1.
Proof.
intros; rewrite pbinomS_eq -binom_rising_sum_l.
apply sum_ext; intros; apply pbinomS_eq.
Qed.
Lemma pbinomS_rising_sum_r :
∀ m n, sum (fun i : 'I_n.+1 ⇒ (pbinom i m).+1) = (pbinom n m.+1).+1.
Proof.
intros; rewrite pbinomS_eq Nat.add_comm -binom_rising_sum_r.
apply sum_ext; intros; rewrite Nat.add_comm; apply pbinomS_eq.
Qed.
End PbinomS_Facts.
Section Pbinom_Facts.
Lemma pbinom_sym : ∀ m n, pbinom m n = pbinom n m.
Proof. intros; apply eq_add_S, pbinomS_sym. Qed.
Lemma pbinom_0_l : ∀ n, pbinom 0 n = 0.
Proof. intros; apply eq_add_S, pbinomS_0_l. Qed.
Lemma pbinom_0_r : ∀ m, pbinom m 0 = 0.
Proof. intros; apply eq_add_S, pbinomS_0_r. Qed.
Lemma pbinom_1_l : ∀ n, pbinom 1 n = n.
Proof. intros; apply eq_add_S, pbinomS_1_l. Qed.
Lemma pbinom_1_r : ∀ m, pbinom m 1 = m.
Proof. intros; apply eq_add_S, pbinomS_1_r. Qed.
Lemma pbinom_le :
∀ m n1 n2, (n1 ≤ n2)%coq_nat → (pbinom m n1 ≤ pbinom m n2)%coq_nat.
Proof. intros; apply Nat.succ_le_mono, pbinomS_le; easy. Qed.
Lemma pbinom_leq : ∀ m n1 n2, n1 ≤ n2 → pbinom m n1 ≤ pbinom m n2.
Proof. intros; apply /leP; apply pbinom_le; apply /leP; easy. Qed.
Lemma pbinom_ge_0 : ∀ m n, (0 ≤ pbinom m n)%coq_nat.
Proof. intros; apply Nat.lt_succ_r, pbinomS_gt_0. Qed.
End Pbinom_Facts.