aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals
AgeCommit message (Collapse)Author
2021-02-20Inline proofs of exist_exp0 and exist_cos0.Guillaume Melquiond
2021-02-19Remove some trivial definition.Guillaume Melquiond
2021-02-19Abstract the non-computational part away.Guillaume Melquiond
2021-02-19Terminate intermediate lemmas with Qed.Guillaume Melquiond
2021-02-19Make intermediate lemmas more explicit, so that they can be terminated by Qed.Guillaume Melquiond
2021-02-19Make most of DRealAbstr opaque.Guillaume Melquiond
The function returned by DRealAbstr starts by a call to the axiom sig_forall_dec, so it is not computable anyway.
2021-02-19Terminate some lemmas with Qed.Guillaume Melquiond
Since the proofs start by applying or destructuring Qed-ed lemmas, they cannot be used in a computational setting, so no need for them to be Defined.
2020-12-09Redefines exp_ineq1 to hold for all non-zero numbers.Avi Shinnar
The original (which holds only for positive numbers) is now called exp_ineq1_pos. A version that holds only for negative numbers is added as exp_ineq1_neg. Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <). Co-authored-by: Barry M. Trager <bmt@us.ibm.com>
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
By default Coq stdlib warnings raise an error, so this is really required.
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
As noted by Hugo Herbelin, Dec is rather used for "decidable".
2020-11-05[numeral notation] Specify RPierre Roux
2020-11-05[numeral notation] RPierre Roux
Previously real constants were parsed by an unproved OCaml code. The parser and printer are now implemented in Coq, which will enable a proof and hopefully make it easier to maintain / make evolve. Previously reals were all parsed as an integer, an integer multiplied by a power of ten or an integer divided by a power of ten. This means 1.02 and 102e-2 were both parsed as 102 / 100 and could not be tell apart when printing. So the printer had to choose between two representations : without exponent or without decimal dot. The choice was made heuristically toward a most compact representation. Now, decimal dot is parsed as a rational and exponents are parsed as a product or division by a power of ten. For instance, 1.02 is parsed as Q2R (102 # 100) whereas 102e-2 is parsed as IZR 102 / IZR (Z.pow_pos 10 2). 1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1 = Q2R (102 # 100) * 10 and 10.2 = Q2R (102 # 10) no longer are.
2020-10-15Consistent indentation + a few bullets in RIneq.v.Hugo Herbelin
2020-09-17Formally deprecate the double induction tactic.Pierre-Marie Pédrot
The doc states it is deprecated since 1386cd9 but this was ages before the deprecation mechanism existed.
2020-07-05Defined arbitrary base logarithms (Rlog) and added natural lemmas concerning ↵Larry D. Lee Jr
ln, exp, and Rlog to the Real library. Additionally made the real exponent notation nonlocal.
2020-06-22Elementary properties about IZR for generic use.Hugo Herbelin
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-05-16Prove that classical reals implement constructive reals. Also move sums, min ↵Vincent Semeria
and max to CoRN. Update stdlib index Remove ConstructiveSum from the index Add changelog entry Make constructive reals experimental
2020-05-10Merge PR #12287: Define CRzero and CRone via CR_of_QMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-05-09Define CRzero and CRone via CR_of_QVincent Semeria
Add real numbers up to 10
2020-05-09Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.Maxime Dénès
Reviewed-by: maximedenes
2020-05-03Merge PR #12231: Simplify division of Cauchy realsMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-05-03Simplify division of Cauchy realsVincent Semeria
Improve comments
2020-05-01Merge PR #12221: Replace QSeqEquiv by QCauchySeq, simplify proofs.Michael Soegtrop
Reviewed-by: MSoegtropIMC
2020-04-30Replace QSeqEquiv by QCauchySeq, simplify proofs.Vincent Semeria
Force Cauchy modulus equal to identity, make division transparent Fix test
2020-04-30Merge PR #12208: Reduce rational numbers in Cauchy real addition, to ↵Michael Soegtrop
accelerate it Reviewed-by: MSoegtropIMC
2020-04-29Reduce rational numbers in Cauchy real addition, to accelerate itVincent Semeria
2020-04-23Merge PR #12117: Make multiplication of Cauchy reals transparent and ↵Hugo Herbelin
accelerate it Reviewed-by: herbelin
2020-04-22Document Cauchy realsVincent Semeria
2020-04-19Use binary integers for Cauchy realsVincent Semeria
2020-04-18Make multiplication of Cauchy reals transparent and accelerate itVincent Semeria
2020-04-01- Adjusted definitions and lemmas for asin and acos to what has been discussedMichael Soegtrop
- Added derivative for asin and acos - Added a few additional trigonometry lemmas - Added Lemmas for the derivative of a decreasing inverse function - Did some cleanup (move lemmas to the files where they belong)
2020-04-01- Addition to the Reals theory :thery
- minus: lemmas `Rminus_eq_0` and `Rmult_minus_distr_r` - sin : sin_inj - cos : cos_inj - sqrt : lemmas `pow2_sqrt` and `inv_sqrt` - atan : lemmas `tan_inj`, `atan_eq0`, `atan_tan` and `tan_atan` - asin : definition and some basic properties - acos : definition and some basic properties
2020-04-01[micromega] use Coqlib.lib_ref to get Coq constants.Frédéric Besson
2020-03-30Missing apartness notationsVincent Semeria
2020-03-27Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move ↵Vincent Semeria
ConstructiveReals into new directory Abstract. Remove imports of implementations inside those Abstract files. Add changelog for constructive reals cleanup Move Cauchy reals into new directory Cauchy Update stdlib index Rename sum_f_R0 Use coqdoc comments Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Improve notations
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-04Add file to register names of reals library used by gappaMichael Soegtrop
2020-02-06replace RList by list RYves Bertot
add an overlay for coquelicot remove functions from RList: In, Rlength, cons_Rlist, app_RList because they are essentially the same as In, length, app, and map from List (beware that the order of arguments changes for map, and the In function contains reversed equalities). adds deprecation warnings for Rlist and Rlength adds deprecated notations for RList.cons and RList.nil
2020-01-17Fix issue #11396 : Rlist hides standard list constructors cons and nilMichael Soegtrop
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
PR #9725 fixes completness bugs introduces some inefficiency. The current PR intends to fix the inefficiency while retaining completness. The fix removes a pre-processing step and instead relies on a more elaborate proof format introducing positivity constraints on the fly. Solve bootstrapping issues: RMicromega <-> Rbase <-> lia. Fixes #11063 and fixes #11242 and fixes #11270
2019-10-28[stdlib]Reals: use “lia” rather than “omega”Vincent Laporte
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional ↵Hugo Herbelin
extensionality Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin Ack-by: maximedenes
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ↵Vincent Semeria
homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers.
2019-10-22Zcomplements: do not use “omega”Vincent Laporte
2019-09-25Merge PR #10713: Define morphisms of real numbers and accelerate Cauchy realsHugo Herbelin
Reviewed-by: herbelin
2019-09-16Define morphisms of real numbers and accelerate Cauchy realsVincent Semeria
Prove that morphisms preserve additions Fix stdlib index Prove that constructive real morphisms preserve multiplications by integers Prove that constructive real morphisms preserve multiplications by rationals Prove CReal_mult_pos_appart_zero Prove that constructive real morphisms preserve multiplications Prove that constructive real morphisms preserve divisions Rewrite convergence in sort Prop, to extract smaller programs Rewrite convergence on integers, to extract smaller programs Fix typos
2019-09-16Remove library-specific code for `Import`.Maxime Dénès
Libraries are now handled like other modules.
2019-09-09[stdlib] Do not put INR_eq in the “real” hint databaseVincent Laporte
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
This could be Prop (for compat with usual Coq), Set (for HoTT), or actually an arbitrary "i". Take lower bound of universes into account in pretyping/engine Reinstate proper elaboration of SProp <= l constraints: replacing is_small with equality with lbound is _not_ semantics preserving! lbound = Set Elaborate template polymorphic inductives with lower bound Prop This will make more constraints explicit Check univ constraints with Prop as lower bound for template inductives Restrict template polymorphic universes to those not bounded from below Fixes #9294 fix suggested by Matthieu Try second fix suggested by Matthieu Take care of modifying elaboration for record declarations as well. Rebase and export functions for debug Remove exported functions used while debugging Add a new typing flag "check_template" and option "-no-template-checl" This parameterizes the new criterion on template polymorphic inductives to allow bypassing it (necessary for backward compatibility). Update checker to the new typing flags structure Switch on the new template_check flag to allow old unsafe behavior in indTyping. This is the only change of code really impacting the kernel, together with the commit implementing unbounded from below and parameterization by the lower bound on universes. Add deprecated option `Unset Template Check` allowing to make proof scripts work with both 8.9 and 8.10 for a while Fix `Template Check` option name and test it Add `Unset Template Check` to Coq89.v Cooking of inductives and template-check tests Cleanup test-suite file for template check / universes(template) flags cookind tests Move test of `Unset Template Check` to the failure/ dir, but comment it for now Template test-suite test explanation Overlays for PR 9918 Overlay for paramcoq Add overlay for fiat_parsers (-no-template-check) Add overlay for fiat_crypto_legacy Update fiat-crypto legacy overlay Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made. Remove overlay that should no longer be necessary The setting in the compat file should handle it Remove now-merged fiat-crypto-legacy overlay Update `Print Assumptions` to reflect the typing flag for template checking Fix About and Print Assumptions for template poly, giving info on which variables are actually polymorphic Fix pretty printing to print global universe levels properly Fix printing of template polymorphic universes Fix pretty printing for template polymorphism on no universe Fix interaction of template check and universes(template) flag Fix indTyping to really check if there is any point in polymorphism: the conclusion sort should be parameterized over at least one local universe Indtyping fixes for template polymorphic Props Allow explicit template polymorphism again Adapt to new indTyping interface Handle the case of template-polymorphic on no universes correctly (morally Type0m univ represented as Prop). Fix check of meaningfullness of template polymorphism in the kernel. It is now done w.r.t the min_univ, the minimal universe inferred for the inductive/record type, independently of the user-written annotation which must only be larger than min_univ. This preserves compatibility with UniMath and template-polymorphism as it has been implemented up-to now. Comment on identity non-template-polymorphism Remove incorrect universes(template) attributes from ssr simpl_fun can be meaningfully template-poly, as well as pred_key (although the use is debatable: it could just as well be in Prop). Move `fun_of_simpl` coercion declaration out of section to respect uniform inheritance Remove incorrect uses of #[universes(template)] from the stdlib Extraction of micromega changes due to moving an ind decl out of a section Remove incorrect uses of #[universes(template)] from plugins Fix test-suite files, removing incorrect #[universes(template)] attributes Remove incorrect #[universes(template)] attributes in test-suite Fix test-suite Remove overlays as they have been merged upstream.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:18:28 +0000