did isabelle and coq fixes for 2000

Author: leejasper851

coq/src/putnam_2000_a1.v

@@ -1,7 +1,7 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2000_a1_solution (x A: R) := 0 < x < A ^ 2.
+Definition putnam_2000_a1_solution : R -> (R -> Prop) := (fun A : R => (fun x : R => 0 < x < A ^ 2)).
 Theorem putnam_2000_a1
     (A: R)
     (hA : A > 0)
-    : forall (x: nat -> R), Series x = A -> putnam_2000_a1_solution (Series (fun j => x j ^ 2)) A.
+    : forall SS : R, ((exists x : nat -> R, (forall j : nat, x j > 0) /\ Series x = A /\ Series (fun j => (x j) ^ 2) = SS) <-> (putnam_2000_a1_solution A) SS).
 Proof. Admitted.

coq/src/putnam_2000_a4.v

@@ -1,4 +1,4 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2000_a4
-    : ex_finite_lim_seq (fun n => sum_n (fun x => sin (INR x) * sin ((INR x) ^ 2)) n).
+    : ex_finite_lim_seq (fun B : nat => RInt (fun x : R => sin x * sin (x ^ 2)) 0 (INR B)).
 Proof. Admitted.

coq/src/putnam_2000_a6.v

@@ -4,6 +4,6 @@ Theorem putnam_2000_a6
     (coeff : nat -> Z)
     (f : R -> R := fun x => sum_n (fun i => (IZR (coeff i)) * (x^i)) n)
     (a : nat -> R)
-    (ha : a O = 0 /\ forall i : nat, a (S n) = f (a n))
+    (ha : a O = 0 /\ forall i : nat, a (S i) = f (a i))
     : (exists m : nat, gt m 0 /\ a m = 0) -> (a (S O) = 0 \/ a (S (S O)) = 0).
 Proof. Admitted.

coq/src/putnam_2000_b1.v

@@ -1,9 +1,12 @@
-Require Import List Nat Reals ZArith.
+Require Import List Nat Reals ZArith Ensembles Finite_sets.
 Open Scope Z.
-Theorem putnam_2000_b1 
-    (a b c: nat -> Z)
-    (n: nat)
-    (habc : forall (j: nat), and (le 1 j) (le j n) -> Z.odd (a j) = true \/ Z.odd (b j) = true \/ Z.odd (c j) = true)
-    : exists (l: list nat), ge (length l) (4 * n / 7) /\ forall (j: nat), In j l -> and (le 1 j) (le j n)
-    -> exists (r s t: Z), Z.odd (Z.add (Z.add (Z.mul r (a j)) (Z.mul s (b j))) (Z.mul t (c j))) = true.
+Theorem putnam_2000_b1
+    (n : nat)
+    (a b c : nat -> Z)
+    (SS : Z -> Z -> Z -> Ensemble nat := (fun r s t : Z => (fun j : nat => le 1 j /\ le j n /\ Z.odd (Z.add (Z.add (Z.mul r (a j)) (Z.mul s (b j))) (Z.mul t (c j))) = true)))
+    (SSsize : Z -> Z -> Z -> nat)
+    (nge1 : ge n 1)
+    (habc : forall j : nat, ((le 1 j) /\ (le j n)) -> (Z.odd (a j) = true \/ Z.odd (b j) = true \/ Z.odd (c j) = true))
+    (hSSsize : forall r s t : Z, cardinal nat (SS r s t) (SSsize r s t))
+    : exists r s t : Z, Rge (INR (SSsize r s t)) (Rdiv (Rmult 4 (INR n)) 7).
 Proof. Admitted.

coq/src/putnam_2000_b2.v

@@ -1,5 +1,5 @@
 Require Import Nat Reals.
 Open Scope R.
 Theorem putnam_2000_b2 
-    : forall (n m: nat), and (ge n m) (ge m 1) -> exists (c: Z), INR (gcd m n) / INR n * Binomial.C n m = IZR c.
+    : forall (n m: nat), and (ge n m) (ge m 1) -> exists (c: Z), (INR (gcd m n) / INR n) * Binomial.C n m = IZR c.
 Proof. Admitted.

coq/src/putnam_2000_b4.v

@@ -1,6 +1,7 @@
-Open Scope R_scope.
-Require Import Reals.
+Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2000_b4
-    (f: R -> R)
-    : continuity f -> forall x, f (2*x*x-1) = 2*x*(f x) -> forall x, -1 <= x <= 1 -> f x = 0. 
+    (f : R -> R)
+    (hf : forall x : R, f (2*x*x-1) = 2*x*(f x))
+    (f_cont : continuity f)
+    : forall x : R, -1 <= x <= 1 -> f x = 0. 
 Proof. Admitted.

coq/src/putnam_2000_b5.v

@@ -1,8 +1,8 @@
 Require Import ZArith Ensembles Finite_sets.
 Theorem putnam_2000_b5
-    (S : nat -> Ensemble Z)
-    (hSfin : forall n : nat, exists m : nat, cardinal _ (S n) m)
-    (hSpos : forall n : nat, forall s : Z, In _ (S n) s -> Z.gt s 0)
-    (hSdef : forall n : nat, forall a : Z, (In _ (S (n + 1)) a) <-> ((In _ (S n) (Z.sub a 1) /\ ~ (In _ (S n) a)) \/ (In _ (S n) a /\ ~ (In _ (S n) (Z.sub a 1)))))
-    : forall n : nat, exists N : nat, N >= n /\ Same_set _ (S N) (Union _ (S 0) (fun i : Z => exists a : Z, In _ (S 0) a /\ i = Z.add a (Z.of_nat N))).
+    (SS : nat -> Ensemble Z)
+    (hSSfin : forall n : nat, exists m : nat, cardinal _ (SS n) m)
+    (hSSpos : forall n : nat, forall s : Z, In _ (SS n) s -> Z.gt s 0)
+    (hSSdef : forall n : nat, forall a : Z, (In _ (SS (n + 1)) a) <-> ((In _ (SS n) (Z.sub a 1) /\ ~ (In _ (SS n) a)) \/ (In _ (SS n) a /\ ~ (In _ (SS n) (Z.sub a 1)))))
+    : forall n : nat, exists N : nat, N >= n /\ Same_set _ (SS N) (Union _ (SS 0) (fun i : Z => exists a : Z, In _ (SS 0) a /\ i = Z.add a (Z.of_nat N))).
 Proof. Admitted.

isabelle/putnam_2000_a5.thy

@@ -1,6 +1,7 @@
 theory putnam_2000_a5 imports
 Complex_Main
 "HOL-Analysis.Finite_Cartesian_Product"
+"HOL-Analysis.Elementary_Metric_Spaces"
 begin
 
 theorem putnam_2000_a5:
@@ -9,7 +10,7 @@ theorem putnam_2000_a5:
   and S :: "(real^2) set"
   assumes rpos: "r > 0"
   and Scard: "finite S \<and> card S = 3"
-  and pint: "\<forall> p \<in> S. p$1 = round (p$1) \<and> p$2 = round (p$2)"
+  and pint: "\<forall> p \<in> S. p$1 \<in> \<int> \<and> p$2 \<in> \<int>"
   and pcirc: "\<forall> p \<in> S. p \<in> sphere z r"
   shows "\<exists> p \<in> S. \<exists> q \<in> S. dist p q \<ge> r powr (1 / 3)"
   sorry

isabelle/putnam_2000_b1.thy

@@ -3,7 +3,7 @@ begin
 
 (* uses (nat \<Rightarrow> int) instead of (Fin N \<Rightarrow> int) *)
 theorem putnam_2000_b1:
-  fixes n :: nat
+  fixes N :: nat
   and a b c :: "nat \<Rightarrow> int"
   assumes Nge1: "N \<ge> 1"
   and hodd: "\<forall>j::nat\<in>{0..(N-1)}. odd (a j) \<or> odd (b j) \<or> odd (c j)"

isabelle/putnam_2000_b4.thy

@@ -3,9 +3,9 @@ begin
 
 theorem putnam_2000_b4:
   fixes f :: "real \<Rightarrow> real"
-  assumes hf : "\<forall>x. f (2 * x^2  - 1) = 2 * x * f x"
+  assumes hf : "\<forall>x::real. f (2 * x^2 - 1) = 2 * x * f x"
     and f_cont : "continuous_on UNIV f"
-  shows "\<forall>x. x \<ge> -1 \<and> x \<le> 1 \<longrightarrow> f x = 0"
+  shows "\<forall>x::real. x \<ge> -1 \<and> x \<le> 1 \<longrightarrow> f x = 0"
   sorry
 
 end