From 726319f6e1ef5a9bfcfe31febf304f1d7b057d5d Mon Sep 17 00:00:00 2001
From: Jimmy Xin <jxin31415@gmail.com>
Date: Fri, 2 Aug 2024 22:40:22 +0200
Subject: [PATCH] 1981-82 coq fixes

---
 coq/src/putnam_1981_a1.v | 11 +++--------
 coq/src/putnam_1981_a3.v |  4 ++--
 coq/src/putnam_1982_a2.v |  2 +-
 coq/src/putnam_1982_a3.v |  2 +-
 coq/src/putnam_1982_a5.v |  1 +
 coq/src/putnam_1982_a6.v |  6 +++---
 6 files changed, 11 insertions(+), 15 deletions(-)

diff --git a/coq/src/putnam_1981_a1.v b/coq/src/putnam_1981_a1.v
index d8b39181..c8b01ce3 100644
--- a/coq/src/putnam_1981_a1.v
+++ b/coq/src/putnam_1981_a1.v
@@ -1,12 +1,7 @@
-Require Import Nat Reals Coquelicot.Coquelicot. From mathcomp Require Import div.
-Definition putnam_1981_a1_solution := 1 / 8.
+Require Import Nat Reals Coquelicot.Coquelicot. From mathcomp Require Import div bigop.
+Definition putnam_1981_a1_solution : R := Rdiv 1 8.
 Theorem putnam_1981_a1
-    (prod_n : (nat -> nat) -> nat -> nat := fix prod_n (m: nat -> nat) (n : nat) :=
-        match n with
-        | O => m 0%nat
-        | S n' => mul (m n') (prod_n m n')
-    end)
-    (P : nat -> nat -> Prop := fun n k => 5 ^ k %| prod_n (fun m => Nat.pow m m) (S n) = true)
+    (P : nat -> nat -> Prop := fun n k => 5 ^ k %| (\prod_(1<=i<n+1) (i^i)) = true)
     (f : nat -> nat)
     (hf : forall (n: nat), gt n 1 -> P n (f n) /\ forall (k: nat), P n k -> le k (f n))
     : Lim_seq (fun n => INR (f n) / INR n ^ 2) = putnam_1981_a1_solution.
diff --git a/coq/src/putnam_1981_a3.v b/coq/src/putnam_1981_a3.v
index 8bc0bf84..c9a7e8b0 100644
--- a/coq/src/putnam_1981_a3.v
+++ b/coq/src/putnam_1981_a3.v
@@ -1,5 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_1981_a3_solution := 14.
+Definition putnam_1981_a3_solution := False.
 Theorem putnam_1981_a3
-    : Lim_seq (fun k => exp (-1*INR k) * (RInt (fun x => (RInt (fun y => (exp x - exp y) / (x - y)) 0 (INR k))) 0 (INR k))) = putnam_1981_a3_solution.
+    : (exists r : R, Lim (fun k => exp (-1*k) * (RInt (fun x => (RInt (fun y => (exp x - exp y) / (x - y)) 0 k)) 0 k)) p_infty = r) <-> putnam_1981_a3_solution.
 Proof. Admitted.
diff --git a/coq/src/putnam_1982_a2.v b/coq/src/putnam_1982_a2.v
index 96b94012..4fa5295f 100644
--- a/coq/src/putnam_1982_a2.v
+++ b/coq/src/putnam_1982_a2.v
@@ -3,6 +3,6 @@ Open Scope R.
 Definition putnam_1982_a2_solution := True.
 Theorem putnam_1982_a2
     (B : nat -> R -> R := fun n x => sum_n (fun m => Rpower (INR m) x) n)
-    (f : nat -> R := fun n => B n (ln 2 / ln (INR n)) / (INR n) * Rpower (ln 2 / ln (INR n)) 2)
+    (f : nat -> R := fun n => B n (ln 2 / ln (INR n)) / ((INR n) * Rpower (ln 2 / ln (INR n)) 2))
     : ex_series (fun n => if (lt_dec n 2) then 0 else f n) <-> putnam_1982_a2_solution.
 Proof. Admitted.
diff --git a/coq/src/putnam_1982_a3.v b/coq/src/putnam_1982_a3.v
index 03cc94e0..4a4c11d4 100644
--- a/coq/src/putnam_1982_a3.v
+++ b/coq/src/putnam_1982_a3.v
@@ -3,5 +3,5 @@ Open Scope R.
 Definition putnam_1982_a3_solution := PI / 2 * ln PI.
 Theorem putnam_1982_a3
     (f : R -> R := fun x => (atan (PI * x) - atan x) / x)
-    : Lim_seq (fun n => RInt f 0 (INR n)) = putnam_1982_a3_solution.
+    : Lim (fun n => RInt f 0 n) p_infty = putnam_1982_a3_solution.
 Proof. Admitted.
diff --git a/coq/src/putnam_1982_a5.v b/coq/src/putnam_1982_a5.v
index 72be8af0..31afca23 100644
--- a/coq/src/putnam_1982_a5.v
+++ b/coq/src/putnam_1982_a5.v
@@ -2,6 +2,7 @@ Require Import Reals.
 Open Scope R.
 Theorem putnam_1982_a5 
     (a b c d: nat)
+    (hpos : Nat.lt 0 a /\ Nat.lt 0 b /\ Nat.lt 0 c /\ Nat.lt 0 d)
     (habcd : Nat.le (Nat.add a c) 1982 /\ INR a / INR b + INR c / INR d < 1)
     : 1 - INR a / INR b - INR c / INR d > 1/pow 1983 3.
 Proof. Admitted.
diff --git a/coq/src/putnam_1982_a6.v b/coq/src/putnam_1982_a6.v
index ef6cfb4a..36c70ba0 100644
--- a/coq/src/putnam_1982_a6.v
+++ b/coq/src/putnam_1982_a6.v
@@ -3,7 +3,7 @@ Open Scope R.
 Definition putnam_1982_a6_solution := False.
 Theorem putnam_1982_a6
     (a: nat -> R) 
-    : (Series a = 1 /\ forall (i j: nat), le i j -> Rabs (a i) > Rabs (a j)) /\
-    forall (f: nat -> nat), Lim_seq (fun i => Rabs (INR (f i - i)) * Rabs (a i)) = 0 ->
-    Series (fun i => a (f i)) = 1 -> putnam_1982_a6_solution.    
+    : ((Series a = 1 /\ forall (i j: nat), le i j -> Rabs (a i) > Rabs (a j)) /\
+    forall (f: nat -> nat), Lim_seq (fun i => Rabs (INR (f i - i)) * Rabs (a i)) = 0 -> exists f', forall x, f' (f x) = x /\ f (f' x) = x -> 
+    Series (fun i => a (f i)) = 1) <-> putnam_1982_a6_solution.    
 Proof. Admitted.