From 4c2f0d6cc0757bedfab3c798482989de92220b19 Mon Sep 17 00:00:00 2001 From: Jasper Lee Date: Wed, 31 Jul 2024 22:01:39 -0400 Subject: [PATCH] did isabelle and coq fixes for Putnam 1997 --- coq/src/commented_problems.v | 33 +++++++++++++++++++++++++++++++++ coq/src/putnam_1997_a1.v | 21 --------------------- coq/src/putnam_1997_a3.v | 6 +++--- coq/src/putnam_1997_a4.v | 2 +- coq/src/putnam_1997_a5.v | 4 ++-- coq/src/putnam_1997_a6.v | 15 ++++++++------- coq/src/putnam_1997_b1.v | 4 ++-- coq/src/putnam_1997_b2.v | 8 +++++--- coq/src/putnam_1997_b3.v | 9 ++++++--- coq/src/putnam_1997_b4.v | 9 --------- coq/src/putnam_1997_b5.v | 12 +++++++----- isabelle/putnam_1997_a5.thy | 3 +-- isabelle/putnam_1997_a6.thy | 8 ++++---- isabelle/putnam_1997_b2.thy | 4 ++-- isabelle/putnam_1997_b4.thy | 4 ++-- isabelle/putnam_1997_b5.thy | 2 +- 16 files changed, 77 insertions(+), 67 deletions(-) delete mode 100644 coq/src/putnam_1997_a1.v delete mode 100644 coq/src/putnam_1997_b4.v diff --git a/coq/src/commented_problems.v b/coq/src/commented_problems.v index 288456a9..0a52aade 100644 --- a/coq/src/commented_problems.v +++ b/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. *) + diff --git a/coq/src/putnam_1997_a1.v b/coq/src/putnam_1997_a1.v deleted file mode 100644 index dc226746..00000000 --- a/coq/src/putnam_1997_a1.v +++ /dev/null @@ -1,21 +0,0 @@ -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. diff --git a/coq/src/putnam_1997_a3.v b/coq/src/putnam_1997_a3.v index 757637c9..c4801a3a 100644 --- a/coq/src/putnam_1997_a3.v +++ b/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. diff --git a/coq/src/putnam_1997_a4.v b/coq/src/putnam_1997_a4.v index 3798d379..5f8a03d6 100644 --- a/coq/src/putnam_1997_a4.v +++ b/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. diff --git a/coq/src/putnam_1997_a5.v b/coq/src/putnam_1997_a5.v index d6404dfd..dfd754f0 100644 --- a/coq/src/putnam_1997_a5.v +++ b/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. diff --git a/coq/src/putnam_1997_a6.v b/coq/src/putnam_1997_a6.v index df96f5da..d4ed81b6 100644 --- a/coq/src/putnam_1997_a6.v +++ b/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. diff --git a/coq/src/putnam_1997_b1.v b/coq/src/putnam_1997_b1.v index 0d29d7c8..6b1f602f 100644 --- a/coq/src/putnam_1997_b1.v +++ b/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. diff --git a/coq/src/putnam_1997_b2.v b/coq/src/putnam_1997_b2.v index 0a2cbe66..9ae3c651 100644 --- a/coq/src/putnam_1997_b2.v +++ b/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. diff --git a/coq/src/putnam_1997_b3.v b/coq/src/putnam_1997_b3.v index 507fc747..d69d930d 100644 --- a/coq/src/putnam_1997_b3.v +++ b/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. diff --git a/coq/src/putnam_1997_b4.v b/coq/src/putnam_1997_b4.v deleted file mode 100644 index f1bbfb47..00000000 --- a/coq/src/putnam_1997_b4.v +++ /dev/null @@ -1,9 +0,0 @@ -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 n m : nat, IZR (a n m) = 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. diff --git a/coq/src/putnam_1997_b5.v b/coq/src/putnam_1997_b5.v index b5573e3a..93dad38f 100644 --- a/coq/src/putnam_1997_b5.v +++ b/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. diff --git a/isabelle/putnam_1997_a5.thy b/isabelle/putnam_1997_a5.thy index ca372927..2d353e29 100644 --- a/isabelle/putnam_1997_a5.thy +++ b/isabelle/putnam_1997_a5.thy @@ -5,8 +5,7 @@ definition putnam_1997_a5_solution where "putnam_1997_a5_solution \ undef (* True *) theorem putnam_1997_a5: fixes N::"nat\nat" - defines "N \ \n. card {t::nat list. (size t = n) \ (\i \ {0.. 0) \ (\i \ {0..j \ {0.. t!i \ t!j) - \ (\i=0.. \n. card {t::nat list. (size t = n) \ (\i \ {0.. 0) \ (\i=0.. putnam_1997_a5_solution" sorry diff --git a/isabelle/putnam_1997_a6.thy b/isabelle/putnam_1997_a6.thy index 7f02a57f..47108332 100644 --- a/isabelle/putnam_1997_a6.thy +++ b/isabelle/putnam_1997_a6.thy @@ -2,13 +2,13 @@ theory putnam_1997_a6 imports Complex_Main begin -definition putnam_1997_a6_solution :: "int \ int \ real" where +definition putnam_1997_a6_solution :: "nat \ nat \ real" where "putnam_1997_a6_solution \ undefined" -(* \ n k. (nat n-1) choose (nat k-1) *) +(* \ n k. (n-1) choose (k-1) *) theorem putnam_1997_a6: - fixes n :: "int" + fixes n :: "nat" and C :: "real" - and x :: "real \ (int \ real)" + and x :: "real \ (nat \ real)" and S :: "real set" defines "S \ {c :: real. x c (n + 1) = 0}" assumes hx0 : "\ c :: real. x c 0 = 0" diff --git a/isabelle/putnam_1997_b2.thy b/isabelle/putnam_1997_b2.thy index 3a189eda..158db71b 100644 --- a/isabelle/putnam_1997_b2.thy +++ b/isabelle/putnam_1997_b2.thy @@ -6,9 +6,9 @@ begin theorem putnam_1997_b2: fixes f g :: "real \ real" assumes hg : "\ x :: real. g x \ 0" - and hfdiff : "(f differentiable_on UNIV) \ (deriv f) differentiable_on UNIV" + and hfdiff : "(f C1_differentiable_on UNIV) \ (deriv f) differentiable_on UNIV" and hfg : "\ x :: real. f x + (deriv^^2) f x = -x * g x * (deriv f x)" - shows "bounded (image f UNIV)" + shows "bounded (image (\x::real. \f x\) UNIV)" sorry end diff --git a/isabelle/putnam_1997_b4.thy b/isabelle/putnam_1997_b4.thy index 16d43ce3..0f7d1526 100644 --- a/isabelle/putnam_1997_b4.thy +++ b/isabelle/putnam_1997_b4.thy @@ -5,8 +5,8 @@ begin theorem putnam_1997_b4: fixes a :: "nat \ nat \ int" - assumes ha : "\ n m :: nat. a n m = coeff ((monom 1 0 + monom 1 1 + monom 1 2)^m) n" - shows "\ k :: nat \ 0. (\ i \ {0..nat \((2*(rat_of_nat k)))/(rat_of_nat 3)\}. (-1)^(i) * (a (k-i) i)) \ {0 :: real..1}" + assumes ha : "\ m n :: nat. a m n = coeff ((monom 1 0 + monom 1 1 + monom 1 2)^m) n" + shows "\ k :: nat \ 0. (\ i \ {0..nat \(2*(rat_of_nat k))/(rat_of_nat 3)\}. (-1)^i * (a (k-i) i)) \ {0 :: real..1}" sorry end \ No newline at end of file diff --git a/isabelle/putnam_1997_b5.thy b/isabelle/putnam_1997_b5.thy index 0ab9f2ba..16b69d1f 100644 --- a/isabelle/putnam_1997_b5.thy +++ b/isabelle/putnam_1997_b5.thy @@ -8,7 +8,7 @@ theorem putnam_1997_b5: and tetration :: "nat \ nat \ nat" assumes hn : "n \ 2" and htetrationbase : "\ a :: nat. tetration a 0 = 1" - and htetration : "\ a n :: nat. tetration a (n+1) = a^(tetration a n)" + and htetration : "\ a m :: nat. tetration a (m+1) = a^(tetration a m)" shows "[tetration 2 n = tetration 2 (n-1)] (mod n)" sorry