Add the ssrZ library
#26
Conversation
pi8027
force-pushed
the
ssrZ
branch
2 times, most recently
from
c871bf8
to
0f72ae0
Compare
|
I think that some others have their own MathComp style libraries to reason about |
|
I was wondering the same question. |
that provides Z <-> int conversion and some structure instances for Z
pi8027
force-pushed
the
ssrZ
branch
2 times, most recently
from
0baa47a
to
601c091
Compare
|
@affeldt-aist Could you remind me why infotheo had to use |
|
infotheo has been using R from the standard library and did a bit of real analysis in which it uses flooring and ceiling functions which led to the use of Z |
|
Good! I hope we will limit the use of |
I've issued myself to do just that, it is only a matter of finding the time, I'll try to do it by mid-october and report to you by then |
| Definition Z_of_int (n : int) : Z := | ||
| match n with | ||
| | Posz n => Z.of_nat n | ||
| | Negz n' => Z.opp (Z.of_nat (n' + 1)) | ||
| end. |
There was a problem hiding this comment.
It would be nice to redefine this with Z_of_int n := n%:~R (see Lemma Z_of_intE below). But, it requires the ringType instance of Z, and Z_of_int and int_of_Z are required to define the choiceType and countType instances of Z. There is some sort of circular dependency here.
theories/ssrZ.v
Outdated
| Canonical Z_normedZmodType := NormedZmodType Z Z Mixin. | ||
| Canonical Z_realDomainType := [realDomainType of Z]. | ||
|
|
||
| Lemma Z_of_intE (n : int) : Z_of_int n = (n%:~R)%R. |
|
Anyway, I'm merging this PR now. I hope we will continue to discuss standardizing the |
that provides
ZandZ_of_int : int -> Zandint_of_Z : Z -> intring morphisms.Another point of this PR is that it will allow us to remove some code from Algebra Tactics.
Close #20