jsCoq – Use Coq in Your Browser

Worksheet on binomial coefficients.

These are:

general statements from library modules Nat_Sum, Nat_Factorial and Nat_Binomial that are equipped with guidance comments for students, and solution(s) for teachers;
alternate proofs general results from the library modules;
proofs that hypotheses of general results are optimal;
or specific statements or questions.

Note that provided script prepsheet will replace lines from marker to next marker (included) by Admitted., and will remove lines from marker (*Begin other solution for the teacher.*) to next marker (included) (*End other solution for the teacher.*) That way, both teacher and student versions of the file are compiling, and teachers can verify the validity of the provided solution(s).

From Teach Require Import WS_Helper.

Section For_beginners.

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_64_lt_63 : binom 6 4 < binom 6 3.
Proof.
(* Hints:
 - Use command "Eval compute in <expr>" to compute both values and convince
   oneself of the correctness of the lemma.
 - Begin the proof by a reduction (with tactic "simpl"). *)
simpl. apply nat_sub_n0_lt. rewrite 15!sub_succ. rewrite sub_0_r. discriminate.
Qed.

(* The following exercise is taken from *)
(* Hyperbole Terminale - Spécialité Mathématiques, Nathan, 2020 (in French). *)

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_ex01a_89 : exists n, 5 <= n /\ binom n 5 = 17 * binom n 4.
Proof.

(* Hint: try n = 89. *)
exists 89. split.
+ apply sub_0_le. rewrite 5!sub_succ. apply sub_0_l.
+ apply (mul_cancel_l _ _ 5). discriminate.
  rewrite binom_mul_S_r. rewrite 4!sub_succ, sub_0_r, mul_assoc. reflexivity.
Qed.

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_ex01a : exists n, 5 <= n /\ binom n 5 = 17 * binom n 4.
Proof.

(* Hint: find a value for n by using pen and paper. *)
exists 89. split.
+ apply sub_0_le. rewrite 5!sub_succ. apply sub_0_l.
+ apply (mul_cancel_l _ _ 5). discriminate.
  rewrite binom_mul_S_r. rewrite 4!sub_succ, sub_0_r, mul_assoc. reflexivity.
Qed.

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_ex01b n : binom n 5 = 17 * binom n 4 -> n < 5 \/ n = 89.
Proof.

(* Hint: discuss wether n < 5 or not. *)
destruct (nat_lt_le_dec n 5) as [Hn | Hn].
+ intros _; left. assumption.
+ assert (Hn' : 4 <= n).
    apply le_trans with 5. apply le_succ_diag_r. assumption.
  rewrite <- (mul_cancel_l _ _ 5). 2: discriminate.
  rewrite binom_mul_S_r. rewrite mul_assoc. rewrite mul_cancel_r.
  2: apply binom_neq_0; assumption.
  intros H. apply nat_sub_add_eq_l in H. 2: assumption.
  right. subst. reflexivity.
Qed.

End For_beginners.

Section Statements_From_Lib.

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_sum_sqr n :
  sum_range 0 n (fun k => (binom n k) ^ 2) = binom (2 * n) n.
Proof.
(* Hints:
 - Transform (2*n) into a sum.
 - Use Vandermonde's identity.
 - Reduce equality on sums to equality on functions.
 - Use symmetry of binomial coefficients.
 - End with application conditions of used lemmas. *)

(* Without automation. *)
replace (2 * n) with (n + n) by apply double_twice.
rewrite binom_vandermonde.
apply sum_range_ext. intros k [_ Hk].
rewrite <- binom_sym. 2: assumption.
rewrite pow_2_r. reflexivity.
Qed.

(* Begin other solution for the teacher. *)
(* With automation. *)
Lemma binom_sum_sqr_with_auto n :
  sum_range 0 n (fun k => (binom n k) ^ 2) = binom (2 * n) n.
Proof.
replace (2 * n) with (n + n) by lia.
rewrite binom_vandermonde.
apply sum_range_ext. intros k Hk.
rewrite <- binom_sym by lia.
now rewrite pow_2_r.
Qed.
(* End other solution for the teacher. *)

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_sum n : sum_range 0 n (fun k => binom n k) = 2 ^ n.
Proof.
(* Hints:
 - Transform 2 into a sum.
 - Use binomial theorem.
 - Reduce equality on sums to equality on functions. *)

(* Without automation. *)
replace 2 with (1+1) by reflexivity.
rewrite binom_formula.
apply sum_range_ext. intros k Hk.
rewrite !pow_1_l.
rewrite !mul_1_r. reflexivity.
Qed.

(* Begin other solution for the teacher. *)
(* With automation. *)
Lemma binom_sum_with_auto n : sum_range 0 n (fun k => binom n k) = 2 ^ n.
Proof.
replace 2 with (1+1) by easy.
rewrite binom_formula.
apply sum_range_ext. intros k Hk.
rewrite !pow_1_l; lia.
Qed.
(* End other solution for the teacher. *)

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_hockey_stick n k :
  sum_range k n (fun i => binom i k) = binom (S n) (S k).
Proof.

assert (H : forall p k, sum_n k p (fun i => binom i k) = binom (k + p) (S k)).
intros p. induction p.
- intros. simpl. rewrite binom_eq_0.
  reflexivity.
  rewrite add_0_r. apply lt_succ_diag_r.
- intros. simpl. rewrite IHp.
  rewrite add_succ_r. rewrite <- binom_pascal. apply add_comm.
(* *)
- unfold sum_range; rewrite H. destruct (nat_lt_le_dec (S n) k) as [H1 | H1].
  + rewrite !binom_eq_0. (* lia solves next subgoals. *)
    reflexivity.
    apply lt_trans with k. assumption. apply lt_succ_diag_r.
    rewrite (nat_sub_0_lt _ _ H1). rewrite add_0_r. apply lt_succ_diag_r.
  + f_equal. (* lia solves the next subgoal. *)
    rewrite (add_sub_assoc _ _ _ H1).
    rewrite add_comm, add_sub. reflexivity.
Qed.

End Statements_From_Lib.

Section Optimality_Of_Hypotheses.

(* Prove that hypotheses of the following lemmas are optimal: *)
(*   binom_S_l, binom_S_r, binom_pred, binom_eq_0, binom_gt_0, binom_neq_0,
   binom_le_alt, binom_lt_S, binom_lt, binom_lt_alt, binom_gt_1,
   binom_committee_chair_iter, binom_fact, binom_fact_div, binom_sym,
   binom_cancellation_alt. *)

(* Hints: these lemmas are of the form (P -> Q). It is thus a matter of proving
 either the equivalence (P <-> Q), or just the reverse implication (Q -> P),
 or rather the contrapositive of the latter (~ P -> ~ Q). *)

(* "_rev_contra" means the contrapositive of the reverse implication. *)

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_S_l_rev_contra n k :
  k = 0 -> binom (S n) k <> binom n (pred k) + binom n k.
Proof.
intros; subst. simpl.
rewrite !binom_0_r.
apply lt_neq, lt_1_2.
Qed.

(* Here, P is of the form (~ P1 \/ ~ P2), its negation is (P1 /\ P2). *)

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_S_r_rev_contra n k :
  n = 0 /\ k = 0 -> binom n (S k) <> binom (pred n) k + binom (pred n) (S k).
Proof.
intros [Hn Hk]; subst. simpl.
apply nat_neq_0_1.
Qed.

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_pred_rev_contra n k :
  n = 0 /\ k = 1 \/ k = 0 ->
  binom n k <> binom (pred n) (pred k) + binom (pred n) k.
Proof.
intros [[Hn Hk] | Hk].
+ subst. simpl. apply nat_neq_0_1.
+ subst. rewrite !binom_0_r. apply not_eq_S, nat_neq_0_1.
Qed.

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_eq_0_rev_contra n k : k <= n -> binom n k <> 0.
Proof.
apply binom_neq_0.
Qed.

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_gt_0_rev_contra n k : n < k-> binom n k <= 0.
Proof.
rewrite le_0_r. apply binom_eq_0.
Qed.

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_neq_0_rev_contra n k : n < k -> binom n k = 0.
Proof.
apply binom_eq_0.
Qed.

(* Here, P is of the form (P1 \/ P2 \/ P3), its negation is
 (~ P1 /\ ~ P2 /\ ~ P3). *)

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_le_alt_rev_contra n1 n2 k :
  (k <> 0 /\ k <= n1 /\ n2 < n1) -> binom n2 k < binom n1 k.
Proof.
intros [Hk1 [Hk2 Hn]]. apply binom_lt. 2: assumption. split. 2: assumption.
apply neq_0_lt_0. assumption.
Qed.

(* Here, P is of the form (P1 /\ P2), its negation is (~ P1 \/ ~ P2). *)

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_lt_S_rev_contra n k :
  (k <= 0 \/ S n < k) -> binom (S n) k <= binom n k.
Proof.
intros [Hk | H].
+ rewrite le_0_r in Hk. subst. simpl. rewrite binom_0_r. apply le_refl.
+ rewrite binom_eq_0. apply le_0_l. assumption.
Qed.

(* Here, P is of the form (P1 /\ P2 /\ P3), its negation is
 (~ P1 \/ ~ P2 \/ ~ P3). *)

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_lt_rev_contra n1 n2 k :
  (k <= 0 \/ n2 < k \/ n2 <= n1) -> binom n2 k <= binom n1 k.
Proof.
rewrite le_0_r. apply binom_le_alt.
Qed.

(* Here, P is of the form (P1 /\ P2), its negation is (~ P1 \/ ~ P2). *)

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_gt_1_rev_contra n k : k <= 0 \/ n <= k -> binom n k <= 1.
Proof.
rewrite le_0_r. intros [H | H].
+ subst. rewrite binom_0_r. apply le_refl.
+ destruct (le_lt_eq_dec _ _ H) as [H' | H'].
  - rewrite binom_eq_0. apply le_0_l. assumption.
  - subst. rewrite binom_diag. apply le_refl.
Qed.

(* Here, P is of the form (~ P1 \/ P2), its negation is (P1 /\ ~ P2). *)

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_committee_chair_iter_rev_contra n k i :
  (k = 0 /\ n < i) ->
  fact (k + i) * fact (n - i) * binom n (k + i) <>
    fact n * fact k * binom (n - i) k.
Proof.
intros [Hk H]; subst. simpl.
rewrite binom_eq_0. 2: assumption.
rewrite mul_0_r.
rewrite nat_sub_0_lt. 2: assumption. simpl.
rewrite !mul_1_r.
apply not_eq_sym, fact_neq_0.
Qed.

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_fact_rev_contra n k :
  n < k -> binom n k * (fact k * fact (n - k)) <> fact n.
Proof.
intros H.
rewrite binom_eq_0. 2: assumption. simpl.
apply not_eq_sym, fact_neq_0.
Qed.

(* Here, P is of the form (~ P1 \/ ~ P2), its negation is (P1 /\ P2). *)

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_fact_div_rev_contra n k :
  (n = 0 /\ k = 1) -> binom n k <> fact n / (fact k * fact (n - k)).
Proof.
intros [Hn Hk]; subst. simpl. apply nat_neq_0_1.
Qed.

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_sym_rev_contra n k : n < k ->  binom n k <> binom n (n - k).
Proof.
intros H.
rewrite binom_eq_0. 2: assumption.
rewrite nat_sub_0_lt. 2: assumption.
rewrite binom_0_r.
apply nat_neq_0_1.
Qed.

(* Here, P is of the form (P1 \/ P2), its negation is (~ P1 /\ ~ P2). *)

(* Fill the proof of next lemma and replace "Admitted" by "Qed". *)
Lemma binom_cancellation_alt_rev_contra n k i :
  k < i /\ i <= n ->
  binom n k * binom k i <> binom n i * binom (n - i) (k - i).
Proof.
intros [H1 H2].
rewrite (binom_eq_0 k i H1). rewrite mul_0_r.
apply not_eq_sym, neq_mul_0. split; apply binom_neq_0.
+ assumption.
+ apply sub_le_mono_r.
  apply lt_le_incl, lt_le_trans with i.
  all: assumption.
Qed.

End Optimality_Of_Hypotheses.