| Age | Commit message (Collapse) | Author |
|---|
|
- 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)
|
|
- 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
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Reviewed-by: JasonGross
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
NArith, PArith: Add facts about iter
|
|
Reviewed-by: ejgallego
|
|
arguments
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
|
|
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
Co-authored-by: Jasper Hugunin <jasper@hugunin.net>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: Matafou
Reviewed-by: ppedrot
|
|
As suggested by Gaëtan Gilbert.
|
|
Following an observation by Enrico Tassi, we remove the `opaque`
parameter from `close_future_proof`, it should never be called with
transparent constants.
We will enforce this thru typing at the proof layer soon.
|
|
|
|
|
|
After the last refactoring commit, the entry_fn function is redundant
and we can just get rid of it and get a more direct code.
|
|
We do some minor refactoring, removing one-use local definitions, and
cleaning up the `EConstr.t -> Constr.t` path, what is going on with
the use of unsafe it now becomes clear.
|
|
This is a small refactoring as these two functions behave very
differently and the invariants are quite different, in fact regular
`return_proof` should not be exported but be part of close proof, but
there is small use in the STM still.
|
|
We make the types of the delayed / non-delayed declaration path
different, as the latter is just creating futures that are forced
right away.
TTBOMK the new code should behave identically w.r.t. old one, modulo
the equation `Future.(force (from_val x)) = x`.
There are some questions as what the code is doing, but in this PR
I've opted to keep the code 100% faithful to the original one, unless
I did a mistake.
|
|
We split the `close_proof` into two variants, one for delayed proof,
and one for the regular proof closing path, _à la_ interactive.
This makes sense as the typing in both cases is different, even if we
still haven't changed it.
We strongly enforce the invariant (for now) that universe polymorphic
proofs cannot be delayed using this API, as the STM expects.
It introduces some minimal, non-interesting code duplication, which
will go away in the next commits.
|
|
Ack-by: Matafou
Reviewed-by: SkySkimmer
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
grammar.
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
Suggested by Gaëtan Gilbert.
|
|
This makes code a bit more clear.
|
|
- problem with metacoq overlay ; it expects to send a non-ground
constant to the kernel, now it fails at prepare.
Record Sigma (A : Type) (B : A -> Type) : Type :=
{ fst : A ; snd : B fst }.
Arguments fst {A B}.
Arguments snd {A B}.
Quote Recursively Definition foo := (fst, snd).
There is a hack on the overlay, we need to discuss it a bit more.
|
|
This will allow to share the definition metadata for example with
obligations; a bit more work is needed to finally move the preparation
of interactive proofs from Proof_global to `prepare_entry`.
|
|
`wits` is actually not used, it is set in equations to the list of
evars corresponding to the goals.
|
|
|
|
|
|
|
|
The only reasons that `prepare_definition` returned a sigma were:
- to obtain the universe binders to be passed to declare
- to obtain the UState.t to be passed to the equations hook
We handle this automatically now; it seems like a reasonably good API
improvement.
However, it is not clear what we do now is right for all cases; must
check.
|
|
This was introduced in #6203 , but as far as I can see this
re-normalization step is not necessary.
|
|
`sigma` here is actually created from `uctx`, we also uniformize
naming.
|
|
This is a step in forcing all entry creation go thru the preparation
functions. We still need to handle plain `Declare.` calls, but this
will be next step.
We need to leave a backdoor for interactive proofs until we unify
proof preparation happening in `Proof_global` with the one happening
in `DeclareDef`, but we are getting there.
TODO: see how to avoid the normalization problems in DeclareObl
|
|
We don't the parameter anymore as the paths are too different now.
Note that this removes a duplicate `check_evars` that has been in
`master` quite some time [double check in `ComDefinition` and in
`DeclareDef.prepare_definition`]
|
|
Preparation of obligation/program entries requires low-level
manipulation that does break the abstraction over `proof_entry`; we
thus introduce `prepare_obligation`, and move the code that prepares
the obligation entry to its own module.
This seems to improve separation of concerns, and helps clarify the
two of three current models in which Coq operates w.r.t. definitions:
- single, ground entries with possibly mutual definitions [regular lemmas]
- single, non-ground entries with possibly mutual definitions [obligations]
- multiple entries [equations]
|
|
Proof "preparation" [as in `DeclareDef.prepare_definition`] is fairly
more complicated in the Program case; in particular, it includes
checking the existential variables, and elaborating a list of entries
from the holes.
Indeed, in the `Program` case we cannot use
`DeclareDef.prepare_definition` while keeping a good level of
abstraction, so we should introduce a `prepare_obligation` function.
This PR is in preparation for that.
|
|
This is a tiny step towards making the code closer to its counterpart
in `DeclareDef`.
|
|
In previous versions of Coq `abstract` could create non-uniform bodies
for mutually recursive definitions (c.f. bug #5065)
Thanks to changes to the trusted base this is not the case anymore,
thus we can remove the workaround.
This way mutual bodies are handled the same in the interactive and
non-interactive case.
|
|
|
