aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2007-07-05Update on numbers.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9947 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-05Added Qpower_mult theorem.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9946 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-03Compatibilité des noms longs de Bool déplacés dans Datatypesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9936 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-02Correction (partielle) du bug #1587notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9931 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-29Added the directory theories/Numbers where axiomatizations and ↵emakarov
implementations (unary, binary, etc.) of different number classes (natural, integer, rational, real, complex, etc.) will be stored.Currently there are axiomatized natural numbers with two implementations and axiomatized integers. Modified Makefile accordingly but dod not include the new files in THEORIESVO yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9916 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-27- Extensions of FMap(Weak)Facts: letouzey
fold properties and induction principles for (weak) maps. - Simplification in SetoidList: the two important results fold_right_equivlistA and fold_right_add are now proved without using removeA and hence do not depend anymore on a decidable equality (good for maps and their arbitrary datas). In fact, removeA is not used at all anymore, but I leave it here (mostly), since it can't hurt. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9914 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-27eqlistA is now equivlistAletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9913 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-26Added zwqipWith.roconnor
Added theory about intractions between nth and map, and zipWith. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9909 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-26additional properties for FMap (and slight rework of SetoidList and ↵letouzey
FSetProperties) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9908 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-25Updated Qpow_tac to work on a a more realistic set of exponent values.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9907 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-22Ajout exist & cie à la table des hints par symétrie avec ex_intro &herbelin
cie (cf message coq-club 21/6/07). De plus, left/right inleft/inright, eux aussi dans Set/Type, y étaient déjà donc l'argument d'être dans Type n'est pas recevable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9906 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-21Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc, notin
et une typo dans Eqdep_deq.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9905 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-21Adding: Field instance for Q.roconnor
: Power function from Q -> Z -> Q. : Absolute value function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9901 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-20ajout de head0 et tail0 en natifbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19safe_shift correct recursionthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9899 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19safe_shift recursionthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9898 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19safe_shift recursionthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9897 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19Adding function is_even, safe_shiftl, safe_shiftrthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9894 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19genN.ml syncthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9893 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-18Correct height computationthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9892 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-14oups: one file forgotten in my previous commitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9891 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-14Rework of FSetProperties, in order to add more easily a Properties functor letouzey
for FMap (for the moment in FMapFacts). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9890 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-11undeletion of E_ST and Equal_ST: these records aren't mandatory, but quite ↵letouzey
useful git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9887 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-08some more properties of fold and elements in FSetPropertiesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9885 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-08Removed an extra \tacindex occurrence for the tactic discriminate.emakarov
Added a tactic "now" which is nonrecursive but generalizes "trivial". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9884 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-07Extension of NArith: Nminus, Nmin, etcletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9883 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-07* For uniformity, FSetAVL uses Implicit Arguments (a bit)letouzey
* Some additionnal properties: - two more induction principles on sets - some results about union, filter, etc - Subset is declared to be a Setoid Relation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9882 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-06tail0thery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9877 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-05Gestion espaces dans notation _ = _ :> _herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9876 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-30mul_norm for Q fixedthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9871 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-28comparison functions should be Defined not Qedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9867 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-27As suggested by Pierre Casteran, fold for FSets/FMaps now takes a letouzey
(A:Type) instead of a (A:Set). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9863 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-25fix for bug #1347 (no more Scope pollution by FSets)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9861 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-22Comparaison JMeq/eq_depherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9849 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-21Added Z and Q implementations with int31.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9846 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-21add_mul_pos uses int31 onlythery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9845 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-15pos_mod fixedthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9824 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-15Correction de sqrt312 (racine carree d'un nombre represente comme un aspiwack
couple de Int31). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9823 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-28Déplacement des opérations sur bool dans l'état initialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9803 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-25Utilisation du nouveau "Unset Elimination Schemes" pour empêcher la création herbelin
des schémas d'élimination standard de JMeq, plutôt que "Reset JMeq_rect". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9793 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-17Correction du bug #1510notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9777 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-13Correction bug #1499notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9767 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-12Transparency of Z_lt_le_decnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9759 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-06simplier version of tail_plusletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9750 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-02Added back the tactics [apply -> ident], etc. to Tactics.v afteremakarov
committing the extension of the general sequence operator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9743 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-02Réparation de NArith/BinPos.v suite au commit #9739notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9740 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-01Removed the definition of extensions of apply to equivalencesemakarov
(apply -> H, etc.), which prevented Coq compilation. These tactics require an extension of syntax: t1; [t2 | .. ], which has to be submitted first. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9739 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-30Added the following theorems to BinPos:emakarov
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
2007-03-30Added new tactics for applying equivalences (iff) to Tactics.v:emakarov
"apply -> t", "apply <- t", "apply -> t in H" and "apply <- t in H" . Also added the tactic false_hyp based on absurd_hyp. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9737 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-06 06:11:57 +0000