| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
CompareSpec expects 3 propositions Peq Plt Pgt instead of 2 relations
eq lt and 2 points x y. For the moment, we still always use (Peq=eq x y),
(Plt=lt x y) (Pgt=lt y x), but this may not be always the case,
especially for Pgt. The former CompSpec is now defined in term of
CompareSpec. Compatibility is preserved (except maybe a rare unfold
or red to break the CompSpec definition).
Typically, CompareSpec looks nicer when we have infix notations, e.g.
forall x y, CompareSpec (x=y) (x<y) (y<x) (x?=x)
while CompSpec is shorter when we directly refer to predicates:
forall x y, CompSpec eq lt x y (compare x y)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13914 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Initial plan was only to add shiftl/shiftr/land/... to N and
other number type, this is only partly done, but this work has
diverged into a big reorganisation and improvement session
of PArith,NArith,ZArith.
Bool/Bool: add lemmas orb_diag (a||a = a) and andb_diag (a&&a = a)
PArith/BinPos:
- added a power function Ppow
- iterator iter_pos moved from Zmisc to here + some lemmas
- added Psize_pos, which is 1+log2, used to define Nlog2/Zlog2
- more lemmas on Pcompare and succ/+/* and order, allow
to simplify a lot some old proofs elsewhere.
- new/revised results on Pminus (including some direct proof of
stuff from Pnat)
PArith/Pnat:
- more direct proofs (limit the need of stuff about Pmult_nat).
- provide nicer names for some lemmas (eg. Pplus_plus instead of
nat_of_P_plus_morphism), compatibility notations provided.
- kill some too-specific lemmas unused in stdlib + contribs
NArith/BinNat:
- N_of_nat, nat_of_N moved from Nnat to here.
- a lemma relating Npred and Nminus
- revised definitions and specification proofs of Npow and Nlog2
NArith/Nnat:
- shorter proofs.
- stuff about Z_of_N is moved to Znat. This way, NArith is
entirely independent from ZArith.
NArith/Ndigits:
- added bitwise operations Nand Nor Ndiff Nshiftl Nshiftr
- revised proofs about Nxor, still using functional bit stream
- use the same approach to prove properties of Nand Nor Ndiff
ZArith/BinInt: huge simplification of Zplus_assoc + cosmetic stuff
ZArith/Zcompare: nicer proofs of ugly things like Zcompare_Zplus_compat
ZArith/Znat: some nicer proofs and names, received stuff about Z_of_N
ZArith/Zmisc: almost empty new, only contain stuff about badly-named
iter. Should be reformed more someday.
ZArith/Zlog_def: Zlog2 is now based on Psize_pos, this factorizes
proofs and avoid slowdown due to adding 1 in Z instead of in positive
Zarith/Zpow_def: Zpower_opt is renamed more modestly Zpower_alt
as long as I dont't know why it's slower on powers of two.
Elsewhere: propagate new names + some nicer proofs
NB: Impact on compatibility is probably non-zero, but should be
really moderate. We'll see on contribs, but a few Require here
and there might be necessary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13651 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12714 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12462 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v
In fact coqdoc was trying to recognize the end of a _emphasis_ and
hence inserted a bogus }. For the moment I've enclosed the phrase
with [ ], but this emphasis "feature" of coqdoc seems _really_
easy to broke. Matthieu ?
2) By the way, this Library document was made from latin1 and utf8
source file, hence bogus characters. All .v containing special
characters are converted to utf8, and their first line is now
mentionning this. (+ killed some old french comments and some
other avoidable special characters).
PLEASE: let's stick to this convention and avoid latin1, at least
in .v files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12250 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
In fact, Qge and Ggt disappear, and we only leave notations for > and >=
that map directly to Qlt and Qle.
We also adopt the same approach for BigN, BigZ, BigQ.
By the way, various clean-up concerning Zeq_bool, Zle_bool and similar
functions for Q.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11205 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
sig, sig2, sumor, list et vector dans Type
- Branchement de prodT/listT vers les nouveaux prod/list
- Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2
- Changements en conséquence dans les théories (notamment Field_Tactic),
ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 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@4965 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4879 85f007b7-540e-0410-9357-904b9bb8a0f7
|
letouzey
herbelin
glondu
notin
barras