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 (*Begin solution for the teacher.*) to next marker (included) (*End solution for the teacher.*)(*Fill the proof here*) Admitted. (*Replace this line with Qed.*) 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"). *)
(* Begin solution for the teacher. *)
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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. *)
  (* Fill the proof here *)
Admitted. (* Replace this line with 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. *)
  (* Fill the proof here *)
Admitted. (* Replace this line with 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. *)
  (* Fill the proof here *)
Admitted. (* Replace this line with Qed. *)

(* 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. *)

Admitted. (* Replace this line with Qed. *)

(* 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.

(* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
  (* Fill the proof here *)
Admitted. (* Replace this line with 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.
(* End solution for the teacher. *)
  (* Fill the proof here *)
Admitted. (* Replace this line with Qed. *)

End Optimality_Of_Hypotheses.