| Age | Commit message (Collapse) | Author |
|---|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11977 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11228 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
pour les listes (trop contraignant)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10913 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
syntaxe interne de ring_lookup et field_lookup qui n'était pas assez
robuste pour supporter une syntaxe [ ... ] dans constr.
Déplacement de now_show de List.v vers Tactics.v, déplacement de "[ _ ]"
au niveau 0.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10872 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
loading and exporting of Setoid to ROmega which uses it for iff.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10775 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
more general.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10295 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
modification de interp_ltac_reference pour passer les ids utilisées
dans le contexte d'appel d'une tactique.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10076 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
------------------------------------------------
See file PreOmega for more details and/or test-suite/succes/*Omega*.v
The zify tactic performs a Z-ification of your current goal,
transforming parts of type nat, N, positive, taking advantage of many
equivalences of operations, and of the positivity implied by these
types.
Integration with omega and romega:
(r)omega : the earlier tactics, 100% compatible
(r)omega with * : full zify applied before the (r)omega run
(r)omega with <types>, where <types> is a sub-list of {nat,N,positive,Z},
applies only specific parts of zify (btw "with Z" means take advantage
of Zmax, Zmin, Zabs and Zsgn).
As a particular consequence, "romega with nat" should now be a
close-to-perfect replacement for omega. Slightly more powerful, since
(forall x:nat, x*x>=0) is provable and also slightly less powerful: if
False is somewhere in the hypothesis, it doesn't use it.
For the moment zify is done in a direct way in Ltac, using rewrite
when necessary, but crucial chains of rewrite may be made reflexive
some day.
Even though zify is designed to help (r)omega, I think it might be
of interest for other tactics (micromega ?). Feel free to complete
zify if your favorite operation / type isn't handled yet.
Side-effects:
- additional results for ZArith, NArith, etc...
- definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope
- romega now start by doing "intros". Since the conclusion will be negated,
and this operation will be justified by means of decidability, it helps
to have as little as possible in the conclusion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10028 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10001 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- deletion of some dead code
- grouping all stuff depending on Z in a nice module Int
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10000 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
utilities from Util. Some additions in Util, and simplifications
in various files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
and generic romega tactic...
For the moment, nothing is visible yet from the user's point of view
(hopefully). But internally, we prepare a romega that can works on
any integer types. ReflOmegaCore is now separated in several modules:
* First, an interface Int that specifies the minimal amount of things
needed on our integer type for romega to work:
- int should be a ring (re-use of ring_theory definition ;-)
- it should come with an total order, compatible with + * -
- we should have a decidable ternary comparison function
- moreover, we ask one (and only one!) critical property specific to
integers: a<b <-> a<=b-1
* Then a functor IntProperties derives from this interface all the
various lemmas on integers that are used in the romega part,
in particular the famous OMEGA?? lemmas.
* The romega reflexive part is now in another functor IntOmega,
that rely on some Int: no more Z inside. The main changes is
that Z0 was a constructor whereas our abstract zero isn't. So
matching Z0 is transformed into (if beq ... 0 then ...). With
extensive use of && and if then else, it's almost clearer this way.
* Finally, for the moment Z_as_Int show that Z fulfills our interface,
and ZOmega = IntOmega(Z_as_Int) is used by the tactic.
Remains to be done:
- revision of the refl_omega to use any Int instead of just Z,
and creating a user interface.
- Int has no particular reason to use the leibniz equality (only
rely on the beq boolean test). Setoids someday ?
- a version with "semi-ring" for nat ? or rather a generic way to plug
additional equations on the fly, e.g. n>=0 for every nat subpart ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9966 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
-----------------------------------
All romega tests in the test-suite are now bug-free. The only known
remaining limitation of romega with respect to omega is that it cannot
handle stuff on nat.
* Equivalences A<->B are now understood by romega (as well as omega),
and seen as (A->B)/\(B->A). There might be a smarter way to procede,
for instance having a primitive Iff construct and trying to break
equivalences as late as possible.
* Conclusion-as-Pprop issue:
After the resolution by the abstract omega machinery, useless parts
are discarded from the reification process by replacing them with
Pprop construct (see really_useful_prop). This allow to decrease
the size of the proof terms and speed up their normalisation, I guess.
But when such Pprop are created in the conclusion, this leads to
failure, since concl is negated, and this is donc only if it is
decidable. And introducing some Pprop might change the decidability
status of the concl: for instance, Pfalse is decidable, whereas
Pprop False is considered as _not_ decidable. Quick fix: no more
really_useful_prop applied on concl (needs careful computation of
useful_var).
* NEGATE_CONTRADICT(_INV):
This trace instrution comes in fact in two flavors, according to a
boolean flag. We now translate to O_NEGATE_CONTRADICT_INV if this
flag is false. (fix Besson's bug #1298)
* EXACT_DIVIDE:
could be used on NeqTerm and not only on EqTerm.
* h_step indexes:
The abstract omega machinery can introduce new hyps. In the list of hyps,
they appears _before_ the regular one (but after the goal seen as an hyp
by negating it). But the normalization steps were applied to regular hyps
thanks to their indexes counted _before_ the addition extra hyps.
* extra hyps (a)normal forms:
extra hyps and variables are initially of the shape
poly(v1,...,v(n-1)) = vn
but O_STATE was expecting them in form 0 = poly(...) + -vn
(by the way, SPLIT_INEQ should be checked someday).
Since the above is one weekend's worth of debugging, there might well
remain some more bugs :-(.
For the record, here's the less painful way to debug a failed romega run:
- activate debug flag in omega.ml and refl_omega.ml
- at the bottom of refl_omega, replace normalise_vm_in_concl with
convert_no_check (see comment there): this allow to skip the usually
_huge_ error message about "Impossible to unify True with ..."
- run the romega
- try to run Qed, and enjoy the nice errror message about a
(omega_tactic ? ? ? ?) that should be reducible to True.
Here starts the real debug work...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9962 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9391 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
romega_scope en compensation (et anticipation) d'une suppression de la récursivité des délimiteurs de scope (ici %term)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9041 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
'properties' de Subversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8660 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
1) dans refl_omega, on donnait a OmegaSolver un generateur de numero
d'equations new_eq_id qui pouvait clasher avec les numeros d'equations
initiaux créés avec new_omega_id.
=>
on sépare en deux compteurs, un pour les equations omegas, l'autre
pour les variables omegas. On en profite pour reinitialiser ces
compteurs à chaque session romega, histoire que romega devienne
reproductible.
2) dans omega.ml, le role de new_eq_id et new_var_id etait interverti
à un endroit.
ATTENTION: ceci peut changer le comportement d'omega. Surveiller le
resultat du prochain bench nocturne.
3) dans ReflOmegaCore.v, on ne traitait pas le cas d'une implication
dans une hypothese lors du recalcul final.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8657 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
et d'"externalisation"; standardisation du nom des fonctions d'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7734 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7726 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
ocaml 3.09
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6764 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6763 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
partielle
- amélioration traduction en nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6762 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- filtrage sur Bigint.zero incorrect: zero était considéré comme une variable
- coq_false et coq_true au lieu de coq_False et coq_true
- vérification chargement ROmega.vo
- Divers
- changement ordre argument interp_goal_concl pour permettre
application partielle
- amélioration débogueur
- ajout interprétation Zsucc, Zopp, et gel de Zmult si non scalaire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6761 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
renaming of constr_of_reference into constr_of_global)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6745 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6514 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par romega (omega2.ml, qui, l'occassion, disparat sous ce nom)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6511 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5431 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5428 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4807 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4799 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4522 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4478 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4354 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3598 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3537 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3394 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3267 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
hack temporaire autour du printer
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3120 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2798 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2745 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
|
