coq-community / corn Goto Github PK

After upgrading to Coq 8.4pl5 I am getting a compilation error:

coqc -R . CoRN -R math-classes/src MathClasses -q math-classes/src/theory/adjunctions.v
File "/Volumes/CORN/corn/math-classes/src/theory/adjunctions.v", line 192, characters 32-38:
Error: Illegal application (Non-functional construction):
The expression "φ c" of type "?1062 ⟶ G ?1063"
cannot be applied to the term
"d" : "?1057"

In our discussion on #30, we decided that sm should be proper with respect to equiv. Does that same reasoning hold for inprod? My intuition tells me it should, as I need that property to prove the following lemma about orthogonal projections:

Section orthogonal_projection.
  Context `{InnerProductSpace K V}.

  Definition proj (u v : V) : V := (⟨ u , v ⟩ / (⟨ u , u ⟩)) · u.

  Lemma lemma1 : forall (c : K) (u1 u2 v : V), u1 = c · u2 -> proj u1 v = proj u2 v.

Adding the following lines to vectorspace.v allows me to rewrite using the equality hypothesis:

Notation "(⟨⟩)" := (inprod) (only parsing) : mc_scope.
[...]
Class InnerProductSpace (K V : Type)
[...]
   ; inprod_proper  :> Proper ((=) ==> (=) ==> (=)) (⟨⟩)

I'm happy to make a pull request if this seems appropriate!

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.16.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 d4e6db7 on repository https://github.com/coq-community/corn - 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

Is there a recommended reading order for the content in this library?
The order in automatically the generated toc.html seems to be violating dependencies between modules.
There used to be an online documentation webpage at http://corn.cs.ru.nl/ which seemed present the material in a sensible order.
It would be great if something like the software foundations book was developed from the generated coqdoc.

Hi there,

I'm trying to do some basic linear algebra proofs. I was using the coq algebra contrib, but discovered math-classes and decided to give it a try!

One thing that's stopping me right now is that the algebra distribution includes some very basic proofs about immediate consequences of the structure laws that I'm not sure how to begin replicating with math-classes. For instance, algebra includes the following lemma:

Lemma MODULE_absorbant_l :
 forall x : Mod, Equal (module_mult (monoid_unit R) x) (monoid_unit Mod).
intros x; try assumption.
apply GROUP_reg_left with (module_mult (monoid_unit R) x); auto with algebra.
apply
 Trans with (module_mult (sgroup_law R (monoid_unit R) (monoid_unit R)) x);
 auto with algebra.
apply Trans with (module_mult (monoid_unit R) x); auto with algebra.
Qed.

Which I believe corresponds to the following statement in math-classes:

  Lemma module_absorbant_l `{Module R M} : forall x : M, sm Rzero x = Munit.

However, I'm not sure how to go about providing a proof for this statement (especially without an auto with algebra analogue). Can you give me some pointers on proving such basic theorems?

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-corn.8.13.0
from official repository https://coq.inria.fr/opam/released/packages/coq-corn/coq-corn.8.13.0/opam.

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

Would you all be interested in a pull request providing a .travis.yml similar to (probably the same as) my PR at math-classes?

The tactic form cofix. without a name 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. Problematic entries in CoRN:

metric2/Limit.v:330: cofix.
metric2/Limit.v:344: cofix.
metric2/Limit.v:357:  cofix.
reals/fast/CRseries.v:45: cofix.
reals/fast/CRseries.v:75: cofix.
reals/fast/CRseries.v:117: cofix.
reals/fast/CRseries.v:164: cofix.
reals/fast/CRseries.v:193: cofix.
reals/fast/CRseries.v:218: cofix.
reals/fast/CRseries.v:239: cofix.
reals/fast/CRseries.v:338: cofix.
reals/fast/CRseries.v:387: cofix.
reals/fast/CRseries.v:497: cofix.
reals/fast/CRseries.v:518: cofix.

since it was written 10 years ago ;-)

Hi guys, quick question:
I want to reference your work for a slides assignment on Coq extractions,
where can I find the formulation of the fundamental theorem of algebra?
A simple grep of your repository got me nowhere ... thanks!

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 79e7ee7 on repository https://github.com/coq-community/corn - 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

Because OS X uses a case-insensitive filesystem, I'm unable to build corn due to errors such as:

Error: The file /private/var/folders/4j/br7bdhjx4b384_snb2087gt00000gn/T/nix-build-coq-corn-8.4-318d7dd8.drv-2/git-export/math-classes/src/implementations/Bool.vo contains library
MathClasses.implementations.bool and not library
MathClasses.implementations.Bool

There are quite a few publications in the regular and grey literature related to Corn, e.g.,

• https://valentinblot.org/pro/M1_report.pdf
• https://link.springer.com/chapter/10.1007/978-3-540-27818-4_7
• https://arxiv.org/abs/0805.2438

Some are listed at the old website, but not all. Ideally, all should be listed in the README file or somewhere else in this repository (both DOIs and archived preprint URLs, when available). Authors of papers not in permanent archives should be encouraged to submit them to such archives (e.g., HAL or arXiv).

I am on Ubuntu 18.04, and I use opam 2.0.0~rc and coq 8.8.1.
This message was found in the middle of the output:

File "./stdlib_omissions/Q.v", line 51, characters 45-46:
Error:
Syntax error: [constr:operconstr level 200] expected after '(' (in [constr:operconstr]).

Makefile:656: recipe for target 'stdlib_omissions/Q.vo' failed
make[1]: *** [stdlib_omissions/Q.vo] Error 1
make[1]: *** Waiting for unfinished jobs....

I have the same error when I use a fresh opam installation.

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 d6cbe5a on repository https://github.com/coq-community/corn - 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

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.16.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 c08a041 on repository https://github.com/coq-community/corn - 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

Dear CoRN Team,

the example files, like examples/RealFaster.v require CoRN modules without qualification. This doesn't work if CoRN is installed as opam package, so users have to patch the examples in order to run them. It also makes it hard to find usable "smoke test kit" files for Coq Platform.

Best regards,

Michael

This issue is about MathClasses. But the MathClasses repo does not seem to have issues enabled.

(* This is how the Plus and Mult classes are currently defined in interfaces.canonical_names*)
Class Plus A := plus: A -> A -> A.
Class Mult A := mult: A -> A -> A.

(* The definition below typechecks. This often causes typeclass resolution
to pick a Plus instance for Mult, or vice versa, and then get all confused. *)
Definition plusAsMult (A:Type) (p:Plus A) : Mult A := p.

(* Perhaps Plus and Mult should be defined as below? *)

Class PPlus A := {pplus: A -> A -> A}.
Class MMult A := {mmult: A -> A -> A}.

(* This does not typecheck, which is good! *)
Definition pplusAsMult (A:Type) (p:PPlus A) : MMult A := p.

The file CLogic.v defines the following two notations:

Notation "{ x : A  |  P }" := (sigT (fun x : A => P):CProp)
  (at level 0, x at level 99) : type_scope.
Notation "{ x : A  |  P  |  Q }" :=
  (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) :
  type_scope.

However the Coq standard library (at least as of 8.5) has the following notations:

Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope.
Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) :
  type_scope.
Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) :
  type_scope.

The first notation clashes with CLogic's notation, the last two notations seem to express what the CLogic notation intends.

This is breaking developments that depend on CoRN, for instance the quantum computing library here: https://www.dropbox.com/sh/fhldyg1mfnxdmcl/AAAvQZz1i1mjdL5TKzwcWwyva/CoRN?dl=0

As per discussion on #31, this project now uses OPAM to install math-classes by default, rather than a git submodule. This change should be reflected in the README.

Currently MathClasses defines Ring to be a commutative ring. I propose to rename it to CommutativeRing, and introduce a Ring for non-commutative rings. Are there any objections? If no, I'll prepare a pull request.

I had to investigate a performance issue in CPoly_Newton.v and I found many Admitted instances.
This issue is just there to track this and (hopefully) prevent a release with these axioms in the opam/released archive (that requires axioms to not be there, or be documented).

While packaging corn for Debian, I had a hard time with the licensing: there's a toplevel stating GPL-2, but in some files, the story is a little different, and the number of exceptions is quite high ; here is my current copyright declaration file:

Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/

Files: *
Copyright: 1998-2022 Evgeny Makarov
	   1998-2022 Robbert Krebbers
	   1998-2022 Eelis van der Weegen
	   1998-2022 Bas Spitters
	   1998-2022 Jelle Herold
	   1998-2022 Russell O'Connor
	   1998-2022 Cezary Kaliszyk
	   1998-2022 Dan Synek
	   1998-2022 Luís Cruz-Filipe
	   1998-2022 Milad Niqui
	   1998-2022 Iris Loeb
	   1998-2022 Herman Geuvers
	   1998-2022 Randy Pollack
	   1998-2022 Freek Wiedijk
	   1998-2022 Jan Zwanenburg
	   1998-2022 Dimitri Hendriks
	   1998-2022 Henk Barendregt
	   1998-2022 Mariusz Giero
	   1998-2022 Rik van Ginneken
	   1998-2022 Dimitri Hendriks
	   1998-2022 Sébastien Hinderer
	   1998-2022 Bart Kirkels
	   1998-2022 Pierre Letouzey
	   1998-2022 Lionel Mamane
	   1998-2022 Nickolay Shmyrev
	   1998-2022 Vincent Semeria
License: GPL-2

Files: algebra/CAbGroups.v
       algebra/CAbMonoids.v
       algebra/CFields.v
       algebra/CGroups.v
       algebra/CMonoids.v
       algebra/COrdAbs.v
       algebra/COrdCauchy.v
       algebra/COrdFields.v
       algebra/COrdFields2.v
       algebra/CPoly_ApZero.v
       algebra/CPoly_Degree.v
       algebra/CPoly_NthCoeff.v
       algebra/CPolynomials.v
       algebra/CRing_Homomorphisms.v
       algebra/CRings.v
       algebra/CSemiGroups.v
       algebra/CSetoidFun.v
       algebra/CSetoidInc.v
       algebra/CSetoids.v
       algebra/CSums.v
       algebra/Cauchy_COF.v
       algebra/Expon.v
       complex/AbsCC.v
       complex/CComplex.v
       complex/Complex_Exponential.v
       complex/NRootCC.v
       coq_reals/Rreals.v
       coq_reals/Rreals_iso.v
       fta/CC_Props.v
       fta/CPoly_Contin1.v
       fta/CPoly_Rev.v
       fta/CPoly_Shift.v
       fta/FTA.v
       fta/FTAreg.v
       fta/KeyLemma.v
       fta/KneserLemma.v
       fta/MainLemma.v
       ftc/COrdLemmas.v
       ftc/CalculusTheorems.v
       ftc/Composition.v
       ftc/Continuity.v
       ftc/Derivative.v
       ftc/DerivativeOps.v
       ftc/Differentiability.v
       ftc/FTC.v
       ftc/FunctSequence.v
       ftc/FunctSeries.v
       ftc/FunctSums.v
       ftc/Integral.v
       ftc/IntervalFunct.v
       ftc/MoreFunSeries.v
       ftc/MoreFunctions.v
       ftc/MoreIntegrals.v
       ftc/MoreIntervals.v
       ftc/NthDerivative.v
       ftc/PartFunEquality.v
       ftc/PartInterval.v
       ftc/Partitions.v
       ftc/RefLemma.v
       ftc/RefSepRef.v
       ftc/RefSeparated.v
       ftc/RefSeparating.v
       ftc/Rolle.v
       ftc/StrongIVT.v
       ftc/Taylor.v
       ftc/TaylorLemma.v
       ftc/WeakIVT.v
       logic/CLogic.v
       logic/CornBasics.v
       logic/PropDecid.v
       metrics/CMetricSpaces.v
       metrics/CPMSTheory.v
       metrics/CPseudoMSpaces.v
       metrics/ContFunctions.v
       metrics/Equiv.v
       metrics/IR_CPMSpace.v
       metrics/LipExt.v
       metrics/Prod_Sub.v
       old/Transparent_algebra.v
       opaque/Opaque_algebra.v
       reals/Bridges_LUB.v
       reals/Bridges_iso.v
       reals/CMetricFields.v
       reals/CPoly_Contin.v
       reals/CReals.v
       reals/CReals1.v
       reals/CSumsReals.v
       reals/CauchySeq.v
       reals/Cauchy_CReals.v
       reals/Cesaro.v
       reals/IVT.v
       reals/Intervals.v
       reals/Max_AbsIR.v
       reals/NRootIR.v
       reals/OddPolyRootIR.v
       reals/PosSeq.v
       reals/Q_dense.v
       reals/Q_in_CReals.v
       reals/R_morphism.v
       reals/RealCount.v
       reals/RealFuncts.v
       reals/RealLists.v
       reals/Series.v
       reals/iso_CReals.v
       tactics/AlgReflection.v
       tactics/CornTac.v
       tactics/DiffTactics1.v
       tactics/DiffTactics2.v
       tactics/DiffTactics3.v
       tactics/FieldReflection.v
       tactics/Rational.v
       tactics/RingReflection.v
       tactics/Step.v
       tactics/csetoid_rewrite.v
       transc/ArTanH.v
       transc/Exponential.v
       transc/InvTrigonom.v
       transc/Pi.v
       transc/PowerSeries.v
       transc/RealPowers.v
       transc/SinCos.v
       transc/TaylorSeries.v
       transc/TrigMon.v
       transc/Trigonometric.v
       model/Zmod/Cmod.v
       model/Zmod/IrrCrit.v
       model/Zmod/ZBasics.v
       model/Zmod/ZDivides.v
       model/Zmod/ZGcd.v
       model/Zmod/ZMod.v
       model/Zmod/Zm.v
       model/abgroups/QSposabgroup.v
       model/abgroups/Qabgroup.v
       model/abgroups/Qposabgroup.v
       model/abgroups/Zabgroup.v
       model/fields/Qfield.v
       model/groups/QSposgroup.v
       model/groups/Qgroup.v
       model/groups/Qposgroup.v
       model/groups/Zgroup.v
       model/monoids/Nm_to_cycm.v
       model/monoids/Nm_to_freem.v
       model/monoids/Nmonoid.v
       model/monoids/Nposmonoid.v
       model/monoids/QSposmonoid.v
       model/monoids/Qmonoid.v
       model/monoids/Qposmonoid.v
       model/monoids/Zmonoid.v
       model/monoids/freem_to_Nm.v
       model/ordfields/Qordfield.v
       model/reals/Cauchy_IR.v
       model/rings/Qring.v
       model/rings/Zring.v
       model/semigroups/Npossemigroup.v
       model/semigroups/Nsemigroup.v
       model/semigroups/QSpossemigroup.v
       model/semigroups/Qpossemigroup.v
       model/semigroups/Qsemigroup.v
       model/semigroups/Zsemigroup.v
       model/setoids/Nfinsetoid.v
       model/setoids/Npossetoid.v
       model/setoids/Nsetoid.v
       model/setoids/Qpossetoid.v
       model/setoids/Qsetoid.v
       model/setoids/Zfinsetoid.v
       model/setoids/Zsetoid.v
       model/structures/Npossec.v
       model/structures/Nsec.v
       model/structures/Qpossec.v
       model/structures/Qsec.v
       model/structures/Zsec.v
Copyright: 1998-2022 Evgeny Makarov
	   1998-2022 Robbert Krebbers
	   1998-2022 Eelis van der Weegen
	   1998-2022 Bas Spitters
	   1998-2022 Jelle Herold
	   1998-2022 Russell O'Connor
	   1998-2022 Cezary Kaliszyk
	   1998-2022 Dan Synek
	   1998-2022 Luís Cruz-Filipe
	   1998-2022 Milad Niqui
	   1998-2022 Iris Loeb
	   1998-2022 Herman Geuvers
	   1998-2022 Randy Pollack
	   1998-2022 Freek Wiedijk
	   1998-2022 Jan Zwanenburg
	   1998-2022 Dimitri Hendriks
	   1998-2022 Henk Barendregt
	   1998-2022 Mariusz Giero
	   1998-2022 Rik van Ginneken
	   1998-2022 Dimitri Hendriks
	   1998-2022 Sébastien Hinderer
	   1998-2022 Bart Kirkels
	   1998-2022 Pierre Letouzey
	   1998-2022 Lionel Mamane
	   1998-2022 Nickolay Shmyrev
	   1998-2022 Vincent Semeria
License: GPL-2+

Files: reals/stdlib/CMTDirac.v
       reals/stdlib/CMTFullSets.v
       reals/stdlib/CMTIntegrableFunctions.v
       reals/stdlib/CMTIntegrableSets.v
       reals/stdlib/CMTMeasurableFunctions.v
       reals/stdlib/CMTPositivity.v
       reals/stdlib/CMTProductIntegral.v
       reals/stdlib/CMTReals.v
       reals/stdlib/CMTbase.v
       reals/stdlib/CMTcast.v
       reals/stdlib/CMTprofile.v
       reals/stdlib/ConstructiveCauchyIntegral.v
       reals/stdlib/ConstructiveDiagonal.v
       reals/stdlib/ConstructiveFastReals.v
       reals/stdlib/ConstructiveFasterReals.v
       reals/stdlib/ConstructivePartialFunctions.v
       reals/stdlib/ConstructiveUniformCont.v
       reals/stdlib/Markov.v
Copyright: 2020 Vincent Semeria
License: Expat

Files: debian/*
Copyright: 2022 Julien Puydt
License: GPL-2

License: Expat
 Permission is hereby granted, free of charge, to any person
 obtaining a copy of this software and associated documentation files
 (the "Software"), to deal in the Software without restriction,
 including without limitation the rights to use, copy, modify, merge,
 publish, distribute, sublicense, and/or sell copies of the Software,
 and to permit persons to whom the Software is furnished to do so,
 subject to the following conditions:
 .
 The above copyright notice and this permission notice shall be
 included in all copies or substantial portions of the Software.
 .
 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
 MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
 BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
 ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 SOFTWARE.

License: GPL-2
 This package is free software; you can redistribute it and/or
 modify it under the terms of the GNU General Public License
 as published by the Free Software Foundation version 2.
 .
 This package is distributed in the hope that it will be useful,
 but WITHOUT ANY WARRANTY; without even the implied warranty of
 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 General Public License for more details.
 .
 You should have received a copy of the GNU General Public License
 along with this program. If not, see <http://www.gnu.org/licenses/>.
 .
 On Debian GNU/Linux systems, the complete text of the GNU General Public
 License version 2 can be found in `/usr/share/common-licenses/GPL-2'

License: GPL-2+
 This package is free software; you can redistribute it and/or
 modify it under the terms of the GNU General Public License
 as published by the Free Software Foundation; either
 version 2 of the License or later.
 .
 This package is distributed in the hope that it will be useful,
 but WITHOUT ANY WARRANTY; without even the implied warranty of
 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 General Public License for more details.
 .
 You should have received a copy of the GNU General Public License
 along with this program. If not, see <http://www.gnu.org/licenses/>.
 .
 On Debian GNU/Linux systems, the complete text of the GNU General Public
 License version 2 can be found in `/usr/share/common-licenses/GPL-2'

I'm trying to update the .nix file for CoRN.
Is would be helpful if you could make a new release with the patch #159, because it is necessary to compile with coq 8.13.
Thanks.

I recently encountered an issue on the following lemma:

  Lemma mult_munit : forall c : R, sm c mon_unit = mon_unit.
    intro c.
    rewrite <- right_identity.
    assert (intermediate : mon_unit = c · mon_unit & - (c · mon_unit)) by
      now rewrite right_inverse.
    rewrite intermediate at 2.
    rewrite associativity.
    rewrite <- distribute_l.
    rewrite right_identity. (* evaluation would stop here *)
    apply right_inverse.
  Qed.

I found that if I changed the instance of Proper for scalar multiplication to use the dot (·) notation and the statement of the lemma to the following, this proof worked exactly as expected:

  Lemma mult_munit : forall c : R, c · mon_unit = mon_unit.

I encountered a similar error with this lemma:

(* Subspaces are specified as a constraint on a vectorspace *)
Class Subspace (K V : Type) 
   {Ke Kplus Kmult Kzero Kone Knegate Krecip} (* scalar operations *)
   {Ve Vop Vunit Vnegate}                     (* vector operations *)
   {sm : ScalarMult K V}
 :=
   { subspace_vectorspace  :>> @VectorSpace K V Ke Kplus Kmult Kzero Kone Knegate Krecip
                                            Ve Vop Vunit Vnegate sm
   ; constraint : V -> Prop
   ; closed_under_sg_op    : forall u v, constraint u -> constraint v ->
                           constraint (u & v)
   ; closed_under_sm       : forall c v, constraint v -> constraint sm c v
   (* We don't include that the zero vector is in the subspace, it follows
      from the closure under scalar multiplication.
    *)
   }.

Section Subspace_Lemmas.
  Context `{VectorSpace K V}.

  Definition zero_prop (vec : V) : Prop := vec = mon_unit.

  Instance zero_subspace : Subspace K V.
  Proof.
    split with (constraint := zero_prop); eauto; intros; unfold zero_prop in * |- *.
    { (* Closure under & *)
      rewrite H0, H1.
      now rewrite left_identity.
    }
    { (* Closure under sm *)
      rewrite H0. (* This step would fail with UNDEFINED_EVARS *)
    }
  Qed.
End Subspace_Lemmas.

But if I changed the closure condition to use the dot notation, everything proceeded just fine.

   ; closed_under_sm       : forall c v, constraint v -> constraint (c · v)

My expectation would be that the notation should be irrelevant in proofs. Is there a good reason that it is not? Is this a bug, or are my expectations not in line with typeclass functionality?

For a little more context, see my question on StackOverflow.

Earlier, I had compiled c-corn on Ubuntu and everything worked perfectly.
Today, I tried to build c-corn on windows and ran into some issues. The scons system was trying to compile a .v file before compiling its dependencies. I guess the supplied SConstruct file is not designed to work natively on Windows? If so, should the README instruct folks running Windows to use Cygwin?
Indeed, the scons problem was solved by using cygwin, i.e. installing python and scons in cygwin and then running scons in the cygwin terminal.

Also, I ran into some filename case-insensitivity issues on windows: https://coq.inria.fr/bugs/show_bug.cgi?id=2554. I fixed some of them. Even the MathClass repository needs to be fixed. I'll create a pull request as soon as I do that.

Also, coqc aborts without any error message while compiling reals/faster/ARAlternatingSum.v at the
following line:
https://github.com/c-corn/corn/blob/master/reals/faster/ARAlternatingSum.v#L209
Changing 50000 to 50 fixed this problem.

This pull request introduced a constructive real numbers interface in Coq's standard library
coq/coq#10632

It is compatible with corn's CReals interface, which opens a way to move corn's files about real numbers into Coq's standard library.

There is a problem of copyright though : corn is under the General Public License, whereas Coq is under the Lesser General Public License. Therefore we would need to change the copyright and license of all corn files that we copy inside Coq's stdlib, making them under LPGL. Also, the names of the authors would need to be removed from the source code files, to go into Coq's global CREDITS file.

There are 19 corn developper listed for the reals : Henk Barendregt, Luís Cruz-Filipe, Herman Geuvers, Mariusz Giero, Rik van Ginneken, Dimitri Hendriks, Sébastien Hinderer, Bart Kirkels, Pierre Letouzey, Iris Loeb, Lionel Mamane, Milad Niqui, Russell O’Connor, Randy Pollack, Nickolay V. Shmyrev, Bas Spitters, Dan Synek, Freek Wiedijk, Jan Zwanenburg.

Their copyright is declared to end in 2006, but still we need them to agree to such an integration.

Does anyone know how to reach them, and how to change corn's license for those files ?

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 to our (possibly a few days old) best knowledge the latest released version of your project (preview) does not work with Coq 8.16+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 e34e331 on repository https://github.com/coq-community/corn - 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.16, preferably before August 31, 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 August 17, 2022, it will be included in an early Coq Platform beta release of the for Coq 8.16+rc1.

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.

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

scons: done reading SConscript files.
scons: Building targets ...
coqc -R . CoRN -R math-classes/src MathClasses -q math-classes/src/misc/decision.v
File ".../corn/math-classes/src/misc/decision.v", line 30, characters 18-23:
Syntax error: '.' expected after [vernac:command](in [vernac_aux]).
scons: *** [math-classes/src/misc/decision.vo] Error 1
scons: building terminated because of errors.

I am compiling CORN with the git version of native-coq (github.com/maximedenes/native-coq) and scons 2.3.3.

I'm surprised that CoRN.metric2.DistanceMetricSpace.DistanceMetricSpace is never used for anything. I would have expected many metric spaces, e.g. the one on rationals (CoRN.model.metric2.Qmetric.Q_as_MetricSpace) and CR to be defined as distance metric spaces. One can always convert a distance metric space to a CoRN.metric2.Metric.MetricSpace using CoRN.metric2.DistanceMetricSpace.ballSpace, but not the other way around in general.
Am I missing something?

The lemmas in this directory should be added to the stdlib and removed from corn.
https://github.com/coq-community/corn/tree/master/stdlib_omissions

When building under Coq 8.4pl5, I'm seeing the following error about "ifb" not being found:

File "/private/var/folders/4j/br7bdhjx4b384_snb2087gt00000gn/T/nix-build-coq-corn-8.4-318d7dd8.drv-2/git-export/tactics/AlgReflection.v", line 177, characters 6-9:
Error: The reference ifb was not found in the current environment.

The Wikipedia definition of an inner product space has the following extra axiom:

0 = ⟨v,v⟩ <-> v = mon_unit 

which isn't present in the current formalism. Should we rewrite the positivity rules as follows?

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

I don't know if this is a bug in Coq or CoRN, but I get a universe inconsistency at the 2nd line (Using Coq 8.4pl3):

Require Import MathClasses.theory.finite_sets.
Require Import CoRN.algebra.CSetoidInc.

I encountered this problem when I was trying to import all CoRN files, that I can search for lemmas I need using SearchAbout/SearchPattern. Is there a workaround to search entire CoRN for lemmas? Are there some files which I can import to search a large part of CoRN/MathClasses?

As of 72696f3 Math Classes are no longer a submodule, and it looks like make is now the preferred build method. Updated build instructions would be appreciated

https://travis-ci.org/coq-community/corn/builds/406537788#L3323-L3324

Currently corn emits 1378 such warnings (computed with make -j4 3>&1- 1>&2- 2>&3- | grep compatibility-notation | wc -l). @JasonGross has prepared two scripts that should help fixing them (coq/coq#8383 (comment) and coq/coq#8383 (comment)). I'm going to test how efficient these are to get rid of compatibility-notation warnings in corn.

While trying to translate between Coquelicot and corn's complex numbers, I noticed that some of the translations were missing from Rreals_iso.v. Specifically, the translations mapping from IR to R were not present for multiplication, negation, etc... although their corresponding theorems in R_morphism.v exist already. Because the lemmas already exist, it would not be too difficult to add the proofs to Rreals_iso.v and I would be happy to make a pull request.