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. (* 2の平方根 *) Module Irrational. Require Import Wf_nat Reals Field. Lemma odd_square n : odd n = odd (n*n). Proof. by rewrite odd_mul andbb. Qed. Lemma even_double_half n : ~~odd n -> n./2.*2 = n. Proof. by rewrite -[RHS]odd_double_half => /negbTE ->. Qed. (* 本定理 *) Theorem main_thm (n p : nat) : n * n = (p * p).*2 -> p = 0. Proof. elim/lt_wf_ind: n p => n. case: (posnP n) => [-> _ [] // | Hn IH p Hnp]. have Hn2 : (n./2 < n)%coq_nat. apply/ltP; by rewrite -divn2 ltn_Pdiv. have even_n : ~~odd n by rewrite odd_square Hnp odd_double. move: Hnp; rewrite -(even_double_half n) //. rewrite -muln2 mulnAC mulnA !muln2 => /double_inj Hnp. have even_p : ~~odd p by rewrite odd_square -Hnp odd_double. move: Hnp; rewrite -(even_double_half p) // => /esym. by rewrite -muln2 mulnAC mulnA !muln2 => /double_inj /esym /IH ->. Qed. (* 無理数 *) Definition irrational (x : R) : Prop := forall (p : Z) (q : nat), q <> 0 -> x <> (IZR p / INR q)%R. Theorem irrational_sqrt_2: irrational (sqrt (INR 2)). Proof. move=> p q Hq Hrt. elim Hq. apply (main_thm (Zabs_nat p)). apply INR_eq. rewrite -mul2n !mult_INR -(sqrt_def (INR 2)) ?{}Hrt; last by auto with real. have Hqr : INR q <> 0%R by auto with real. case: p => /= [|p|p]. by field. rewrite INR_IPR /IZR; by field. rewrite INR_IPR /IZR; by field. Qed. End Irrational. (* 京大・理・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. Theorem mpr_a2 : coprime (pnat (prod2 ab ab)) (pirr (prod2 ab ab)). Proof. rewrite /=. rewrite [b*a]mulnC addnn -muln2. rewrite !coprime_mulr /coprime. rewrite (gcdnC _ a) gcdnMDl. rewrite -/(coprime a (2 * b * b)) !coprime_mulr !Hab. rewrite coprimen2 odd_a /=. Abort. 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). Admitted. Theorem 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). Admitted. End Problem2. (* 名古屋大学 2013 *) Section Nagoya2013. Definition Sk k n := \sum_(1<=i 1. Definition Tm n := \sum_(1<=k i _. by rewrite Sk1 muln1. Print ordinal. 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). Admitted. 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.