aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers
AgeCommit message (Collapse)Author
2021-04-12[zify] More aggressive application of saturation rulesBESSON Frederic
The role of the `zify_saturate` tactic is to augment the goal with positivity constraints. The premisses were previously obtained from the context. If they are not present, we instantiate the saturation lemma anyway. Also, - Remove saturation rules for Z.mul, the reasoning is performed by lia/nia - Run zify_saturate after zify_to_euclidean_division_equations - Better lemma for Z.power - Ensure that lemma are generated once Co-authored-by: Andrej Dudenhefner <mrhaandi> Closes #12184, #11656
2021-02-26Signed primitive integersAna
Signed primitive integers defined on top of the existing unsigned ones with two's complement. The module Sint63 includes the theory of signed primitive integers that differs from the unsigned case. Additions to the kernel: les (signed <=), lts (signed <), compares (signed compare), divs (signed division), rems (signed remainder), asr (arithmetic shift right) (The s suffix is not used when importing the Sint63 module.) The printing and parsing of primitive ints was updated and the int63_syntax_plugin was removed (we use Number Notation instead). A primitive int is parsed / printed as unsigned or signed depending on the scope. In the default (Set Printing All) case, it is printed in hexadecimal.
2021-01-20Use cbn instead of simpl in a proof of HexadecimalNat.Pierre-Marie Pédrot
This reduces the tactic invocation time from 10s to 0.25s on my machine. I was growing tired of having to wait for that file while compiling the stdlib.
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2021-01-18Fix #13579 (hnf on primitives raises an anomaly)Pierre Roux
Also works for simpl.
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
(use "with ... at ..." instead)
2020-12-15Modify Numbers/Cyclic/Int63/Int63.v to compile with -mangle-namesJasper Hugunin
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
Ack-by: SkySkimmer Ack-by: ppedrot Reviewed-by: vbgl
2020-12-02Put all Int63 primitives in a separate filePierre Roux
Following a request from Pierre-Marie Pédrot in #13258
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
By default Coq stdlib warnings raise an error, so this is really required.
2020-11-09Merge PR #13173: Lint stdlib with -mangle-names #4coqbot-app[bot]
Reviewed-by: anton-trunov
2020-11-05[numeral notation] Prove RPierre Roux
2020-11-05[numeral notation] Specify RPierre Roux
2020-11-05[numeral notation] Prove QPierre Roux
2020-11-05[numeral notation] Specify QPierre Roux
2020-11-05[numeral notation] QPierre Roux
Previously rationals were all parsed as a pair numerator, denominator. This means 1.02 and 102e-2 were both parsed as 102 # 100 and could not be tell apart when printing. So the printer had to choose between two representations : without exponent or without decimal dot. The choice was made heuristically toward a most compact representation. Now, decimal dot is still parsed as a power of ten denominator but exponents are parsed as a product or division by Z.pow_pos. For instance, 1.02 is parsed as 102 # 100 whereas 102e-2 is parsed as (102 # 1) / (Z.pow_pos 10 2 # 1). 1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1 = (102 # 100) * (10 # 1) = 1020 # 100 and 10.2 = 102 # 10 no longer are. A nice side effect is that exponents can no longer blow up during parsing. Previously 1e1_000_000 literally produced a numerator with a million digits, now it just yields (1 # 1) * (Z.pow_pos 10 1_000_000 # 1).
2020-11-05[numeral notation] Remove proofs for QPierre Roux
Just to get a cleaner log, this will be proved again in a few commits.
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-08Modify Numbers/Integer/Abstract/ZBits.v to compile with -mangle-namesJasper Hugunin
As before, add a `bitwise as` tactic notation.
2020-10-08Modify Numbers/Integer/Abstract/ZLcm.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZGcd.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZDivFloor.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZDivTrunc.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZPow.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZParity.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZSgnAbs.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZMaxMin.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZMulOrder.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZAddOrder.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZAdd.v to compile with -mangle-namesJasper Hugunin
All that really needed to be done was add an explicit intro before nzinduct, but all the issues in this file could be fixed by moving n m p before the colon, and I couldn't stop my self.
2020-09-16Modify Numbers/Natural/Abstract/NBits.v to compile with -mangle-namesJasper Hugunin
The bitwise tactic was performing `intros ?m`, and the name m got used later in many proofs. I defined a tactic notation `bitwise as m` to be able to provide the name for `m` explicitly. I did not make the notation local, because it seems like it would be useful for any clients using `bitwise` who want to avoid generated names. I have relatively little experience with writing Ltac and tactic notations, so if my solution can be improved, please show me how.
2020-09-16Modify Numbers/Natural/Abstract/NLcm.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NGcd.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NDiv.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NPow.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NParity.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NMaxMin.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NSub.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NAddOrder.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NOrder.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NAdd.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NBase.v to compile with -mangle-namesJasper Hugunin
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-08-25Modify Numbers/NatInt/NZGcd.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZDiv.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZLog.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZSqrt.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZPow.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZParity.v to compile with -mangle-namesJasper Hugunin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:25:13 +0000