From 0d7d834251f68b9a7b9c9d45e40ff7f3fd76ce23 Mon Sep 17 00:00:00 2001 From: George Tsoukalas Date: Tue, 27 Aug 2024 16:31:42 +0000 Subject: [PATCH] Migrated to depend on MathComp. --- coq/src/putnam_1979_a1.v | 20 ++++++++++++++------ coq/src/putnam_1979_a2.v | 25 +++++++++++++++++++++++-- coq/src/putnam_1979_a3.v | 28 +++++++++++++++------------- coq/src/putnam_1979_a5.v | 23 +++++++++++++++++------ coq/src/putnam_1979_a6.v | 23 +++++++++++++++-------- coq/src/putnam_1979_b2.v | 25 +++++++++++++++++++------ coq/src/putnam_1979_b6.v | 6 ++++++ coq/src/putnam_1980_a2.v | 22 ++++++++++++++++------ coq/src/putnam_1980_a3.v | 21 ++++++++++++++++----- coq/src/putnam_1980_a4.v | 21 ++++++++++++++------- coq/src/putnam_1980_a5.v | 27 +++++++++++++++++---------- coq/src/putnam_1980_b1.v | 19 +++++++++++++++---- coq/src/putnam_1980_b3.v | 27 +++++++++++++++++---------- coq/src/putnam_1980_b6.v | 19 ++++++++++++------- 14 files changed, 216 insertions(+), 90 deletions(-) diff --git a/coq/src/putnam_1979_a1.v b/coq/src/putnam_1979_a1.v index e6b37ef4..06476b5f 100644 --- a/coq/src/putnam_1979_a1.v +++ b/coq/src/putnam_1979_a1.v @@ -1,8 +1,16 @@ -Require Import Nat List. -Definition putnam_1979_a1_solution := 2 :: repeat 3 659. +From mathcomp Require Import all_algebra all_ssreflect. +From mathcomp Require Import multiset. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope mset_scope. + +(* Note: The documentation in finmap/multisets.v appears to contain a typo, `mset n a` is not defined, though `msetn n a` seems to do the intended thing. *) +Definition putnam_1979_a1_solution : {mset nat} := 2 |` (msetn 659 3). Theorem putnam_1979_a1 - (l : list nat) - (hl : fold_left add l 0 = 1979) - (hlmax : forall m: list nat, fold_left add m 0 = 1979 /\ fold_left mul l 1 >= fold_left mul m 1) - : l = putnam_1979_a1_solution. + (P : {mset nat} -> Prop) + (hP : forall A : {mset nat}, P A <-> ((exists a : nat, a \in A) /\ (forall i : nat, i \in A -> i > 0) /\ (\sum_(j <- A) j = 1979))) + : P putnam_1979_a1_solution /\ (forall A : {mset nat}, P A -> \prod_(j <- putnam_1979_a1_solution) j >= \prod_(j <- A) j). Proof. Admitted. diff --git a/coq/src/putnam_1979_a2.v b/coq/src/putnam_1979_a2.v index e27a5273..77b2421a 100644 --- a/coq/src/putnam_1979_a2.v +++ b/coq/src/putnam_1979_a2.v @@ -1,6 +1,27 @@ -Require Import Basics Reals Coquelicot.Coquelicot. +(* Require Import Basics Reals Coquelicot.Coquelicot. Definition putnam_1979_a2_solution (k : R) := k >= 0. Theorem putnam_1979_a2 : forall (k: R), (exists (f: R -> R), continuity f /\ forall x, (compose f f) x = k * pow x 9) <-> putnam_1979_a2_solution k. -Proof. Admitted. +Proof. Admitted. *) + +From mathcomp Require Import all_algebra all_ssreflect. +From mathcomp Require Import reals topology sequences derive normedtype realfun real_interval. +From mathcomp Require Import classical_sets. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope ring_scope. +Local Open Scope classical_set_scope. + +Import numFieldNormedType.Exports. + +About continuous. + +Variable R : realType. +Definition putnam_1979_a2_solution : set R := [set x : R | x >= 0]. +Theorem putnam_1979_a2 + : forall k : R, (exists f : R -> R, continuous f /\ (forall x : R, f (f x) = k * x ^+ 9)) <-> k \in putnam_1979_a2_solution. +Proof. Admitted. \ No newline at end of file diff --git a/coq/src/putnam_1979_a3.v b/coq/src/putnam_1979_a3.v index 8e23210e..40963028 100644 --- a/coq/src/putnam_1979_a3.v +++ b/coq/src/putnam_1979_a3.v @@ -1,14 +1,16 @@ -Require Import Reals Coquelicot.Coquelicot. -Open Scope R. -Definition putnam_1979_a3_solution (x y: R) := x = IZR (floor x) /\ y = IZR (floor y). +From mathcomp Require Import all_algebra all_ssreflect. +From mathcomp Require Import reals sequences. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope ring_scope. + +Variable R : realType. +Definition putnam_1979_a3_solution : (R*R)%type -> Prop := fun '(a, b) => exists m : int, a = m%:~R /\ b = m%:~R. Theorem putnam_1979_a3 - (A := fix a (x y: R) (n: nat) := - match n with - | O => x - | S O => y - | S ((S n'') as n') => (a x y n'' * a x y n') / (2 * a x y n'' - a x y n') - end) - : forall (n: nat), exists (x y: R), (A x y n+1 <> 2 * A x y n) /\ - (~ exists (r: R), A x y n = IZR (floor (A x y n)) /\ INR n < r) - <-> putnam_1979_a3_solution x y. -Proof. Admitted. + (x : R ^nat) + (hx : forall n : nat, x n <> 0 /\ (ge n 3 -> x n = (x (n.-2)) * (x (n.-1))/(2 * (x (n.-2)) - (x (n.-1))))) + : (forall m : nat, exists n : nat, gt n m /\ (exists a : int, x n = a%:~R)) <-> putnam_1979_a3_solution (x 1%nat, x 2%nat). +Proof. Admitted. \ No newline at end of file diff --git a/coq/src/putnam_1979_a5.v b/coq/src/putnam_1979_a5.v index ea9ee3ff..460283ea 100644 --- a/coq/src/putnam_1979_a5.v +++ b/coq/src/putnam_1979_a5.v @@ -1,7 +1,18 @@ -Require Import Reals Coquelicot.Coquelicot. -Open Scope R. -Theorem putnam_1979_a5 - (f : R -> R := fun x => Rpower x 3 - 10 * pow x 2 + 29 * x - 25) - : exists (r1 r2: R), r1 <> r2 /\ f r1 = 0 /\ f r2 = 0 /\ - ~ exists (r: R), forall (n: nat), exists (p q: Z), n = Z.to_nat (floor (IZR p * r1)) /\ n = Z.to_nat (floor (IZR q * r2)) /\ INR n < r. +From mathcomp Require Import all_algebra all_ssreflect. +From mathcomp Require Import reals. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope ring_scope. + +Variable R : realType. +Theorem putnam_1979_a5 + (S : R -> nat -> int) + (hS : forall (x : R) (n : nat), S x n = floor (n%:R * x)) + (P : R -> Prop) + (hP : forall (x : R), P x <-> (x ^+ 3) - 10 * (x ^+ 2) + 29 * x - 25 = 0) + : exists (a b : R), (a <> b) /\ P a /\ P b /\ (forall n : nat, exists m : int, m >= n%:Z /\ (exists c d : nat, S a c = m /\ S b d = m)). Proof. Admitted. + diff --git a/coq/src/putnam_1979_a6.v b/coq/src/putnam_1979_a6.v index 99ee5063..d56166e1 100644 --- a/coq/src/putnam_1979_a6.v +++ b/coq/src/putnam_1979_a6.v @@ -1,8 +1,15 @@ -Require Import Reals Coquelicot.Coquelicot. -Open Scope R. -Theorem putnam_1979_a6 - (a: nat -> R) - : forall n: nat, 0 <= a n <= 1 -> - exists (b: R), 0 <= b <= 1 -> - sum_n (fun n => 1/(b - a n)) n <= 8 * INR n * sum_n (fun i => 1/(2*(INR i+1) - 1)) n. -Proof. Admitted. +From mathcomp Require Import all_algebra all_ssreflect fintype. +From mathcomp Require Import reals. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope ring_scope. + +Variable R : realType. +Theorem putnam_1979_b6 + (p : seq R) + (hp : all (fun x => 0 <= x <= 1) p) + : exists x : R, 0 <= x <= 1 /\ (all (fun i => x != i) p) /\ (\sum_(i <- p) 1/`|x - i|) <= 8*(size p)%:R*(\sum_(0 <= i < (size p).+1) (1%R)/(2*(i%:R) + 1)). +Proof. Admitted. \ No newline at end of file diff --git a/coq/src/putnam_1979_b2.v b/coq/src/putnam_1979_b2.v index 7fc378d5..5474eba3 100644 --- a/coq/src/putnam_1979_b2.v +++ b/coq/src/putnam_1979_b2.v @@ -1,8 +1,21 @@ -Require Import Reals Coquelicot.Coquelicot. -Definition putnam_1979_b2_solution (a b: R):= (Rpower b (b/(b-a))) / ((exp 1) * Rpower a (a/(b-a))). +From mathcomp Require Import all_algebra all_ssreflect. +From mathcomp Require Import boolp reals measure lebesgue_measure lebesgue_integral topology normedtype exp sequences. +From mathcomp Require Import classical_sets. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import numFieldNormedType.Exports. + +Local Open Scope ring_scope. +Local Open Scope classical_set_scope. + +Variable R : realType. +Definition mu := [the measure _ _ of @lebesgue_measure R]. +Definition putnam_1979_b2_solution : R -> R -> R := fun a b => (expR ((b/(b-a)) * ln b))/(expR 1 * (expR ((a/(b-a)) * ln a))). Theorem putnam_1979_b2 - (a b: R) + (a b : R) (hab : 0 < a < b) - : Lim_seq (fun lam => Rpower (RInt (fun x => Rpower (b*x + a*(1-x)) (INR lam)) 0 1) 1/INR lam) - = putnam_1979_b2_solution a b. -Proof. Admitted. + (f : R -> R := fun t : R => expR (1/t * ln (\int[mu]_(x in [set x : R | 0 <= x <= 1]) expR (t * ln (b * x + a * (1 - x)))))) + : f @ (dnbhs 0) --> putnam_1979_b2_solution a b. +Proof. Admitted. \ No newline at end of file diff --git a/coq/src/putnam_1979_b6.v b/coq/src/putnam_1979_b6.v index ad84ddee..10fd62d6 100644 --- a/coq/src/putnam_1979_b6.v +++ b/coq/src/putnam_1979_b6.v @@ -8,3 +8,9 @@ Theorem putnam_1979_b6 (sum2 := fold_left (fun acc x => Re x) l 0) : sqrt (Re sum1) <= sum2. Proof. Admitted. + + +From mathcomp Require Import all_algebra all_ssreflect. +From mathcomp Require Import reals complex. + +About Rcomplex. \ No newline at end of file diff --git a/coq/src/putnam_1980_a2.v b/coq/src/putnam_1980_a2.v index d6945afa..94697aab 100644 --- a/coq/src/putnam_1980_a2.v +++ b/coq/src/putnam_1980_a2.v @@ -1,8 +1,18 @@ -Require Import Nat Ensembles Finite_sets. -Definition putnam_1980_a2_solution (m n: nat) := (6*m*m + 3*m + 1) * (6*n*n + 3*n + 1). +From mathcomp Require Import all_algebra all_ssreflect. +From mathcomp Require Import classical_sets cardinality. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope classical_set_scope. +Local Open Scope card_scope. + +Definition putnam_1980_a2_solution : nat -> nat -> nat := fun r s : nat => (1 + 4 * r + 6 * r ^2) * (1 + 4 * s + 6 * s ^ 2). Theorem putnam_1980_a2 - (gcd3 : nat -> nat -> nat -> nat := fun a b c => gcd (gcd a b) c) - (f: Ensemble (nat*nat)) - : forall (m n: nat) (a b c d: nat), - (f (m, n) <-> gcd3 a b c = 3 ^ m * 7 ^ n \/ gcd3 a b d = 3 ^ m * 7 ^ n \/ gcd3 a c d = 3 ^ m * 7 ^ n \/ gcd3 b c d = 3 ^ m * 7 ^ n) -> cardinal (nat*nat) f (putnam_1980_a2_solution m n). + (r s : nat) + (abcdlcm : nat -> nat -> nat -> nat -> Prop) + (rpos : r > 0 /\ s > 0) + (habcdlcm : forall a b c d, abcdlcm a b c d <-> (a > 0 /\ b > 0 /\ c > 0 /\ d > 0 /\ (3 ^ r * 7 ^ s = lcmn (lcmn a b) c) /\ (3 ^ r * 7 ^ s = lcmn (lcmn a b) d) /\ (3 ^ r * 7 ^ s = lcmn (lcmn a c) d) /\ (3 ^ r * 7 ^ s = lcmn (lcmn b c) d))) + : [set t : 4.-tuple nat | abcdlcm (tnth t (inord 0)) (tnth t (inord 1)) (tnth t (inord 2)) (tnth t (inord 3))] #= `I_(putnam_1980_a2_solution r s). Proof. Admitted. diff --git a/coq/src/putnam_1980_a3.v b/coq/src/putnam_1980_a3.v index 3ecf0891..1a021d47 100644 --- a/coq/src/putnam_1980_a3.v +++ b/coq/src/putnam_1980_a3.v @@ -1,7 +1,18 @@ -Require Import Reals Coquelicot.Coquelicot. -Open Scope R. -Definition putnam_1980_a3_solution := PI/4. +From mathcomp Require Import all_algebra all_ssreflect. +From mathcomp Require Import reals lebesgue_integral measure lebesgue_measure trigo sequences exp. +From mathcomp Require Import classical_sets. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope ring_scope. +Local Open Scope classical_set_scope. + +(* Note: Unaware of definition of non-integer powers, workaround is exp log*) +Variable R : realType. +Definition mu := [the measure _ _ of @lebesgue_measure R]. +Definition putnam_1980_a3_solution : R := pi/4. Theorem putnam_1980_a3 - (f : R -> R := fun x => 1/(1 + Rpower (tan x) (sqrt 2))) - : RInt f 0 PI/2 = putnam_1980_a3_solution. + : \int[mu]_(x in [set t : R | 0 < t < pi/2]) (fun (x : R) => 1/(1 + expR (ln (@tan R x) * (@Num.sqrt R 2)))) x = putnam_1980_a3_solution. Proof. Admitted. diff --git a/coq/src/putnam_1980_a4.v b/coq/src/putnam_1980_a4.v index e7296972..3a4ee75e 100644 --- a/coq/src/putnam_1980_a4.v +++ b/coq/src/putnam_1980_a4.v @@ -1,8 +1,15 @@ -Require Import Reals BinInt. -Open Scope Z. +From mathcomp Require Import all_algebra all_ssreflect. +From mathcomp Require Import reals. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope ring_scope. + +Variable R : realType. Theorem putnam_1980_a4 - : (forall (a b c: Z), (~ (a = 0 \/ b = 0 /\ c = 0) /\ Z.abs a < 10^6 /\ Z.abs b < 10^6 /\ Z.abs c < 10^6) -> - Rgt (Rabs (Rplus (Rplus (IZR a) (Rmult (IZR b) (sqrt 2))) (Rmult (IZR c) (sqrt 3)))) (Rpower 10 (-21)) ) - /\ (exists (a b c: Z), - Rlt (Rabs (Rplus (IZR a) (Rplus (Rmult (IZR b) (sqrt 2)) (Rmult (IZR c) (sqrt 3))))) (Rpower 10 (-11)) ). -Proof. Admitted. +(abcvals : int -> int -> int -> Prop) +(habcvals : forall (a b c : int), (abcvals a b c <-> (~ (a = 0 /\ b = 0 /\ c = 0) /\ `|a| < 10^6 /\ `|b| < 10^6 /\ `|c| < 10^6))) +: (exists (a b c : int), abcvals a b c /\ `|a%:~R + b%:~R * (@Num.sqrt R 2) + c%:~R * (@Num.sqrt R 3)| < 10^(-11)) /\ (forall (a b c : int), abcvals a b c -> `|a%:~R + b%:~R * (@Num.sqrt R 2) + c%:~R * (@Num.sqrt R 3)| > 10^(-21)). +Proof. Admitted. \ No newline at end of file diff --git a/coq/src/putnam_1980_a5.v b/coq/src/putnam_1980_a5.v index 0045678f..08a4425b 100644 --- a/coq/src/putnam_1980_a5.v +++ b/coq/src/putnam_1980_a5.v @@ -1,11 +1,18 @@ -Require Import Reals Coquelicot.Coquelicot. +From mathcomp Require Import all_algebra all_ssreflect. +From mathcomp Require Import reals trigo lebesgue_integral lebesgue_measure measure. +From mathcomp Require Import classical_sets cardinality. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Variable R : realType. +Definition mu := [the measure _ _ of @lebesgue_measure R]. Theorem putnam_1980_a5 - (n : nat) - (npos : gt n 0) - (coeff : nat -> R) - (hcoeff : coeff n <> 0) - (p : R -> R := fun x => sum_n (fun i => coeff i * x ^ i) (S n)) - (h1 : nat -> Prop := fun a => RInt (fun x => p x * sin x) 0 (INR a) = 0) - (h2 : nat -> Prop := fun a => RInt (fun x => p x * cos x) 0 (INR a) = 0) - : exists (m: nat), forall (b: nat), h1 b /\ h2 b -> lt b m. -Proof. Admitted. + (P : {poly R}) + (Pnonconst : gtn (size P) (1%nat)) + : finite_set [set x : R | \int[mu]_(t in [set t : R | 0 <= t <= x]) (fun x => P.[x] * (sin x)) t = 0 /\ \int[mu]_(t in [set t : R | 0 <= t <= x]) (fun x => P.[x] * (cos x)) t = 0]. +Proof. Admitted. \ No newline at end of file diff --git a/coq/src/putnam_1980_b1.v b/coq/src/putnam_1980_b1.v index cbf54a5b..d43b7fd1 100644 --- a/coq/src/putnam_1980_b1.v +++ b/coq/src/putnam_1980_b1.v @@ -1,6 +1,17 @@ -Require Import Reals Rtrigo_def. -Open Scope R. -Definition putnam_1980_b1_solution (k: R) := k >= 1/2. +From mathcomp Require Import all_algebra all_ssreflect. +From mathcomp Require Import reals sequences. +From mathcomp Require Import classical_sets. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Variable R : realType. +Definition putnam_1980_b1_solution : set R := [set x : R | x >= 1/2]. Theorem putnam_1980_b1 - : forall (k: R), forall (x: R), cosh x <= exp (k*x*x) <-> putnam_1980_b1_solution k. + (c : R) + : (forall x : R, (expR x + expR (-x)) / 2 <= expR (c * x^2)) <-> c \in putnam_1980_b1_solution. Proof. Admitted. diff --git a/coq/src/putnam_1980_b3.v b/coq/src/putnam_1980_b3.v index 190e3575..5d3805ad 100644 --- a/coq/src/putnam_1980_b3.v +++ b/coq/src/putnam_1980_b3.v @@ -1,12 +1,19 @@ -Require Import Reals. -Open Scope R. -Definition putnam_1980_b3_solution (b: R) := b >= 3. +From mathcomp Require Import all_algebra all_ssreflect. +From mathcomp Require Import sequences reals. +From mathcomp Require Import classical_sets. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Variable R : realType. +Definition putnam_1980_b3_solution : set R := [set x : R | x >= 3]. Theorem putnam_1980_b3 - (b: R) - (A := fix a (n: nat) : R := - match n with - | O => b - | S n' => 2 * a n' - INR (n' * n') - end) - : forall (n: nat), A n > 0 <-> putnam_1980_b3_solution b. + (a : R) + (u : R ^nat) + (hu : u 0%nat = a /\ (forall n : nat , u n.+1 = 2 * u n - ((n%:R) ^ 2))) + : (forall n : nat, u n > 0) <-> a \in putnam_1980_b3_solution. Proof. Admitted. diff --git a/coq/src/putnam_1980_b6.v b/coq/src/putnam_1980_b6.v index 87fb0ac8..b549bc6b 100644 --- a/coq/src/putnam_1980_b6.v +++ b/coq/src/putnam_1980_b6.v @@ -1,9 +1,14 @@ -Require Import Reals Nat Znumtheory QArith Coquelicot.Coquelicot. From mathcomp Require Import div. +From mathcomp Require Import all_algebra all_ssreflect. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope ring_scope. + Theorem putnam_1980_b6 - (A := fix f (n i: nat) := - match (n,i) with - | (O,i') => 1/INR i' - | (S n', i') => (INR n' + 1)/(INR i') * sum_n (fun x => f n' (Nat.add n' x)) (Nat.sub i' n') - end) - : forall (n p: nat), and (gt p n) (gt n 1) /\ prime (Z.of_nat p) -> exists (a b: nat), A n p = INR a/INR b /\ p %| b/(gcd a b) = false. +(G : (int * int)%type -> rat) +(hG : forall d n : nat, leq d n -> ((d = 1%nat -> G (d%:Z, n%:Z) = (1%:Q)/(n%:Q)) /\ (gtn d (1%nat) -> G (d%:Z, n%:Z) = ((d%:Z%:Q)/(n%:Z%:Q)) * \sum_(d <= i < n.+1) (G (d%:Z - 1, i%:Z - 1))))) +: forall (d p : nat), (ltn (1%nat) d /\ leq d p /\ prime p) -> ~ (p%:Z %| (denq (G (d%:Z, p%:Z))))%Z. Proof. Admitted. +