Migrated to depend on MathComp.

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.

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.

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.

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.
+

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.
+