Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. (* Rework your last proof using the full syntax of ssreflect. *) (* Solve the following equations. Search is your best friend. *) Lemma ex5_arit1 n m : n + (m * n + 0) = n * m.+1. (*D*) Proof. by rewrite addn0 -mulSn mulnC. Qed. Lemma ex5_arit2 n m : n %/ 2 + m = (2 * m + n) %/ 2. (*D*) Proof. by rewrite mulnC divn_addl_mul // addnC. Qed. Lemma ex5_arit3 n m p : 0 < p -> p %| n -> n %/ p + m = (p * m + n) %/ p. (*D*) Proof. by move=> *; rewrite divn_addl ?dvdn_mulr // mulKn // addnC. Qed. (* Prove this by induction. *) Lemma size_iota_sumn l : sumn (map (addn 1) l) = size l + sumn l. Proof. (*D*) elim: l => //= x xs IH. (*D*) by rewrite !addSn [x + _]addnC addnA -IH // add0n addnC. Qed. (* Prove the following Theorem by induction. *) Theorem ex5_gauss n : (n * n.-1) %/ 2 = sumn (iota 0 n). (*D*) elim: n => //= n IH; rewrite (iota_addl 1 0) add0n. (*D*) rewrite size_iota_sumn. (*D*) rewrite -IH{IH} size_iota -[X in X + _](@mulnK _ 2) // -divn_addl ?dvdn_mull //. (*D*) by rewrite [_ * _.-1]mulnC !mulnS muln0 addn0 -addnA -!mulSn; case: n. Qed. (* Advanced part *) (* Read the documentation of the wlog tactic *) (* Prove the following lemma without using dvdn_pexp2r following one the two informal proofs. The first one is more detailed, the second one is more challenging. If you want to try the second one, just skip ahead without reading the following informal proof. *) Lemma ex5_dvdn : forall m n k, k > 0 -> (m ^ k %| n ^ k) -> (m %| n). Proof. (*D*) move=> m n k k_gt0 dv_mn_k. (* Without loss of generality n is positive, since any number divides 0 *) (*D*) wlog n_gt0 : / 0 < n by case: n {dv_mn_k}; rewrite ?dvdn0 // => ?; apply. (* Given d := gcdn m n, n can be written as n' * d and m as m' * d *) (*D*) Search _ gcdn. Search _ dvdn. Search _ dvdn gcdn. (*D*) pose d := gcdn m n. (*D*) have /dvdnP[n' def_n] : (d %| n). exact: dvdn_gcdr. (*D*) have /dvdnP[m' def_m] : (d %| m). exact: dvdn_gcdl. (* We also have d > 0 *) (*D*) have d_gt0: d > 0 by rewrite gcdn_gt0 n_gt0 orbT. (* We can now refine our assumption to m' ^ k %| n' ^ k since for b positive, a * b %| c * b -> a %| c *) (*D*) have {dv_mn_k}dv_mn_k : m' ^ k %| n' ^ k. (*D*) move: dv_mn_k; rewrite def_m def_n !expn_mull. (*D*) Search _ muln dvdn. (*D*) by rewrite dvdn_pmul2r // expn_gt0 d_gt0. (* We can also prove that (m' ^ k) and (n' ^ k) are coprime since the gcdn of m' and n' is 1, or equivalently (gcdn m' n') * d = d *) (*D*) have cop_m'kn'k : coprime (m' ^ k) (n' ^ k). (*D*) rewrite coprime_pexpl // coprime_pexpr // /coprime. (*D*) have : (gcdn m' n') * d == d. by rewrite muln_gcdl -def_m -def_n. (*D*) by rewrite -eqn_div ?divnn ?d_gt0. (* From this coprimality and the refiner hypothesis follows that m' ^ k = 1 = gcdn (m' ^ k) (n' ^ k). Hint: gcdn a (a %% b) = gcdn a b *) (*D*) have : m' ^ k == 1. (*D*) Search _ dvdn modn. Print dvdn. (*D*) by rewrite -(eqnP cop_m'kn'k) -gcdn_modr (eqnP dv_mn_k) gcdn0. (* Since m'^k = 1 also m' = 1. Thus m = d and d %| n *) (*D*) Search _ expn. Search _ dvdn gcdn. (*D*) rewrite -(exp1n k) eqn_exp2r // def_m => /eqP->. (*D*) by rewrite mul1n dvdn_gcdr. Qed. Lemma ex5_dvdn_advanced : forall m n k, k > 0 -> (m ^ k %| n ^ k) -> (m %| n). Proof. (* Without loss of generality we can assume (m ^ k) and (n ^ k) are coprime (i.e. dividing n and m by their gcdn). Since (m ^ k) also divides (n ^ k), (m ^ k) is 1, thus m is 1, thus it trivially divides n. *) (*D*) move=> m n k k_gt0 dv_mknk. (*D*) wlog: m n dv_mknk / coprime (m ^ k) (n ^ k) => [cop_n'm'| /eqnP]. (*D*) wlog n_gt0 : / 0 < n by case: {dv_mknk} n; rewrite ?dvdn0 // => ?; apply. (*D*) have [n' def_n] := dvdnP (dvdn_gcdr m n); set d := gcdn m n in def_n. (*D*) have [m' def_m] := dvdnP (dvdn_gcdl m n); rewrite -/d in def_m. (*D*) have d_gt0 : d > 0 by rewrite gcdn_gt0 orbC n_gt0. (*D*) rewrite def_m def_n !expn_mull dvdn_pmul2r ?expn_gt0 ?d_gt0 // in dv_mknk *. (*D*) rewrite dvdn_mul // {}cop_n'm' // coprime_pexpl ?coprime_pexpr // /coprime. (*D*) by rewrite -(eqn_pmul2r d_gt0) mul1n muln_gcdl -def_m -def_n. (*D*) by rewrite -gcdn_modr (eqnP dv_mknk) gcdn0 -(exp1n k) => /(expIn k_gt0)->. Qed.