aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals
AgeCommit message (Collapse)Author
2010-02-18Removed redundant and ill-named technical lemma.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12797 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-18Removed SeqProp's dependency on Classical.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12796 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-18Removed Rtrigo's dependency on Classical.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12795 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-17Removed Rseries' dependency on Classical.gmelquio
This is a tradeoff: the Archimedean property is used instead through the discrete logarithm. Thanks to P-M. Pedrot for demonstrating this proof scheme on coq-club. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12787 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-17Removed Rlimit's dependency on Classical.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12783 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-17Removed Rderiv's dependency on Classical.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12782 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*letouzey
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
2010-01-07Rework of GenericMinMax: new axiomatic, split logical/decidable parts, ↵letouzey
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
2010-01-07OrderTac: use TotalOrder, no more "change" before calling "order" (stuff ↵letouzey
with Inline) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12636 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-17Reverse order of arguments in min_case_strong for better uniformity (and ↵letouzey
compatibility...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12595 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are ↵letouzey
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
2009-12-06Fix anomaly when using typeclass resolution with filtered hyps in evars.msozeau
Make setoid_rewrite-through-rewrite's selection of occurences more robust: do not try unification with reduction if not needed. This changes a few scripts that were using reduction in a far from obvious way and could break more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12562 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-16Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsletouzey
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
2009-11-10DecidableType: A specification via boolean equality as an alternative to eq_decletouzey
+ 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
2009-11-03ROrderedType + Rminmax : Coq's Reals can be seen as OrderedType.letouzey
This way we get properties of Rmin / Rmax (almost) for free. TODO: merge Rbasic_fun and Rminmax... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12463 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-02Remove various useless {struct} annotationsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-02Added alternate versions of existing lemmas on sqrt.gmelquio
Indeed, since sqrt is a total function, most lemmas are true, even for negative inputs. For instance, sqrt_le_1 was 0 <= x -> 0 <= y -> x <= y -> sqrt x <= sqrt y while sqrt_le_1_alt is just x <= y -> sqrt x <= sqrt y. Naming is done by adding _alt suffixes. In an ideal world (Coq 9.0?), these new lemmas should just replace the original ones. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12457 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-04Removal of trailing spaces.serpyc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12371 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-04Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12370 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-28Fix the stdlib doc compilation + switch all .v file to utf8letouzey
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
2009-09-27Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12358 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-09-11Added the following lemmas to homogenize Reals a bit:gmelquio
- Rmult_eq_compat_r, Rmult_eq_reg_r, Rplus_le_reg_r, Rmult_lt_reg_r, Rmult_le_reg_r (mirrored variants of the existing _l lemmas); - minus_IZR, opp_IZR (Ropp_Ropp_IZR), abs_IZR (mirrored Rabs_Zabs); - Rle_abs (RRle_abs); - Zpower_pos_powerRZ (signed variant of Zpower_nat_powerRZ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12321 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-27Parsing files for numerals (+ ascii/string) moved into pluginsletouzey
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
2009-03-17- gros commit sur ring et field: passage des arguments simplifiebarras
- tacinterp.ml: les arguments tactiques de Tactic Notation n'etaient pas evalues, laissant des variables libres (symptome: exc Not_found) - reals: Open Local --> Local Open - ListTactics: syntaxe des listes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11989 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-06Fixed bug #2036 (wrong copy-paste in RIneq) [copy of 11887 in branch v8.2]herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11888 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-16Take advantage of natdynlink when available: almost all contribs become ↵letouzey
loadable plugins - Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode). - Features that were available without any Require are now loaded systematically when launching coqtop (see Coqtop.load_initial_plugins): extraction, jprover, cc, ground, dp, recdef, xml - The other plugins are loaded when a corresponding Require is done: quote, ring, field, setoid_ring, omega, romega, micromega, fourier - I experienced a crash (segfault) while turning subtac into a plugin, so this one stays statically linked into coqtop for now - When the ocaml version doesn't support natdynlink, or if "-natdynlink no" is explicitely given to configure, coqtop is statically linked with all of the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear. - How should coqdep handle a "Declare ML Module "foo"" if foo is an archive and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the same location as the .v during the build, but can be moved later in any place of the ml loadpath. This is clearly an experimentation. Feedback most welcome... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11687 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-12MAJ et bricoles diversesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10923 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-06Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :herbelin
- si on met Rle_ge et Rge_le tous les deux en Resolve (et de même pour Rlt_gt et Rgt_lt) alors on introduit un cycle, - si on en met un des deux en Immediate, alors on perd la symétrie car si un développement n'a un lemme en hints que pour Rge (resp Rle), alors il ne sera pas utilisable si on met Rge_le (resp Rle_ge) en Immediate (et c'est ce qui arrive notamment dans HighSchoolGeometry). L'idéal serait d'introduire une notion de raisonnement modulo équivalence dans auto afin que chaque lemme sur Rle (resp Rge) soit systématiquement applicable aussi face à Rge (resp Rle) sans redondances et sans cycle. Ainsi Rle_ge and co n'auraient pas un statut de hints mais plutôt un statut de conversions implicites entre notions synonymes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10762 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-05Suite 10760herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10761 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-05- Retour en arrière sur la capacité du nouvel apply à utiliser lesherbelin
lemmes se terminant par False ou not sur n'importe quelle formule (cela crée trop d'incompatibilités dans les "try apply" etc.); de toutes façons, "contradict" joue presque ce rôle (à ceci près qu'il ne traverse pas les conjonctions) (tactics/tactics.ml). - Quelques corrections sur RIneq.v - le hint Rlt_not_eq avait été oublié dans la phase de restructuration, - davantage de noms canoniques (O -> 0, etc.), - nouvelle tentative de ramener "auto" vers Rle (avec Rle_ge) plutôt que vers Rge qui est moins souvent associé à des hints. - Utilisation du formateur deep_ft pour afficher les scripts de preuve afin d'éviter le besoin d'un "Set Printing Depth" (vernacentries.ml). - Suppression de certaines utilisations de l'Anomaly de meta_fvalue qui ne correspondaient pas à des comportements anormaux (reductionops.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10760 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-04- Amélioration de la présentation de RIneq, même si un nettoyage desherbelin
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
2008-03-23Commit d'une preuve de l'axiome d'Archimède qui traînait dans mes placards.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10711 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-23Une passe sur les réels:herbelin
- Renommage de Rlt_not_le de Fourier_util en Rlt_not_le_frac_opp pour éviter la confusion avec le Rlt_not_le de RIneq. - Quelques variantes de lemmes en plus dans RIneq. - Déplacement des énoncés de sigT dans sig (y compris la complétude) et utilisation de la notation { l:R | }. - Suppression hypothèse inutile de ln_exists1. - Ajout notation ² pour Rsqr. Au passage: - Déplacement de dec_inh_nat_subset_has_unique_least_element de ChoiceFacts vers Wf_nat. - Correction de l'espace en trop dans les notations de Specif.v liées à "&". - MAJ fichier CHANGES Note: il reste un axiome dans Ranalysis (raison technique: Ltac ne sait pas manipuler un terme ouvert) et dans Rtrigo.v ("sin PI/2 = 1" non prouvé). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10710 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-01Marche-arrière sur la suppression de l'hypothèse inutile de Rpower_Oherbelin
(rapport de bug 1807). Cf explication dans le fichier et/ou dans le bug-tracker. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10613 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-29Argumentation plus poussée de pourquoi on retire la condition x>0 dansherbelin
Rpower_O alors qu'on la garde pour les autres propriétés de la puissance. (résultat d'une discussion avec Assia et Jean-Marc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10609 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27Application patch #1807 sur hypothèse inutile de Rpower_Oherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10599 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Essai de prise en compte de delta dans unify_0 (même sur termes non clos). herbelin
- Pour éviter de pénaliser auto, eauto, autorewrite, mise en place d'une option "modulo_conv" pour contrôler l'usage de cette delta. - Pour éviter que rewrite ne réussise trop souvent, la delta est désactivée pour les tactiques d'élimination (une étude fine reste à faire). - On n'utilise aussi delta que sur les sous-termes du problème d'unification initial. C'est une heuristique qui est intuitive mais qui reste à être évaluée. - Au bilan, le surcoût en temps de compilation des theories est d'un peu moins d'1%. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10557 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-24Nicer proofs.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10476 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-24remove Fourier Failure warnings.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10474 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-24Prove the decidability of arithmetical statements using the real numbers.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10473 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-27Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0herbelin
(crédits à Sylvie Boldo) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10146 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-15Changement dans ring et field, beaucoup de correction d'erreurs,bgregoir
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
2006-12-11Changement dans le kernel : bgregoir
- essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-30fixed field_simplify + changed precedence of let and fun in ltacbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9319 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-30LegacyRfield was opening R_scopebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9317 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-27simplif de la partie ML de ring/fieldbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9302 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-27Le caractère ² fait planter make docnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9298 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Mise en forme des theoriesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 04:54:16 +0000