Merge pull request #167 from trishullab/jasper

2002 and 2003 isabelle and coq fixes (except 2003_b5 for coq)

coq/src/commented_problems.v

@@ -76,4 +76,29 @@ Theorem putnam_2010_a5:
             forall (a b: R -> R -> R),
                 cross_product a b = a. 
 Proof. Admitted.
-End putnam_2010_a5. *)
+End putnam_2010_a5. *)
+
+(* Require Import Reals 
+GeoCoq.Main.Tarski_dev.Ch16_coordinates_with_functions
+GeoCoq.Axioms.Definitions
+GeoCoq.Main.Highschool.triangles.
+Context `{T2D:Tarski_2D} `{TE:@Tarski_euclidean Tn TnEQD}.
+Open Scope R.
+Definition putnam_2003_b5_solution (pt_to_R : Tpoint -> (R * R)) (dist : Tpoint -> Tpoint -> R) (P Op : Tpoint) := sqrt 3 * (1 - (dist P Op) ^ 2 - 1).
+Theorem putnam_2003_b5
+    (pt_to_R : Tpoint -> (R * R))
+    (F_to_R : F -> 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)
+    (Triangle : Tpoint -> Tpoint -> Tpoint -> Prop := fun x y z => ~ Col x y z) (* copied from GeoCoq.Axioms.euclidean_axioms *)
+    (A B C Op Op' P: Tpoint)
+    (fixpoint : dist Op Op' = R1)
+    (hABC : OnCircle A Op Op' /\ OnCircle B Op Op' /\ OnCircle C Op Op')
+    (hABC' : Main.Highschool.triangles.equilateral A B C)
+    (hp : InCircle P Op Op')
+    (a : R := dist P A)
+    (b : R := dist P B)
+    (c : R := dist P C)
+    : exists (A' B' C' : Tpoint) (D: Cs O E A' B' C'),
+    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. *)

coq/src/putnam_2002_a1.v

@@ -1,8 +1,10 @@
 Require Import Reals Factorial Coquelicot.Coquelicot.
 Definition putnam_2002_a1_solution (k n: nat) := Rpower (-1 * INR k) (INR n) * INR (fact n).
 Theorem putnam_2002_a1
+    (k : nat)
     (p : (nat -> R) -> R -> nat -> R := fun a x n => sum_n (fun i => a i * x ^ i) n)
-    : forall (N k: nat), gt k 0 -> exists (a: nat -> R) (n: nat), forall (x: R), 
-    (Derive_n (fun x => 1 / (x ^ k - 1)) N) x = (p a x n) / (x ^ k - 1) ^ (n + 1) ->
-    p a x 1%nat = putnam_2002_a1_solution k n.
+    (kpos : gt k 0)
+    : forall (N: nat), forall (a: nat -> R) (n: nat),
+    (forall (x: R), (Derive_n (fun x => 1 / (x ^ k - 1)) N) x = (p a x n) / (x ^ k - 1) ^ (n + 1)) ->
+    p a 1 n = putnam_2002_a1_solution k n.
 Proof. Admitted.

coq/src/putnam_2002_b3.v

@@ -1,5 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_2002_b3 
-    : forall (n: nat), ge n 1 -> let n := INR n in 1 / (2 * n * exp 1) < 1 / (exp 1) - Rpower (1 - 1 / n) n < 1 / (n * (exp 1)).
+    : forall (n: nat), gt n 1 -> let n := INR n in 1 / (2 * n * exp 1) < 1 / (exp 1) - Rpower (1 - 1 / n) n < 1 / (n * (exp 1)).
 Proof. Admitted.

coq/src/putnam_2003_a1.v

@@ -1,8 +1,8 @@
 Require Import Nat List Ensembles Finite_sets Coquelicot.Coquelicot.
-Definition putnam_2003_a1_solution (n: nat) := n.
+Definition putnam_2003_a1_solution : nat -> nat := (fun n : nat => n).
 Theorem putnam_2003_a1
     (n: nat)
     (hn : n > 0)
-    (E: Ensemble (list nat) := fun l => forall (i j: nat), i < length l /\ j < length l /\ i < j -> nth i l 0 <= nth j l 0 /\ fold_left add l 0 = n)
+    (E: Ensemble (list nat) := fun l => fold_left add l 0 = n /\ (forall i : nat, i < length l -> nth i l 0 > 0) /\ (forall (i j: nat), i < length l /\ j < length l /\ i < j -> nth i l 0 <= nth j l 0) /\ last l 0 <= hd 0 l + 1)
     : cardinal (list nat) E (putnam_2003_a1_solution n).
 Proof. Admitted.

coq/src/putnam_2003_a2.v

@@ -6,7 +6,11 @@ Theorem putnam_2003_a2
         | _, nil => nil
         | h1 :: t1, h2 :: t2 => (h1 + h2) :: suml t1 t2
     end)
-    : forall (n: nat) (a b: list R), length a = n /\ length b = n ->
-    (fold_left Rmult a 1) ^ (1 / n) + (fold_left Rmult b 1) ^ (1 / n) <=
+    (n : nat)
+    (a b : list R)
+    (npos : ge n 1)
+    (ablen : length a = n /\ length b = n)
+    (abnneg : forall i : nat, lt i n -> nth i a 0 >= 0 /\ nth i b 0 >= 0)
+    : (fold_left Rmult a 1) ^ (1 / n) + (fold_left Rmult b 1) ^ (1 / n) <=
     (fold_left Rmult (Suml a b) 1) ^ (1 / n).
 Proof. Admitted.

coq/src/putnam_2003_a3.v

@@ -2,5 +2,5 @@ Require Import Reals Coquelicot.Coquelicot.
 Definition putnam_2003_a3_solution := 2 * sqrt 2 - 1.
 Theorem putnam_2003_a3
     (f : R -> R := fun x => Rabs (sin x + cos x + tan x + 1 / tan x + 1 / cos x  + 1 / sin x))
-    : exists (minx: R), forall (x: R), f minx <= f x -> f minx = putnam_2003_a3_solution.
+    : (exists x : R, f x = putnam_2003_a3_solution) /\ (forall x : R, f x >= putnam_2003_a3_solution).
 Proof. Admitted.

coq/src/putnam_2003_a4.v

@@ -2,7 +2,7 @@ Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2003_a4
     (a b c A B C: R)
     (ha : a <> 0)
-    (hA :A <> 0)
+    (hA : A <> 0)
     (hp : forall (x: R), Rabs (a * x ^ 2 + b * x + c) <= Rabs (A * x ^ 2 + B * x + C))
     : Rabs (b ^ 2 - 4 * a * c) <= Rabs (B ^ 2 - 4 * A * C).
 Proof. Admitted.

coq/src/putnam_2003_b1.v

@@ -1,7 +1,8 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2003_b1_solution := True.
+Definition putnam_2003_b1_solution := False.
 Theorem putnam_2003_b1
     (p : (nat -> R) -> R -> nat -> R := fun coeff x n => sum_n (fun i => coeff i * x ^ i) n)
-    : exists (coeffa coeffb coeffc coeffd: nat -> R) (na nb nc nd: nat), forall (x y: R),
-    1 + x * y * (x * y) ^ 2 = (p coeffa x na) * (p coeffc y nc) + (p coeffb x nb) * (p coeffd y nd).
+    : (exists (coeffa coeffb coeffc coeffd: nat -> R) (na nb nc nd: nat), forall (x y: R),
+    1 + x * y + x ^ 2 * y ^ 2 = (p coeffa x na) * (p coeffc y nc) + (p coeffb x nb) * (p coeffd y nd))
+    <-> putnam_2003_b1_solution.
 Proof. Admitted.

coq/src/putnam_2003_b3.v

@@ -2,13 +2,15 @@ Require Import Nat List Reals Coquelicot.Coquelicot.
 Theorem putnam_2003_b3
     (lcmn := fix lcm_n (args : list nat) : nat :=
         match args with
-        | nil => 0%nat
+        | nil => 1%nat
         | h :: args' => div (h * (lcm_n args')) (gcd h (lcm_n args'))
     end)
     (prodn := fix prod_n (m: nat -> R) (n : nat) : R :=
         match n with
         | O => m 0%nat
-        | S n' => m n' * prod_n m n'
+        | S n' => m n * prod_n m n'
     end)
-    : forall (n: nat), gt n 0 -> INR (fact n) = prodn (fun i => INR (lcmn (seq 0 (div n (i + 1))))) n.
+    (n : nat)
+    (npos : gt n 0)
+    : INR (fact n) = prodn (fun i => INR (lcmn (seq 1 (div n (i + 1))))) (sub n 1).
 Proof. Admitted.

coq/src/putnam_2003_b4.v

@@ -1,13 +1,13 @@
 Require Import Reals ZArith Coquelicot.Coquelicot.
 Theorem putnam_2003_b4
     (a b c d e: Z)
+    (r1 r2 r3 r4: R)
     (ha : ~ Z.eq a 0)
     : let a := IZR a in 
     let b := IZR b in 
     let c := IZR c in 
     let d := IZR d in 
     let e := IZR e in 
-    exists (r1 r2 r3 r4: R), forall (z: R), 
-    a * z ^ 4 + b * z ^ 3 + c * z ^ 2 + d * z + e = a * (z - r1) * (z - r2) * (z - r3) * (z - r4) ->
-    (exists (p q: Z), r1 + r2 = IZR p / IZR q) /\ r1 + r2 <> r3 + r4 -> exists (p q: Z), r1 * r2 = IZR p / IZR q.
+    (forall (z: R), a * z ^ 4 + b * z ^ 3 + c * z ^ 2 + d * z + e = a * (z - r1) * (z - r2) * (z - r3) * (z - r4)) ->
+    ((exists (p q: Z), r1 + r2 = IZR p / IZR q) /\ r1 + r2 <> r3 + r4) -> (exists (p q: Z), r1 * r2 = IZR p / IZR q).
 Proof. Admitted.

coq/src/putnam_2003_b6.v

@@ -1,5 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2003_b6
-    : forall (f: R -> R) (x: R), 0 <= x <= 1 -> continuity_pt f x ->
-    RInt (fun x => RInt (fun y => Rabs (f x + f y)) 0 1) 0 1 >= RInt (fun x => Rabs (f x)) 0 1.
+    (f : R -> R)
+    (hf : continuity f)
+    : RInt (fun x => RInt (fun y => Rabs (f x + f y)) 0 1) 0 1 >= RInt (fun x => Rabs (f x)) 0 1.
 Proof. Admitted.

isabelle/putnam_2002_a2.thy

@@ -1,6 +1,7 @@
 theory putnam_2002_a2 imports Complex_Main
 "HOL-Analysis.Finite_Cartesian_Product"
 "HOL-Analysis.Linear_Algebra"
+"HOL-Analysis.Elementary_Metric_Spaces"
 begin
 
 theorem putnam_2002_a2:

isabelle/putnam_2002_a3.thy

@@ -3,7 +3,7 @@ begin
 
 theorem putnam_2002_a3:
   fixes n Tn :: "int"
-  defines "Tn \<equiv> card {S :: int set. S \<subseteq> {1..16} \<and> S \<noteq> {} \<and> (\<exists> k :: int. k = (real 1)/(card S) * (\<Sum> s \<in> S. s))}"
+  defines "Tn \<equiv> card {S :: int set. S \<subseteq> {1..n} \<and> S \<noteq> {} \<and> (\<exists> k :: int. k = (real 1)/(card S) * (\<Sum> s \<in> S. s))}"
   assumes hn : "n \<ge> 2"
   shows "even (Tn - n)"
   sorry

isabelle/putnam_2002_b5.thy

@@ -5,8 +5,7 @@ begin
 fun digits :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
   "digits b n = (if b < 2 then (replicate n 1) else (if n < b then [n] else [n mod b] @ digits b (n div b)))"
 theorem putnam_2002_b5:
-  shows "\<exists> n :: nat. card {b :: nat. length (digits b n) = 3 \<and> digits b n = rev (digits b n)} \<ge> 2002"
+  shows "\<exists> n :: nat. card {b :: nat. b \<ge> 1 \<and> length (digits b n) = 3 \<and> digits b n = rev (digits b n)} \<ge> 2002"
   sorry
 
 end
-

isabelle/putnam_2003_a2.thy

@@ -4,7 +4,8 @@ begin
 (* Note: Boosted domain to infinite set *)
 theorem putnam_2003_a2:
   fixes n::nat and a b::"nat\<Rightarrow>real"
-  assumes abnneg : "\<forall>i \<in> {0..<n}. a i \<ge> 0 \<and> b i \<ge> 0"
+  assumes npos: "n \<ge> 1"
+  and abnneg: "\<forall>i \<in> {0..<n}. a i \<ge> 0 \<and> b i \<ge> 0"
   shows "((\<Prod>i=0..<n. a i) powr (1/n)) + ((\<Prod>i=0..<n. b i) powr (1/n)) \<le> ((\<Prod>i=0..<n. (a i + b i)) powr (1/n))"
   sorry
 

isabelle/putnam_2003_b6.thy

@@ -1,13 +1,12 @@
 theory putnam_2003_b6 imports Complex_Main
-"HOL-Analysis.Lebesgue_Measure"
-"HOL-Analysis.Set_Integral"
+"HOL-Analysis.Interval_Integral"
 begin
 
 theorem putnam_2003_b6:
   fixes f :: "real \<Rightarrow> real"
   assumes hf : "continuous_on UNIV f"
   shows "set_lebesgue_integral lebesgue {(x, y). 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1} (\<lambda> t :: real \<times> real. \<bar>f (fst t) + f (snd t)\<bar>)
-        \<ge> interval_lebesgue_integral lebesgue 0 1 f"
+        \<ge> interval_lebesgue_integral lebesgue 0 1 (\<lambda>x::real. \<bar>f x\<bar>)"
   sorry
 
 end

lean4/src/putnam_2002_b5.lean

@@ -4,5 +4,5 @@ open BigOperators
 open Nat Set Topology Filter
 
 theorem putnam_2002_b5
-: ∃ n : ℕ, {b : ℕ | (Nat.digits b n).length = 3 ∧ List.Palindrome (Nat.digits b n)}.ncard ≥ 2002 :=
+: ∃ n : ℕ, {b : ℕ | b ≥ 1 ∧ (Nat.digits b n).length = 3 ∧ List.Palindrome (Nat.digits b n)}.ncard ≥ 2002 :=
 sorry