| Age | Commit message (Collapse) | Author |
|---|
|
Bvector uses only Minus, so let's avoid loading Arith
(and hence ArithRing and hence parts of Z, N)
Program.Syntax no longer need Lists now that list is in Datatypes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12785 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
There was already a Ndiv and Nmod, but hiddent in ZOdiv_def. We
higlight it by putting it in a separate file, prove its specification
without using Z (but for the moment can't avoid a detour via nat,
though), and then instantiate general results from Natural/Abstract/NDiv
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12726 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
With these properties, we can kill Arith/MinMax, NArith/Nminmax,
and leave ZArith/Zminmax as a compatibility file only. Now
the instanciations NPeano.Nat, NBinary.N, ZBinary.Z, BigZ, BigN
contains all theses facts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Old stuff DecidableType.v and OrderedType.v stay there and keep their
names for the moment, for compatibility.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12641 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Leibniz part
Moreover, instantiation like MinMax are now made without redefining
generic properties (easier maintenance). We start using inner modules
for qualifying (e.g. Z.max_comm).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12638 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
with Inline)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12636 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
compatibility...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12595 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in */*/vo.itarget
On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
if you want a partial build, make a specific rule such as theories-light
Beware: these vo.itarget should not contain comments. Even if this is legal
for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We can now have a diamond-like approch to extentions of signatures,
instead of a linear-only chains as earlier...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12529 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
As show by contrib TreeAutomata, the Peqb now placed in BinPos
was using 1st arg as "struct", instead of 2nd arg as earlier.
Fix that, and remove the "Import BinPos BinNat" hack in Ndec
(merci Hugo :-).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12503 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
+ adaptation of {Nat,N,P,Z,Q,R}_as_DT for them to provide both eq_dec and eqb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12488 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12462 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- A richer OrderedTypeFull interface : OrderedType + predicate "le"
- Implementations {Nat,N,P,Z,Q}OrderedType.v, also providing "order" tactics
- By the way: as suggested by S. Lescuyer, specification of compare is
now inductive
- GenericMinMax: axiomatisation + properties of min and max out of
OrderedTypeFull structures.
- MinMax.v, {Z,P,N,Q}minmax.v are specialization of GenericMinMax,
with also some domain-specific results, and compatibility layer
with already existing results.
- Some ML code of plugins had to be adapted, otherwise wrong "eq",
"lt" or simimlar constants were found by functions like coq_constant.
- Beware of the aliasing problems: for instance eq:=@eq t instead of
eq:=@eq M.t in Make_UDT made (r)omega stopped working (Z_as_OT.t
instead of Z in statement of Zmax_spec).
- Some Morphism declaration are now ambiguous: switch to new syntax
anyway.
- Misc adaptations of FSets/MSets
- Classes/RelationPairs.v: from two relations over A and B, we
inspect relations over A*B and their properties in terms of classes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12461 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 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
|
|
The compare functions are still functions-by-tactics, but now their
computational parts are completely pure (no use of lt_eq_lt_dec in
nat_compare anymore), while their proofs parts are simply calls
to (opaque) lemmas. This seem to improve the efficiency of sets/maps,
as mentionned by T. Braibant, D. Pous and S. Lescuyer.
The earlier version of nat_compare is now called nat_compare_alt,
there is a proof of equivalence named nat_compare_equiv.
By the way, various improvements of proofs, in particular in Pnat.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12247 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- "*" implements Arthur Charguéraud's "introv"
- "**" works as "; intros" (see also "*" in ssreflect).
- Simplifying the proof of Z_eq_dec, as suggested by Frédéric Blanqui.
- Shy attempt to seize the opportunity to clean Zarith_dec but Coq's
library is really going anarchically (see a summary of the various
formulations of total order, dichotomy of order and decidability of
equality and in stdlib-project.tex in branch V8revised-theories).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12171 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Idea: make coqtop more independant of the standard library.
In the future, we can imagine loading the syntax for numerals right
after their definition. For the moment, it is easier to stay lazy
and load the syntax plugins slightly before the definitions.
After this commit, the main (sole ?) references to theories/
from the core ml files are in Coqlib (but many parts of coqlib
are only used by plugins), and it mainly concerns Init
(+ Logic/JMeq and maybe a few others).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12024 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
and, with a now generic intropattern "[]", also "as []_eqn", "as []_eqn:H"
for "destruct" with equality keeping.
- Fixed an accuracy loss in error location.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11732 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
inductive types was not taken into account).
- Virtually extended tauto to
- support arbitrary-length disjunctions and conjunctions,
- support arbitrary complex forms of disjunctions and
conjunctions when in the contravariant of an implicative hypothesis,
- stick with the purely propositional fragment and not apply reflexivity.
This is virtual in the sense that it is not activated since it breaks
compatibility with the existing tauto.
- Modified the notion of conjunction and unit type used in hipattern in a
way that is closer to the intuitive meaning (forbid dependencies
between parameters in conjunction; forbid indices in unit types).
- Investigated how far "iff" could be turned into a direct inductive
definition; modified tauto.ml4 so that it works with the current and
the alternative definition.
- Fixed a bug in the error message from lookup_eliminator.
- Other minor changes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11721 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- make the modifiers "value of" and "type of" for "set" working (it was not!),
- clear unselected hypotheses in the "in" clause of "induction/destruct" when
the destructed term is a variable (experimental),
- support for generalization of hypotheses in the induction hypotheses using
the "in" clause of "induction" (e.g. "induction n in m, H" will
generalize over m -- would it be better to have an explicit
"over"/"generalizing" clause ?).
Added clause "as" to "apply in".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11509 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
actuellement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11466 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t)))
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This way, no more references to NBinDefs.N when doing "Print N".
Long-term migration to theories/Numbers is still planned, but it needs
more works, for instance to adapt both positive and N and Z at once.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
As suggested by Hugo, Notation "p ~ 1" instead of Notation "p ~1" avoids potential
conflict with stuff like ~1=1.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10793 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Hints reste à faire. (dommage que Rge et Rle ne soient pas
convertibles)
- Ajout de Nnat et Ndigits dans NArith.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10751 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
of the fix I added an optional "by" annotation for rewrite to solve said
conditions in the same tactic call. Most of the theories have been
updated, only FSets is missing, Pierre will take care of it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
More details in the header of BinPos.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10547 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10304 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
A file ZOdiv is added which contains results about this euclidean division.
Interest compared with Zdiv: ZOdiv implements others (better?) conventions
concerning negative numbers, in particular it is compatible with Caml
div and mod.
ZOdiv is only partially finished...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10302 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10299 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
theories/Numbers/Natural/Binary/NBinDefs. Most of the entities in the new BinNat are notations for the development in Numbers. Also added min and max to the new natural numbers and integers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10298 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
present in Ints. For the moment, mainly:
- Q parts go in QArith
- Some of the Zdivide & Zgcd stuff go in Znumtheory
More to come ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10281 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
binary positive numbers.
Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10226 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
things compile: abstract natural numbers and integers with plus, times, minus, and order; Peano and binary implementations for natural numbers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10161 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10130 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
------------------------------------------------
See file PreOmega for more details and/or test-suite/succes/*Omega*.v
The zify tactic performs a Z-ification of your current goal,
transforming parts of type nat, N, positive, taking advantage of many
equivalences of operations, and of the positivity implied by these
types.
Integration with omega and romega:
(r)omega : the earlier tactics, 100% compatible
(r)omega with * : full zify applied before the (r)omega run
(r)omega with <types>, where <types> is a sub-list of {nat,N,positive,Z},
applies only specific parts of zify (btw "with Z" means take advantage
of Zmax, Zmin, Zabs and Zsgn).
As a particular consequence, "romega with nat" should now be a
close-to-perfect replacement for omega. Slightly more powerful, since
(forall x:nat, x*x>=0) is provable and also slightly less powerful: if
False is somewhere in the hypothesis, it doesn't use it.
For the moment zify is done in a direct way in Ltac, using rewrite
when necessary, but crucial chains of rewrite may be made reflexive
some day.
Even though zify is designed to help (r)omega, I think it might be
of interest for other tactics (micromega ?). Feel free to complete
zify if your favorite operation / type isn't handled yet.
Side-effects:
- additional results for ZArith, NArith, etc...
- definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope
- romega now start by doing "intros". Since the conclusion will be negated,
and this operation will be justified by means of decidability, it helps
to have as little as possible in the conclusion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10028 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9883 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9740 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Pplus_xO
Pmult_Sn_m
Pcompare_eq_Lt (a generalization of Pcompare_Gt_Lt)
Pcompare_eq_Gt (a generalization of Pcompare_Lt_Gt)
Pcompare_refl_id (a generalization of Pcompare_refl)
Pcompare_Lt_eq_Lt (a generalization of Pcompare_Lt_Lt)
Pcompare_Gt_eq_Gt (a generalization of Pcompare_Gt_Gt)
Pcompare_p_Sp
Pcompare_p_Sq (one of the defining axioms of < )
Pcompare_1 (1 is the least positive number)
Added the following theorems to BinNat:
Nrect (defined in terms of new Prect)
Nrect_base
Nrect_step (the analogout statement in BinPos is called Prect_succ)
Nrec_base
Nrec_step
Nmult_Sn_m
Nsucc_0
Ncompare_0 (0 is the least natural number)
Ncompare_n_Sm (one of the defining axioms of < )
Also, defined Nind and Nrec in terms of Nrect.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9738 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9701 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
égalité décidable + maj dépendances
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9467 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
suggérée par Conor McBride qui ne fait pas intervenir eq_rect et
qui permet de montrer "facilement" (mais avec l'axiome K) les équations
de réduction de Prec.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9465 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
maintenant les differentes tactics marchent mieux mais le code
est moche ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9454 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9210 85f007b7-540e-0410-9357-904b9bb8a0f7
|
