| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
universe polymorphic constructors.
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16749 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The problem occurs when a customized ring/field structure
declared with a so-called "morphism" (see 24.5 in the manual) tactic
allowing to reify (numerical) constants efficiently.
When declaring a ring/field structure, the user can provide a cast
function phi in order to express numerical constants in another type than
the carrier of the ring. This is useful for instance when the ring is
abstract (like the type R of reals) and one needs to express constants
to large to be parsed in unary representation (for instance using a
phi : Z -> R).
Formerly, the completeness of the tactic required (phi 1) (resp. (phi 0))
to be convertible to 1 (resp. 0), which is not the case when phi is
opaque. This was not documented untill recently
but I moreover think this is also not desirable
since the user can have good reasons to work with such an opaque case phi.
Hence this commit:
- adds two constructors to PExpr and FExpr for a correct reification
- unplugs the optimizations in reification: optimizing reification
is much less efficient than using a cast known to the tactic.
TODO : It would probably be worth declaring IZR as a cast in the ring/field
tactics provided for Reals in the std lib.
The completeness of the tactic formerly relied on the fact that
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16730 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The field tactic post-processes the data generated during normalization
to ensure that vanished denominators do not cancel: essentially, this
step removes duplicates from a list of polynomials and uses the
clean list to generate the conjunction of associated non-zero conditions. This
conjunction is the proof obligation the user has to prove by hand after
a successful call to the field tactic.
The computation of the proof obligation statement
was performed using a fine-tuned reduction strategy, coded in
the newring.ml4 file (see the fv-protect tactic).
However, not only this strategy information was forgotten by the kernel,
but the strategy used at Qed time caused a real explosion (examples
normalized in 70s by the tactic have a one hour Qed). No idea why.
The fix consists in opacifying the part of the goal irrelevant to
computation and call the vm on the duplicate removal step. BTW this step
is programmed in a naive way and can probably be made more efficient.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16728 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This file should compile now twice as fast as earlier.
A large part of this speedup comes from swithching to
proofs without "auto" (and also improving them quite a lot).
Nicer lemma statements thanks to notations and
separate scopes (%ring, %coef, %poly).
The Field_correct lemma lost some args (sign_theory ...)
during the refactoring. After inspection, this looks legitimate,
so I've hack the field tactic accordingly. The args were there
probably due to some intuition or similar interfering with local
vars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16721 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- For instance, refl_equal --> eq_refl
- Npos, Zpos, Zneg now admit more uniform qualified aliases
N.pos, Z.pos, Z.neg.
- A new module BinInt.Pos2Z with results about injections from
positive to Z
- A result about Z.pow pushed in the generic layer
- Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
- Using tactic Z.le_elim instead of Zle_lt_or_eq
- Some cleanup in ring, field, micromega
(use of "Equivalence", "Proper" ...)
- Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
- In ZMake and ZMake, functor parameters are now named NN and ZZ
instead of N and Z for avoiding confusions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12729 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
- algo de Janet (finalement pas utilise)
- le hash-cons des certificats de Benjamin et Laurent pas encore integre
- traitement des puissances jusqu'a 6 (methode totalement naive)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12088 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Théo Zimmermann
Pierre-Marie Pédrot
Maxime Dénès
Matthieu Sozeau
amahboub
letouzey
herbelin
barras
glondu