Merge pull request #198 from trishullab/michael

Isabelle & Coq verifications: 1983-1986

Author: GeorgeTsoukalas

coq/src/commented_problems.v

@@ -166,3 +166,21 @@ Theorem putnam_1997_b4
     : 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. *)
 
+(* From mathcomp Require Import ssralg ssrnum fintype seq poly. 
+Open Scope ring_scope.
+Variable (R: numDomainType).
+Definition putnam_1985_a6_solution : {poly R} := 6%:R *: 'X^2 + 5%:R *: 'X + 1%:R.
+Theorem putnam_1985_a6
+    (g : {poly R} := 3%:R *: 'X^2 + 7%:R *: 'X + 2%:R)
+    (Comp_poly_n := fix comp_poly_n (p : {poly R}) (n : nat) : {poly R} :=
+        match n with 
+        | O => 1
+        | S n' => comp_poly (comp_poly_n p n') p
+    end)
+    : forall (f: {poly R}), f`_0 = 0 -> 
+    forall (n: nat),
+    let F : {poly R} := Comp_poly_n f n in
+    let G : {poly R} := Comp_poly_n g n in
+    (\sum_(i < size F) F`_i)  = (\sum_(i < size G) G`_i)
+    <-> f = putnam_1985_a6_solution.
+Proof. Admitted. *)

coq/src/putnam_1983_a3.v

@@ -1,6 +1,13 @@
-Require Import Nat Reals ZArith Znumtheory Coquelicot.Coquelicot.
-Open Scope R.
+Require Import Nat ZArith Znumtheory.
+Open Scope nat_scope.
+Fixpoint nat_sum (a : nat -> nat) (k : nat) : nat := 
+    match k with
+    | O => a O
+    | S k' => a k + nat_sum a k'
+    end.
 Theorem putnam_1983_a3
-    (f : nat -> nat -> R := fun n p => sum_n (fun i => INR ((i+1) * n^i)) (p-1))
-    : forall (p m n: nat), odd p = true /\ prime (Z.of_nat p) /\ (floor (f m p)) mod Z.of_nat p = (floor (f n p)) mod Z.of_nat p -> Z.of_nat m mod Z.of_nat p = Z.of_nat n mod Z.of_nat p.
+    (p : nat)
+    (hp : odd p = true /\ prime (Z.of_nat p))
+    (f : nat -> nat := fun n => nat_sum (fun i => (i+1) * n^i) (p-2))
+    : forall (a b : nat), a < p /\ b < p /\ a <> b -> (f a) mod p <> (f b) mod p.
 Proof. Admitted.

coq/src/putnam_1983_a4.v

@@ -1,7 +1,9 @@
-Require Import Binomial Reals Znumtheory Coquelicot.Coquelicot.
+Require Import Binomial Reals Coquelicot.Coquelicot.
 Open Scope nat_scope.
 Theorem putnam_1983_a4
-    (m: nat)
-    (hm : m mod 6 = 5)
-    : sum_n (fun n => (if (eq_nat_dec (n mod 3) 2) then Binomial.C m n else R0)) (m-2) <> R0.
+    (k : nat)
+    (kpos : k > 0)
+    (m : nat := 6 * k - 1)
+    (s : R := sum_n_m (fun j => Rmult ((-1) ^ (j + 1)) (Binomial.C m (3 * j - 1))) 1 (2*k - 1))
+    : s <> R0.
 Proof. Admitted.

coq/src/putnam_1983_a5.v

@@ -1,5 +1,5 @@
-Require Import Nat Reals Coquelicot.Coquelicot.
-Definition putnam_1983_a5_solution := true.
+Require Import Nat ZArith Reals Coquelicot.Coquelicot.
+Definition putnam_1983_a5_solution := True.
 Theorem putnam_1983_a5
-    : exists (a: R), forall (n: nat), gt n 0 -> even (Z.to_nat (floor (Rpower a (INR n))) - n) = putnam_1983_a5_solution.
+    : (exists a : R, a > 0 /\ forall n : nat, gt n 0 -> Z.Even (floor (a^n) - Z.of_nat n)) <-> putnam_1983_a5_solution.
 Proof. Admitted.

coq/src/putnam_1983_a6.v

@@ -1,5 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Definition putnam_1983_a6_solution := 2 / 9.
 Theorem putnam_1983_a6
-    : Lim_seq (fun a => let a := INR a in a ^ 4 * exp (-a ^ 3) * RInt (fun x => RInt (fun y => exp (x ^ 3 + y ^ 3)) 0 (a - x)) 0 a) = putnam_1983_a6_solution.
+    (F : R -> R := fun a => (a ^ 4 / exp (a ^ 3)) * RInt (fun x => RInt (fun y => exp (x ^ 3 + y ^ 3)) 0 (a - x)) 0 a)
+    : filterlim F (Rbar_locally p_infty) (locally putnam_1983_a6_solution).
 Proof. Admitted.

coq/src/putnam_1983_b4.v

@@ -1,12 +1,13 @@
-Require Import Reals Coquelicot.Coquelicot.
-Open Scope R.
+Require Import ZArith Reals Coquelicot.Coquelicot.
+Open Scope Z_scope.
 Theorem putnam_1983_b4
-    (m: nat)
-    (f : R -> R := fun n => n + IZR (floor (sqrt n)))
+    (m : Z)
+    (hm : m > 0)
+    (f : Z -> Z := fun n => n + floor (sqrt (IZR n)))
     (A := fix a (n: nat) :=
         match n with
-        | O => INR m
+        | O => m
         | S n' => f (a n')
     end)
-    : exists (i: nat) (q: Z), A i = IZR (floor (A i)) /\ floor (A i) = Z.mul q q.
+    : exists (i : nat) (s : Z), A i = s^2.
 Proof. Admitted.

coq/src/putnam_1983_b5.v

@@ -2,6 +2,6 @@ Require Import Nat Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1983_b5_solution := ln (4/PI).
 Theorem putnam_1983_b5
-    (mindist : R -> R := fun x => Rmin (Rabs (x - IZR (floor x))) (Rabs (x - IZR (floor (x+1)))))
-    : Lim_seq (fun n => 1/(INR n) * (RInt (fun x => mindist (INR n/x)) 1 (INR n))) = putnam_1983_b5_solution.
+    (mindist : R -> R := fun x => Rmin (x - IZR (floor x)) (IZR (floor (x+1)) - x))
+    : Lim_seq (fun n => (1/INR n) * (RInt (fun x => mindist (INR n/x)) 1 (INR n))) = putnam_1983_b5_solution.
 Proof. Admitted.

coq/src/putnam_1984_a2.v

@@ -1,7 +1,8 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope nat_scope.
+(* Uses division by 0 in the first term of the series. *)
 Definition putnam_1984_a2_solution := 2%R.
 Theorem putnam_1984_a2
-    (f : nat -> R := fun n => Rdiv (pow 6 n) ((pow 3 (n+1) - pow 2 (n+1)) * pow 3 n - pow 2 n))
+    (f : nat -> R := fun n => Rdiv (pow 6 n) ((pow 3 (n+1) - pow 2 (n+1)) * (pow 3 n - pow 2 n)))
     : Series f = putnam_1984_a2_solution.
 Proof. Admitted.

coq/src/putnam_1984_a5.v

@@ -1,6 +1,6 @@
 Require Import Reals Factorial Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1984_a5_solution := INR (fact 9 * fact 8 * fact 4 / fact 25).
+Definition putnam_1984_a5_solution := INR (fact 9 * fact 8 * fact 4) / INR (fact 25).
 Theorem putnam_1984_a5
     : RInt (fun z => RInt (fun y => RInt (fun x => x * pow y 9 * pow z 8 * pow (1 - x - y - z) 4) 0 (1 - y - z)) 0 (1 - z)) 0 1 = putnam_1984_a5_solution.
 Proof. Admitted.

coq/src/putnam_1984_b1.v

@@ -1,15 +1,23 @@
-Require Import Factorial ZArith Reals Coquelicot.Coquelicot.
+Require Import Factorial ZArith.
 Open Scope Z.
-Definition putnam_1984_b1_solution (coeff1 coeff2 : nat -> Z) (n1 n2 : Z) := (coeff1 = fun x => match x with | O => 3 | S O => 1 | _ => 0 end) /\ (coeff2 = fun x => match x with | O => -2 | S O => -1 | _ => 0 end) /\ n1 = 1 /\ n2 = 1.
+Fixpoint nat_sum (a : nat -> nat) (k : nat) : nat := 
+    match k with
+    | O => a O
+    | S k' => a k + nat_sum a k'
+    end.
+Fixpoint Z_sum (a : nat -> Z) (k : nat) : Z := 
+    match k with
+    | O => a O
+    | S k' => a k + Z_sum a k'
+    end.
+Definition putnam_1984_b1_solution : (nat -> Z) * (nat -> Z) := (fun x => match x with | O => 3 | S O => 1 | _ => 0 end, fun x => match x with | O => -2 | S O => -1 | _ => 0 end).
 Theorem putnam_1984_b1
-    (f : nat -> Z := fun n => (floor (sum_n (fun i => INR (fact (i + 1))) n)))
-    (p: (nat -> Z) -> Z -> (nat -> Z) := fun coeff n => (fun x => (floor (sum_n (fun i => IZR ((coeff i) * (Z.of_nat (x ^ i)))) (Z.to_nat n + 1)))))
-    : exists (coeff1 coeff2 : nat -> Z) (n1 n2 : Z), 
-    let fix F (n: nat) :=
-        match n with
-        | O => f 0%nat
-        | S O => f 1%nat
-        | S ((S n'') as n') => (p coeff1 n1) n' * F n' + (p coeff2 n2) n'' * F n''
-    end in
-    f = F -> putnam_1984_b1_solution coeff1 coeff2 n1 n2.
+    (f : nat -> Z)
+    (poly : nat -> (nat -> Z) -> nat -> Z := fun k p n => Z_sum (fun i => (p i) * (Z.of_nat (n ^ i))) k)
+    (deg : (nat -> Z) -> nat)
+    (finpoly : (nat -> Z) -> Prop := fun p => (exists k : nat, p k <> 0) /\ (exists m : nat, forall n : nat, gt n m -> p n = 0))
+    (hdeg : forall p : nat -> Z, finpoly p -> (p (deg p) <> 0 /\ forall n : nat, gt n (deg p) -> p n = 0))
+    (hf : forall n : nat, gt n 0 -> f n = (Z_sum (fun i => Z.of_nat (fact i)) n) - Z.of_nat (fact 0))
+    : finpoly (fst putnam_1984_b1_solution) /\ finpoly (snd putnam_1984_b1_solution) /\ 
+    forall n : nat, ge n 1 -> f (Nat.add n 2) = poly (deg (fst putnam_1984_b1_solution)) (fst putnam_1984_b1_solution) n * f (Nat.add n 1) + poly (deg (snd putnam_1984_b1_solution)) (snd putnam_1984_b1_solution) n * f n.
 Proof. Admitted.