Questions tagged [arithmetic]
Questions on basic arithmetic involving numerical quantities only.
4 questions
2
votes
1
answer
142
views
Is it possible to simplify/normalize nat arithmetic expressions in Coq?
I'm writing a tactic to apply some normalizing rewriting rules on a substitution algebra, similar to the autosubst project. I've made a sigma tactic that applies ...
- 155
11
votes
1
answer
175
views
What did Coq 8.15 change about divmod?
I noticed that Coq 8.15 (possibly 8.14) made some significant changes to divmod. In particular, Nat.divmod_0q0 seems to have been removed and the ...
- 243
16
votes
4
answers
564
views
Is there a proof assistant for Peano Arithmetic?
Is there a proof assistant for Peano Arithmetic (PA)?
Or, for some well known and better developed proof assistant is there a way to employ it to write down PA proofs ? Are there even tools to check ...
- 261
12
votes
1
answer
88
views
Tools to check correctness of decimal floating point arithmetic
I have implemented (in TeX, but it doesn't matter for this question) a library of functions that evaluate basic arithmetic, as well as some transcendental functions such as cosine, on decimal floating ...
- 502