coq/theories/Numbers/Cyclic/Int63, 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.
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.
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







Explicitly annotate all hint declarations of the standard library.
2020-11-16T11:28:27+00:00

Pierre-Marie Pédrot

2020-11-14T16:55:07+00:00

68cd077344ce37db1a601079dbc4fdcae6c8d41f

By default Coq stdlib warnings raise an error, so this is really required.





By default Coq stdlib warnings raise an error, so this is really required.







Bring Int63 notations into line with stdlib
2020-08-09T23:23:13+00:00

Jason Gross

2020-06-07T20:20:08+00:00

d39730a03b03bdbb23f0ad042a2bb87055d91d00

We also put them in a module, so users can `Require Int63. Import
Int63.Int63Notations` without needing to unqualify the primitives.

In particular, we change
- `a \% m` into `a mod m` to correspond with the notation in ZArith
- `m == n` into `m =? n` to correspond with the eqb notations elsewhere
- `m < n` into `m <? n` to correspond with the ltb notations elsewhere
- `m <= n` into `m <=? n` to correspond with the leb notations elsewhere
- `m ≤ n` into `m ≤? n` for consistency with the non-unicode notation

The old notations are still accessible as deprecated notations.

Fixes #12454





We also put them in a module, so users can `Require Int63. Import
Int63.Int63Notations` without needing to unqualify the primitives.

In particular, we change
- `a \% m` into `a mod m` to correspond with the notation in ZArith
- `m == n` into `m =? n` to correspond with the eqb notations elsewhere
- `m < n` into `m <? n` to correspond with the ltb notations elsewhere
- `m <= n` into `m <=? n` to correspond with the leb notations elsewhere
- `m ≤ n` into `m ≤? n` for consistency with the non-unicode notation

The old notations are still accessible as deprecated notations.

Fixes #12454







Merge PR #12122: Avoid registering as keywords the #... in Primitive
2020-05-09T10:53:20+00:00

Maxime Dénès

2020-05-09T10:53:20+00:00

3a7ff44f1ffaff3a8bb8c5a9c95a9b102e31c476

Ack-by: SkySkimmer
Reviewed-by: maximedenes





Ack-by: SkySkimmer
Reviewed-by: maximedenes







add order properties about bool
2020-05-04T13:44:59+00:00

Olivier Laurent

2020-04-02T22:45:03+00:00

f0aaf94f61f996808c29e37c827fc5d85761bddb