From 48f7eacc5e0a9e65e6b2a31f987c09d970a9dc17 Mon Sep 17 00:00:00 2001 From: MichaelHenryJennings Date: Thu, 25 Jul 2024 02:23:50 -0500 Subject: [PATCH] 1995 Isabelle & Coq verifications --- coq/src/putnam_1995_a1.v | 10 +++++----- coq/src/putnam_1995_a2.v | 2 +- coq/src/putnam_1995_a4.v | 15 ++++++++++----- coq/src/putnam_1995_a5.v | 10 +++++----- coq/src/putnam_1995_b4.v | 7 +++++-- coq/src/putnam_1995_b6.v | 4 ++-- isabelle/putnam_1995_a2.thy | 2 +- lean4/src/putnam_1995_a2.lean | 2 +- lean4/src/putnam_1995_a4.lean | 6 +++--- lean4/src/putnam_1995_b6.lean | 2 +- 10 files changed, 34 insertions(+), 26 deletions(-) diff --git a/coq/src/putnam_1995_a1.v b/coq/src/putnam_1995_a1.v index 816fbecc..c69c3024 100644 --- a/coq/src/putnam_1995_a1.v +++ b/coq/src/putnam_1995_a1.v @@ -1,11 +1,11 @@ Require Import Reals Ensembles Coquelicot.Coquelicot. Theorem putnam_1995_a1 - (S T U : Ensemble R) - (hS : forall a : R, forall b : R, In _ S a /\ In _ S b -> In _ S (a * b)) - (hsub : Included _ T S /\ Included _ U S) - (hunion : Same_set _ (Union _ T U) S) + (E T U : Ensemble R) + (hE : forall a : R, forall b : R, In _ E a /\ In _ E b -> In _ E (a * b)) + (hsub : Included _ T E /\ Included _ U E) + (hunion : Same_set _ (Union _ T U) E) (hdisj : Disjoint _ T U) (hT3 : forall a b c : R, In _ T a /\ In _ T b /\ In _ T c -> In _ T (a * b * c)) - (hS3 : forall a b c : R, In _ S a /\ In _ S b /\ In _ S c -> In _ S (a * b * c)) + (hU3 : forall a b c : R, In _ U a /\ In _ U b /\ In _ U c -> In _ U (a * b * c)) : (forall a b : R, In _ T a /\ In _ T b -> In _ T (a * b)) \/ (forall a b : R, In _ U a /\ In _ U b -> In _ U (a * b)). Proof. Admitted. diff --git a/coq/src/putnam_1995_a2.v b/coq/src/putnam_1995_a2.v index cafa7f43..4262c924 100644 --- a/coq/src/putnam_1995_a2.v +++ b/coq/src/putnam_1995_a2.v @@ -2,5 +2,5 @@ Require Import Reals Coquelicot.Coquelicot. Open Scope R. Definition putnam_1995_a2_solution : R -> R -> Prop := fun (a b: R) => a = b. Theorem putnam_1995_a2 - : forall (a b: R), a > 0 /\ b > 0 /\ ex_finite_lim_seq (fun n => RInt (fun x => sqrt (sqrt (x + a) - sqrt x) - sqrt (sqrt x - (x - b))) b (INR n)) <-> putnam_1995_a2_solution a b. + : forall (a b: R), a > 0 /\ b > 0 -> ((exists limit : R, filterlim (fun n : R => RInt (fun x => sqrt (sqrt (x + a) - sqrt x) - sqrt (sqrt x - (x - b))) b n) (Rbar_locally p_infty) (locally limit)) <-> putnam_1995_a2_solution a b). Proof. Admitted. diff --git a/coq/src/putnam_1995_a4.v b/coq/src/putnam_1995_a4.v index 80ac1618..e30a0c8f 100644 --- a/coq/src/putnam_1995_a4.v +++ b/coq/src/putnam_1995_a4.v @@ -1,9 +1,14 @@ -Require Import Reals ZArith Coquelicot.Coquelicot. +Require Import Nat ZArith Coquelicot.Coquelicot. +Open Scope Z_scope. +Fixpoint Z_sum (a : nat -> Z) (k : nat) : Z := + match k with + | O => a O + | S k' => a k + Z_sum a k' + end. Theorem putnam_1995_a4 (n : nat) (hn : gt n 0) - (necklace : nat -> R) - (hnecklaceint : forall i : nat, exists k : Z, necklace i = IZR k) - (hnecklacesum : sum_n necklace n = INR n - 1) - : exists cut : nat, le cut (n-1) /\ (forall k : nat, le k (n-1) -> (sum_n (fun i => necklace ((cut + i) mod n)) k) <= INR k). + (necklace : nat -> Z) + (hnecklacesum : Z_sum necklace (n - 1) = (Z.of_nat n) - 1) + : exists cut : nat, le cut (n-1) /\ (forall k : nat, le k (n-1) -> (Z_sum (fun i => necklace (Nat.modulo (cut + i) n)) k) <= Z.of_nat k). Proof. Admitted. diff --git a/coq/src/putnam_1995_a5.v b/coq/src/putnam_1995_a5.v index 5ca09564..d0312b61 100644 --- a/coq/src/putnam_1995_a5.v +++ b/coq/src/putnam_1995_a5.v @@ -1,9 +1,9 @@ Require Import Nat Reals Coquelicot.Coquelicot. From mathcomp Require Import fintype. Definition putnam_1995_a5_solution : Prop := True. Theorem putnam_1995_a5 - (hdiffx := fun (n : nat) (x : nat -> (R -> R)) => forall (i : nat) (t : R), ge i 0 /\ le i (Nat.sub n 1) -> ex_derive (x i) t) - (ha := fun (n : nat) (a : nat -> nat -> R) => forall i j : nat, ge i 0 /\ le i (Nat.sub n 1) -> a i j > 0) - (hcomb := fun (n : nat) (x : nat -> (R -> R)) (a : nat -> nat -> R) => (forall t : R, forall i : nat, ge i 0 /\ le i (Nat.sub n 1) -> Derive (x i) t = sum_n (fun j => a i j * ((x j) t)) n)) - (hxlim := fun (n : nat) (x : nat -> (R -> R)) => (forall i : nat, (ge i 0 /\ le i (Nat.sub n 1)) -> filterlim (x i) (Rbar_locally p_infty) (locally 0))) - : putnam_1995_a5_solution <-> (forall (n : nat) (x : nat -> (R -> R)) (a : nat -> nat -> R), (ge n 0 /\ hdiffx n x /\ ha n a /\ hcomb n x a /\ hxlim n x) -> ~(forall b : nat -> R, (forall t : R, 0 = sum_n (fun i => (b i) * ((x i) t)) (Nat.sub n 1)) -> (forall i : nat, (ge i 0 /\ le i (Nat.sub n 1)) -> b i = 0) )). + (hdiffx := fun (n : nat) (x : nat -> (R -> R)) => forall (i : nat) (t : R), le i (Nat.sub n 1) -> ex_derive (x i) t) + (ha := fun (n : nat) (a : nat -> nat -> R) => forall i j : nat, le i (Nat.sub n 1) /\ le j (Nat.sub n 1) -> a i j > 0) + (hcomb := fun (n : nat) (x : nat -> (R -> R)) (a : nat -> nat -> R) => (forall t : R, forall i : nat, le i (Nat.sub n 1) -> Derive (x i) t = sum_n (fun j => a i j * ((x j) t)) (n - 1))) + (hxlim := fun (n : nat) (x : nat -> (R -> R)) => (forall i : nat, le i (Nat.sub n 1) -> filterlim (x i) (Rbar_locally p_infty) (locally 0))) + : putnam_1995_a5_solution <-> (forall (n : nat) (x : nat -> (R -> R)) (a : nat -> nat -> R), (gt n 0 /\ hdiffx n x /\ ha n a /\ hcomb n x a /\ hxlim n x) -> ~(forall b : nat -> R, (forall t : R, 0 = sum_n (fun i => (b i) * ((x i) t)) (n - 1)) -> (forall i : nat, le i (Nat.sub n 1) -> b i = 0))). Proof. Admitted. diff --git a/coq/src/putnam_1995_b4.v b/coq/src/putnam_1995_b4.v index 794c361f..89fbd543 100644 --- a/coq/src/putnam_1995_b4.v +++ b/coq/src/putnam_1995_b4.v @@ -1,6 +1,9 @@ Require Import Reals ZArith Coquelicot.Coquelicot. Open Scope R. -Definition putnam_1995_b4_solution (a b c d: Z) := (a, b, c, d) = (3%Z,1%Z,5%Z,2%Z). +Definition putnam_1995_b4_solution : Z * Z * Z * Z := (3%Z,1%Z,5%Z,2%Z). Theorem putnam_1995_b4 - : exists (a b c d: Z), exists (contfrac: R), contfrac = 2207 - 1 / contfrac -> pow contfrac (1 / 8) = (IZR a + IZR b * sqrt (IZR c))/IZR d <-> putnam_1995_b4_solution a b c d. + (contfrac : R) + (hcontfrac : contfrac = 2207 - 1/contfrac) + : let (abc, d) := putnam_1995_b4_solution in let (ab, c) := abc in let (a, b) := ab in + pow contfrac (1 / 8) = (IZR a + IZR b * sqrt (IZR c))/IZR d. Proof. Admitted. diff --git a/coq/src/putnam_1995_b6.v b/coq/src/putnam_1995_b6.v index 48603752..681cc04c 100644 --- a/coq/src/putnam_1995_b6.v +++ b/coq/src/putnam_1995_b6.v @@ -1,5 +1,5 @@ Require Import Reals Ensembles Coquelicot.Coquelicot. Theorem putnam_1995_b6 - (S : R -> Ensemble nat := fun alpha => (fun x : nat => exists n : nat, ge n 1 /\ INR x = IZR (floor ((INR n) * alpha)))) - : ~ exists alpha beta gamma : R, alpha > 0 /\ beta > 0 /\ gamma > 0 /\ (Disjoint _ (S alpha) (S beta) /\ Disjoint _ (S beta) (S gamma) /\ Disjoint _ (S gamma) (S alpha)) /\ (~ Same_set _ (fun x : nat => ge x 1) (Union _ (Union _ (S alpha) (S beta)) (S gamma))). + (E : R -> Ensemble nat := fun alpha => fun x : nat => exists n : nat, ge n 1 /\ Z.of_nat x = floor (INR n * alpha)) + : ~ exists alpha beta gamma : R, alpha > 0 /\ beta > 0 /\ gamma > 0 /\ (Disjoint _ (E alpha) (E beta) /\ Disjoint _ (E beta) (E gamma) /\ Disjoint _ (E gamma) (E alpha)) /\ (Same_set _ (fun x : nat => ge x 1) (Union _ (Union _ (E alpha) (E beta)) (E gamma))). Proof. Admitted. diff --git a/isabelle/putnam_1995_a2.thy b/isabelle/putnam_1995_a2.thy index 30458e02..13780fd1 100644 --- a/isabelle/putnam_1995_a2.thy +++ b/isabelle/putnam_1995_a2.thy @@ -7,7 +7,7 @@ definition putnam_1995_a2_solution :: "(real \ real) set" where "putnam_1 theorem putnam_1995_a2: fixes habconv :: "(real \ real) \ bool" defines "habconv \ (\(a::real,b::real). (\limit::real. filterlim (\t::real. interval_lebesgue_integral lebesgue b t (\x::real. sqrt (sqrt (x+a) - sqrt x) - sqrt (sqrt x - sqrt (x-b)))) (nhds limit) at_top))" - shows "\ab::real\real. habconv ab \ ab \ putnam_1995_a2_solution" + shows "\ab::real\real. fst ab > 0 \ snd ab > 0 \ (habconv ab \ ab \ putnam_1995_a2_solution)" sorry end diff --git a/lean4/src/putnam_1995_a2.lean b/lean4/src/putnam_1995_a2.lean index 40da99b0..daf4282e 100644 --- a/lean4/src/putnam_1995_a2.lean +++ b/lean4/src/putnam_1995_a2.lean @@ -8,5 +8,5 @@ abbrev putnam_1995_a2_solution : Set (ℝ × ℝ) := sorry theorem putnam_1995_a2 (habconv : (ℝ × ℝ) → Prop := fun ⟨a,b⟩ => ∃ limit : ℝ, Tendsto (fun t : ℝ => ∫ x in (Set.Icc b t), (sqrt (sqrt (x + a) - sqrt x) - sqrt (sqrt x - sqrt (x - b)))) atTop (𝓝 limit)) -: ∀ ab : ℝ × ℝ, habconv ab ↔ ab ∈ putnam_1995_a2_solution := +: ∀ ab : ℝ × ℝ, ab.1 > 0 ∧ ab.2 > 0 → (habconv ab ↔ ab ∈ putnam_1995_a2_solution) := sorry diff --git a/lean4/src/putnam_1995_a4.lean b/lean4/src/putnam_1995_a4.lean index 801e1fff..4f8661a8 100644 --- a/lean4/src/putnam_1995_a4.lean +++ b/lean4/src/putnam_1995_a4.lean @@ -6,7 +6,7 @@ open Filter Topology Real theorem putnam_1995_a4 (n : ℕ) (hn : n > 0) -(necklace : Fin n → ℤ) -(hnecklacesum : ∑ i : Fin n, necklace i = n - 1) -: ∃ cut : Fin n, ∀ k : Fin n, ∑ i : {j : Fin n | j.1 ≤ k}, necklace (cut + i) ≤ k := +(necklace : ℕ → ℤ) +(hnecklacesum : ∑ i ∈ Finset.range n, necklace i = n - 1) +: ∃ cut ∈ Finset.range n, ∀ k ∈ Finset.range n, ∑ i ≤ k, necklace ((cut + i) % n) ≤ k := sorry diff --git a/lean4/src/putnam_1995_b6.lean b/lean4/src/putnam_1995_b6.lean index 43c1da03..4f3da7c9 100644 --- a/lean4/src/putnam_1995_b6.lean +++ b/lean4/src/putnam_1995_b6.lean @@ -5,5 +5,5 @@ open Filter Topology Real Nat theorem putnam_1995_b6 (S : ℝ → Set ℕ := fun α => {x : ℕ | ∃ n : ℕ, n ≥ 1 ∧ x = floor (n * α)}) -: ¬ ∃ α β γ : ℝ, α > 0 ∧ β > 0 ∧ γ > 0 ∧ (S α) ∩ (S β) = ∅ ∧ (S β) ∩ (S γ) = ∅ ∧ (S α) ∩ (S γ) = ∅ ∧ ℕ+ = (S α) ∪ (S β) ∪ (S γ) := +: ¬ ∃ α β γ : ℝ, α > 0 ∧ β > 0 ∧ γ > 0 ∧ (S α) ∩ (S β) = ∅ ∧ (S β) ∩ (S γ) = ∅ ∧ (S α) ∩ (S γ) = ∅ ∧ Set.Ici 1 = (S α) ∪ (S β) ∪ (S γ) := sorry