I would like to use the LeftCancellation instance for (N, *), which is given here. Unfortunately, I encounter the indicated error when trying the following proof:

  Context `{Naturals N}.
  Lemma multiplication_increases : forall x y : N, 1 ≤ x -> 1 ≤ y -> y ≤ x * y.
    intros x y one_leq_x one_geq_x.

    assert (y_neq_0 : y ≠ 0) by (apply nat_ne_0_ge_1; assumption).
    assert (y_neq_0_instance : PropHolds (y ≠ 0)) by (unfold PropHolds; assumption).
      
    rewrite commutativity.
    setoid_replace y with (y * 1) at 1 by (now rewrite right_identity).

    rewrite (left_cancellation (.*.) y).
    (* Error: build_signature: no constraint can apply on a dependent argument *)
  Qed.

I've found just a few things on some mailing lists about this error, but nothing that really explains it in detail. Has anyone gotten this LeftCancellation lemma working before?

The current release 8.11.0, is not compatible with Coq 8.12. Can we have a new release which supports 8.12?

This would also be the first MIT-licensed release (and could presumably end up in the Coq Platform).

I am working on building automation for simplifying algebraic expressions in different structures using reflection. I have a working simplifier for group expressions, and am planning to add a sorting step to group terms in abelian groups. Just as a matter of exploration, I may also want to implement ring and field tactics as well (even though the standard library tactics work just fine), and it would also be worth thinking about simplifying module, vector space, and algebra expressions automatically.

A lot of the implementation is boilerplate: the reified expression type and the denotation projections are boring. The only interesting part is the function that defines the simplification (and the proof of correctness). It makes me wonder whether there is a way to use the universal algebra facilities to do reification for different structures generically. However, I'm not familiar enough with the UA portion of the library (or experienced enough building automation) to tell whether this approach is likely to be fruitful.

I'll probably keep exploring this idea but I wanted to get your thoughts before diving down a rabbit hole.

This can be done as in the
https://github.com/HoTT/HoTT

@Zimmi48 , does the coq-community has standard template for this?
It makes sense to role out this tools uniformly

Currently the master branch of math-classes is compatible with Coq 8.6-8.10 + Coq master but the latest release is only compatible with Coq 8.6-8.9. It would be good to tag a new version (and publish it in opam) so that we can start testing corn with Coq 8.10.

Probably best to merge #73 first though.

I'm interested in working with ordered rings with decidable equality (in particular, I would like to show that the field of fractions of an ordered ring is also ordered in the natural way, and that an ordered commutative ring is an integral domain).

As noted in the comments of interfaces/orders.v, the deeply nested class hierarchy for orders is difficult to work with. The comment says "we will, later on, provide means to go back and forth between the usual classical notions and these constructive notions." but I can't tell whether this connection has been done or how to use it if it has.

Apologies if this is an inappropriate place to ask.

I am getting a lot of warnings like these:

[notation-overridden,parsing]
Warning: Notation _ ≠ _ was already used in scope type_scope.
[notation-overridden,parsing]

If there is a way to avoid these, short of totally disabling notation overriding warnings globally?

Dear math-classes Team,

@VincentSe requested here (coq/platform#31) and @palmskog requested here (coq/platform#14) to include your development into the Coq Platform, which is the standard user facing distribution of Coq.

Coq Platform has a "full" and "extended" level. Inclusion in the "full" level requires an explicit statement by the maintainers, that they agree to the charter of the Coq Platform and intend to publish compatible releases for each release of Coq in a reasonable time frame. For the "extended" level the rules are more relaxed. For developments in the "full" level, users should be able to rely on that the package is maintained, so that they can base their own development on it without a large risk that they have to factor it out again later cause of maintenance issues.

Can you please comment in the Coq Platform issues mentioned above if you do want your package included in the Coq Platform in agreement to the Coq Platform charter, and if so which level you would prefer?

Best regards,

Michael

A clean checkout of math-classes fails to build because two files seem to mistakenly import MathClasses.theory.Streams instead of Coq.Lists.Streams.

The tail end of the build fails with:

Warning: in file ./interfaces/canonical_names.v, library MathClasses.theory.Streams is required and has not been found in the loadpath!
COQC interfaces/canonical_names.v
File "./interfaces/canonical_names.v", line 2, characters 0-34:
Warning: Option Automatic Introduction is deprecated
[deprecated-option,deprecated]
File "./interfaces/canonical_names.v", line 3, characters 0-38:
Warning: Option Automatic Coercions Import is deprecated
[deprecated-option,deprecated]
File "./interfaces/canonical_names.v", line 5, characters 15-41:
Error: Unable to locate library MathClasses.theory.Streams.

I was able to get past this by changing the imports of interfaces/canonical_names.v and theory/streams.v.

One needs the additional axioms, see #15.

   ; in_pos_def1    :> ∀ v, PropHolds (0 ≤ ⟨v,v⟩)
   ; in_pos_def2    :> ∀ v, 0 = ⟨v,v⟩ <-> v = mon_unit
   ; inprod_proper :> Proper ((=) ==> (=) ==> (=)) (⟨⟩)

Please add support for Coq-8.13. The current OPAM version supports up to 8.12.

I have pinned coq-8.5.3 and attempt to install math-classes:

max1 ~$ opam install coq-math-classes
The following actions will be performed:
  ∗  install coq-math-classes 1.0.6

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq-released] https://coq.inria.fr/opam/released/archives/coq-math-classes.1.0.6+opam.tar.gz downloaded

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[ERROR] The compilation of coq-math-classes failed at "make -j4".
Processing  1/1: [coq-math-classes: rm]
#=== ERROR while installing coq-math-classes.1.0.6 ============================#
# opam-version 1.2.2
# os           linux
# command      make -j4
# path         /home/lord/.opam/4.04.0/build/coq-math-classes.1.0.6
# compiler     4.04.0
# exit-code    2
# env-file     /home/lord/.opam/4.04.0/build/coq-math-classes.1.0.6/coq-math-classes-24645-c61e7b.env
# stdout-file  /home/lord/.opam/4.04.0/build/coq-math-classes.1.0.6/coq-math-classes-24645-c61e7b.out
# stderr-file  /home/lord/.opam/4.04.0/build/coq-math-classes.1.0.6/coq-math-classes-24645-c61e7b.err
### stdout ###
# [...]
# "coqc"  -q  -R "." MathClasses   categories/empty.v
# "coqc"  -q  -R "." MathClasses   theory/categories.v
# "coqc"  -q  -R "." MathClasses   interfaces/universal_algebra.v
# "coqc"  -q  -R "." MathClasses   theory/strong_setoids.v
# "coqc"  -q  -R "." MathClasses   theory/ua_homomorphisms.v
# "coqc"  -q  -R "." MathClasses   theory/ua_mapped_operations.v
# "coqc"  -q  -R "." MathClasses   theory/ua_packed.v
# "coqc"  -q  -R "." MathClasses   theory/ua_term_monad.v
# "coqc"  -q  -R "." MathClasses   categories/dual.v
# "coqc"  -q  -R "." MathClasses   categories/functors.v
### stderr ###
# File "./categories/dual.v", line 42, characters 10-11:
# Syntax error: [tactic:hints_path] expected after '[' (in [vernac:command]).
# make: *** [categories/dual.vo] Error 1
# make: *** Waiting for unfinished jobs....



=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
  ∗  install coq-math-classes 1.0.6
No changes have been performed

The version 1.0.6 is marked as compatible with coq>=8.5 while it is only compatible with 8.6. Version 1.0.5 installs OK.

After importing minmax, typeclass instance databse printing is broken:

Require Import MathClasses.orders.minmax.
Print HintDb typeclass_instances.

Anomaly: index to an anonymous variable. Please report at http://coq.inria.fr/bugs/.

The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021.
The corresponding Coq Platform release 2021.11 should be released before November 30, 2021.
It can be delayed in case of difficulties until January 31, 2022, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.14+rc1.

Coq Platform CI is currently testing opam package coq-math-classes.8.13.0~flex
from platform patch repository https://github.com/coq/platform/tree/main/opam/opam-coq-archive/extra-dev/packages/coq-math-classes/coq-math-classes.8.13.0~flex/opam.

Note: The ~flex extension to the opam version means that we had to patch version restrictions in the opam package and possibly the make file to accept the new version of Coq, but no other changes were required.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2021.11, please inform us as soon as possible and before November 15, 2021!

The working branch of Coq Platform, which already supports Coq version 8.14+rc1, can be found here https://github.com/coq/platform/tree/main.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#139

I just tried to compile version 8.18.0 against Coq 8.19, and it didn't work because of various changes ; I think theory/groups.v needs:

-    (try bottomup (choice (hints group_cancellation) <- associativity)).
+    (try bottomup (choice (hints group_cancellation) (<- associativity))).

because of the new grammar for rewrite_strat, but the error:

File "./theory/groups.v", line 42, characters 2-73:
Error: Cannot find a relation to rewrite.

still eludes me.

I'm trying to write a proof involving an inequality between rational numbers, and I'd love to be able to destruct (decide (x ≤ 0)). However, when I attempt that, I get the following error:

Unable to satisfy the following constraints:
In environment:
R : Type
e : Equiv R
plus0 : Plus R
mult0 : Mult R
zero0 : Zero R
one0 : One R
neg : Negate R
recip0 : DecRecip R
U : RationalsToFrac R
H : Rationals R
x, y : R → R
k_Ω : R
k_Ω_neq_0 : k_Ω ≠ 0
n0_Ω : R
HΩ : ∀ n : R, n0_Ω ≤ n → k_Ω * y n ≤ x n
n : R
n_geq_n0_Ω : n0_Ω ≤ n

?Le : "Le R"
?Zero : "Zero R"
?Decision : "Decision (k_Ω ≤ 0)"

Obviously, the Le and Zero errors are red herrings, but I can't actually seem to find a decision procedure for Rationals, other than on actual instances.

For instance = and +. This causes a ton of conflict, and has caused me to write stuff like this:

Require Import MathClasses.interfaces.canonical_names.
(* math-classes uses (=) to denote equivalence, but we will use it for equality *)
Infix "=" := eq : type_scope.
Notation "(=)" := eq (only parsing) : mc_scope.
Notation "( x =)" := (eq x) (only parsing) : mc_scope.
Notation "(= x )" := (λ y, eq y x) (only parsing) : mc_scope.

Could we perhaps separate this into two files, one that exports stuff compatible with standard notation, and one that doesn't?

The Coq team released Coq 8.19.0 on January 24th, 2024.
The corresponding Coq Platform release 2024.01 should be released before April 30th, 2024.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.

This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (8.18.0) does not work with Coq 8.19.0.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.

Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit f9712ba on repository https://github.com/coq-community/math-classes - which likely means that this commit does work in Coq CI.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.19, preferably before March 31st, 2024?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.

In case the tag and opam package are available before March 31st, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.19.0.

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.19~2024.01+beta1 which already supports Coq version 8.19.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

Please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#405

The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an exception.

This issue is to inform you that to our (possibly a few days old) best knoweldege the latest released version of your project (8.13.0) does not work with Coq 8.15.0.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.

Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit 5da1f41 on repository https://github.com/coq-community/math-classes - which likely means that this commit does work in Coq CI.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.15, preferably before February 14, 2022?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.

In case the tag and opam package are available before January 25, 2022, it will be included in an early Coq Platform beta release of the for Coq 8.15.0.

The working branch of Coq Platform, which already supports Coq version 8.15.0, can be found here https://github.com/coq/platform/tree/main.

Please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#193

I was surprised when unfolding rationals_le to see that it specifies that le x y if there is a fraction p/q made of nats such that y=x+p/q:

Instance rationals_le `{Rationals Q} : Le Q | 10 := λ x y,
  ∃ num, ∃ den, y = x + naturals_to_semiring nat Q num / naturals_to_semiring nat Q den.

Why not use any type that is an instance of Naturals?

The Coq team released Coq 8.18.0 on September 7th, 2023.
The corresponding Coq Platform release 2023.10 should be released before November 30th, 2023.
It can be delayed in case of difficulties until January 15th, 2023, but this should be an exception.

This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (8.17.0) does not work with Coq 8.18.0.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.

Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit 7a57556 on repository https://github.com/coq-community/math-classes - which likely means that this commit does work in Coq CI.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.18, preferably before October 31st, 2023?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.

In case the tag and opam package are available before October 31st, 2023, it will be included in an early Coq Platform beta release of the for Coq 8.18.0.

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.18+beta1 which already supports Coq version 8.18.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

Please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#372

This project should be able to compile with -w "+compatibility-notation" to prepare for the Coq 8.9 release. See also coq/coq#8383.

I just added math-classes to Coq Platform (sorry for the long delay). In Coq Platform we have a so called "smoke test kit", which runs one or two example files from each package in order to test if the package has been properly installed. The example should test as much as possible, but shouldn't run longer than a few seconds (<10). Can you please suggest one or two files for this purpose?

Preferably the files should run with math-classes installed via opam without patching require statements and without -Q or -R options.

Even after repairing the Stream dependencies (see: this issue), make fails with:

COQC implementations/ZType_integers.v
File "./implementations/ZType_integers.v", line 4, characters 2-23:
Error:
Cannot find a physical path bound to logical path matching suffix
Bignums.SpecViaZ.

There is an undocumented dependency on the BigNums package. After building and installing it, math-classes does compile.

The Coq team released Coq 8.16+rc1 on June 01, 2022.
The corresponding Coq Platform release 2022.09 should be released before September 15, 2022.
It can be delayed in case of difficulties until October 15, 2022, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.16+rc1.

Coq Platform CI is currently testing opam package coq-math-classes.8.15.0
from platform patch repository https://github.com/coq/platform/tree/main/opam/opam-coq-archive/released/packages/coq-math-classes/coq-math-classes.8.15.0/opam. This means we had to weaken some version restrictions in the opam package, but no other changes were required.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2022.09, please inform us as soon as possible and before August 31, 2022!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.16+rc1~2022.09~preview1 which already supports Coq version 8.16+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#274

This option has been marked as deprecated for some time now, I'd lilke to remove it from Coq (see coq/coq#8094 for context).

Could math-classes be adapted to not use this option?

The Coq team released Coq 8.17+rc1 on December 29th, 2022 and plans to release Coq 8.17.0 around March 7th, 2023.
The corresponding Coq Platform release 2023.03 should be released before April 14th, 2023.
It can be delayed in case of difficulties until June 30, 2023, but this should be an exception.

This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (8.15.0) does not work with Coq 8.17+rc1.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.

Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit 754ddc7 on repository https://github.com/coq-community/math-classes - which likely means that this commit does work in Coq CI.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.17, preferably before March 21st, 2023?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.

In case the tag and opam package are available before March 21st, 2023, it will be included in an early Coq Platform beta release of the for Coq 8.17+rc1.

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.17~2023.03+preview1 which already supports Coq version 8.17+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

Please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#335

The current OPAM package does not support Coq-8.11. Please consider supporting 8.11
From OPAM package:

depends:      "ocaml" "coq" {(>= "8.6" & < "8.11~")} "coq-bignums"

I think this is a very important project in coq-community, but with one big drawback, which is its ad-hoc public domain dedication in lieu of a widely recognized license. In some jurisdictions, public domain dedications are not possible, so the international legal status of the project is unclear.

This issue has been raised before by @Zimmi48, who advocated a the SPDX-listed CC-0 or Unlicense licenses. I believe the Unlicense is to be preferred since this project has code and not just documentation.

@spitters as the maintainer of the project, how would you view a pull request to change the license to the Unlicense?

The tactic form cofix. is deprecated as it depends on the name of the current lemma.

See coq/coq#7196.

The backwards compatible fix is to use cofix name_of_the_fixpoint.

Currently Coq v8.6 is not supported. I see v8.6 branch, last touched by @mattam82 in October. I tried to compile it, and it hangs on compiling theory/adjunctions.v.