coq/theories/Numbers, branch master The formal proof system [zify] More aggressive application of saturation rules 2021-04-12T20:03:30+00:00 BESSON Frederic 2021-03-31T20:16:50+00:00 8193ca191cc435c108a4842ae38a11d74c7c20a5 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 
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
Signed primitive integers 2021-02-26T13:32:41+00:00 Ana 2020-12-01T08:52:12+00:00 4302a75d82b9ac983cd89dd01c742c36777d921b 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. 
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.
Use cbn instead of simpl in a proof of HexadecimalNat. 2021-01-20T17:21:23+00:00 Pierre-Marie Pédrot 2021-01-20T17:21:23+00:00 d995de51f725729b5da4fbe45823b1110627c785 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. 
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.
Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly) 2021-01-19T12:45:27+00:00 Pierre-Marie Pédrot 2021-01-19T12:45:27+00:00 071c50e9c2755e93766e5fb047b0a9065934e8fe Ack-by: SkySkimmer Reviewed-by: ppedrot 
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Support locality attributes for Hint Rewrite (including export) 2021-01-18T12:08:17+00:00 Gaëtan Gilbert 2021-01-07T12:55:23+00:00 4419a101a4f5a108be90cf4e420f0b6961e6caac We deprecate unspecified locality as was done for Hint. Close #13724 
We deprecate unspecified locality as was done for Hint.

Close #13724
Fix #13579 (hnf on primitives raises an anomaly) 2021-01-18T11:09:11+00:00 Pierre Roux 2020-12-31T17:08:29+00:00 f724ed1e270eb48060a510ff99219227c342ad6c Also works for simpl. 
Also works for simpl.
Deprecate "at ... with ..." in change tactic 2021-01-03T06:34:15+00:00 Jim Fehrle 2020-12-30T20:39:53+00:00 46c28054eb404175e5ba9485c3b5efbfe1b81619 (use "with ... at ..." instead) 
(use "with ... at ..." instead)
Modify Numbers/Cyclic/Int63/Int63.v to compile with -mangle-names 2020-12-16T04:45:01+00:00 Jasper Hugunin 2020-12-16T04:45:01+00:00 0f8d5745a3edd428aa5677880b5dcc5077f5b91b 






Merge PR #13275: Put all Int63 primitives in a separate file
2020-12-02T15:57:04+00:00

Vincent Laporte

2020-12-02T15:57:04+00:00

11730fa0ed2cb10da1ffc00f4f1140572134937e

Ack-by: SkySkimmer
Ack-by: ppedrot
Reviewed-by: vbgl





Ack-by: SkySkimmer
Ack-by: ppedrot
Reviewed-by: vbgl







Put all Int63 primitives in a separate file
2020-12-02T08:26:53+00:00

Pierre Roux

2020-10-26T13:43:05+00:00

853b838681db635f51fc3c7ba3dfe26bc6712d72

Following a request from Pierre-Marie Pédrot in #13258





Following a request from Pierre-Marie Pédrot in #13258