coq/theories/Reals, branch master The formal proof system Inline proofs of exist_exp0 and exist_cos0. 2021-02-20T08:49:45+00:00 Guillaume Melquiond 2021-02-20T08:49:45+00:00 3caa323fd4176c2217a9f681fb60a73c1ccdb6c8 






Remove some trivial definition.
2021-02-19T18:39:38+00:00

Guillaume Melquiond

2021-02-19T18:37:50+00:00

fccbde39ff8085f73bdb46dac278f88474a1e202












Abstract the non-computational part away.
2021-02-19T18:29:46+00:00

Guillaume Melquiond

2021-02-19T18:29:46+00:00

21ed2bfa901108d69893bc8480d215edeb255d6d












Terminate intermediate lemmas with Qed.
2021-02-19T18:10:25+00:00

Guillaume Melquiond

2021-02-19T18:10:25+00:00

88e688182ded232f474102d400e4e4e95861f94d












Make intermediate lemmas more explicit, so that they can be terminated by Qed.
2021-02-19T18:05:35+00:00

Guillaume Melquiond

2021-02-19T18:05:35+00:00

19752f81e096daac43119a144f8065dabbdb1e82












Make most of DRealAbstr opaque.
2021-02-19T15:47:11+00:00

Guillaume Melquiond

2021-02-19T15:47:11+00:00

cec70c45e25d9a2a53ada7b9941b92663b08c7e0

The function returned by DRealAbstr starts by a call to the axiom
sig_forall_dec, so it is not computable anyway.





The function returned by DRealAbstr starts by a call to the axiom
sig_forall_dec, so it is not computable anyway.







Terminate some lemmas with Qed.
2021-02-19T15:28:35+00:00

Guillaume Melquiond

2021-02-19T15:13:45+00:00

b45ffd0bc0904e3d3325724e99b94239f5153b64

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.





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.







Redefines exp_ineq1 to hold for all non-zero numbers.
2020-12-09T13:40:11+00:00

Avi Shinnar

2020-12-06T02:56:15+00:00

29d2ffb5f5569efe8614efa30be560efc72a34f5

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>





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>







Explicitly annotate all hint declarations of the standard library.
2020-11-16T11:28:27+00:00

Pierre-Marie Pédrot

2020-11-14T16:55:07+00:00

68cd077344ce37db1a601079dbc4fdcae6c8d41f

By default Coq stdlib warnings raise an error, so this is really required.





By default Coq stdlib warnings raise an error, so this is really required.







Rename Dec and HexDec to Decimal and Hexadecimal
2020-11-04T23:20:53+00:00

Pierre Roux

2020-10-28T09:32:58+00:00

36ac26532028bfc6f84e4dfc849b51f42a3d8286

As noted by Hugo Herbelin, Dec is rather used for "decidable".





As noted by Hugo Herbelin, Dec is rather used for "decidable".