From 87873cd266a06c0e6751066e2ff743e8a6a345a9 Mon Sep 17 00:00:00 2001 From: George Tsoukalas Date: Sat, 9 Nov 2024 20:58:26 +0000 Subject: [PATCH] Fix Isabelle, Coq formalizations pursuant to #229, #238, #243. --- coq/src/putnam_2017_a2.v | 13 +++++-------- coq/src/putnam_2022_a1.v | 2 +- isabelle/putnam_1963_a3.thy | 5 ++--- isabelle/putnam_1984_a6.thy | 20 ++++++++++---------- isabelle/putnam_1994_a1.thy | 2 +- isabelle/putnam_1994_b3.thy | 6 ++---- isabelle/putnam_2009_b4.thy | 5 +++-- isabelle/putnam_2017_a2.thy | 10 +++++----- isabelle/putnam_2021_a1.thy | 5 ++--- isabelle/putnam_2022_a1.thy | 2 +- 10 files changed, 32 insertions(+), 38 deletions(-) diff --git a/coq/src/putnam_2017_a2.v b/coq/src/putnam_2017_a2.v index 54f086a0..42bedd5a 100644 --- a/coq/src/putnam_2017_a2.v +++ b/coq/src/putnam_2017_a2.v @@ -9,12 +9,9 @@ Local Open Scope ring_scope. Variable R : realType. Theorem putnam_2017_a2 - (Q : nat -> R -> R) - (hQbase : forall x : R, Q 0%nat x = 1 /\ Q 1%nat x = x) - (hQn : forall n : nat, ge n 2 -> forall x : R, Q n x = ((Q (n.-1) x) ^+ 2 - 1) / (Q (n.-2) x)) - : forall n : nat, gt n 0 -> - exists P : {poly R}, - size P = n.+1 /\ - (forall i : nat, exists c : int, P`_i = c%:~R) /\ - Q n = (fun x : R => P.[x]). + (Q : nat -> {poly R}) + (hQbase : Q 0%nat = 1%:P /\ Q 1%nat = 'X) + (hQn : forall n : nat, Q (n.+2) * Q n = Q (n.+1) ^+ 2 - 1%:P) + (n : nat) (hn : lt 0 n) : + exists P : {poly int}, Q n = map_poly intr P. Proof. Admitted. \ No newline at end of file diff --git a/coq/src/putnam_2022_a1.v b/coq/src/putnam_2022_a1.v index 1b7ba336..23f811b9 100644 --- a/coq/src/putnam_2022_a1.v +++ b/coq/src/putnam_2022_a1.v @@ -1,5 +1,5 @@ Require Import Reals Coquelicot.Coquelicot. -Definition putnam_2022_a1_solution : R -> R -> Prop := (a = 0 /\ b = 0) \/ (Rabs a >= 1) \/ (Rabs a < 1 /\ (b < ln (1 - (1 - sqrt (1 - a ^ 2)) / a) ^ 2 - Rabs a * (1 - (1 - sqrt (1 - a ^ 2)) / a) \/ b > ln (1 - (1 + sqrt (1 - a ^ 2) / a) ^ 2 - Rabs a * (1 + sqrt (1 - a ^ 2) / a)))). +Definition putnam_2022_a1_solution : R -> R -> Prop := fun a b => (a = 0 /\ b = 0) \/ (Rabs a >= 1) \/ (0 < Rabs a < 1 /\ (b < ln (1 + ((1 - sqrt (1 - a ^2))/ a) ^ 2) - a * (1 - sqrt (1 - a ^ 2) / a) \/ b > ln (1 + ((1 + sqrt (1 - a ^ 2)) / a) ^ 2) - a * (1 + sqrt (1 - a ^ 2) / a))). Theorem putnam_2022_a1 : forall a b : R, (exists! (x: R), a * x + b = ln (1 + x ^ 2) / ln 10) <-> putnam_2022_a1_solution a b. Proof. Admitted. diff --git a/isabelle/putnam_1963_a3.thy b/isabelle/putnam_1963_a3.thy index 5f2916d2..c6bc93aa 100644 --- a/isabelle/putnam_1963_a3.thy +++ b/isabelle/putnam_1963_a3.thy @@ -13,9 +13,8 @@ theorem putnam_1963_a3: assumes hP : "(\ x. P 0 x = x) \ (\ (i :: nat) (y :: real \ real). P (i + 1) y = P i (\ x. x * deriv y x - (real_of_nat i) * y x))" and hn : "0 < n" and hf : "continuous_on {1..} f" - shows "((\ k :: nat < n. - ((deriv^^k) y) C1_differentiable_on {1..} ∧ - ((deriv^^k) y) 1 = 0) \ + and hy : "\ k :: nat < n. ((deriv^^k) y) C1_differentiable_on {1..}" + shows "((\ k :: nat < n. ((deriv^^k) y) 1 = 0) \ (\ x :: real. x \ 0 \ (P n y) x = f x)) \ (\ x :: real \ 1. y x = interval_lebesgue_integral lebesgue 1 (ereal x) (putnam_1963_a3_solution f n x))" sorry diff --git a/isabelle/putnam_1984_a6.thy b/isabelle/putnam_1984_a6.thy index 29e3bc87..686978d5 100644 --- a/isabelle/putnam_1984_a6.thy +++ b/isabelle/putnam_1984_a6.thy @@ -2,18 +2,18 @@ theory putnam_1984_a6 imports Complex_Main "HOL-Number_Theory.Cong" begin -definition putnam_1984_a6_solution :: "bool \ nat" where "putnam_1984_a6_solution \ undefined" -(* (True, 4) *) +definition putnam_1984_a6_solution :: "nat" where "putnam_1984_a6_solution \ undefined" +(* 4 *) theorem putnam_1984_a6: fixes f :: "nat \ nat" - and kadistinct :: "nat \ (nat \ nat) \ bool" - and gpeq :: "(nat \ nat) \ nat \ bool" - defines "kadistinct \ \ (k :: nat) (a :: nat \ nat). k \ 1 \ (\ i j :: nat. (i < k \ j < k \ i \ j) \ a i \ a j)" - and "gpeq \ \ (g :: nat \ nat) (p :: nat). p > 0 \ (\ (s :: nat) \ 1. g s = g (s + p))" - assumes hf : "\ n > 0. f n = (if [fact n \ 0] (mod 10) then ((fact n) mod 10) else f ((fact n) div 10))" - shows "let (b, n) = putnam_1984_a6_solution in \ g :: nat \ nat. -(\ (k :: nat) (a :: nat \ nat). kadistinct k a \ g (\ i=0..(k-1). a i) = f (\ i=0..(k-1). 5^(a i))) -\ (if b then gpeq g n \ (\ p :: nat. gpeq g p \ p \ n) else \(\ p :: nat. gpeq g p))" + and IsPeriodicFrom :: "nat \ (nat \ nat) \ nat \ bool" + and P :: "nat \ (nat \ nat) \ nat \ bool" + assumes hf : "\ n > 0. f n = (if [fact n \ 0] (mod 10) then ((fact n) mod 10) else f ((fact n) div 10))" + and P_def : "\ x g p. P x g p \ (if p = 0 then (\ q > 0. \ IsPeriodicFrom x g q) else p = (LEAST q ::nat. 0 < q \ IsPeriodicFrom x g q))" + and IsPeriodicFrom_def : "\ x f p. (IsPeriodicFrom x f p \ (\ (s :: nat) \ x. f s = f (s + p)))" + shows "\ g :: nat \ nat. + (\ (k :: nat) (a :: nat \ nat). (k > 0 \ inj a) \ (f (\ i=0..(k-1). 5^(a i)) = g (\ i=0..(k-1). a i)) \ + P 1 g putnam_1984_a6_solution)" sorry end \ No newline at end of file diff --git a/isabelle/putnam_1994_a1.thy b/isabelle/putnam_1994_a1.thy index ed9662d4..5093bb76 100644 --- a/isabelle/putnam_1994_a1.thy +++ b/isabelle/putnam_1994_a1.thy @@ -4,7 +4,7 @@ begin theorem putnam_1994_a1: fixes a :: "nat \ real" assumes ha: "\n::nat\1. 0 < a n \ a n \ a (2*n) + a (2*n+1)" - shows "\(\s::real. filterlim (\N::nat. (\n::nat=1..N. a n)) (nhds s) at_top)" + shows "filterlim (\N::nat. (\n::nat=1..N. a n)) at_top at_top" sorry end diff --git a/isabelle/putnam_1994_b3.thy b/isabelle/putnam_1994_b3.thy index 6c1868be..3cd62bf4 100644 --- a/isabelle/putnam_1994_b3.thy +++ b/isabelle/putnam_1994_b3.thy @@ -5,10 +5,8 @@ begin definition putnam_1994_b3_solution :: "real set" where "putnam_1994_b3_solution \ undefined" (* {..<1} *) theorem putnam_1994_b3: - fixes k :: real - and allfexN :: bool - assumes hallfexN: "allfexN \ (\f::real\real. (((\x::real. f x > 0) \ f differentiable_on UNIV \ (\x::real. deriv f x > f x)) \ (\N::real. \x::real>N. f x > exp (k*x))))" - shows "allfexN \ k \ putnam_1994_b3_solution" + shows "{k :: real. (\ f::real\real. ((\ x. 0 < f x \ f x < deriv f x) \ f differentiable_on UNIV) \ + (\ N::real. \ x::real>N. f x > exp (k * x)))} = putnam_1994_b3_solution" sorry end diff --git a/isabelle/putnam_2009_b4.thy b/isabelle/putnam_2009_b4.thy index cf87a090..673b1340 100644 --- a/isabelle/putnam_2009_b4.thy +++ b/isabelle/putnam_2009_b4.thy @@ -2,6 +2,7 @@ theory putnam_2009_b4 imports Complex_Main "HOL-Computational_Algebra.Polynomial" "HOL-Analysis.Set_Integral" "HOL-Analysis.Lebesgue_Measure" +"HOL-Analysis.Interval_Integral" begin definition putnam_2009_b4_solution :: nat where "putnam_2009_b4_solution \ undefined" @@ -11,9 +12,9 @@ interpretation mvpolyspace: vector_space "mvpolyscale" sorry theorem putnam_2009_b4: fixes balanced :: "(real poly poly) \ bool" and V :: "(real poly poly) set" - defines "balanced \ (\P::real poly poly. (\r::real>0. (set_lebesgue_integral lebesgue (sphere 0 r) (\x::real^2. poly (poly P (monom (x$2) 0)) (x$1))) / (2*pi*r) = 0))" + defines "balanced \ (\P::real poly poly. (\r::real>0. (interval_lebesgue_integral lebesgue 0 (2*pi) (\ t. poly (poly P (monom (r * sin t) 0)) (r * cos t))) / (2*pi*r) = 0))" assumes hV: "\P::real poly poly. (P \ V \ (balanced P \ degree P \ 2009 \ (\i::nat. degree (coeff P i) \ 2009)))" shows "mvpolyspace.dim V = putnam_2009_b4_solution" sorry -end +end \ No newline at end of file diff --git a/isabelle/putnam_2017_a2.thy b/isabelle/putnam_2017_a2.thy index 75403d58..800dbbc4 100644 --- a/isabelle/putnam_2017_a2.thy +++ b/isabelle/putnam_2017_a2.thy @@ -3,10 +3,10 @@ theory putnam_2017_a2 imports Complex_Main begin theorem putnam_2017_a2: - fixes Q :: "nat \ real \ real" - assumes hQbase: "\x::real. Q 0 x = 1 \ Q 1 x = x" - and hQn: "\n::nat>2. \x::real. Q n x = ((Q (n-1) x)^2 - 1) / Q (n-2) x" - shows "\n::nat>0. \P::real poly. (\i::nat. coeff P i = round (coeff P i)) \ Q n = poly P" + fixes Q :: "nat \ real poly" + assumes hQbase: "\x::real. Q 0 = monom 1 0 \ Q 1 = monom 1 1" + and hQn: "\n::nat. Q (n + 2) * Q n = (Q (n-1))^2 - 1" + shows "\n::nat>0. \P::int poly. Q n = map_poly real_of_int P" sorry -end +end \ No newline at end of file diff --git a/isabelle/putnam_2021_a1.thy b/isabelle/putnam_2021_a1.thy index 33a97afc..b47d6397 100644 --- a/isabelle/putnam_2021_a1.thy +++ b/isabelle/putnam_2021_a1.thy @@ -5,9 +5,8 @@ definition putnam_2021_a1_solution :: nat where "putnam_2021_a1_solution \ int) list) \ bool" - assumes "P \ (\l::(int\int) list. length l \ 1 \ l!0 = (0,0) \ last l = (2021,2021) \ - (\n::nat\{0..((length l)-2)}. sqrt ((fst (l!n) - fst (l!(n + 1)))^2 + (snd (l!n) - snd (l!(n + 1)))^2) = 5))" - shows "(LEAST llen::nat. (\l::(int\int) list. P l \ llen = length l)) = putnam_2021_a1_solution" + assumes P_def : "\ l. (P l \ successively (\ p q. (fst p - fst q) ^ 2 + (snd p - snd q) ^ 2 = 25) l)" + shows "(LEAST k :: nat. \ l. P ((0, 0) # l) \ last l = (2021, 2021) \ length l = k) = putnam_2021_a1_solution" sorry end diff --git a/isabelle/putnam_2022_a1.thy b/isabelle/putnam_2022_a1.thy index 4c7eec7f..6ddcf33f 100644 --- a/isabelle/putnam_2022_a1.thy +++ b/isabelle/putnam_2022_a1.thy @@ -2,7 +2,7 @@ theory putnam_2022_a1 imports Complex_Main begin definition putnam_2022_a1_solution :: "(real \ real) set" where "putnam_2022_a1_solution \ undefined" -(* {(a, b). (a = 0 \ b = 0) \ ((abs a) \ 1) \ (0 < (abs a) \ (abs a) < 1 \ (b < (ln (1 - (1 - sqrt (1 - a^2))/a))^2 - (abs a) * (1 - sqrt (1 - a^2))/a \ b > (ln (1 - (1 + sqrt (1 - a^2))/a))^2 - (abs a) * (1 + sqrt (1 - a^2))/a))} *) +(* {(a, b). (a = 0 \ b = 0) \ ((abs a) \ 1) \ (0 < (abs a) \ (abs a) < 1 \ (b < (ln (1 + (1 - sqrt (1 - a^2))/a)^2) - (abs a) * (1 - sqrt (1 - a^2))/a \ b > (ln (1 + (1 + sqrt (1 - a^2))/a)^2) - (abs a) * (1 + sqrt (1 - a^2))/a))} *) theorem putnam_2022_a1: shows "{(a, b). \! x :: real. a * x + b = ln (1 + x^2)} = putnam_2022_a1_solution" sorry