aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Natural
AgeCommit message (Collapse)Author
2010-02-17Arith's min and max placed in Peano (+basic specs max_l and co)letouzey
This allow for instance to remove the dependency of List.v toward Min.v To prove max_l and co, we push Le.le_pred and Le.le_S_n into Peano. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12784 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-10Euclidean division for NArithletouzey
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
2010-02-09Numbers: properties of min/max with respect to 0,S,P,add,sub,mulletouzey
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
2010-02-09NPeano improved, subsumes NatOrderedTypeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12717 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-09NSub: a missing lemma (sub usually decreases)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12716 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-09NBinary improved, contains more, subsumes NOrderedTypeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12715 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-08DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generationletouzey
- Records of operations and specs in CyclicAxioms are now type classes (under a module ZnZ for qualification). We benefit from inference and from generic names: (ZnZ.mul x y) instead of (znz_mul (some_ops...) x y). - Beware of typeclasses unfolds: the line about Typeclasses Opaque w1 w2 ... is critical for decent compilation time (x2.5 without it). - Functions defined via same_level are now obtained from a generic version by (Eval ... in ...) during definition. The code obtained this way should be just as before, apart from some (minor?) details. Proofs for these functions are _way_ simplier and lighter. - The macro-generated NMake_gen.v contains only generic iterators and compare, mul, div_gt, mod_gt. I hope to be able to adapt these functions as well soon. - Spec of comparison is now fully done with respect to Zcompare - A log2 function has been added. - No more unsafe_shiftr, we detect the underflow directly with sub_c git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12713 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-29Division in numbers: kills some Include to avoid bad alias Zsucc = ZDiv.Z.Z'.Sletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12704 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-25NMake (and hence BigN): shiftr, shiftl now in the signature NSigletouzey
we export the "safe" version of these functions, working for all input and not only reasonably small shifting arg. The former "unsafe" shiftr and shiftl are now unsafe_shiftr and unsafe_shiftl. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12688 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-25NMake: several things need not be macro-generatedletouzey
The macro-generated .v file is now NMake_gen.v, while NMake.v now contain the static things (i.e. definition of gcd via mod). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12687 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-19Ring31 : a ring structure and tactic for int31letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12685 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-19NMake_gen: fix previous commit (some spaces were critical), remove some more ↵letouzey
spaces git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12684 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-19NMake_gen: no more spaces at end of linesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12683 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-18More improvements of BigN, BigZ, BigQ:letouzey
- ring/field: detection of constants for ring/field, detection of power, potential use of euclidean division. - for BigN and BigZ, x^n now takes a N as 2nd arg instead of a positive - mention that we can use (r)omega thanks to (ugly) BigN.zify, BigZ.zify. By the way, BigN.zify could still be improved (no insertion of positivity hyps yet, unlike the original zify). - debug of BigQ.qify (autorewrite was looping on spec_0). - for BigQ, start of a generic functor of properties QProperties. - BigQ now implements OrderedType, TotalOrder, and contains facts about min and max. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12681 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-17BigN, BigZ, BigQ: presentation via unique module with both ops and propsletouzey
We use the <+ operation to regroup all known facts about BigN (resp BigZ, ...) in a unique module. This uses also the new ! feature for controling inlining. By the way, we also make sure that these new BigN and BigZ modules implements OrderedTypeFull and TotalOrder, and also contains facts about min and max (cf. GenericMinMax). Side effects: - In NSig and ZSig, specification of compare and eq_bool is now done with respect to Zcompare and Zeq_bool, as for other ops. The order <= and < are also defined via Zle and Zlt, instead of using compare. Min and max are axiomatized instead of being macros. - Some proofs rework in QMake - QOrderedType and Qminmax were in fact not compiled by make world Still todo: OrderedType + MinMax for BigQ, etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12680 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-14Avoid some more re-declarations of Equivalence instancesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12671 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12Numbers/.../NDefOps: one more property about ltbletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12654 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12Numbers: some more proofs about sub,add,le,lt for natural numbersletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12653 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12Numbers: two more Local Obligation Tacticletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12652 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-11Support "Local Obligation Tactic" (now the default in sections).msozeau
Update Numbers that was implicitely using [simpl_relation] instead of the default tactic [program_simpl]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12647 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-08Numbers: BigN and BigZ get instantiations of all properties about div and modletouzey
NB: for declaring div and mod as a morphism, even when divisor is zero, I've slightly changed the definition of div_eucl: it now starts by a check of whether the divisor is zero. Not very nice, but this way we can say that BigN.div and BigZ.div _always_ answer like Zdiv.Zdiv. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12646 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07Include can accept both Module and Module Typeletouzey
Syntax Include Type is still active, but deprecated, and triggers a warning. The syntax M <+ M' <+ M'', which performs internally an Include, also benefits from this: M, M', M'' can be independantly modules or module type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07Numbers: separation of funs, notations, axioms. Notations via module, ↵letouzey
without scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12639 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-06Patch on subtyping check of opaque constants.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12631 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-05Numbers abstract layer: more Module Type, used especially for divisions.letouzey
Properties are now rather passed as functor arg instead of via Include or some inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12629 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-05Division in Numbers: factorisation of signaturesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12624 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-04Specific syntax for Instances in Module Type: Declare Instanceletouzey
NB: the grammar entry is placed in vernac:command on purpose even if it should have gone into vernac:gallina_ext. Camlp4 isn't factorising rules starting by "Declare" in a correct way otherwise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12623 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-18RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndletouzey
As a consequence, revert to some pedestrian proofs of Equivalence here and there, without the need for the Measure class. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12598 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-15A generic euclidean division in Numbers (Still Work-In-Progress)letouzey
- For Z, we propose 3 conventions for the sign of the remainder... - Instanciation for nat in NPeano. - Beginning of instanciation in ZOdiv. Still many proofs to finish, etc, etc, but soon we will have a decent properties database for all divisions of all instances of Numbers (e.g. BigZ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12590 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-30Fix backtracking heuristic in typeclass resolution. msozeau
Now that backtracking is working correctly, we need to avoid a non-termination issue introduced by the [RelCompFun] definition in RelationPairs, by adding a [Measure] typeclass. It could be used to have a uniform notation for measures/interpretations in Numbers and be but in the interfaces too, only the mimimal change was implemented. Fix syntax change in test-suite scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12547 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)letouzey
- In fact, Bind Scope has no retrospective effect. Since we don't want it inside functor, we use it late, and hence we are forced to use manual "Arguments Scope" commands. - Added syntax for power in BigN / BigZ / BigQ. - Added syntax p#q in BigQ for representing fractions (constructor BigQ.Qq) as in QArith. Display of a rational numeral is hence either an integer (constructor BigQ.Qz) or something like 6756 # 8798. - Fix of function BigQ.Qred that was not simplifing (67#1) into 67. - More tests in test-suite/output/NumbersSyntax.v A nice one not in the test-suite: Time Eval vm_compute in BigQ.red ((2/3)^(-100000) * (2/3)^(100000)). = 1 : bigQ Finished transaction in 3. secs (3.284206u,0.004s) :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12507 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12Repair interpretation of numeral for BigQ, add a printer (close #2160)letouzey
on the way: - Added a testsuite output file - Try to avoid nasty unfolding (fix nfun ...) in type of I31. Idealy we would need a "Eval compute in" for the type of a inductive constructor - Stop opening Scopes for BigQ, BigN, BigZ by default The user should do some Open Scope. TODO: there's a bug that prevent BigQ.opp to have arg in bigQ_scope (and so on for other operations), even with some Bind Scope around. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12504 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-10SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMaxletouzey
To retrieve the old behavior of spec_sub0 and spec_sub with precondition on order, just chain spec_sub with Zmax_r or Zmax_l. Idem with spec_pred0 and spec_pred. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12490 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-10Simplification of Numbers, mainly thanks to Includeletouzey
- No more nesting of Module and Module Type, we rather use Include. - Instead of in-name-qualification like NZeq, we use uniform short names + modular qualification like N.eq when necessary. - Many simplification of proofs, by some autorewrite for instance - In NZOrder, we instantiate an "order" tactic. - Some requirements in NZAxioms were superfluous: compatibility of le, min and max could be derived from the rest. - NMul removed, since it was containing only an ad-hoc result for ZNatPairs, that we've inlined in the proof of mul_wd there. - Zdomain removed (was already not compiled), idea of a module with eq and eqb reused in DecidableType.BooleanEqualityType. - ZBinDefs don't contain any definition now, migrate it to ZBinary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12489 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-06Numbers: finish files NStrongRec and NDefOpsletouzey
- NStrongRec provides a "strong" recursor based on the usual one: recursive calls can be done here on any lower value. See binary log in NDefOps for an example of use. - NDefOps contains alternative definitions of usual operators (add, mul, ltb, pow, even, half, log) via usual or strong recursor, and proofs of correctness and/or of equivalence with axiomatized operators. These files were in the archive but not being compiled, some proofs of correction for functions defined there were missing. By the way, some more iff-style lemmas in Bool. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12476 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-06Numbers: more (syntactic) changes toward new style of type classesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12475 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-03Numbers: start using Classes stuff, Equivalence, Proper, Instance, etcletouzey
TODO: finish removing the "Add Relation", "Add Morphism" fun_* fun2_* TODO: now that we have Include, flatten the hierarchy... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12464 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-08Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-08Implicit argument of Logic.eq become maximally insertedletouzey
This allow in particular to write eq instead of (@eq _) in signatures of morphisms. I dont really see how this could break existing code, no change in the stdlib was mandatory. We'll check the contribs tomorrow... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12379 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-20Many fixes in unification:msozeau
- Restore failure when types don't unify in [unify_types] (undoing r12075) but try to be more clever about cumulativity using the meta's [instance_status] information. - Fix second-order abstraction when K is not allowed to ensure that we don't unify twice with the same subterm in [w_unify_to_subterm_list]. A more elaborate solution would be give the list to [w_unify_to_subterm] so that it keeps going when it finds an already-found instantiation. - Two "obvious" errors fixed: taking the wrong instance status when unifying with a meta on the right and forgoting type equations in [w_merge]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12136 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-12Uniformity with the rest of the StdLib : _symm --> _symletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11675 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-14Add user syntax for creating hint databases [Create HintDb foomsozeau
[discriminated]] with a switch for using the more experimantal dnet impl for every hint. Also add [Hint Transparent/Opaque] which parameterize the dnet and the unification flags used by auto/eauto with a particular database. Document all this. Remove [Typeclasses unfold] directives that are no longer needed (everything is unfoldable by default) and move to [Typeclasses Transparent/Opaque] syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11409 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-26Even better test for choosing rewrite or setoid_rewrite.msozeau
Now there is a class "SetoidRelation" for registering relations that should always be considered as setoids and never unfolded. Every "Add Relation" command adds an instance and impl,iff are there by default. Now the test is: if there is a SetoidRelation instance, use it ; otherwise, allow unfolding to find an eq or fallback on setoid_rewrite. To avoid searching for SetoidRelation instances repeateadly we check that it is really needed first by unfolding the hyp. Only two scripts relied on the now-forbidden semantics of rewriting by an @eq inside a setoid relation, in Numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11269 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-04Fix bug #1899: no more strange notations for Qge and Qgtletouzey
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
2008-07-01Various bug fixes in type classes and subtac:msozeau
- Cases on multiple objects - Avoid dangerous coercion with evars in subtac_coercion - Resolve typeclasses method-by-method to get better error messages. - Correct merging of instance databases (and add debug printer) - Fix a script in NOrder where a setoid_replace was not working before. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11198 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-27Enhanced discrimination nets implementation, which can now work withmsozeau
goals containing existentials and use transparency information on constants (optionally). Only used by the typeclasses eauto engine for now, but could be used for other hint bases easily (just switch a boolean). Had to add a new "creation" hint to be able to set said boolean upon creation of the typeclass_instances hint db. Improve the proof-search algorithm for Morphism, up to 10 seconds gained in e.g. Field_theory, Ring_polynom. Added a morphism declaration for [compose]. One needs to declare more constants as being unfoldable using the [Typeclasses unfold] command so that discrimination is done correctly, but that amounts to only 6 declarations in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11184 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-18Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkherbelin
(résolution entre autres des bugs 1882, 1883, 1884). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11145 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
for increased consistency with bignums parts (commit part II: names of files + additional translation minus --> sub) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11040 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-02In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
for increased consistency with bignums parts (commit part I: content of files) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11039 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 20:49:22 +0000