MathComp Analysis and idiomatic Coq formalizations

[palmskog]

I've looked through several of the Coq formalizations, and one problem I see is the mixing of modules and idioms from different overlapping libraries, such as Coq's Stdlib, Coquelicot, and MathComp Analysis. It's likely that nonidiomatic use of libraries will make it difficult for both humans and AI to solve a problem.

The best solution would likely be to focus on formalizing as many problems as possible using MathComp Analysis, which together with other MathComp libraries comprise a unfied Coq library of mathematics comparable to Lean's Mathlib, as described in #190. MathComp Analysis likely contains a superset of the results concerning reals in Coquelicot and Stdlib. When using MathComp, it's customary to avoid explicitly using Stdlib, e.g., one uses the MathComp type int instead of Z.

I give two examples of what I believe are idiomatic statements using MathComp Analysis. Since I nearly always use regular MathComp without reals, there is no guarantee that this is fully idiomatic, but it may still get the ideas across.

diff --git a/coq/src/putnam_1962_b5.v b/coq/src/putnam_1962_b5.v
index f1c3491..6030f23 100644
--- a/coq/src/putnam_1962_b5.v
+++ b/coq/src/putnam_1962_b5.v
@@ -1,7 +1,15 @@
-Require Import Reals Coquelicot.Coquelicot.
-Theorem putnam_1962_b5
-    (n : nat)
-    (ng1 : gt n 1)
-    : (3 * INR n + 1) / (2 * INR n + 2) < sum_n_m (fun i : nat => (INR i / INR n) ^ n) 1 n /\
-    sum_n_m (fun i : nat => (INR i / INR n) ^ n) 1 n < 2.
+From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
+From mathcomp Require Import boolp classical_sets functions.
+From mathcomp Require Import reals.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+
+Theorem putnam_1962_b5 (R : realType) (n : nat) (ng1 : gtn n 1) :
+ (3 * n%:R + 1) / (2 * n%:R + 2) < \sum_(1 <= i < n.+1) ((i%:R / n%:R)^n : R) < 2.
 Proof. Admitted.

diff --git a/coq/src/putnam_1963_b1.v b/coq/src/putnam_1963_b1.v
index 9ac0d11..f3cca65 100644
--- a/coq/src/putnam_1963_b1.v
+++ b/coq/src/putnam_1963_b1.v
@@ -1,9 +1,15 @@
-Require Import ZArith. From mathcomp Require Import fintype ssralg ssrnat ssrnum poly polydiv.
-Open Scope ring_scope.
-Definition putnam_1963_b1_solution : Z := 2.
-Theorem putnam_1963_b1
-    (R : numDomainType)
-    (ZtoR : Z -> {poly R} := fun a => if (0 <=? a)%Z then (Z.to_nat a)%:R else -(Z.to_nat (-a))%:R)
-    : (forall a : Z, ('X^2 - 'X + ZtoR a) %| ('X^13 + 'X + 90%:R) = true <-> a = putnam_1963_b1_solution).
-Proof. Admitted.
+From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
+From mathcomp Require Import boolp classical_sets functions.
+From mathcomp Require Import reals.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.

+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+
+Definition putnam_1963_b1_solution : int := 2.
+Theorem putnam_1963_b1 (R : realType) (a : int) :
+ (('X^2 - 'X + a%:~R) : {poly R}) %| ('X^13 + 'X + 90) <-> a = putnam_1963_b1_solution.
+Proof. Admitted.

[LasseBlaauwbroek]

Note that the second formalization doesn't seem quite correct to me. It deprives the contestant of determining that the set of solutions is a singleton. Should probably rather be something like this:

Definition putnam_1963_b1_solution (i : int) : Prop := i = 2.
Theorem putnam_1963_b1 (R : realType) (a : int) :
 (('X^2 - 'X + a%:~R) : {poly R}) %| ('X^13 + 'X + 90) <-> putnam_1963_b1_solution a.

[palmskog]

@LasseBlaauwbroek you're probably right, I was just aiming for a straight translation of the original Coq statement to idiomatic MathComp Analysis. Another orthogonal question is definitely whether an idiomatic Coq statement captures the mathematical English meaning (I wish those were kept more accessible outside a JSON).

[LasseBlaauwbroek]

Edit: Moved to #195 to keep concerns separate.

[GeorgeTsoukalas]

Hi Karl,

Thank you for the feedback! We are going to begin migrating the Coq formalizations to depend mostly on Mathcomp shortly. I think this way we'll get the formalizations to be more idiomatic (maybe not perfect) and smooth out any kinks as we proceed. Thanks for providing some examples as well, it is a helpful starting point.

[GeorgeTsoukalas]

A set of modified formalizations from years 1979 and 1980 appears in #201. Idiomaticity-wise, what do you think? Most have been changed to rely on mathcomp. I am particularly interested in any common shortcuts that we missed which could be used in the formalizations.

[GeorgeTsoukalas]

A further set of modified formalizations from years 1973 to 1978 appears in #211. Let me know if you have any comments.

[GeorgeTsoukalas]

A further set of modified formalizations from years 1969 to 1972 appears in #214. Let me know if you have any comments.