| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
| |
This closes #146 and makes `make quick` faster.
The changes were generated by adding [Global Set Suggest Proof Using.]
to GlobalSettings.v, and then following [the instructions for a script I
wrote](https://github.com/JasonGross/coq-tools#proof-using-helper).
|
| | |
|
| |
|
|
|
|
| |
[ZToField] -> [F.of_Z]
[FieldToZ] -> [F.to_Z]
[Zmod.lem] -> [F.lem]
|
| |
|
|
|
|
|
|
|
|
|
|
| |
ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.
Backwards-incompatible changes:
F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1
|
| |
|
|
| |
general contexts.
|
| |
|
|
| |
and finished encoding admits.
|
|
|
function.
|
Andres Erbsen
Jason Gross
jadep