Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
From mathcomp Require Import all_ssreflect. (* 京大・理・2009年 *) Record ext2 : Set := Ext2 {pnat: nat; pirr: nat}. Definition prod2 (a b : ext2) := Ext2 (pnat a * pnat b + 2 * pirr a * pirr b) (pnat a * pirr b + pirr a * pnat b). Section Problem1. Variables a b : nat. Hypothesis odd_a : odd a. Hypothesis Hab : coprime a b. Definition ab := Ext2 a b. Theorem odd_a2 : odd (pnat (prod2 ab ab)). Proof. rewrite /=. Search _ odd addn. by rewrite odd_add odd_mul odd_a /= -mulnA mul2n odd_double. Qed. Lemma coprimeMDl k c d : coprime c (k * c + d) = coprime c d. Proof. by rewrite /coprime gcdnMDl. Qed. Theorem mpr_a2 : coprime (pnat (prod2 ab ab)) (pirr (prod2 ab ab)). Proof. rewrite /=. rewrite [b*a]mulnC addnn -muln2. rewrite !coprime_mulr. rewrite coprime_sym coprimeMDl. rewrite !coprime_mulr !Hab. rewrite coprimen2 odd_a /=. rewrite addnC coprime_sym coprimeMDl. rewrite !coprime_mulr coprime_sym !Hab /=. (* have ->: 2 * b * b = b * b * 2 by ring. *) rewrite -mulnA mulnC coprime_sym coprimeMDl. by rewrite coprime_mulr !coprime2n odd_a. Qed. End Problem1. Section Problem2. Lemma odd_coprime2 ab n : odd (pnat ab) -> coprime (pnat ab) (pirr ab) -> let ab2n := iter n (fun ab => prod2 ab ab) ab in odd (pnat ab2n) && coprime (pnat ab2n) (pirr ab2n). Proof. elim: n => [|n IHn] odd_a copr_ab. Admitted. Lemma prod2A a b c : prod2 a (prod2 b c) = prod2 (prod2 a b) c. Proof. rewrite /prod2. destruct a, b, c => /=. f_equal; ring. Qed. Lemma prod2e a : prod2 a (Ext2 1 0) = a. Admitted. Lemma prod2_iter n ab x : iter n (prod2 ab) x = prod2 (iter n (prod2 ab) (Ext2 1 0)) x. Admitted. Lemma prod2_2n n ab : iter n (fun ab => prod2 ab ab) ab = iter (2^n) (prod2 ab) (Ext2 1 0). Admitted. Lemma prod2_2n_Sn n ab : iter n (fun ab => prod2 ab ab) ab = iter (2^n - n.+1) (prod2 ab) (iter n (prod2 ab) ab). Proof. have Hn : 2^n - n.+1 + n.+1 = 2^n. by rewrite subnK // ltn_expl. Admitted. Lemma not_odd_coprime ab ab' n : odd (pnat ab) -> coprime (pnat ab) (pirr ab) -> odd (pnat ab') && coprime (pnat ab') (pirr ab') = false -> let abn := iter n (prod2 ab) ab' in odd (pnat abn) && coprime (pnat abn) (pirr abn) = false. Proof. move=> odd_a copr_ab. elim: n ab' => // n IHn ab' Hab'. move: {IHn}(IHn (prod2 ab ab')). rewrite iterSr. apply. case odd_a': (odd (pnat ab')) Hab'. Admitted. Lemma odd_coprime ab n : odd (pnat ab) -> coprime (pnat ab) (pirr ab) -> let abn := iter n (prod2 ab) ab in odd (pnat abn) && coprime (pnat abn) (pirr abn). Proof. move=> odd_a copr_ab /=. set abn := iter n _ _. case Hneg: (_ && _) => //. move: (not_odd_coprime _ _ (2^n - n.+1) odd_a copr_ab Hneg). rewrite -prod2_2n_Sn => <-. by apply odd_coprime2. Qed. End Problem2. Section Nagoya2013. Definition Sk k n := \sum_(1<=i 1. Definition Tm n := \sum_(1<=k i _. by rewrite Sk1 muln1. rewrite big_mkord. congr subn. apply eq_bigr => i _. by rewrite !exp1n !muln1. Qed. Lemma Tm2 : Tm 2 = 3^m - 3. Proof. rewrite /Tm. have ->: 3^m - 3 = 2^m - 2 + (3^m - 1 - 2^m). rewrite addnC. rewrite addnBA. rewrite subnK. by rewrite -subnDA. rewrite subn1 -ltnS prednK. by apply ltn_exp2r, ltnW. by rewrite expn_gt0. rewrite -{1}(exp1n m). rewrite ltn_exp2r //. by apply ltnW. rewrite -Tm1. rewrite [in 3^m](_ : 3 = 1+2) //. rewrite Pascal. transitivity (Tm 1 + (\sum_(1 <= k < m) 'C(m,k) * 2^k)). rewrite -big_split /=. apply eq_bigr => i _. rewrite -mulnDr. congr muln. rewrite /Sk !big_cons !big_nil. by rewrite !addn0. congr addn. transitivity ((\sum_(0 <= k < m.+1) 'C(m,k) * 2^k) - 1 - 2^m). Qed. Theorem Tmn n : Tm n.+1 = n.+2^m - n.+2. Proof. elim:n => [|n IHn] /=. by apply Tm1. Admitted. Theorem Skp p k : p > 2 -> prime p -> 1 <= k < p.-1 -> p %| Sk k p.-1. Admitted. End Nagoya2013.