did 1996 fixes for isabelle and coq

coq/src/putnam_1994_b4.v

@@ -9,7 +9,7 @@ Theorem putnam_1994_b4
     end)
     (Mmultn := fix Mmult_n {T : Ring} {n : nat} (A : matrix n n) (p : nat) :=
         match p with
-        | O => A
+        | O => mk_matrix n n (fun i j : nat => if Nat.eqb i j then one else zero)
         | S p' => @Mmult T n n n A (Mmult_n A p')
     end)
     (A := mk_matrix 2 2 (fun i j => 

coq/src/putnam_1996_a1.v

@@ -1,10 +1,8 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1996_a1_solution := (1 + sqrt 2) / 2.
-Theorem putnam_1996_a1 
-    (minA : R)
-    (packable : R -> R -> R -> R -> Prop := fun n1 n2 a1 a2 => (n1 + n2) <= Rmax a1 a2 /\ Rmax n1 n2 <= Rmin a1 a2)
-    (hminA : R -> R -> R -> R -> Prop := fun n1 n2 a1 a2 => a1 * a2 = minA /\ packable n1 n2 a1 a2)
-    (hminAlb : R -> R -> R -> R -> Prop :=  fun n1 n2 a1 a2 => forall (A: R), a1 * a2 = A /\ (packable n1 n2 a1 a2 -> minA <= A))
-    : (forall (n1 n2: R), pow n1 2 + pow n2 2 = 1 -> exists a1 a2 : R, hminA n1 n2 a1 a2 /\ hminAlb n1 n2 a1 a2) <-> minA =putnam_1996_a1_solution.
+Theorem putnam_1996_a1
+    (packable : R -> R -> R -> R -> Prop := (fun n1 n2 a1 a2 : R => (n1 + n2) <= Rmax a1 a2 /\ Rmax n1 n2 <= Rmin a1 a2))
+    (Aprop : R -> Prop := (fun A : R => forall n1 n2 : R, (n1 > 0 /\ n2 > 0 /\ pow n1 2 + pow n2 2 = 1) -> exists a1 a2 : R, a1 > 0 /\ a2 > 0 /\ a1 * a2 = A /\ packable n1 n2 a1 a2))
+    : Aprop putnam_1996_a1_solution /\ (forall A : R, Aprop A -> A >= putnam_1996_a1_solution).
 Proof. Admitted.

coq/src/putnam_1996_a3.v

@@ -1,10 +1,11 @@
 Require Import Nat Ensembles Finite_sets. From mathcomp Require Import fintype.
 Definition putnam_1996_a3_solution : Prop := False.
 Theorem putnam_1996_a3
-    (student_choices : nat -> Ensemble nat)
-    (hinrange : forall n : nat, Included _ (student_choices n) (fun i : nat => le 1 i /\ le i 6))
-    : putnam_1996_a3_solution <-> (exists S : Ensemble nat, Included _ S (fun i : nat => le 1 i /\ le i 20) /\ cardinal _ S 5 /\ 
-        (exists c1 c2 : nat, Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => le 1 i /\ le i 6) /\ 
-        (Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => (forall s : nat, In _ S s -> In _ (student_choices s) i)
-        \/ Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => forall s : nat, In _ S s -> ~ (In _ (student_choices s) i)))))).
+    (studentchoicesinrange : (nat -> Ensemble nat) -> Prop := (fun studentchoices : (nat -> Ensemble nat) => forall n : nat, Included _ (studentchoices n) (fun i : nat => le 1 i /\ le i 6)))
+    (studentchoicesprop : (nat -> Ensemble nat) -> Prop := (fun studentchoices : (nat -> Ensemble nat) =>
+        exists S : Ensemble nat, Included _ S (fun i : nat => le 1 i /\ le i 20) /\ cardinal _ S 5 /\ 
+        (exists c1 c2 : nat, (le 1 c1 /\ le c1 6) /\ (le 1 c2 /\ le c2 6) /\ c1 <> c2 /\
+        ((Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => forall s : nat, In _ S s -> In _ (studentchoices s) i))
+        \/ (Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => forall s : nat, In _ S s -> ~ (In _ (studentchoices s) i)))))))
+    : (forall studentchoices : (nat -> Ensemble nat), studentchoicesinrange studentchoices -> studentchoicesprop studentchoices) <-> putnam_1996_a3_solution.
 Proof. Admitted.

coq/src/putnam_1996_a4.v

@@ -2,10 +2,10 @@ Require Import Basics FinFun Reals Ensembles Finite_sets. From mathcomp Require
 Local Open Scope R_scope.
 Theorem putnam_1996_a4
     (A : finType)
-    (S : Ensemble (A * A * A))
-    (hSdistinct: forall a b c : A, In _ S (a, b, c) -> a <> b /\ b <> c /\ c <> a)
-    (hS1 : forall a b c : A, In _ S (a, b, c) -> In _ S (b, c, a))
-    (hS2 : forall a b c : A, In _ S (a, b, c) -> ~ (In _ S (c, b, a)))
-    (hS3 : forall a b c d : A, (In _ S (a, b, c)) /\ (In _ S (c, d, a)) <-> (In _ S (b, c, d) /\ In _ S (d, a, b)))
-    : exists g : A -> R, Injective g /\ (forall a b c : A, g a < g b /\ g b < g c -> In _ S (a, b, c)).
+    (SS : Ensemble (A * A * A))
+    (hSdistinct: forall a b c : A, In _ SS (a, b, c) -> a <> b /\ b <> c /\ c <> a)
+    (hS1 : forall a b c : A, In _ SS (a, b, c) <-> In _ SS (b, c, a))
+    (hS2 : forall a b c : A, In _ SS (a, b, c) <-> ~ (In _ SS (c, b, a)))
+    (hS3 : forall a b c d : A, (In _ SS (a, b, c) /\ In _ SS (c, d, a)) <-> (In _ SS (b, c, d) /\ In _ SS (d, a, b)))
+    : exists g : A -> R, Injective g /\ (forall a b c : A, g a < g b /\ g b < g c -> In _ SS (a, b, c)).
 Proof. Admitted.

coq/src/putnam_1996_a5.v

@@ -1,8 +1,8 @@
 Require Import Binomial Reals Znumtheory Coquelicot.Coquelicot. From mathcomp Require Import div.
 Open Scope R.
 Theorem putnam_1996_a5 
-    (p: nat)
+    (p : nat)
     (hp : prime (Z.of_nat p) /\ gt p 3)
-    (k := floor (2 * INR p / 3))
-    : exists (m: nat), sum_n (fun i => Binomial.C p (i+1)) (Z.to_nat k) = INR m * pow (INR p) 2.
+    (k : nat := Z.to_nat (floor (2 * INR p / 3)))
+    : exists (m : nat), sum_n_m (fun i => Binomial.C p i) 1 k = INR m * pow (INR p) 2.
 Proof. Admitted.

coq/src/putnam_1996_a6.v

@@ -1,8 +1,8 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1996_a6_solution (c: R) (f: R -> R) :=  if Rle_dec c (1/4) then exists (d: R), f = (fun _ => d) else forall (x: R), 0 <= x <= c -> continuity_pt f x /\ f 0 = f c /\ forall (x: R), x > 0 -> f x = f (pow x 2 + c) /\ (forall (x: R), x < 0 -> f x = f (-x)).
+Definition putnam_1996_a6_solution (c: R) (f: R -> R) :=  if Rle_dec c (1/4) then (exists (d: R), f = (fun _ => d)) else ((forall (x: R), 0 <= x <= c -> continuity_pt f x) /\ f 0 = f c /\ (forall (x: R), x > 0 -> f x = f (pow x 2 + c)) /\ (forall (x: R), x < 0 -> f x = f (-x))).
 Theorem putnam_1996_a6
     (c: R)
     (hc : c > 0)
-    : forall (f: R -> R), continuity f /\ forall (x: R), f x = pow x 2 + c <-> putnam_1996_a6_solution c f.
+    : forall (f: R -> R), (continuity f /\ (forall (x: R), f x = pow x 2 + c)) <-> putnam_1996_a6_solution c f.
 Proof. Admitted.

coq/src/putnam_1996_b2.v

@@ -1,10 +1,8 @@
-Require Import Reals Coquelicot.Coquelicot.
+Require Import Reals Coquelicot.Coquelicot. From mathcomp Require Import bigop.
 Open Scope R.
 Theorem putnam_1996_b2
-    (oddfact := fix odd_fact (n : nat) : R :=
-        match n with
-        | O => 1 
-        | S n' => (2 * INR n - 1) * odd_fact n'
-    end)
-    : forall (n: nat), gt n 0 -> pow ((2 * INR n - 1) / exp 1) ((2 * n - 1) / 2) < oddfact n < pow ((2 * INR n + 1) / exp 1) ((2 * n + 1) / 2).
+    (n : nat)
+    (prododd : R := INR (\prod_(1 <= i < (n + 1)) (2 * i - 1)))
+    (npos : gt n 0)
+    : Rpower ((2 * INR n - 1) / exp 1) ((2 * INR n - 1) / 2) < prododd < Rpower ((2 * INR n + 1) / exp 1) ((2 * INR n + 1) / 2).
 Proof. Admitted.

coq/src/putnam_1996_b3.v

@@ -1,11 +1,9 @@
-Require Import Nat List Reals Coquelicot.Coquelicot.
-Open Scope R.
-Definition putnam_1996_b3_solution : nat -> R := fun n => (2 * INR n ^ 3 + 3 * INR n ^ 2 - 11 * INR n + 18) / 6.
+Require Import Reals Coquelicot.Hierarchy Nat.
+Definition putnam_1996_b3_solution : nat -> R := (fun n => (2 * INR n ^ 3 + 3 * INR n ^ 2 - 11 * INR n + 18) / 6).
 Theorem putnam_1996_b3
-    (m: nat -> R)
-    (n: nat)
-    (hn : ge n 2)
-    (hmub : sum_n (fun i => INR ((nth i (seq 1 (S n)) 0%nat) * (nth ((i + 1) mod n) (seq 1 (S n)) 0%nat))) n <= m n)
-    (hm : sum_n (fun i => INR ((nth i (seq 1 (S n)) 0%nat) * (nth ((i + 1) mod n) (seq 1 (S n))) 0%nat)) n = m n)
-    : m = putnam_1996_b3_solution.
+    (n : nat)
+    (xset : (nat -> nat) -> Prop := (fun x : nat -> nat => forall y : nat, (le 1 y /\ le y n) -> exists! i, (le 0 i /\ le i (n - 1)) /\ x i = y))
+    (xsum : (nat -> nat) -> R := (fun x : nat -> nat => sum_n (fun i : nat => INR (x i) * INR (x ((i + 1) mod n))) (n - 1)))
+    (nge2 : ge n 2)
+    : (exists x : nat -> nat, xset x /\ xsum x = putnam_1996_b3_solution n) /\ (forall x : nat -> nat, xset x -> xsum x <= putnam_1996_b3_solution n).
 Proof. Admitted.

coq/src/putnam_1996_b4.v

@@ -4,15 +4,15 @@ Definition putnam_1996_b4_solution := False.
 Theorem putnam_1996_b4
     (Mmultn := fix Mmult_n {T : Ring} {n : nat} (A : matrix n n) (p : nat) :=
         match p with
-        | O => A
+        | O => mk_matrix n n (fun i j : nat => if Nat.eqb i j then one else zero)
         | S p' => @Mmult T n n n A (Mmult_n A p')
     end)
     (scale_c : R -> matrix 2 2 -> matrix 2 2 := fun c A =>  mk_matrix 2 2 (fun i j => c * coeff_mat 0 A i j))
     (sinA_mat : nat -> matrix 2 2 -> matrix 2 2 := fun n A => scale_c ((pow (-1) n) / INR (fact (2 * n + 1))) (Mmultn A (Nat.add (Nat.mul 2 n) 1)))
-    : exists (A: matrix 2 2), 
+    : (exists (A: matrix 2 2), 
     Series (fun n => coeff_mat 0 (sinA_mat n A) 0 0) = 1    /\
     Series (fun n => coeff_mat 0 (sinA_mat n A) 0 1) = 1996 /\
     Series (fun n => coeff_mat 0 (sinA_mat n A) 1 0) = 0    /\
-    Series (fun n => coeff_mat 0 (sinA_mat n A) 1 1) = 1    <->
+    Series (fun n => coeff_mat 0 (sinA_mat n A) 1 1) = 1)   <->
     putnam_1996_b4_solution.
 Proof. Admitted.

isabelle/putnam_1996_a3.thy

@@ -6,9 +6,11 @@ definition putnam_1996_a3_solution :: "bool" where
 "putnam_1996_a3_solution \<equiv> undefined"
 (* False *)
 theorem putnam_1996_a3:
-  fixes student_choices :: "nat \<Rightarrow> (nat set)"
-  assumes hinrange : "\<forall> n :: nat. student_choices n \<subseteq> {1..6}"
-  shows "putnam_1996_a3_solution \<longleftrightarrow> (\<exists> S :: nat set. S \<subseteq> {1::nat..20} \<and> card S = 5 \<and> (\<exists> c1 \<in> {1 :: nat..6}. \<exists> c2 \<in> {1 :: nat..6}. c1 \<noteq> c2 \<and> ({c1, c2} \<subseteq> (\<Inter> s \<in> S. student_choices s) \<or> {c1, c2} \<subseteq> (\<Inter> s \<in> S. UNIV - (student_choices s))) ))"
+  fixes studentchoicesinrange :: "(nat \<Rightarrow> (nat set)) \<Rightarrow> bool"
+  and studentchoicesprop :: "(nat \<Rightarrow> (nat set)) \<Rightarrow> bool"
+  defines "studentchoicesinrange \<equiv> (\<lambda>studentchoices::nat\<Rightarrow>(nat set). (\<forall>n::nat. studentchoices n \<subseteq> {1..6}))"
+  and "studentchoicesprop \<equiv> (\<lambda>studentchoices::nat\<Rightarrow>(nat set). (\<exists> S :: nat set. S \<subseteq> {1::nat..20} \<and> card S = 5 \<and> (\<exists> c1 \<in> {1 :: nat..6}. \<exists> c2 \<in> {1 :: nat..6}. c1 \<noteq> c2 \<and> ({c1, c2} \<subseteq> (\<Inter> s \<in> S. studentchoices s) \<or> {c1, c2} \<subseteq> (\<Inter> s \<in> S. (UNIV - studentchoices s))))))"
+  shows "(\<forall>studentchoices::nat\<Rightarrow>(nat set). studentchoicesinrange studentchoices \<longrightarrow> studentchoicesprop studentchoices) \<longleftrightarrow> putnam_1996_a3_solution"
   sorry
 
 end

isabelle/putnam_1996_a4.thy

@@ -1,15 +1,17 @@
 theory putnam_1996_a4 imports Complex_Main
+"HOL-Library.Cardinality"
 
 begin
 
 theorem putnam_1996_a4: 
-  fixes S :: "('A \<times> 'A \<times> 'A) set"
+  fixes S :: "('A::finite \<times> 'A \<times> 'A) set"
     and n :: "nat"
   assumes hA : "CARD('A) = n"
+    and hSdistinct: "\<forall>a b c::'A. ((a, b, c) \<in> S \<longrightarrow> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c))"
     and hS1 : " \<forall> a b c :: 'A. (a, b, c) \<in> S \<longleftrightarrow> (b, c, a) \<in> S"
     and hS2 : " \<forall> a b c :: 'A. (a, b, c) \<in> S \<longleftrightarrow> (c, b, a) \<notin> S"
     and hS3 : " \<forall> a b c d :: 'A. ((a, b, c) \<in> S \<and> (c, d, a) \<in> S) \<longleftrightarrow> ((b, c, d) \<in> S \<and> (d, a, b) \<in> S)"
-  shows "\<exists> g :: 'A \<Rightarrow> real. inj g \<and> (\<forall> a b c :: 'A. (g a < g b \<and> g c < g c) \<longrightarrow> (a, b, c) \<in> S)"
+  shows "\<exists> g :: 'A \<Rightarrow> real. inj g \<and> (\<forall> a b c :: 'A. (g a < g b \<and> g b < g c) \<longrightarrow> (a, b, c) \<in> S)"
   sorry
 
 end

isabelle/putnam_1996_a5.thy

@@ -1,13 +1,13 @@
 theory putnam_1996_a5 imports Complex_Main
-
+"HOL-Computational_Algebra.Primes"
 begin
 
 theorem putnam_1996_a5:
   fixes p k :: "nat"
   defines "k \<equiv> nat \<lfloor>2 * p / 3\<rfloor>"
   assumes hpprime : "prime p"
     and hpge3 : "p > 3"
-  shows "p^2 dvd (\<Sum> i \<in> {1 :: nat..k}. p choose i)"
+  shows "(p^2) dvd (\<Sum> i \<in> {1 :: nat..k}. p choose i)"
   sorry
 
 end

isabelle/putnam_1996_b1.thy

@@ -12,7 +12,7 @@ theorem putnam_1996_b1:
   and n :: nat
   defines "selfish \<equiv> \<lambda> s. card s \<in> s"
   assumes npos: "n \<ge> 1"
-  shows "card {s :: nat set. s \<subseteq> {1..n} \<and> selfish s \<and> (\<forall> ss :: nat set. ss \<subseteq> s \<longrightarrow> \<not>selfish ss)} = putnam_1996_b1_solution n"
+  shows "card {s :: nat set. s \<subseteq> {1..n} \<and> selfish s \<and> (\<forall> ss :: nat set. ss \<subset> s \<longrightarrow> \<not>selfish ss)} = putnam_1996_b1_solution n"
   sorry
 
 end

isabelle/putnam_1996_b3.thy

@@ -3,7 +3,7 @@ Complex_Main
 begin
 
 definition putnam_1996_b3_solution :: "nat \<Rightarrow> nat" where "putnam_1996_b3_solution \<equiv> undefined"
-(* \<lambda> n :: nat. (2 * n ^ 3 + 3 * n ^ 2 - 11 * n + 18) div 6 *) 
+(* \<lambda> n :: nat. (2 * n ^ 3 + 3 * n ^ 2 + 18 - 11 * n) div 6 *)
 theorem putnam_1996_b3:
   fixes n :: nat
   and xset :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"

isabelle/putnam_1996_b4.thy

@@ -11,7 +11,7 @@ theorem putnam_1996_b4:
   and matpow :: "real^2^2 \<Rightarrow> nat \<Rightarrow> real^2^2"
   defines "matsin \<equiv> \<lambda> A :: real^2^2. \<Sum> n :: nat. ((-1) ^ n / fact (2 * n + 1)) *\<^sub>R (matpow A (2 * n + 1))"
   and "mat1996 \<equiv> \<chi> i j. if i = 1 then (if j = 1 then 1 else 1996) else (if j = 1 then 0 else 1)"  
-  assumes hmatpow: "\<forall> A :: real^2^2. matpow A 0 = mat 1 \<and> (\<forall> k :: nat. matpow A (k + 1) = A * (matpow A k))"
+  assumes hmatpow: "\<forall> A :: real^2^2. matpow A 0 = mat 1 \<and> (\<forall> k :: nat. matpow A (k + 1) = A ** (matpow A k))"
   shows "(\<exists> A :: real^2^2. matsin A = mat1996) \<longleftrightarrow> putnam_1996_b4_solution"
   sorry
 

lean4/src/putnam_1996_a3.lean

@@ -4,6 +4,6 @@ open BigOperators
 abbrev putnam_1996_a3_solution : Prop := sorry
 -- False
 theorem putnam_1996_a3
-(student_choices : Finset.range 20 → Set (Finset.range 6))
-: putnam_1996_a3_solution ↔ ∃ S : Set (Finset.range 20), ∃ c1 c2 : Finset.range 6, c1 ≠ c2 ∧ S.ncard = 5 ∧ ({c1, c2} ⊆ ⋂ s ∈ S, student_choices s ∨ ({c1, c2} ⊆ ⋂ s ∈ S, (student_choices s)ᶜ)) :=
+(studentchoicesprop : (Finset.range 20 → Set (Finset.range 6)) → Prop := (fun studentchoices : (Finset.range 20 → Set (Finset.range 6)) => ∃ S : Set (Finset.range 20), ∃ c1 c2 : Finset.range 6, c1 ≠ c2 ∧ S.encard = 5 ∧ ({c1, c2} ⊆ (⋂ s ∈ S, studentchoices s) ∨ {c1, c2} ⊆ (⋂ s ∈ S, (studentchoices s)ᶜ))))
+: (∀ studentchoices : (Finset.range 20 → Set (Finset.range 6)), studentchoicesprop studentchoices) ↔ putnam_1996_a3_solution :=
 sorry