Merge pull request #143 from trishullab/george

Split Coq files into individual problems.

coq/assignment.v

@@ -120,16 +120,6 @@ Theorem putnam_1999_a2
 Proof. Admitted.
 End putnam_1999_a2.
 
-(* Section putnam_1999_a5.
-Require Import Reals NewtonInt. From mathcomp Require Import all_algebra all_ssreflect ssrnat ssrnum ssralg fintype poly seq.
-Open Scope ring_scope.
-Theorem putnam_1999_a5:
-    forall (R: numDomainType) (p: {poly R}),
-        (size p = 1999%nat) ->
-        exists (C: R), Num.norm p.[0] <= GRing.mul C (Num.norm p.[0]).
-Proof. Admitted.
-End putnam_1999_a5. *)
-
 Section putnam_1999_b4.
 Require Import Reals Coquelicot.Derive.
 Open Scope R_scope.
@@ -198,20 +188,6 @@ Theorem putnam_2010_a4
 Proof. Admitted.
 End putnam_2010_a4.
 
-(* Section putnam_2010_a5.
-Require Import Reals. From mathcomp Require Import fingroup ssreflect ssrbool eqtype seq choice fintype div path tuple bigop prime finset.
-Open Scope R.
-Variable R3: finGroupType.
-Definition cross_product (a b : R -> R -> R) : R -> R -> R := a. 
-Theorem putnam_2010_a5:
-    forall (G: {group R3}),
-        forall (a b: R -> R -> R),
-            cross_product a b = a \/ cross_product a b = a ->
-            forall (a b: R -> R -> R),
-                cross_product a b = a. 
-Proof. Admitted.
-End putnam_2010_a5. *)
-
 Section putnam_2023_a1.
 Require Import Reals List Rtrigo_def Coquelicot.Derive.
 Open Scope R.

coq/batch2.v

@@ -28,20 +28,6 @@ Theorem putnam_2023_b5
 Proof. Admitted. 
 End putnam_2023_b5.
 
-(* TODO: missing determinant refinement in coqeal *) 
-(* Section putnam_2023_b6. 
-Require Import Nat Finite_sets.
-From mathcomp Require Import matrix ssrbool ssralg fintype.
-Variable putnam_2023_b6_solution : nat -> nat.
-Open Scope ring_scope.
-Theorem putnam_2023_b6: 
-    forall (n: nat), 
-        let s (i j: nat) := cardinal (nat*nat) (fun p => let (a, b) := p in 1 <= i <= n /\ 1 <= j <= n /\ eq (add (mul a i) (mul b j)) n) in
-        (\matrix_(i < n, j < n) s i j)
-        = (\matrix_(i < n, j < n) s i j).
-Proof. Admitted. 
-End putnam_2023_b6. *)
-
 Section putnam_2022_a6. 
 Require Import Nat Reals Coquelicot.Hierarchy. From mathcomp Require Import div fintype seq ssralg ssrbool ssrnat ssrnum .
 Definition putnam_2022_a6_solution := fun n : nat => n.

coq/batch6.v

@@ -1,15 +1,3 @@
-(* Skipped due to lack of surface integral function *)
-(* Section putnam_2019_a4. 
-Require Import PeanoNat. Require Import Reals Coquelicot.Derive.
-Definition putnam_2019_a4_solution := false. 
-Theorem putnam_2019_a4: 
-    forall (f: R -> R),
-    continuity f -> 
-    forall (x y z: R), x*x + y*y + z*z = 1 ->
-    True.
-Proof. Admitted. 
-End putnam_2019_a4. *)
-
 Section putnam_2016_b5. 
 Require Import Reals Rpower.
 Open Scope R.
@@ -75,12 +63,6 @@ Theorem putnam_2015_a5
 Proof. Admitted.
 End putnam_2015_a5.
 
-(* Skipped due to inability to use det in mathcomp *)
-(* Section putnam_2015_a6. 
-Theorem putnam_2015_a6: True.
-Proof. Admitted.
-End putnam_2015_a6. *)
-
 Section putnam_2015_b1. 
 Require Import Reals List Coquelicot.Derive.
 Open Scope R_scope.
@@ -91,11 +73,4 @@ Theorem putnam_2015_b1
     (g : R -> R := fun x => f x + 6 * (Derive_n f 1) x + 12 * (Derive_n f 2) x + 8 * (Derive_n f 3) x)
     : exists (l': list R), length l = 2%nat /\ NoDup l' /\ forall x, In x l' -> g x = 0.
 Proof. Admitted.
-End putnam_2015_b1.
-
-(* Skipped due to inability to use det in mathcomp *)
-(* Section putnam_2014_a2. 
-From mathcomp Require Import div.
-    Theorem putnam_2014_a2: True.
-Proof. Admitted.
-End putnam_2014_a2. *)
+End putnam_2015_b1.

coq/batch8.v

@@ -1,9 +1,3 @@
-(* Skipped due to inability to use groups in mathcomp *)
-(* Section putnam_2018_a4. 
-Theorem putnam_2018_a4: True.
-Proof. Admitted.
-End putnam_2018_a4.  *)
-
 Section putnam_2018_b1. 
 Require Import Logic Ensembles Finite_sets Nat List.
 Open Scope nat_scope.
@@ -100,23 +94,6 @@ Theorem putnam_2013_a6
 Proof. Admitted.
 End putnam_2013_a6. 
 
-(* TODO: WIP *)
-(* NOTE -- Divide-and-conquer recursion is hard to formulate in Coq. A proof must be provided for termination *)
-(* Section putnam_2013_b1. 
-Require Import ZArith Nat List Lia Ensembles Finite_sets Reals Program Coquelicot.Hierarchy. 
-Open Scope Z.
-Program Fixpoint Aa (n : nat) {measure n} : Z :=
-  match n with
-  | O => 0
-  | S O => 1
-  | S (S m) => if even m then Aa (div2 (m+2)) else if even (div2 (m+2)) then Aa (div2 (m+2)) else (-1) * Aa (div2 (m+2))
-  end.
-Next Obligation. Proof. destruct m. simpl; auto. induction m. simpl; auto. simpl. Admitted.
-Theorem putnam_2013_b1: 
-    sum_n (fun n => (Aa n)*(Aa (n+2))) 2013 = 1.
-Proof. Admitted.
-End putnam_2013_b1.  *)
-
 Section putnam_2013_b4. 
 Require Import Reals. From Coquelicot Require Import Coquelicot Continuity RInt.
 Open Scope R.

coq/batch9.v

@@ -23,12 +23,6 @@ Theorem putnam_2016_a3
 Proof. Admitted.
 End putnam_2016_a3. 
 
-(* Skipped due to inability to use groups in mathcomp *)
-(* Section putnam_2016_a5. 
-Theorem putnam_2016_a5: True.
-Proof. Admitted.
-End putnam_2016_a5.  *)
-
 Section putnam_2016_b2. 
 Require Import Bool Reals Coquelicot.Lim_seq Coquelicot.Rbar. 
 Definition putnam_2016_b2_solution (a b : R) := a = 3/4 /\ b = 4/3.
@@ -84,8 +78,7 @@ Theorem putnam_2012_a6
 Proof. Admitted.
 End putnam_2012_a6. 
 
-(* -- NOTE: this formalization differs from the original statement by assigning a value of zero to all values outside the specified domain/range. *)
-(* -- The problem is still solvable given this modification. *)
+(* Note: this formalization differs from the original statement by assigning a value of zero to all values outside the specified domain/range. The problem is still solvable given this modification. *)
 Section putnam_2012_b1. 
 Require Import Reals RIneq.
 Open Scope R.

coq/batch_51.v

@@ -1,6 +1,3 @@
-(* Batch 51:
-Putnam 1965 A2 A3 A4 A5 A6 B2 B3 B4 B5 B6 *)
-
 Section putnam_1965_a2.
 Require Import Coquelicot.Hierarchy Reals.
 Theorem putnam_1965_a2

coq/batch_5262024.v

@@ -169,7 +169,7 @@ Theorem putnam_1987_b4
 Proof. Admitted.
 End putnam_1987_b4.
 
-(* NOTE -- omitted the second part of the proof - an example of existence - due to lack of full solution description *)
+(* Note: omitted the second part of the proof - an example of existence - due to lack of full solution description *)
 Section putnam_1988_a2.
 Require Import Basics Reals Coquelicot.Coquelicot.
 Open Scope R.

coq/batch_612024.v

@@ -1,4 +1,4 @@
-(* NOTE -- Two external functions have been defined for usage in both solution and problem statement. *)
+(* Note: -- Two external functions have been defined for usage in both solution and problem statement. *)
 Section putnam_2014_b1.
 Require Import Nat Ensembles List. From mathcomp Require Import div fintype seq ssrbool.
 Fixpoint hd (n: nat) (l:list 'I_n) := match l with | nil => 0 | x :: _ => x end.

coq/batch_622024.v

@@ -352,10 +352,10 @@ Theorem putnam_1997_a1
     (l1 : dist Hp Op = 11)
     (l2 : dist Op Mp = 5)
     (s : Rectangle Hp Op Mp Fp)
-    (hHp : Bet A Fp Hp)                 (* H as the intersection of the altitudes *)
-    (hOp : is_circumcenter Op A B C)    (* O the center of the circumscribed circle *)
-    (hMp : Midpoint B C Mp)             (* M the midpoint of BC *)
-    (hFp : Perp A C B Fp /\ Col A C Fp) (* foot of the altitude *)
+    (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.
 End putnam_1997_a1.

coq/batch_6252024.v

@@ -18,18 +18,6 @@ Theorem putnam_1973_a4
 Proof. Admitted.
 End putnam_1973_a4.
 
-(* TODO: How to get the cardinality of a set with cardinal? Could not figure out a clean way*)
-(* Section putnam_1973_a6.
-Require Import Reals Finite_sets Ensembles Coquelicot.Coquelicot. From mathcomp Require Import fintype.
-Theorem putnam_1973_a6
-    (h_nint : nat -> ('I_7 -> (R * R)) -> nat := fun n lines => 
-        let intersection_set (p : R * R) : Prop := exists! S : Ensemble 'I_7, cardinal _ S n /\ (forall i : 'I_7, In _ S i -> (snd p = (snd (lines i)) * (fst p) + (fst (lines i)))) in
-            cardinal _ intersection_set
-    )
-    : ~ (exists lines: 'I_7 -> (R * R), (forall i j : 'I_7, i <> j -> (lines i <> lines j)) /\ h_nint 3 lines >= 6 /\ h_nint 2 lines >= 4).
-Proof. Admitted.
-End putnam_1973_a6. *)
-
 Section putnam_1973_b1.
 Require Import Basics Nat Reals Ensembles Finite_sets Coquelicot.Coquelicot. From mathcomp Require Import fintype.
 Theorem putnam_1973_b1
@@ -163,7 +151,6 @@ Theorem putnam_1971_b6
 Proof. Admitted.
 End putnam_1971_b6.
 
-
 Section putnam_1966_a1.
 Require Import Reals Nat ZArith Coquelicot.Coquelicot.
 Theorem putnam_1966_a1
@@ -182,7 +169,6 @@ Theorem putnam_1966_a3
 Proof. Admitted.
 End putnam_1966_a3.
 
-
 Section putnam_1966_a4.
 Require Import Nat List ZArith Reals Coquelicot.Coquelicot.
 Theorem putnam_1966_a4

coq/src/commented_problems.v

@@ -0,0 +1,79 @@
+
+(* TODO: WIP *)
+(* NOTE -- Divide-and-conquer recursion is hard to formulate in Coq. A proof must be provided for termination *)
+(* Section putnam_2013_b1. 
+Require Import ZArith Nat List Lia Ensembles Finite_sets Reals Program Coquelicot.Hierarchy. 
+Open Scope Z.
+Program Fixpoint Aa (n : nat) {measure n} : Z :=
+  match n with
+  | O => 0
+  | S O => 1
+  | S (S m) => if even m then Aa (div2 (m+2)) else if even (div2 (m+2)) then Aa (div2 (m+2)) else (-1) * Aa (div2 (m+2))
+  end.
+Next Obligation. Proof. destruct m. simpl; auto. induction m. simpl; auto. simpl. Admitted.
+Theorem putnam_2013_b1: 
+    sum_n (fun n => (Aa n)*(Aa (n+2))) 2013 = 1.
+Proof. Admitted.
+End putnam_2013_b1.  *)
+
+(* Skipped due to lack of surface integral function *)
+(* Section putnam_2019_a4. 
+Require Import PeanoNat. Require Import Reals Coquelicot.Derive.
+Definition putnam_2019_a4_solution := false. 
+Theorem putnam_2019_a4: 
+    forall (f: R -> R),
+    continuity f -> 
+    forall (x y z: R), x*x + y*y + z*z = 1 ->
+    True.
+Proof. Admitted. 
+End putnam_2019_a4. *)
+
+(* TODO: missing determinant refinement in coqeal *) 
+(* Section putnam_2023_b6. 
+Require Import Nat Finite_sets.
+From mathcomp Require Import matrix ssrbool ssralg fintype.
+Variable putnam_2023_b6_solution : nat -> nat.
+Open Scope ring_scope.
+Theorem putnam_2023_b6: 
+    forall (n: nat), 
+        let s (i j: nat) := cardinal (nat*nat) (fun p => let (a, b) := p in 1 <= i <= n /\ 1 <= j <= n /\ eq (add (mul a i) (mul b j)) n) in
+        (\matrix_(i < n, j < n) s i j)
+        = (\matrix_(i < n, j < n) s i j).
+Proof. Admitted. 
+End putnam_2023_b6. *)
+
+(* TODO: How to get the cardinality of a set with cardinal? Could not figure out a clean way*)
+(* Section putnam_1973_a6.
+Require Import Reals Finite_sets Ensembles Coquelicot.Coquelicot. From mathcomp Require Import fintype.
+Theorem putnam_1973_a6
+    (h_nint : nat -> ('I_7 -> (R * R)) -> nat := fun n lines => 
+        let intersection_set (p : R * R) : Prop := exists! S : Ensemble 'I_7, cardinal _ S n /\ (forall i : 'I_7, In _ S i -> (snd p = (snd (lines i)) * (fst p) + (fst (lines i)))) in
+            cardinal _ intersection_set
+    )
+    : ~ (exists lines: 'I_7 -> (R * R), (forall i j : 'I_7, i <> j -> (lines i <> lines j)) /\ h_nint 3 lines >= 6 /\ h_nint 2 lines >= 4).
+Proof. Admitted.
+End putnam_1973_a6. *)
+
+(* Section putnam_1999_a5.
+Require Import Reals NewtonInt. From mathcomp Require Import all_algebra all_ssreflect ssrnat ssrnum ssralg fintype poly seq.
+Open Scope ring_scope.
+Theorem putnam_1999_a5:
+    forall (R: numDomainType) (p: {poly R}),
+        (size p = 1999%nat) ->
+        exists (C: R), Num.norm p.[0] <= GRing.mul C (Num.norm p.[0]).
+Proof. Admitted.
+End putnam_1999_a5. *)
+
+(* Section putnam_2010_a5.
+Require Import Reals. From mathcomp Require Import fingroup ssreflect ssrbool eqtype seq choice fintype div path tuple bigop prime finset.
+Open Scope R.
+Variable R3: finGroupType.
+Definition cross_product (a b : R -> R -> R) : R -> R -> R := a. 
+Theorem putnam_2010_a5:
+    forall (G: {group R3}),
+        forall (a b: R -> R -> R),
+            cross_product a b = a \/ cross_product a b = a ->
+            forall (a b: R -> R -> R),
+                cross_product a b = a. 
+Proof. Admitted.
+End putnam_2010_a5. *)

coq/src/putnam_1965_a2.v

@@ -0,0 +1,4 @@
+Require Import Coquelicot.Hierarchy Reals.
+Theorem putnam_1965_a2
+    : forall n : nat, gt n 0 -> sum_n (fun r : nat => ((INR n - 2 * INR r) * (C n r) / INR n) ^ 2) ((n - 1) / 2) = (C (2 * n - 2) (n - 1)) / INR n.
+Proof. Admitted.

coq/src/putnam_1965_a3.v

@@ -0,0 +1,8 @@
+(* Note: The MAA archive contains an error on this problem; the second term in the sum of the second limit should read "a2", not "a4". *)
+Require Import Reals Coquelicot.Complex Coquelicot.Hierarchy.
+Theorem putnam_1965_a3
+    (a : nat -> R)
+    (alpha : C)
+    (euler : R -> C := (fun x : R => Cplus (cos x) (Cmult Ci (sin x))))
+    : (filterlim (fun n : nat => Cdiv (sum_n (fun k : nat => euler (a k)) (n - 1)) (INR n)) eventually (locally alpha)) <-> (filterlim (fun n : nat => Cdiv (sum_n (fun k : nat => euler (a k)) (n ^ 2 - 1)) (INR (n ^ 2))) eventually (locally alpha)).
+Proof. Admitted.

coq/src/putnam_1965_a4.v

@@ -0,0 +1,8 @@
+Require Import Bool ssreflect ssrfun. From mathcomp Require Import fintype.
+Variables G B : finType.
+Theorem putnam_1965_a4
+    (dances : G -> B -> Prop)
+    (h : ~(exists b : B, forall g : G, dances g b) /\ (forall g : G, exists b : B, dances g b))
+    (nonempty : inhabited G /\ inhabited B)
+    : exists (g h : G) (b c : B), dances g b /\ dances h c /\ ~dances h b /\ ~dances g c.
+Proof. Admitted.

coq/src/putnam_1965_a5.v

@@ -0,0 +1,5 @@
+Require Import Nat Finite_sets. From mathcomp Require Import fintype perm.
+Definition putnam_1965_a5_solution : nat -> nat := (fun n : nat => 2 ^ (n - 1)).
+Theorem putnam_1965_a5
+    : forall n : nat, n > 0 -> cardinal {perm 'I_n} (fun p : {perm 'I_n} => forall m : 'I_n, m > 0 -> exists k : 'I_n, k < m /\ (nat_of_ord (p m) = (p k) + 1 \/ nat_of_ord (p m) = (p k) - 1)) (putnam_1965_a5_solution n).
+Proof. Admitted.

coq/src/putnam_1965_a6.v

@@ -0,0 +1,8 @@
+Require Import Reals Coquelicot.Coquelicot.
+Theorem putnam_1965_a6
+    (u v m : R)
+    (pinter : (R * R) -> Prop := (fun p : R * R => u * (fst p) + v * (snd p) = 1 /\ (Rpower (fst p) m) + (Rpower (snd p) m) = 1))
+    (hm : m > 1)
+    (huv : u >= 0 /\ v >= 0)
+    : ((exists! p : R * R, pinter p) /\ (exists p : R * R, fst p >= 0 /\ snd p >= 0 /\ pinter p)) <-> (exists n : R, (Rpower u n) + (Rpower v n) = 1 /\ powerRZ m (-1) + powerRZ n (-1) = 1).
+Proof. Admitted.

coq/src/putnam_1965_b2.v

@@ -0,0 +1,13 @@
+Require Import Coquelicot.Hierarchy Reals. From mathcomp Require Import fintype.
+Theorem putnam_1965_b2
+    (n : nat)
+    (won : 'I_n -> 'I_n -> bool)
+    (ordofnat : nat -> 'I_n)
+    (w : 'I_n -> R := (fun r : 'I_n => sum_n (fun j : nat => if (won r (ordofnat j)) then 1 else 0) (n - 1)))
+    (l : 'I_n -> R := (fun r : 'I_n => INR n - 1 - w r))
+    (hn : gt n 1)
+    (hirrefl : forall i : 'I_n, won i i = false)
+    (hantisymm : forall i j : 'I_n, i <> j -> won i j = negb (won j i))
+    (hordofnat : forall i : 'I_n, ordofnat (nat_of_ord i) = i)
+    : sum_n (fun r : nat => (w (ordofnat r)) ^ 2) (n - 1) = sum_n (fun r : nat => (l (ordofnat r)) ^ 2) (n - 1).
+Proof. Admitted.

coq/src/putnam_1965_b3.v

@@ -0,0 +1,4 @@
+Require Import Finite_sets Reals Coquelicot.Coquelicot.
+Theorem putnam_1965_b3
+    : cardinal (R * R * R) (fun abc : R * R * R => let '(a, b, c) := abc in (IZR (floor a) = a /\ IZR (floor b) = b /\ IZR (floor c) = c /\ a > 0 /\ a <= b /\ c > 0 /\ a ^ 2 + b ^ 2 = c ^ 2 /\ a * b / 2 = 2 * (a + b + c))) 3.
+Proof. Admitted.

coq/src/putnam_1965_b4.v

@@ -0,0 +1,7 @@
+Require Import Reals Coquelicot.Hierarchy Ensembles.
+Definition putnam_1965_b4_solution : (((R -> R) -> R -> R) * ((R -> R) -> R -> R)) * ((Ensemble R) * (R -> R)) := (((fun (h : R -> R) (x : R) => h x + x), (fun (h : R -> R) (x : R) => h x + 1)), ((fun x : R => x >= 0), sqrt)).
+Theorem putnam_1965_b4
+    (f : nat -> R -> R)
+    (hf : forall n : nat, gt n 0 -> f n = (fun x : R => (sum_n (fun i : nat => (C n (2 * i)) * x ^ i) (n / 2)) / (sum_n (fun i : nat => (C n (2 * i + 1)) * x ^ i) ((n - 1) / 2))))
+    : let '((p, q), (s, g)) := putnam_1965_b4_solution in (forall n : nat, gt n 0 -> f (Nat.add n 1) = (fun x : R => p (f n) x / q (f n) x) /\ s = (fun x : R => exists L : R, filterlim (fun n : nat => f n x) eventually (locally L)) /\ (forall x : R, s x -> filterlim (fun n : nat => f n x) eventually (locally (g x)))).
+Proof. Admitted.

coq/src/putnam_1965_b5.v

@@ -0,0 +1,7 @@
+Require Import Ensembles Finite_sets. From mathcomp Require Import fintype.
+Theorem putnam_1965_b5
+    (E V : nat)
+    (simple : (Ensemble ('I_V * 'I_V)) -> Prop := (fun G : Ensemble ('I_V * 'I_V) => (forall v : 'I_V, ~G (v, v)) /\ (forall v w : 'I_V, G (v, w) -> G (w, v))))
+    (hE : 4 * E <= Nat.pow V 2)
+    : exists G : Ensemble ('I_V * 'I_V), simple G /\ cardinal ('I_V * 'I_V) G (2 * E) /\ ~(exists a b c : 'I_V, G (a, b) /\ G (a, c) /\ G (b, c)).
+Proof. Admitted.

coq/src/putnam_1965_b6.v

@@ -0,0 +1,8 @@
+Require Import GeoCoq.Main.Tarski_dev.Ch16_coordinates_with_functions Ensembles.
+Context `{Tarski_2D}.
+Theorem putnam_1965_b6
+    (A B C D : Tpoint)
+    (hABCD : forall R SS P Q : Tpoint, (R <> P /\ SS <> Q /\ OnCircle A P R /\ OnCircle B P R /\ OnCircle C Q SS /\ OnCircle D Q SS) -> (exists I : Tpoint, OnCircle I P R /\ OnCircle I Q SS))
+    : (Col A B C /\ Col A B D) \/ (exists R P : Tpoint, R <> P /\ OnCircle A P R /\ OnCircle B P R /\ OnCircle C P R /\ OnCircle D P R).
+Proof. Admitted.
+End putnam_1965_b6.

coq/src/putnam_1966_a1.v

@@ -0,0 +1,5 @@
+Require Import Reals Nat ZArith Coquelicot.Coquelicot.
+Theorem putnam_1966_a1
+    (f : nat -> R := fun n => (sum_n (fun m => (if (even m) then INR m else INR (m-1)) : R) n) / 2)
+    : forall x y : nat, ge x y -> INR x * INR y = f (add x y) - f (sub x y).
+Proof. Admitted.