did isabelle and coq fixes for Putnam 1997

coq/src/commented_problems.v

@@ -133,3 +133,36 @@ Theorem putnam_2003_b5
     Triangle A' B' C' /\ dist A' B' = a /\ dist B' C' = b /\ dist C' A' = c /\
     F_to_R (signed_area A' B' C' D A' B' C') = (putnam_2003_b5_solution pt_to_R dist P Op).
 Proof. Admitted. *)
+
+(* Require Import Reals Rgeom ZArith 
+GeoCoq.Main.Tarski_dev.Ch16_coordinates_with_functions 
+GeoCoq.Main.Annexes.midpoint_theorems
+GeoCoq.Main.Highschool.circumcenter.
+Context `{T2D:Tarski_2D} `{TE:@Tarski_euclidean Tn TnEQD}.
+Open Scope R.
+Definition putnam_1997_a1_solution := 28.
+Theorem putnam_1997_a1
+    (pt_to_R : Tpoint -> (R * R))
+    (dist : Tpoint -> Tpoint -> R := fun A B => let (a, b) := pt_to_R A in let (c, d) := pt_to_R B in dist_euc a b c d)
+    (A B C : Tpoint)
+    (Hp Op Mp Fp : Tpoint)
+    (l1 : dist Hp Op = 11)
+    (l2 : dist Op Mp = 5)
+    (s : Rectangle Hp Op Mp Fp)
+    (hHp : Bet A Fp Hp)
+    (hOp : is_circumcenter Op A B C)
+    (hMp : Midpoint B C Mp)
+    (hFp : Perp A C B Fp /\ Col A C Fp)
+    : dist B C = putnam_1997_a1_solution.
+Proof. Admitted. *)
+
+(* Require Import Nat Reals Coquelicot.Coquelicot ZArith.
+Theorem putnam_1997_b4
+    (a : nat -> nat -> Z)
+    (max_degree : nat -> nat)
+    (coeff : nat -> (nat -> R))
+    (hpoly : forall (m : nat) (x : R), sum_n (fun i => (coeff m i) * (x^i)) (max_degree m) = (1 + x + x^2)^m)
+    (ha : forall m n : nat, IZR (a m n) = coeff m n)
+    : forall k : nat, ge k 0 -> 0 <= (sum_n (fun i => (-1)^i * (IZR (a (Nat.sub k i) i))) (Z.to_nat (Coquelicot.Rcomplements.floor (2 * INR k / 3)))) <= 1.
+Proof. Admitted. *)
+

coq/src/putnam_1997_a3.v

@@ -1,6 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1997_a3_solution := sqrt (exp 1).
+Definition putnam_1997_a3_solution : R := sqrt (exp 1).
 Theorem putnam_1997_a3
     (evenfact := fix even_fact (n : nat) : R :=
         match n with
@@ -10,9 +10,9 @@ Theorem putnam_1997_a3
     (evenfactsqr := fix even_fact_sqr (n : nat) : R :=
         match n with
         | O => 1 
-        | S n' => pow (2 * INR n) 2 * evenfact n'
+        | S n' => pow (2 * INR n) 2 * even_fact_sqr n'
     end)
     (f : R -> R := fun x => Series (fun n => pow (-1) n * pow x (2 * n + 1) / evenfact n))
     (g : R -> R := fun x => Series (fun n => pow x (2 * n) / evenfactsqr n))
-    : Lim_seq (fun n => sum_n (fun m => RInt (fun x => f x * g x) 0 (INR m)) n) = putnam_1997_a3_solution.
+    : Lim_seq (fun t : nat => RInt (fun x => f x * g x) 0 (INR t)) = putnam_1997_a3_solution.
 Proof. Admitted.

coq/src/putnam_1997_a4.v

@@ -1,4 +1,4 @@
-(* Note: This formalization is only a statement finite groups (due to mathcomp), but the idea ot the problem does not rely on the cardinal of the group, so we include it*)
+(* Note: This formalization is only a statement finite groups (due to mathcomp), but the idea of the problem does not rely on the cardinal of the group, so we include it*)
 Require Import Basics. From mathcomp Require Import fingroup.
 Open Scope group_scope.
 Variable T : finGroupType.

coq/src/putnam_1997_a5.v

@@ -2,7 +2,7 @@ Require Import Nat Ensembles Finite_sets List Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1997_a5_solution := True.
 Theorem putnam_1997_a5
-    (E: Ensemble (list nat) := fun l => length l = 10%nat /\ sum_n (fun i => 1/ INR (nth i l 0%nat)) 10 = 1)
+    (E: Ensemble (list nat) := fun l => length l = 10%nat /\ (forall i : nat, lt i 10 -> gt (nth i l 0%nat) 0) /\ sum_n (fun i => 1/ INR (nth i l 0%nat)) 9 = 1)
     (m: nat)
-    : cardinal (list nat) E m /\ odd m = true <-> putnam_1997_a5_solution.
+    : cardinal (list nat) E m -> (odd m = true <-> putnam_1997_a5_solution).
 Proof. Admitted.

coq/src/putnam_1997_a6.v

@@ -1,15 +1,16 @@
 Require Import Binomial Nat Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1997_a6_solution (n k: nat) := Binomial.C (n - 1) (k - 1).
+Definition putnam_1997_a6_solution : nat -> nat -> R := (fun n k : nat => Binomial.C (n - 1) (k - 1)).
 Theorem putnam_1997_a6
-    (X := fix x (n: nat) (c: R) (k: nat) : R :=
+    (n : nat)
+    (maxc : R)
+    (X := fix x (c: R) (k: nat) : R :=
         match k with
         | O => 0 
         | S O => 1 
-        | S ((S k'') as k') => (c * x n c k' - INR (n - k) * x n c k'') / INR k'
+        | S ((S k'') as k') => (c * x c k' - INR (n - k) * x c k'') / INR k'
     end)
-    : forall (n: nat), exists (maxc: R), forall (c: R),
-    X n c (S n) = 0 /\ X n maxc (S n) = 0 -> c <= maxc ->
-    forall (k: nat), and (le 1 k) (le k n) -> 
-    X n c k = putnam_1997_a6_solution n k.
+    (npos : gt n 0)
+    (hmaxc : X maxc (add n 1) = 0 /\ (forall c : R, X c (add n 1) = 0 -> c <= maxc))
+    : forall (k: nat), (le 1 k /\ le k n) -> X maxc k = putnam_1997_a6_solution n k.
 Proof. Admitted.

coq/src/putnam_1997_b1.v

@@ -1,7 +1,7 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1997_b1_solution (n: nat) := INR n.
+Definition putnam_1997_b1_solution : nat -> R := (fun n : nat => INR n).
 Theorem putnam_1997_b1
     (rnd : R -> R := fun x => Rmin (Rabs (IZR (floor x) - x)) (Rabs (IZR (floor (x + 1)) - x)))
-    : forall (n: nat), gt n 0 -> sum_n (fun m => Rmin (rnd ((INR m + 1) / (6 * INR n))) (rnd ((INR m + 1) / (3 * INR n)))) (6 * n - 1) = putnam_1997_b1_solution n.
+    : forall (n: nat), gt n 0 -> sum_n_m (fun m => Rmin (rnd (INR m / (6 * INR n))) (rnd (INR m / (3 * INR n)))) 1 (6 * n - 1) = putnam_1997_b1_solution n.
 Proof. Admitted.

coq/src/putnam_1997_b2.v

@@ -1,7 +1,9 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1997_b2 
-    (f g: R -> R)
-    (habsbdd : R -> Prop := fun m => forall x, -m <= abs (f x) <= m)
-    : exists (M: R), forall (x: R), ex_derive_n f 2 x /\ g x >= 0 /\ f x + Derive_n f 2 x = -x * g x * Derive f x -> habsbdd M.
+    (f g : R -> R)
+    (hg : forall x : R, g x >= 0)
+    (hfdiff : forall x : R, ex_derive f x /\ ex_derive_n f 2 x)
+    (hfg : forall x : R, f x + Derive_n f 2 x = -x * g x * Derive f x)
+    : exists M : R, (forall x : R, -M <= abs (f x) <= M).
 Proof. Admitted.

coq/src/putnam_1997_b3.v

@@ -1,7 +1,10 @@
 Require Import Reals Coquelicot.Coquelicot. From mathcomp Require Import div.
 Open Scope R.
-Definition putnam_1997_b3_solution (n: nat) := and (le 1 n) (le n 4) \/ and (le 20 n) (le n 24)  \/ and (le 100 n) (le n 104) \/ and (le 120 n) (le n 124).
+Definition putnam_1997_b3_solution : nat -> Prop := (fun n : nat => (le 1 n /\ le n 4) \/ (le 20 n /\ le n 24) \/ (le 100 n /\ le n 104) \/ (le 120 n /\ le n 124)).
 Theorem putnam_1997_b3
-    : forall (n: nat), gt n 0 -> exists (p q: nat), gt p 0 /\ gt q 0 /\ coprime p q = true /\
-    sum_n (fun m => 1 / INR (m + 1)) n = INR p / INR q -> neq (q mod 5) 0 -> putnam_1997_b3_solution n.
+    (n : nat)
+    (p q : nat)
+    (hn : gt n 0)
+    (hpq : gt p 0 /\ gt q 0 /\ coprime p q = true /\ sum_n_m (fun m => 1 / INR m) 1 n = INR p / INR q)
+    : neq (q mod 5) 0 <-> putnam_1997_b3_solution n.
 Proof. Admitted.

coq/src/putnam_1997_b5.v

@@ -1,9 +1,11 @@
 Require Import Nat.
-Theorem putnam_1997_b5 
-    (pown := fix pow_n (b n: nat) : nat :=
-      match n with
+Theorem putnam_1997_b5
+    (powm := fix pow_m (b m: nat) : nat :=
+      match m with
       | O => 1
-      | S n' => b * pow_n b n'
+      | S m' => b ^ (pow_m b m')
     end)
-    : forall (n: nat), n >= 2 -> pown 2 n-1 mod n = pown 2 n-2.
+    (n : nat)
+    (hn : n >= 2)
+    : (powm 2 n) mod n = (powm 2 (n-1)) mod n.
 Proof. Admitted.

isabelle/putnam_1997_a5.thy

@@ -5,8 +5,7 @@ definition putnam_1997_a5_solution where "putnam_1997_a5_solution \<equiv> undef
 (* True *)
 theorem putnam_1997_a5:
   fixes N::"nat\<Rightarrow>nat"
-  defines "N \<equiv> \<lambda>n. card {t::nat list. (size t = n) \<and> (\<forall>i \<in> {0..<n}. t!i > 0) \<and> (\<forall>i \<in> {0..<n}. \<forall>j \<in> {0..<n}. i < j \<longrightarrow> t!i \<le> t!j) 
-    \<and> (\<Sum>i=0..<n. 1 / (t!i)) = 1}"
+  defines "N \<equiv> \<lambda>n. card {t::nat list. (size t = n) \<and> (\<forall>i \<in> {0..<n}. t!i > 0) \<and> (\<Sum>i=0..<n. 1 / (t!i)) = 1}"
   shows "odd (N 10) \<longleftrightarrow> putnam_1997_a5_solution"
   sorry
 

isabelle/putnam_1997_a6.thy

@@ -2,13 +2,13 @@ theory putnam_1997_a6 imports Complex_Main
 
 begin
 
-definition putnam_1997_a6_solution :: "int \<Rightarrow> int \<Rightarrow> real" where
+definition putnam_1997_a6_solution :: "nat \<Rightarrow> nat \<Rightarrow> real" where
 "putnam_1997_a6_solution \<equiv> undefined"
-(* \<lambda> n k. (nat n-1) choose (nat k-1) *)
+(* \<lambda> n k. (n-1) choose (k-1) *)
 theorem putnam_1997_a6:
-  fixes n :: "int"
+  fixes n :: "nat"
     and C :: "real"
-    and x :: "real \<Rightarrow> (int \<Rightarrow> real)"
+    and x :: "real \<Rightarrow> (nat \<Rightarrow> real)"
     and S :: "real set"
   defines "S \<equiv> {c :: real. x c (n + 1) = 0}"
   assumes hx0 : "\<forall> c :: real. x c 0 = 0"

isabelle/putnam_1997_b2.thy

@@ -6,9 +6,9 @@ begin
 theorem putnam_1997_b2:
   fixes f g :: "real \<Rightarrow> real"
   assumes hg : "\<forall> x :: real. g x \<ge> 0"
-    and hfdiff : "(f differentiable_on UNIV) \<and> (deriv f) differentiable_on UNIV"
+    and hfdiff : "(f C1_differentiable_on UNIV) \<and> (deriv f) differentiable_on UNIV"
     and hfg : "\<forall> x :: real. f x + (deriv^^2) f x = -x * g x * (deriv f x)"
-  shows "bounded (image f UNIV)"
+  shows "bounded (image (\<lambda>x::real. \<bar>f x\<bar>) UNIV)"
   sorry
 
 end

isabelle/putnam_1997_b4.thy

@@ -5,8 +5,8 @@ begin
 
 theorem putnam_1997_b4:
   fixes a :: "nat \<Rightarrow> nat \<Rightarrow> int"
-  assumes ha : "\<forall> n m :: nat. a n m = coeff ((monom 1 0 + monom 1 1 + monom 1 2)^m) n"
-  shows "\<forall> k :: nat \<ge> 0. (\<Sum> i \<in> {0..nat \<lfloor>((2*(rat_of_nat k)))/(rat_of_nat 3)\<rfloor>}. (-1)^(i) * (a (k-i) i)) \<in> {0 :: real..1}" 
+  assumes ha : "\<forall> m n :: nat. a m n = coeff ((monom 1 0 + monom 1 1 + monom 1 2)^m) n"
+  shows "\<forall> k :: nat \<ge> 0. (\<Sum> i \<in> {0..nat \<lfloor>(2*(rat_of_nat k))/(rat_of_nat 3)\<rfloor>}. (-1)^i * (a (k-i) i)) \<in> {0 :: real..1}" 
   sorry
 
 end

isabelle/putnam_1997_b5.thy

@@ -8,7 +8,7 @@ theorem putnam_1997_b5:
     and tetration :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   assumes hn : "n \<ge> 2"
     and htetrationbase : "\<forall> a :: nat. tetration a 0 = 1"
-    and htetration : "\<forall> a n :: nat. tetration a (n+1) = a^(tetration a n)"
+    and htetration : "\<forall> a m :: nat. tetration a (m+1) = a^(tetration a m)"
   shows "[tetration 2 n = tetration 2 (n-1)] (mod n)"
   sorry