search

math-comp / mczify

Micromega tactics for Mathematical Components
23 stars 8 forks source link

Add the `ssrZ` library #26

Closed pi8027 closed 3 years ago

pi8027 commented 3 years ago

that provides

Another point of this PR is that it will allow us to remove some code from Algebra Tactics.

Close #20

pi8027 commented 3 years ago

I think that some others have their own MathComp style libraries to reason about Z, and it would be nice to standardize such the library at some point. Any opinion? CC: @affeldt-aist @CohenCyril

affeldt-aist commented 3 years ago

I was wondering the same question. We have been considering isolating the ssrR.v and ssrZ.v files from infotheo following the request of a user, see https://github.com/affeldt-aist/monae/issues/56 They are two files that provide a renaming of the lemmas of the standard library a la MathComp but they are a bit ad hoc.

pi8027 commented 3 years ago

@affeldt-aist Could you remind me why infotheo had to use Z rather than int? Is there something to do (e.g., getting rid of Z) on this point?

affeldt-aist commented 3 years ago

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 we now plan to limit the use of Z in monae (which depends on infotheo) and think of getting rid of R and Z in infotheo because soon there will be enough material in mathcomp-analysis to make this possible

pi8027 commented 3 years ago

Good! I hope we will limit the use of Z to the case we need efficient computation on integers.

affeldt-aist commented 3 years ago

Good! I hope we will limit the use of Z to the case we need efficient computation on integers.

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

pi8027 commented 3 years ago

Anyway, I'm merging this PR now. I hope we will continue to discuss standardizing the ssrZ library.