| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
of Zdiv
Some details:
- ZAux.v is the only file left in Ints/Z. The few elements that remain in it
are rather specific or compatibility oriented. Others parts and files have
been either deleted when unused or pushed into some place of ZArith.
- Ints/List/ is removed since it was not needed anymore
- Ints/Tactic.v disappear: some of its tactic were unused, some already in
Tactics.v (case_eq, f_equal instead of eq_tac), and the nice contradict
has been added to Tactics.v
- Znumtheory inherits lots of results about Zdivide, rel_prime, prime, Zgcd, ...
- A new file Zpow_facts inherits lots of results about Zpower. Placing them
into Zpower would have been difficult with respect to compatibility
(import of ring)
- A few things added to Zmax, Zabs, Znat, Zsqrt, Zeven, Zorder
- Adequate adaptations to Ints/num/* (mainly renaming of lemmas)
Now, concerning Zdiv, the behavior when dividing by a negative number is now
fully proved. When this was possible, existing lemmas has been extended,
either from strictly positive to non-zero divisor, or even to arbitrary
divisor (especially when playing with Zmod). These extended lemmas are named
with the suffix _full, whereas the original restrictive lemmas are retained
for compatibility. Several lemmas now have shorter proofs (based on unicity
lemmas). Lemmas are now more or less organized by themes (division and order,
division and usual operations, etc). Three possible choices of spec for
divisions on negative numbers are presented: this Zdiv, the ocaml approach
and the remainder-always-positive approach. The ugly behavior of Zopp
with the current choice of Zdiv/Zmod is now fully covered. A embryo of
division "a la Ocaml" is given: Odiv and Omod.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10291 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9438 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9302 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6983 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
hypothesis of Zlt/Zgt_square_simpl (cg #948)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6898 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6884 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4933 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4873 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4845 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4819 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
de la partie Omega dans contrib/omega
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4801 85f007b7-540e-0410-9357-904b9bb8a0f7
|
letouzey
herbelin
barras
notin