Merge pull request #214 from trishullab/george

Move to mathcomp (69-72) & Lean slight modifications

coq/src/putnam_1969_a4.v

@@ -1,7 +1,19 @@
-Section putnam_1969_a4.
-Require Import Reals. From Coquelicot Require Import Hierarchy RInt.
-Open Scope R.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals exp sequences topology normedtype measure lebesgue_measure lebesgue_integral.
+From mathcomp Require Import classical_sets.
+Import numFieldNormedType.Exports.
+Import Order.TTheory GRing.Theory Num.Theory.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+
+Variable R : realType.
+Definition mu := [the measure _ _ of @lebesgue_measure R].
 Theorem putnam_1969_a4
-    : filterlim (fun n : nat => sum_n_m (fun i => (-1)^(i+1)*(Rpower (INR i) (-(INR i)))) 1 n) eventually (locally (RInt (fun x => (Rpower x x)) 0 1)).
-Proof. Admitted.
-End putnam_1969_a4.
+    (f : nat -> R := fun n => \sum_(1 <= i < n.+1) ((-1)^(i.+1) / ((i%:R) ^+ i)))
+    : f @ \oo --> (\int[mu]_(x in [set t : R | 0 < t < 1]) (expR (x * ln x))).
+Proof. Admitted.

coq/src/putnam_1969_a5.v

@@ -1,11 +1,18 @@
-Section putnam_1969_a5.
-Require Import Reals Ranalysis.
-Open Scope R.
-Theorem putnam_1969_a5
-    (x y : R -> R)
-    (hx : derivable x)
-    (hy : derivable y)
-    : forall t : R, t > 0 -> ((x 0 = y 0) <-> exists u : R -> R, continuity u /\ x t = 0 /\ y t = 0 /\
-    derive x hx = (fun p : R => -2 * y p + u p) /\ derive y hy = (fun p : R => -2 * x p + u p)).
-Proof. Admitted.
-End putnam_1969_a5.
+From mathcomp Require Import all_ssreflect ssrnum ssralg.
+From mathcomp Require Import reals exp sequences topology normedtype derive.
+From mathcomp Require Import classical_sets.
+Import numFieldNormedType.Exports.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+
+Variable R : realType.
+Theorem putnam_1969_a5 :
+    forall x y : R -> R, (forall t : R, differentiable x t /\ differentiable y t) -> 
+    (forall t : R, t > 0 -> x 0 = y 0 <-> exists u : R -> R, continuous u /\
+    (x t = 0 /\ y t = 0 /\ forall p : R, x^`() p = -2 * y p + u p /\ y^`() p = -2 * x p + u p)).
+Proof. Admitted.

coq/src/putnam_1969_a6.v

@@ -1,10 +1,20 @@
-Section putnam_1969_a6.
-Require Import Reals. From Coquelicot Require Import Hierarchy.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals exp sequences topology normedtype.
+From mathcomp Require Import classical_sets.
+Import numFieldNormedType.Exports.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+
+Variable R : realType.
 Theorem putnam_1969_a6
     (x : nat -> R)
     (y : nat -> R)
     (hy1 : forall n : nat, ge n 2 -> y n = x (Nat.sub n 1) + 2 * (x n))
-    (hy2 : exists c : R, filterlim y eventually (locally c))
-    : exists C : R, filterlim x eventually (locally C).
-Proof. Admitted.
-End putnam_1969_a6.
+    (hy2 : exists c : R, y @ \oo --> c)
+    : exists C : R, x @ \oo --> C.
+Proof. Admitted.

coq/src/putnam_1969_b3.v

@@ -1,10 +1,19 @@
-Section putnam_1969_b3.
-Require Import Reals. From Coquelicot Require Import Hierarchy.
-Open Scope R.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals exp sequences topology normedtype trigo.
+From mathcomp Require Import classical_sets.
+Import numFieldNormedType.Exports.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+
+Variable R : realType.
 Theorem putnam_1969_b3
     (T : nat -> R)
-    (hT1 : forall n : nat, ge n 1 -> (T n) * (T (Nat.add n 1)) = INR n)
-    (hT2 : filterlim (fun n => (T n)/(T (Nat.add n 1))) eventually (locally 1))
-    : PI * (T (S O))^2 = 2.
-Proof. Admitted.
-End putnam_1969_b3.
+    (hT1 : forall n : nat, ge n 1 -> (T n) * (T (n.+1)) = n%:R)
+    (hT2 : (fun n => (T n)/(T n.+1)) @ \oo --> 1)
+    : pi * (T 1%nat) ^+ 2 = 2.
+Proof. Admitted.

coq/src/putnam_1969_b5.v

@@ -1,6 +1,10 @@
 Section putnam_1969_b5.
 Require Import Reals Finite_sets. From Coquelicot Require Import Coquelicot.
 Open Scope R.
+
+(* Note: Not moving this problem to a mathcomp-dependent formalization as mathcomp-analysis 
+   does not yet include an easy definition for eventually, which currently only supports nats.
+   See line 657 of mathcomp-analysis/topology.v which has yet to extend eventually to arbitrary lattices.*)
 Theorem putnam_1969_b5
     (a : nat -> R)
     (ha : forall n : nat, 0 < a n < a (Nat.add n 1))
@@ -9,4 +13,4 @@ Theorem putnam_1969_b5
     (hk : forall x : R, cardinal nat (fun n => a n <= x) (k x))
     : filterlim (fun t : R => INR (k t)/t) (Rbar_locally p_infty) (locally 0).
 Proof. Admitted.
-End putnam_1969_b5.
+End putnam_1969_b5.

coq/src/putnam_1970_a1.v

@@ -1,14 +1,24 @@
-Section putnam_1970_a1.
-Require Import Reals Ensembles stdpp.sets. From Coquelicot Require Import Coquelicot.
-Open Scope R.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals exp sequences topology normedtype trigo.
+From mathcomp Require Import classical_sets cardinality.
+Import numFieldNormedType.Exports.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+Local Open Scope card_scope.
+
+Variable R : realType.
 Theorem putnam_1970_a1
     (a b : R)
     (ha : a > 0)
     (hb : b > 0)
-    (f : R -> R := fun x : R => exp (a*x) * cos (b*x))
+    (f : R -> R := fun x : R => expR (a * x) * cos (b * x))
     (p : nat -> R)
-    (hp : exists c : R, c > 0 /\ forall x : R, ball 0 c x -> Series (fun n => (p n)*x^n) = f x)
-    (T : nat -> Prop := fun n => p n = 0) 
-    : (T = Empty_set nat \/ pred_infinite T).
-Proof. Admitted.
-End putnam_1970_a1.
+    (hp : exists c : R, c > 0 /\ forall x : R, ball 0 c x -> (fun n : nat => \sum_(0 <= i < n) (p i) * x ^+ i) @ \oo --> f x)
+    (S := [set n : nat | p n = 0])
+    : S = set0 \/ infinite_set S.
+Proof. Admitted.

coq/src/putnam_1970_a2.v

@@ -1,9 +1,16 @@
-Section putnam_1970_a2.
-Require Import Reals.
-Open Scope R.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+
+Variable R : realType.
 Theorem putnam_1970_a2
     (A B C D E F G : R)
-    (hle : B^2 - 4*A*C < 0)
-    : exists delta : R, delta > 0 /\ ~exists x y : R, 0 < x^2 + y^2 < delta^2 /\ A*x^2 + B*x*y + C*y^2 + D*x^3 + E*x^2*y + F*x*y^2 + G*y^3 = 0.
+    (hle : B ^+ 2 - 4 * A * C < 0)
+    : exists delta : R, delta > 0 /\ (~ exists x y : R, 0 < x ^+ 2 + y ^+ 2 < delta ^+ 2 /\ 
+    A * x ^+ 2 + B * x * y + C * y ^+ 2 + D * x ^+ 3 + E * x ^+ 2 * y + F * x * y ^+ 2 + G * y ^+ 3 = 0).
 Proof. Admitted.
-End putnam_1970_a2.

coq/src/putnam_1970_a4.v

@@ -1,8 +1,18 @@
-Section putnam_1970_a4.
-Require Import Reals. From Coquelicot Require Import Hierarchy.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals exp sequences topology normedtype.
+From mathcomp Require Import classical_sets.
+Import numFieldNormedType.Exports.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+
+Variable R : realType.
 Theorem putnam_1970_a4
     (x : nat -> R)
-    (hxlim : filterlim (fun n => x n - x (Nat.sub n 2)) eventually (locally 0))
-    : filterlim (fun n => (x n - x (Nat.sub n 1)) / (INR n)) eventually (locally 0).
+    (hxlim : (fun n : nat => x n - x (Nat.sub n 2)) @ \oo --> 0)
+    : (fun n : nat => (x n - x (Nat.sub n 1)) / n%:R) @ \oo --> 0.
 Proof. Admitted.
-End putnam_1970_a4.

coq/src/putnam_1970_b1.v

@@ -1,12 +1,18 @@
-Section putnam_1970_b1.
-Require Import Reals. From Coquelicot Require Import Hierarchy.
-Open Scope R.
-Definition putnam_1970_b1_solution := exp (2 * ln 5 - 4 + 2 * atan 2).
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals exp sequences topology trigo normedtype.
+From mathcomp Require Import classical_sets.
+Import numFieldNormedType.Exports.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+
+Variable R : realType.
+Definition putnam_1970_b1_solution : R := expR (2 * ln 5 - 4 + 2 * atan 2).
 Theorem putnam_1970_b1
-    (f : nat -> nat -> R)
-    (hbc : forall n : nat, f n O = 1)
-    (hi : forall n i : nat, f n (Nat.add i 1) = (f n i) * Rpower ((INR n)^2 + (INR (i + 1))^2) (1/(INR n)))
-    (g : nat -> R := fun n : nat => 1/((INR n)^4) * f (Nat.mul 2 n) (Nat.mul 2 n))
-    : filterlim g eventually (locally putnam_1970_b1_solution).
-Proof. Admitted.
-End putnam_1970_b1.
+    (f : nat -> R := fun n => 1/(n%:R ^+ 4) * \prod_(1 <= i < n.*2.+1) expR (1/(n%:R) * ln ((n%:R ^+ 2) + (i%:R ^+ 2))))
+    : f @ \oo --> putnam_1970_b1_solution.
+Proof. Admitted.

coq/src/putnam_1970_b2.v

@@ -1,11 +1,21 @@
-Section putnam_1970_b2.
-Require Import Reals. From Coquelicot Require Import Coquelicot.
-Open Scope R.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals sequences measure lebesgue_measure lebesgue_integral normedtype.
+From mathcomp Require Import classical_sets.
+Import numFieldNormedType.Exports.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+
+Variable R : realType.
+Definition mu := [the measure _ _ of @lebesgue_measure R].
 Theorem putnam_1970_b2
-    (a b c d : R)
     (T : R)
-    (H : R -> R := fun t => a*t^3 + b*t^2 + c*t + d)
+    (H : {poly R})
     (hT : T > 0)
-    : (H (-T/sqrt 3) + H (T/sqrt 3))/2 = 1/(2*T) * RInt H (-T) T.
-Proof. Admitted.
-End putnam_1970_b2.
+    (hH : le (size H) 4%nat)
+    : (H.[(-T/(@Num.sqrt R 3))] + H.[(T/(@Num.sqrt R 3))])/2 = 1/(2*T) * \int[mu]_(t in [set x : R | -T <= x <= T]) H.[t].
+Proof. Admitted.

coq/src/putnam_1970_b3.v

@@ -1,11 +1,21 @@
-Section putnam_1970_b3.
-Require Import Reals Ensembles. From Coquelicot Require Import Hierarchy.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals exp sequences topology normedtype.
+From mathcomp Require Import classical_sets.
+Import numFieldNormedType.Exports.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+
+Variable R : realType.
 Theorem putnam_1970_b3
-    (T : Ensemble (R * R))
+    (S : set (R * R))
     (a b : R)
     (hab : a < b)
-    (hT : forall s : R * R, In (R * R) T s -> a < fst s < b)
-    (hSclosed : closed T)
-    : closed (fun y : R => exists x : R, In (R * R) T (x, y)).
+    (hS : forall s : R * R, s \in S -> a < s.1 < b)
+    (hSclosed : closed S)
+    : closed [set y : R | exists x : R, (x, y) \in S].
 Proof. Admitted.
-End putnam_1970_b3.

coq/src/putnam_1970_b4.v

@@ -1,13 +1,21 @@
-Section putnam_1970_b4.
-Require Import Reals Ranalysis.
-Open Scope R.
+From mathcomp Require Import all_ssreflect ssrnum ssralg.
+From mathcomp Require Import reals exp sequences topology normedtype derive.
+From mathcomp Require Import classical_sets.
+Import numFieldNormedType.Exports.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+
+Variable R : realType.
 Theorem putnam_1970_b4
     (x : R -> R)
-    (hd1 : derivable x)
-    (hd2 : derivable (derive x hd1))
+    (hdiff : (forall t : R, 0 <= t <= 1 -> differentiable x t) /\ (forall t : R, 0 <= t <= 1 -> differentiable (x^`()) t))
     (hx : x 1 - x 0 = 1)
-    (hv : derive x hd1 0 = 0 /\ derive x hd1 1 = 0)
-    (hs : forall t : R, 0 < t < 1 -> Rabs (derive x hd1 t) <= 3/2)
-    : exists t : R, 0 <= t <= 1 /\ Rabs (derive (derive x hd1) hd2 t) >= 9/2.
+    (hv : x^`() 0 = 0 /\ x^`() 1 = 0)
+    (hs : forall t : R, 0 < t < 1 -> `| x^`() t | <= 3/2)
+    : exists t : R, 0 <= t <= 1 /\ `| (x^`(2)) t | >= 9/2.
 Proof. Admitted.
-End putnam_1970_b4.

coq/src/putnam_1970_b5.v

@@ -1,9 +1,18 @@
-Section putnam_1970_b5.
-Require Import Reals Basics Ranalysis.
-Open Scope R.
-Theorem putnam_1970_b5
-    (ramp : nat -> (R -> R) := fun n => (fun x => Rmin (Rmax x (-(INR n))) (INR n)))
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals exp sequences topology normedtype.
+From mathcomp Require Import classical_sets.
+Import numFieldNormedType.Exports.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+Local Open Scope classical_set_scope.
+
+Variable R : realType.
+Theorem putnam_1970_b5_solution
+    (ramp : int -> (R -> R) := fun (n : int) => (fun (x : R) => if x <= -n%:~R then -n%:~R else (if -n%:~R <= x <= n%:~R then x else n%:~R)))
     (F : R -> R)
-    : continuity F <-> (forall n : nat, continuity (compose (ramp n) F)).
-Proof. Admitted.
-End putnam_1970_b5.
+    : continuous F <-> (forall n : nat, continuous (ramp (n%:Z) \o F)).
+Proof. Admitted.

coq/src/putnam_1971_a1.v

@@ -1,8 +1,11 @@
 Require Import Reals Ensembles Finite_sets Coquelicot.Coquelicot.
+
+Local Coercion IZR : Z >-> R.
+
 Theorem putnam_1971_a1
     (S : Ensemble (Z * Z * Z))
     (hS : cardinal _ S 9)
     (L : (Z * Z * Z) * (Z * Z * Z) -> Ensemble (R * R * R)
-       := fun '((a,b,c), (d,e,f)) => fun (x : R * R * R) => (exists t : R, 0 < t < 1 /\ x = (t * (IZR a) + (1 - t) * (IZR d), t * (IZR b) + (1 - t) * (IZR e), t * (IZR c) + (1 - t) * (IZR f))))
+       := fun '((a,b,c), (d,e,f)) => fun (x : R * R * R) => (exists t : R, 0 < t < 1 /\ x = (t * a + (1 - t) * d, t * b + (1 - t) * e, t * c + (1 - t) * f)))
     : exists x y z : Z, exists P Q : Z * Z * Z, In _ S P /\ In _ S Q /\ P <> Q /\ In _ (L (P,Q)) (IZR x, IZR y, IZR z).
 Proof. Admitted.