Add mathcomp package for Coq

[Bubbler-4]

Please complete the following information about the package:

• Name: mathcomp
• Language Name: Coq
• Website: https://github.com/math-comp/math-comp
• Install command: opam install coq-mathcomp-ssreflect

Following are optional, but will help us consider adding:

• Why is this useful?

The Mathematical Components Library is an extensive and coherent repository of formalized mathematical theories. It is based on the Coq proof assistant, powered with the Coq/SSReflect language.

These formal theories cover a wide spectrum of topics, ranging from the formal theory of general purpose data structures like lists, prime numbers or finite graphs, to advanced topics in algebra. The repository includes the foundation of formal theories used in a formal proof of the Four Colour Theorem (Appel - Haken, 1976) and a mechanization of the Odd Order Theorem (Feit - Thompson, 1963), a landmark result of finite group theory, which utilizes the library extensively.

It is a library designed for mathematical theory developments, mainly number theory (on natural numbers), finite sets and graphs. Especially, the number theory part includes many facts about prime numbers and GCD. It also comes with notations and facts for "big operators" e.g. sum and product.

• Example Code: (from chapter 0 of the MathComp book, jscoq)

From mathcomp Require Import all_ssreflect.

Example gauss n :
  \sum_(0 <= i < n.+1) i = n * n.+1 %/ 2.
Proof.
elim: n =>[|n IHn]; first by apply: big_nat1.
rewrite big_nat_recr //= IHn addnC -divnMDl //. 
by rewrite mulnS muln1 -addnA -mulSn -mulnS.
Qed.

---

:+1: reactions might help.

[kazk]

The example code outputs the following to stderr:

File "./Solution.v", line 1, characters 0-43:
Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "_ <= _ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "_ < _ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "_ <= _ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "_ < _ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
File "./Solution.v", line 1, characters 0-43:
Warning: Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]

Using coq-mathcomp-ssreflect.1.9.0. Is this expected? I don't think this will affect pass/fail, but these will be shown with the test results.

[monadius]

I also get the same warnings when I load all_ssreflect. It is possible to temporarily turn off these warnings with the following commands:

Set Warnings "-parsing".
From mathcomp Require Import all_ssreflect.
Set Warnings "parsing".

[kazk]

Deployed