Merge pull request #147 from trishullab/jasper

batch19982005hard lean fixes and Isabelle

isabelle/putnam_1998_a2.thy

@@ -0,0 +1,19 @@
+theory putnam_1998_a2 imports Complex_Main
+"HOL-Analysis.Lebesgue_Measure"
+begin
+
+theorem putnam_1998_a2:
+  fixes quadrant :: "(real^2) \<Rightarrow> bool"
+  and isarc :: "(real^2) \<Rightarrow> (real^2) \<Rightarrow> bool"
+  and arc :: "(real^2) \<Rightarrow> (real^2) \<Rightarrow> ((real^2) set)"
+  and A :: "(real^2) \<Rightarrow> (real^2) \<Rightarrow> real"
+  and B :: "(real^2) \<Rightarrow> (real^2) \<Rightarrow> real"
+  defines "quadrant \<equiv> (\<lambda>P::real^2. P$1 > 0 \<and> P$2 > 0 \<and> dist 0 P = 1)"
+  and "isarc \<equiv> (\<lambda>P Q::real^2. quadrant P \<and> quadrant Q \<and> P$1 > Q$1)"
+  and "arc \<equiv> (\<lambda>P Q::real^2. {R::real^2. quadrant R \<and> P$1 > R$1 \<and> R$1 > Q$1})"
+  and "A \<equiv> (\<lambda>P Q::real^2. measure lebesgue {S::real^2. (\<exists>R\<in>(arc P Q). R$1 = S$1 \<and> R$2 > S$2 \<and> S$2 > 0)})"
+  and "B \<equiv> (\<lambda>P Q::real^2. measure lebesgue {S::real^2. (\<exists>R\<in>(arc P Q). R$2 = S$2 \<and> R$1 > S$1 \<and> S$1 > 0)})"
+  shows "\<exists>f::real\<Rightarrow>real. \<forall>P Q::real^2. (isarc P Q \<longrightarrow> A P Q + B P Q = f (arctan (Q$2/Q$1) - arctan (P$2/P$1)))"
+  sorry
+
+end

isabelle/putnam_1998_a6.thy

@@ -0,0 +1,15 @@
+theory putnam_1998_a6 imports Complex_Main
+"HOL-Analysis.Lebesgue_Measure"
+begin
+
+theorem putnam_1998_a6:
+  fixes A B C :: "real^2"
+  and threesquare :: "(real^2) \<Rightarrow> (real^2) \<Rightarrow> (real^2) \<Rightarrow> bool"
+  assumes hint: "\<forall>i\<in>{1,2}. \<exists>a b c::int. A$i = a \<and> B$i = b \<and> C$i = c"
+  and htriangle: "A \<noteq> B \<and> A \<noteq> C \<and> B \<noteq> C"
+  and harea: "(dist A B + dist B C) ^ 2 < 8 * (measure lebesgue (convex hull {A, B, C})) + 1"
+  assumes "threesquare \<equiv> (\<lambda>P Q R::real^2. dist Q P = dist Q R \<and> (P - Q) \<bullet> (R - Q) = 0)"
+  shows "threesquare A B C \<or> threesquare B C A \<or> threesquare C A B"
+  sorry
+
+end

isabelle/putnam_2002_a2.thy

@@ -0,0 +1,12 @@
+theory putnam_2002_a2 imports Complex_Main
+"HOL-Analysis.Finite_Cartesian_Product"
+"HOL-Analysis.Linear_Algebra"
+begin
+
+theorem putnam_2002_a2:
+  fixes hemi :: "(real^3) \<Rightarrow> ((real^3) set)"
+  defines "hemi \<equiv> (\<lambda>V::real^3. {P::real^3. P \<bullet> V \<ge> 0})"
+  shows "\<forall>S::(real^3) set. ((S \<subseteq> sphere 0 1 \<and> card S = 5) \<longrightarrow> (\<exists>V::real^3. V \<noteq> 0 \<and> card (S \<inter> hemi V) \<ge> 4))"
+  sorry
+
+end

isabelle/putnam_2003_a5.thy

@@ -0,0 +1,17 @@
+theory putnam_2003_a5 imports Complex_Main
+begin
+
+(* uses (nat \<Rightarrow> int) instead of (Fin (2*m) \<Rightarrow> int) *)
+theorem putnam_2003_a5:
+  fixes n :: nat
+  and dyckpath :: "nat \<Rightarrow> ((nat \<Rightarrow> int) set)"
+  and noevenreturn :: "nat \<Rightarrow> ((nat \<Rightarrow> int) set)"
+  assumes npos: "n > 0"
+  defines "dyckpath \<equiv> (\<lambda>m::nat. {p::nat\<Rightarrow>int. (\<forall>k::nat\<ge>2*m. p k = 0) \<and>
+  p ` {0..(2*m-1)} \<subseteq> {-1, 1} \<and> (\<Sum>k::nat\<in>{0..(2*m-1)}. p k) = 0 \<and> (\<forall>j::nat\<in>{0..(2*m-1)}. (\<Sum>k::nat\<in>{0..j}. p k) \<ge> 0)})"
+  and "noevenreturn \<equiv> (\<lambda>m::nat. {p::nat\<Rightarrow>int. (\<forall>k::nat\<ge>2*m. p k = 0) \<and>
+  \<not>(\<exists>i::nat\<in>{0..(2*m-1)}. \<exists>j::nat\<in>{0..(2*m-1)}. i < j \<and> p i = 1 \<and> (\<forall>k::nat\<in>{(i+1)..j}. p i = -1) \<and> even (j - i) \<and> (\<Sum>k::nat\<in>{0..j}. p k) = 0)})"
+  shows "\<exists>f::(nat\<Rightarrow>int)\<Rightarrow>(nat\<Rightarrow>int). (\<forall>y\<in>(dyckpath (n-1)). \<exists>!x::nat\<Rightarrow>int. x \<in> (dyckpath n \<inter> noevenreturn n) \<and> f x = y)"
+  sorry
+
+end

isabelle/putnam_2003_b2.thy

@@ -0,0 +1,14 @@
+theory putnam_2003_b2 imports Complex_Main
+begin
+
+(* uses (nat \<Rightarrow> nat \<Rightarrow> rat) instead of (Fin n \<Rightarrow> {1..n} \<Rightarrow> rat) *)
+theorem putnam_2003_b2:
+  fixes n :: nat
+  and seq :: "nat \<Rightarrow> nat \<Rightarrow> rat"
+  assumes hn: "n > 0"
+  and hinit: "\<forall>j::nat\<in>{1..n}. seq 0 j = 1 / (rat_of_nat j)"
+  and havg: "\<forall>k::nat\<in>{1..(n-1)}. \<forall>j::nat\<in>{1..(n-k)}. seq k j = (seq (k-1) j + seq (k-1) (j+1)) / 2"
+  shows "seq (n-1) 1 < 2 / (rat_of_nat n)"
+  sorry
+
+end

isabelle/putnam_2003_b5.thy

@@ -0,0 +1,13 @@
+theory putnam_2003_b5 imports Complex_Main
+"HOL-Analysis.Lebesgue_Measure"
+begin
+
+theorem putnam_2003_b5:
+  fixes A B C :: "real^2"
+  assumes hABC: "dist 0 A = 1 \<and> dist 0 B = 1 \<and> dist 0 C = 1 \<and> dist A B = dist A C \<and> dist A B = dist B C"
+  shows "\<exists>f::real\<Rightarrow>real. \<forall>P::real^2. dist 0 P < 1 \<longrightarrow> (\<exists>X Y Z::real^2.
+  dist X Y = dist P A \<and> dist Y Z = dist P B \<and> dist X Z = dist P C \<and>
+  measure lebesgue (convex hull {X, Y, Z}) = f (dist 0 P))"
+  sorry
+
+end

isabelle/putnam_2004_a5.thy

@@ -0,0 +1,18 @@
+theory putnam_2004_a5 imports Complex_Main
+begin
+
+(* uses (nat \<times> nat) instead of (Fin m \<times> Fin n) *)
+theorem putnam_2004_a5:
+  fixes m n :: nat
+  and adj :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+  and connected :: "((nat \<times> nat) \<Rightarrow> bool) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+  and cmr :: "((nat \<times> nat) \<Rightarrow> bool) \<Rightarrow> nat"
+  assumes mnpos: "m * n > 0"
+  defines "adj \<equiv> (\<lambda>(a::nat,b::nat)(c::nat,d::nat). a < m \<and> b < n \<and> c < m \<and> d < n \<and> ((a = c \<and> dist b d = 1) \<or> (b = d \<and> dist a c = 1)))"
+  and "connected \<equiv> (\<lambda>(C::(nat\<times>nat)\<Rightarrow>bool)(P::nat\<times>nat)(Q::nat\<times>nat). (\<exists>(S::(nat\<times>nat) list). length S > 0 \<and>
+  S!0 = P \<and> last S = Q \<and> (\<exists>p::bool. \<forall>i::nat\<in>{0..((length S)-1)}. C (S!i) = p) \<and> (\<forall>i::nat\<in>{0..((length S)-2)}. adj (S!i) (S!(i+1)))))"
+  and "cmr \<equiv> (\<lambda>C::(nat\<times>nat)\<Rightarrow>bool. card {R::(nat\<times>nat) set. (\<exists>P\<in>R. fst P < m \<and> snd P < n \<and> (\<forall>Q::nat\<times>nat. (Q \<in> R \<longleftrightarrow> connected C P Q)))})"
+  shows "(\<Sum>C\<in>{C'::(nat\<times>nat)\<Rightarrow>bool. (\<forall>i::nat\<ge>m. \<forall>j::nat\<ge>n. C (i,j) = False)}. cmr C) > (2 ^ (m*n)) * (m*n / 8)"
+  sorry
+
+end

isabelle/putnam_2004_b4.thy

@@ -0,0 +1,16 @@
+theory putnam_2004_b4 imports Complex_Main
+begin
+
+definition putnam_2004_b4_solution :: "nat \<Rightarrow> complex \<Rightarrow> complex" where "putnam_2004_b4_solution \<equiv> undefined"
+(* (\<lambda>(n::nat)(z::complex). z + n) *)
+theorem putnam_2004_b4:
+  fixes n :: nat
+  and Rk :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+  and R :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+  assumes nge2: "n \<ge> 2"
+  defines "Rk \<equiv> (\<lambda>(k::nat)(Q::complex). k + exp (\<i> * 2 * pi / n) * (Q - k))"
+  assumes hR: "R 0 = id \<and> (\<forall>k::nat. R (k+1) = Rk (k+1) \<circ> R k)"
+  shows "R n = putnam_2004_b4_solution n"
+  sorry
+
+end

isabelle/putnam_2005_a2.thy

@@ -0,0 +1,19 @@
+theory putnam_2005_a2 imports Complex_Main
+begin
+
+(* uses (nat \<Rightarrow> (int \<times> int)) instead of ({1..(3*n)} \<Rightarrow> (int \<times> int)) *)
+definition putnam_2005_a2_solution :: "nat \<Rightarrow> nat" where "putnam_2005_a2_solution \<equiv> undefined"
+(* (\<lambda>n::nat. if n = 1 then 0 else 2 ^ (n - 2)) *)
+theorem putnam_2005_a2:
+  fixes n :: nat
+  and S :: "(int \<times> int) set"
+  and unit :: "(int \<times> int) \<Rightarrow> (int \<times> int) \<Rightarrow> bool"
+  and rooktour :: "(nat \<Rightarrow> (int \<times> int)) \<Rightarrow> bool"
+  assumes npos: "n > 0"
+  defines "S \<equiv> {1..n} \<times> {1..3}"
+  and "unit \<equiv> (\<lambda>(a::int,b::int)(c::int,d::int). (a = c \<and> \<bar>d - b\<bar> = 1) \<or> (b = d \<and> \<bar>c - a\<bar> = 1))"
+  and "rooktour \<equiv> (\<lambda>p::nat\<Rightarrow>(int\<times>int). (\<forall>P\<in>S. \<exists>!i::nat\<in>{1..(3*n)}. p i = P) \<and> (\<forall>i::nat\<in>{1..(3*n-1)}. unit (p i) (p (i+1))) \<and> p 0 = (0, 0) \<and> (\<forall>i::nat>(3*n). p i = (0, 0)))"
+  shows "card {p::nat\<Rightarrow>(int\<times>int). rooktour p \<and> p 1 = (1, 1) \<and> p (3*n) = (n, 1)} = putnam_2005_a2_solution n"
+  sorry
+
+end

isabelle/putnam_2005_b5.thy

@@ -0,0 +1,22 @@
+theory putnam_2005_b5 imports Complex_Main
+"HOL-Analysis.Derivative"
+begin
+
+theorem putnam_2005_b5:
+  fixes n :: nat
+  and P :: "('n::finite \<Rightarrow> real) \<Rightarrow> real"
+  and ispoly :: "(('n \<Rightarrow> real) \<Rightarrow> real) \<Rightarrow> bool"
+  and P2deriv :: "'n \<Rightarrow> ('n \<Rightarrow> real) \<Rightarrow> real"
+  and Psumsq :: "('n \<Rightarrow> real) \<Rightarrow> real"
+  assumes npos: "n > 0"
+  and pncard: "CARD('n) = n"
+  defines "ispoly \<equiv> (\<lambda>P'::('n\<Rightarrow>real)\<Rightarrow>real. (\<exists>l::(real\<times>('n\<Rightarrow>nat)) list. \<forall>x::'n\<Rightarrow>real. P' x = (\<Sum>j::nat=0..((length l)-1). (fst (l!j)) * (\<Prod>i::'n\<in>UNIV. (x i) ^ ((snd (l!j)) i)))))"
+  assumes Ppoly: "ispoly P"
+  defines "P2deriv \<equiv> (\<lambda>(i::'n)(x::'n\<Rightarrow>real). (deriv^^2) (\<lambda>xi::real. P (\<lambda>i'::'n \<Rightarrow> if i' = i then xi else x i')) (x i))"
+  assumes hderiv: "\<forall>x::'n\<Rightarrow>real. (\<Sum>i::'n\<in>UNIV. P2deriv i x) = 0"
+  defines "Psumsq \<equiv> (\<lambda>x::'n\<Rightarrow>real. (\<Sum>i::'n\<in>UNIV. (x i)^2))"
+  assumes hsumsq: "\<exists>Q::('n\<Rightarrow>real)\<Rightarrow>real. ispoly Q \<and> (\<forall>x::'n\<Rightarrow>real. (Psumsq x) * (Q x) = P x)"
+  shows "P = (\<lambda>x::'n\<Rightarrow>real. 0)"
+  sorry
+
+end

lean4/src/putnam_1998_a6.lean

@@ -6,7 +6,7 @@ open Set Function Metric
 theorem putnam_1998_a6
 (A B C : Fin 2 → ℝ)
 (hint : ∀ i : Fin 2, ∃ a b c : ℤ, A i = a ∧ B i = b ∧ C i = c)
-(htriangle : A ≠ B ∧ B ≠ C ∧ A ≠ C ∧ ¬Collinear ℝ {A, B, C})
+(htriangle : A ≠ B ∧ A ≠ C ∧ B ≠ C)
 (harea : (Euclidean.dist A B + Euclidean.dist B C) ^ 2 < 8 * (MeasureTheory.volume (convexHull ℝ {A, B, C})).toReal + 1)
 (threesquare : (Fin 2 → ℝ) → (Fin 2 → ℝ) → (Fin 2 → ℝ) → Prop := fun P Q R ↦ Euclidean.dist Q P = Euclidean.dist Q R ∧ Matrix.dotProduct (P - Q) (R - Q) = 0)
 : (threesquare A B C ∨ threesquare B C A ∨ threesquare C A B) :=

lean4/src/putnam_2002_a2.lean

@@ -6,5 +6,5 @@ open Nat
 theorem putnam_2002_a2
 (sphere : Set (Fin 3 → ℝ) := {P : Fin 3 → ℝ | Euclidean.dist 0 P = 1})
 (hemi : (Fin 3 → ℝ) → Set (Fin 3 → ℝ) := fun V ↦ {P : Fin 3 → ℝ | Matrix.dotProduct P V ≥ 0})
-: (∀ (S : Set (Fin 3 → ℝ)), S ⊆ sphere ∧ S.encard = 5 → ∃ V : (Fin 3 → ℝ), V ≠ 0 ∧ (S ∩ hemi V).encard = 4) :=
+: (∀ (S : Set (Fin 3 → ℝ)), S ⊆ sphere ∧ S.encard = 5 → ∃ V : (Fin 3 → ℝ), V ≠ 0 ∧ (S ∩ hemi V).encard ≥ 4) :=
 sorry

lean4/src/putnam_2003_a5.lean

@@ -9,6 +9,6 @@ theorem putnam_2003_a5
 (dyckpath : (m : ℕ) → Set ((Fin (2 * m)) → ℤ) := fun m ↦ {p : Fin (2 * m) → ℤ |
       range p ⊆ {-1, 1} ∧ ∑ k : Fin (2 * m), p k = 0 ∧ ∀ j : Fin (2 * m), ∑ k : Fin (2 * m), ite (k ≤ j) (p k) 0 ≥ 0})
 (noevenreturn : (m : ℕ) → Set ((Fin (2 * m)) → ℤ) := fun m ↦ {p : Fin (2 * m) → ℤ |
-      ¬∃ i j : Fin (2 * m), i < j ∧ p i = 1 ∧ ∀ k ∈ Ioc i j, p i = -1 ∧ Even (j.1 - i.1) ∧ ∑ k : Fin (2 * m), ite (k ≤ j) (p k) 0 = 0})
+      ¬∃ i j : Fin (2 * m), i < j ∧ p i = 1 ∧ (∀ k ∈ Ioc i j, p i = -1) ∧ Even (j.1 - i.1) ∧ ∑ k : Fin (2 * m), ite (k ≤ j) (p k) 0 = 0})
 : (∃ f : ((Fin (2 * n)) → ℤ) → (Fin (2 * (n - 1)) → ℤ), ∀ y ∈ dyckpath (n - 1), ∃! x, x ∈ dyckpath n ∩ noevenreturn n ∧ f x = y) :=
 sorry

lean4/src/putnam_2003_b2.lean

@@ -3,11 +3,12 @@ open BigOperators
 
 open MvPolynomial Set
 
+-- uses (ℕ → ℕ → ℚ) instead of (Fin n → Icc 1 n → ℚ)
 theorem putnam_2003_b2
 (n : ℕ)
 (hn : n > 0)
 (seq : ℕ → ℕ → ℚ)
 (hinit : ∀ j ∈ Icc 1 n, seq 0 j = 1 / j)
 (havg : ∀ k ∈ Icc 1 (n - 1), ∀ j ∈ Icc 1 (n - k), seq k j = (seq (k - 1) j + seq (k - 1) (j + 1)) / 2)
-: (seq (n - 1) 0 < 2 / n) :=
+: (seq (n - 1) 1 < 2 / n) :=
 sorry

lean4/src/putnam_2005_a2.lean

@@ -3,6 +3,7 @@ open BigOperators
 
 open Nat Set
 
+-- uses (ℕ → ℤ × ℤ) instead of (Icc 1 (3 * n) → ℤ × ℤ)
 abbrev putnam_2005_a2_solution : ℕ → ℕ := sorry
 -- fun n ↦ if n = 1 then 0 else 2 ^ (n - 2)
 theorem putnam_2005_a2