Merge pull request #225 from trishullab/george

Modify Coq problems to mathcomp & some Lean formalizations.

coq/src/putnam_2012_a6.v

@@ -1,7 +1,22 @@
-Require Import Reals. From Coquelicot Require Import Coquelicot Continuity RInt.
-Open Scope R_scope.
-Definition putnam_2012_a6_solution := True.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals normedtype topology sequences measure lebesgue_measure lebesgue_integral.
+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].
+Definition putnam_2012_a6_solution : Prop := True.
 Theorem putnam_2012_a6
-    (p : ((R * R) -> R) -> Prop := fun f : (R * R) -> R => (forall v : R*R, continuity_pt f v) /\ forall x1 x2 y1 y2 : R, x2 > x1 -> y2 > y1 -> (x2-x1) * (y2 - y1) = 1 ->  RInt (fun y => RInt (fun x => f (x, y)) x1 x2) y1 y2 = 0)
-    : (forall f : (R * R) -> R, forall x y : R, p f -> f (x, y) = 0) <-> putnam_2012_a6_solution.
-Proof. Admitted.
+    (p : ((R * R) -> R) -> Prop)
+    (hp : forall f : (R * R) -> R, p f <->
+        continuous f /\ forall x1 x2 y1 y2 : R, x2 > x1 -> y2 > y1 -> (x2 - x1) * (y2 - y1) = 1 ->
+            \int[mu]_(x in [set x | x1 <= x <= x2]) (fun x' => \int[mu]_(y in [set y | y1 <= y <= y2]) f (x', y)) x = 0)
+    : (forall f, forall x y, p f -> f (x, y) = 0) <-> putnam_2012_a6_solution.
+Proof. Admitted.

coq/src/putnam_2012_b1.v

@@ -1,16 +1,23 @@
-(* Note: this formalization differs from the original statement by assigning a value of zero to all values outside the specified domain/range. The problem is still solvable given this modification. *)
-Require Import Reals RIneq.
-Open Scope R.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals sequences exp topology.
+From mathcomp Require Import classical_sets.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+
+Variable R : realType.
 Theorem putnam_2012_b1
-    (A: list (R -> R)) 
-    (fPlus : (R -> R) -> (R -> R) -> (R -> R) := fun f g => fun x => f x + g x)
-    (fMinus : (R -> R) -> (R -> R) -> (R -> R) := fun f g => fun x => f x - g x)
-    (fMult : (R -> R) -> (R -> R) -> (R -> R) := fun f g => fun x => f x * g x)
-    (to_Rplus : ((R -> R) -> R -> R) := fun f => fun x => if Rle_dec x 0 then 0 else if Rle_dec (f x) 0 then 0 else f x)
-    (f1 := to_Rplus (fun x => (Rpower (exp 1) x) - 1))
-    (f2 := to_Rplus (fun x => ln (x+1)))
-    : (In f1 A /\ In f2 A) /\ 
-    (forall (f g: R -> R), In f A /\ In g A -> In (fPlus f g) A) /\
-    (forall (f g: R -> R), In f A /\ In g A /\ forall (x: R), f x >= g x -> In (fMinus f g) A)
-    <-> (forall (f g: R -> R), In f A /\ In g A -> In (fMult f g) A).
-Proof. Admitted.
+    (S : set (R -> R))
+    (hS : forall f : R -> R, f \in S -> forall x : R, 0 <= x -> 0 <= f x)
+    (f1 : R -> R := fun x => expR x - 1)
+    (f2 : R -> R := fun x => ln (x + 1))
+    (hf1 : f1 \in S)
+    (hf2 : f2 \in S)
+    (hsum : forall f g : R -> R, f \in S -> g \in S -> (fun x => f x + g x) \in S)
+    (hcomp : forall f g : R -> R, f \in S -> g \in S -> (fun x => f (g x)) \in S)
+    (hdiff : forall f g : R -> R, f \in S -> g \in S -> (forall x : R, f x >= g x) -> (fun x => f x - g x) \in S)
+    : forall f g : R -> R, f \in S -> g \in S -> (fun x => f x * g x) \in S.
+Proof. Admitted.

coq/src/putnam_2013_a6.v

@@ -1,19 +1,21 @@
-Require Import List ZArith.
-Open Scope Z.
-Theorem putnam_2013_a6 
-    (W := fix w (v : Z*Z) : Z :=
-        match v with
-        | (-2, -2) => -1 | (-2, -1) => -2 | (-2,  0) =>  2 | (-2,  1) => -2 | (-2,  2) => -1
-        | (-1, -2) => -2 | (-1, -1) =>  4 | (-1,  0) => -4 | (-1,  1) =>  4 | (-1,  2) => -2
-        | ( 0, -2) =>  2 | ( 0, -1) => -4 | ( 0,  0) => 12 | ( 0,  1) => -4 | ( 0,  2) =>  2
-        | ( 1, -2) =>  -2 | ( 1, -1) =>  4 | ( 1,  0) => -4 | ( 1,  1) =>  4 | ( 1,  2) => -2
-        | ( 2, -2) =>  -1 | ( 2, -1) => -2 | ( 2,  0) =>  2 | ( 2,  1) => -2 | ( 2,  2) => -1
-        | _ => 0
-    end)
-    (A : list (Z * Z * (Z * Z)) -> Z := fun l =>
-        fst (fold_left (fun acc pq => 
-        let p := (fst (fst pq), snd (fst pq)) in
-        let q := (fst (snd pq), snd (snd pq)) in
-        (Z.add (fst acc) (W (fst p - fst q, snd p - snd q)), Z.add (snd acc) (W (fst p - fst q, snd p - snd q)))) l (0, 0)) )
-    : forall (l : list (Z * Z * (Z * Z))), length l <> Z.to_nat 0 -> A l > 0.
-Proof. Admitted.
+From mathcomp Require Import all_algebra all_ssreflect.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+
+Theorem putnam_2013_a6
+    (w : int -> int -> int)
+    (A : seq (int * int) -> int)
+    (hwn1 : w (-2) (-2) = -1 /\ w 2 (-2) = -1 /\ w (-2) 2 = -1 /\ w 2 2 = -1)
+    (hwn2 : w (-1) (-2) = -2 /\ w 1 (-2) = -2 /\ w (-2) (-1) = -2 /\ w 2 (-1) = -2 /\ w (-2) 1 = -2 /\ w 2 1 = -2 /\ w (-1) 2 = -2 /\ w 1 2 = -2)
+    (hw2 : w 0 (-2) = 2 /\ w (-2) 0 = 2 /\ w 2 0 = 2 /\ w 0 2 = 2)
+    (hw4 : w (-1) (-1) = 4 /\ w 1 (-1) = 4 /\ w (-1) 1 = 4 /\ w 1 1 = 4)
+    (hwn4 : w 0 (-1) = -4 /\ w (-1) 0 = -4 /\ w 1 0 = -4 /\ w 0 1 = -4)
+    (hw12 : w 0 0 = 12)
+    (hw0 : forall a b : int, (`|a| > 2 \/ `|b| > 2) -> w a b = 0)
+    (ha : forall s : seq (int * int), A s = \sum_(a <- s) (\sum_(b <- s) w (a.1 - b.1) (a.2 - b.2)))
+    : forall s : seq (int * int), gt (size s) 0 -> uniq s -> A s > 0.
+Proof. Admitted. 

coq/src/putnam_2014_a4.v

@@ -15,7 +15,6 @@ Theorem putnam_2014_a4
     (ed := @expectation _ _ _ P X = 1%:E)
     (ed2 := @expectation _ _ _ P (X * X) = 2%:E)
     (ed3 := @expectation _ _ _ P (X * X * X) = 5%:E)
-    (minval : R)
-    (de := distribution P X)
-    : forall (P : probability T R), (minval <= (pmf X 0) /\ exists (P : probability T R), minval = (pmf X 0)) <-> minval = putnam_2014_a4_solution.
+    : (forall (P : probability T R), putnam_2014_a4_solution <= (pmf X 0)) /\ 
+      (exists (P : probability T R), putnam_2014_a4_solution = (pmf X 0)).
 Proof. Admitted.

coq/src/putnam_2014_a5.v

@@ -1,9 +1,15 @@
-From mathcomp Require Import ssrnat ssrnum ssralg fintype poly polydiv.
-Open Scope ring_scope.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals.
+From mathcomp Require Import complex.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+
+Variable R : realType.
 Theorem putnam_2014_a5
-    (R: numDomainType)
-    (j k : nat)
-    (pj : {poly R}:= \sum_(i < j.+1) ((i%:R + 1) *: 'X^i))
-    (pk : {poly R} := \sum_(i < k.+1) ((i%:R + 1) *: 'X^i))
-    : j <> k -> gcdp_rec pj pk = 1.
+    (P : nat -> {poly R[i]} := fun n => \sum_(1 <= i < n.+1) i%:R *: 'X^(i.-1))
+    : forall j k : nat, (gt j 0 /\ gt k 0) -> j <> k -> gcdp_rec (P j) (P k) = 1.
 Proof. Admitted.

coq/src/putnam_2015_b4.v

@@ -1,17 +1,27 @@
-Require Import Nat List Reals Coquelicot.Coquelicot. From mathcomp Require Import div.
-Open Scope nat_scope.
-Definition putnam_2015_b4_solution := (17, 21). 
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals normedtype sequences topology.
+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 putnam_2015_b4_solution : int * int := (17%Z, 21%Z).
 Theorem putnam_2015_b4
-    (Exprl2 := fix exprl2 (l : list nat) : R :=
-    match l with
-    | a :: b :: c :: _ => Rdiv (2 ^ a) (3 ^ b * 5 ^ c)
-    | _ => R0 
-    end)
-    (Exprl := fix exprl (l : list (list nat)) : list R :=
-    match l with
-    | nil => nil
-    | h :: t => Exprl2 h :: exprl t
-    end)
-    : forall (E: list (list nat)) (l: list nat), (In l E <-> (length l = 3 /\ let a := nth 0 l 0 in let b := nth 1 l 0 in let c := nth 2 l 0 in a > 0 /\ b > 0 /\ c > 0 /\ a < c + b /\ b < a + c /\ c < a + b)) ->
-    exists (p q: nat), coprime p q = true /\ fold_left Rplus (Exprl E) R0  = Rdiv (INR p) (INR q) /\  (p, q) = putnam_2015_b4_solution.
-Proof. Admitted.
+    (tri_fun : nat -> nat -> nat -> R := fun i j k : nat => 
+        if (ltn i (Nat.add j k)) && (ltn j (Nat.add i k)) && (ltn k (Nat.add i j)) then (2 ^+ i) / ((3 ^+ j * 5 ^+ k)) else 0)
+    (f : nat -> R := fun n : nat => 
+        \sum_(1 <= i < n)
+        (\sum_(1 <= j < n) 
+        (\sum_(1 <= k < n) 
+        (tri_fun i j k))))
+    (C : rat)
+    (hf : (fun n : nat => f n) @ \oo --> ratr C)
+    : (numq C, denq C) = putnam_2015_b4_solution.
+Proof. Admitted.

coq/src/putnam_2015_b5.v

@@ -1,18 +1,17 @@
-Require Import Reals. From mathcomp Require Import fintype perm ssrbool.
-Open Scope nat_scope.
-Definition putnam_2015_b5_solution := 4.
+From mathcomp Require Import all_algebra all_ssreflect fingroup perm.
+From mathcomp Require Import classical_sets cardinality.
+
+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.
+
+Definition putnam_2015_b5_solution : nat := 4.
 Theorem putnam_2015_b5
-    (cond := fun (n : nat) (π :  {perm 'I_n}) =>
-        forallb (fun i =>
-        forallb (fun j =>
-            if Z.to_nat (Z.abs (Z.of_nat (nat_of_ord i) - Z.of_nat (nat_of_ord j))) =? 1 then
-            Z.to_nat (Z.abs  (Z.of_nat (nat_of_ord (π i)) - Z.of_nat (nat_of_ord (π j)))) <=? 2
-            else true
-        ) (ord_enum n)
-        ) (ord_enum n))
-    (P : nat -> nat := fun n => 
-        let perms := enum 'S_n in
-            let valid_perms := filter (fun π => cond n π) perms in
-        length valid_perms)
-    : forall (n: nat), n >= 2 -> P (n+5) - P (n+4) - P (n+3) + P n = putnam_2015_b5_solution.
+    (P : nat -> nat)
+    (hP := forall n : nat, [set : 'I_(P n)] #= [set pi : 'S_n | forall i j : 'I_n, `|i%:Z - j%:Z| = 1 -> `|(pi i)%:Z - (pi j)%:Z| <= 2])
+    : forall n : nat, ge n 2 -> (P (Nat.add n 5))%:Z - (P (Nat.add n 4))%:Z - (P (Nat.add n 3))%:Z + (P n)%:Z = putnam_2015_b5_solution.
 Proof. Admitted.

coq/src/putnam_2016_b2.v

@@ -1,8 +1,27 @@
-Require Import Bool Reals Coquelicot.Lim_seq Coquelicot.Rbar. 
-Definition putnam_2016_b2_solution (a b : R) := a = 3/4 /\ b = 4/3.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals normedtype sequences exp topology.
+From mathcomp Require Import classical_sets cardinality.
+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.
+Local Open Scope card_scope.
+
+Variable R : realType.
+
+Definition putnam_2016_b2_solution : R*R := (3/4, 4/3).
 Theorem putnam_2016_b2
-    (squarish : nat -> bool := fun n => existsb ( fun m => Nat.eqb n (m * m) || (forallb (fun p => leb ((n-m)*(n-m)) ((n-p)*(n-p))) (seq 0 (S n))) ) (seq 0 (S n)))
-    (squarish_set : nat -> list nat := fun n => filter (fun x => squarish x) (seq 1 n))
-    (a b: R)
-    : Lim_seq (fun N => INR (length (squarish_set N)) / Rpower (INR N) a) = Finite b <-> putnam_2016_b2_solution a b.
+    (is_square : int -> Prop := fun n => (exists m : int, n = m ^+ 2))
+    (squarish : int -> Prop := fun n => is_square n \/ (exists w : int, is_square `|n - w ^+2| /\ forall v : int, `|n - w ^+2| <= `|n - v ^+2|))
+    (S : int -> nat)
+    (hS : forall n : nat, [set: 'I_(S n%:Z)] #= [set i : 'I_n | ge i 1 /\ le i n /\ squarish i])
+    (p : R -> R -> Prop)
+    (hp : forall alpha beta, p alpha beta <-> (alpha > 0 /\ beta > 0 /\ (fun N : nat => (S N)%:R / (expR (alpha * ln N%:R))) @ \oo --> beta))
+    : (forall alpha beta, p alpha beta <-> (alpha, beta) = putnam_2016_b2_solution) \/ ~ exists alpha beta, p alpha beta.
 Proof. Admitted.
+

coq/src/putnam_2016_b5.v

@@ -1,8 +1,8 @@
 Require Import Reals Rpower.
 Open Scope R.
-Definition putnam_2016_b5_solution (f: R -> R) : Prop := exists (c: R), c > 0 /\ forall (x: R), x > 1 -> f x = Rpower x c .
+Definition putnam_2016_b5_solution : (R -> R) -> Prop := fun f => exists (c: R), c > 0 /\ forall (x: R), x > 1 -> f x = Rpower x c .
 Theorem putnam_2016_b5
     (f : R -> R)
     (fle : Prop := (forall x : R, x > 1 -> f x > 1) /\ (forall x y : R, (x > 1 /\ y > 1 /\ x*x <= y <= x*x*x) -> ((f x) * (f x) <= f y <= (f x) * (f x) * (f x))))
     : fle <-> putnam_2016_b5_solution f.
-Proof. Admitted.
+Proof. Admitted.

coq/src/putnam_2017_a2.v

@@ -1,13 +1,20 @@
-Require Import Nat QArith Reals. From mathcomp Require Import seq ssrnat ssrnum ssralg poly. 
-Open Scope ring_scope.
+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_2017_a2
-    (Q := fix q (n: nat) (x: R) : R :=
-        match n with
-        | O => R1
-        | S O => x
-        | S ((S n'') as n') => Rdiv (Rminus (Rmult (q n' x) (q n' x)) 1) (q n'' x)
-    end)
-    : forall (n: nat), ge n 0 -> 
-    exists (R : numDomainType) (p : {poly R}) (i : nat), (exists (z : Z), p`_i = if (Z.ltb z 0) then -(Z.to_nat z)%:R else (Z.to_nat z)%:R) /\
-    exists (z : Z), forall (x: RbaseSymbolsImpl.R), Q n x = IZR z /\ (if (Z.ltb z 0) then -(Z.to_nat z)%:R else (Z.to_nat z)%:R) = p.[n%:R].
-Proof. Admitted.
+    (Q : nat -> R -> R)
+    (hQbase : forall x : R, Q 0%nat x = 1 /\ Q 1%nat x = x)
+    (hQn : forall n : nat, ge n 2 -> forall x : R, Q n x = ((Q (n.-1) x) ^+ 2 - 1) / (Q (n.-2) x))
+    : forall n : nat, gt n 0 -> 
+        exists P : {poly R}, 
+            size P = n.+1 /\ 
+            (forall i : nat, exists c : int, P`_i = c%:~R) /\
+            Q n = (fun x : R => P.[x]).
+Proof. Admitted.

coq/src/putnam_2017_a4.v

@@ -1,15 +1,23 @@
-Require Import Nat Ensembles List Finite_sets Reals Coquelicot.Coquelicot. From mathcomp Require Import div fintype seq ssrbool.
-Theorem putnam_2017_a4 
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals derive normedtype sequences topology exp.
+From mathcomp Require Import classical_sets cardinality.
+
+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.
+
+(* Note: A seq formalization seems most natural, however it seems messy to define the complement of s in score, so we omit that requirement which follows from the rest of the goal. *)
+Variable R : realType.
+Theorem putnam_2017_a4
     (N : nat)
-    (M : nat := mul 2 N)
-    (score : nat -> 'I_11)
-    (hsurj : forall (k: 'I_11), exists (i : 'I_M), score i = k)
-    (havg : (sum_n (fun i => INR (nat_of_ord (score i))) M) / INR M = 7.4)
-    (E_bool : nat -> bool)
-    : 
-    exists (presS: nat -> Prop) (E: Ensemble nat), cardinal nat E N /\ 
-    (forall (n: nat), E n <-> (presS n /\ and (le 0 n) (le n 10))) /\
-    (forall i, E_bool i = true <-> E i) /\
-    (sum_n (fun i => if (E_bool i) then INR (nat_of_ord (score i)) else 0) N) / INR N = 7.4 /\
-    (sum_n (fun i => if E_bool i then 0 else INR (nat_of_ord (score i))) N) / INR N = 7.4.
-Proof. Admitted.
+    (score : seq 'I_11)
+    (hscore : size score = N.*2)
+    (hsurj : forall k : 'I_11, has (fun a => a == k) score)
+    (avg_fun : seq 'I_11 -> R := fun s => (\sum_(i <- s) i%:R) / (size s)%:R)
+    (havg : avg_fun score = 74/10)
+    : exists s : seq 'I_11, subseq s score /\ size s = N /\ avg_fun s = 74/10.
+Proof. Admitted.

coq/src/putnam_2018_a3.v

@@ -1,8 +1,16 @@
-Require Import Reals List Rtrigo_def Coquelicot.Derive.
-Open Scope R.
+From mathcomp Require Import all_algebra all_ssreflect.
+From mathcomp Require Import reals trigo.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+
+Variable R : realType.
 Definition putnam_2018_a3_solution : R := 480/49.
 Theorem putnam_2018_a3
-    (val : list R -> R := fun X => fold_right Rmult 1 (map (fun x => cos (INR 3 * x)) X))
-    : (exists (X : list R), length X = 10%nat /\ putnam_2018_a3_solution = val X) /\
-    (forall (X : list R), length X = 10%nat /\ putnam_2018_a3_solution >= val X).
-Proof. Admitted.
+    (cos_sum : R -> seq R -> R := fun k s => \prod_(x <- s) cos (k * x))
+    : (exists (s : seq R), size s = 10%nat /\ cos_sum 1 s = 0 /\ putnam_2018_a3_solution = cos_sum 3 s) /\
+    (forall (s : seq R), size s = 10%nat -> cos_sum 1 s = 0 -> putnam_2018_a3_solution >= cos_sum 3 s).
+Proof. Admitted.