| Age | Commit message (Collapse) | Author |
|---|
|
extensionality tactic to apply the axiom properly and fix test-suite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10415 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from
svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses
........
r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line
Comment grammar error
........
r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines
The initial Type Classes patch.
This patch introduces type classes and instance definitions a la Haskell.
Technically, it uses the implicit arguments mechanism which was extended a bit.
The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters.
It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac).
........
r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line
Fix interface
........
r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line
Fix more xlate code
........
r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines
Update coqdoc for type classes, fix proof state not being displayed on Next Obligation.
........
r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines
Bug fixes in Instance decls.
........
r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines
Streamline typeclass context implementation, prepare for class binders in proof statements.
........
r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line
Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions
........
r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines
Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context.
........
r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line
Stupid bug
........
r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line
Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints
........
r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line
Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors
........
r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines
Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent.
New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental.
Other bugs related to naming in typeclasses fixed.
........
r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines
Progress on setoids using type classes, recognize setoid equalities in hyps better.
Streamline implementation to return more information when resolving setoids (return the results setoid).
........
r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line
Syntax change, more like Coq
........
r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line
Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax
........
r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines
Work on type classes based rewrite tactic.
........
r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines
Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets.
........
r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line
Forgot to add a file
........
r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines
Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and
implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts.
........
r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines
Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations.
Add useful tactics to Program.Subsets.
........
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10400 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10370 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10364 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10263 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
sans bêta-normaliser face à un bêta-rédex dont l'argument ne
correspond pas à ce qui est à réécrire.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10224 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
filtrage; sauts de line intempestifs dans pretty.ml)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10179 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10172 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
de plusieurs bugs d'indice, de List.rev, d'oubli d'application de
whd_evar + code plus concis pour l'argument optionnel "filter").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10145 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10134 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
the latter is bound to a var which is not a quantified one - this led
to remove a line marked "temporary compatibility" ... ; made a distinction
between quantified hypothesis as for "intros until" and binding names as
in "apply with"; in both cases, we now expect that a identifier not used
as a variable, as in "apply f_equal with f:=g" where "f" is a true binder
name in f_equal, must not be used as a variable elsewhere [see
corresponding change in Ints/Tactic.v])
- Fixing bug 1643 (bug in the algorithm used to possibly reuse a
global name in the recursive calls of a coinductive term)
- Fixing bug 1699 (bug in contracting nested patterns at printing time
when the return clause of the subpatterns is dependent)
- Fixing bug 1697 (bug in the TacAssert clause of Tacinterp.subst_tactic)
- Fixing bug 1678 (bug in converting constr_pattern to constr in Constrextern)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10131 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10125 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
-----------------------------------------------
- Les fonctions evar_define et real_clean font un travail plus fin :
- S'il y a plusieurs manières d'inverser l'instance d'une evar, on
retarde le choix au lieu de faire un choix arbitraire.
- Si l'instance contient une evar et que cette evar n'est pas inversible,
on essaie aussi d'inverser ou de restreindre (un sous-terme) de
l'evar qui était initialement à instancier.
- Incidemment, real_clean est renommé en invert_instance, un nom qui
reflète mieux la diversité du travail fait par ce fameux real_clean.
- La fonction solve_refl garde les problèmes qui contiennent encore de
l'information.
- Changements secondaires :
- Délégation de la gestion des variables modifiées et des problèmes à
reconsidérer (get_conv_pbs) à Evd (qui s'en charge par effet de bord
au moment du define) (incidemment get_conv_pbs devient
extract_conv_pbs)
- Essai d'un mécanisme différent de restriction des evars : pour
éviter des contextes mal formés (comme do_restrict pouvait a priori
le faire), on utilise maintenant un contexte bien formé doublé d'un
filtre signalant les instances interdites. C'est a priori plus
souple (par ex : si une variable du contexte a un type dépendant
d'une evar, on peut attendre de connaître cette evar avec de
déterminer si cette variable du contexte, qui peut-être dépend via
cette evar d'une autre variable interdite, doit être finalement
interdite ou pas)
- Nettoyages divers.
- Ce que evarutil ne fait toujours pas :
- Utiliser l'inversion et/ou l'unification d'ordre supérieur (par
exemple pour résoudre "?ev[S n]=n"); en particulier, la notion
d'inversion unique ne prend pas en compte l'unification d'ordre
supérieur et peut donc faire des choix irréversibles vis à vis de
l'unif d'ordre supérieur.
- Utiliser (systématiquement -- et précautionneusement) les types
des solutions trouvées pour résoudre davantage de problèmes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10124 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
de solutions distinctes faites modulo égalité d'alias uniquement et pas
modulo toute la puissance de la convertibilité)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10123 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10120 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10114 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
l'unification sait maintenant résoudre des équations du genre
"?n[...;x:=?m[...;y:=t;...]] = t" lorsque x et y sont uniques vérifiant
cette propriété (la solution est alors de poser ?m:=y et ?n:=x); le
type de t est aussi pris en compte dans cette situation (ce genre de
problème permet de résoudre des cas simples d'unification avec dépendance:
cf l'exemple de foldrn dans test-suite/success/Fixpoint.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10092 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10085 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10077 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
|
|
implicitement suggéré par le rapport de bug #1671
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10069 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
bugs soumis sur Coq-bugs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10068 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10062 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10040 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@9988 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@9920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
métas permettant de savoir si une instance de méta vient d'un
with-binding ou d'une unification, et si elle a déjà été typée ou pas.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9866 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(en particulier, la décision de quelle instance garder quand une méta
a plusieurs solutions importe; comment trouver une critère objectif ?
la compatibilité demande à donner préférence aux instances trouvées
par with-bindings).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9855 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
apply afin de reculer au plus tard les décisions irréversibles et en
particulier de pouvoir typer les with-bindings modulo coercions :
- l'unification des types des métas données en with-bindings est
retardé à après l'unification (unify_0) de telle sorte que les
instances trouvées par unify_0 soient prioritaires et que la
décision d'insérer éventuellement des coercions autour des valeurs
données en with-bindings se fasse au dernier moment;
- toujours pour permettre d'insérer ultimement des coercions,
l'instantiation des with-bindings ne se fait plus
l'appel unify_0 (cf clenv_unique_resolver);
- pour permettre ce retardement sans limiter le test de conversion
que unify_0 fait sur les termes clos, on transmet à unify_0 les
métas données en with-bindings (ainsi l'instantiation de ces métas
peut être faite dynamiquement au moment du test de clôture);
- parce que les métas données en with-bindings qui sont en position
de rédex (cas d'un "apply f_equal with (f:=fun ...)" peuvent
simplifier le problème d'unification (et elles ne sont pas de
toutes façons pas réinférables au premier ordre), on continue à
les substituer avant l'appel à unify_0 (cf meta_reducible_instance);
- pour l'unification du second-ordre, on continue d'instancier les
with-bindings et d'unifier les types des with-bindings avant
unification;
- reste à régler un problème de compatibilité lorsque le résultat de
l'unification des types des with-bindings est utilisé pour rendre
un terme clos et pour permettre à unify_0 d'utiliser la conversion.
+ meilleure compatibilité de apply, split, left, right pour le code
qui l'utilise avec des bindings clos
+ nettoyage et uniformisation des clenv_match_args, clenv_missing, et assimilés
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9850 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9838 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9827 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
@nil".
Ajout @ref au niveau constr pour allègement syntaxe.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9819 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
discussion avec Georges)
- La notion d'insertion maximale n'est plus globale mais attachée à
chaque implicite
- Correction de petits bugs dans le calcul des implicites
- Raffinement de la notion "sous contexte" pour l'affichage des coercions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9817 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9816 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9809 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9769 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9764 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9763 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
fix/cofix avec réutilisation du nom de la constante dans les appels
récursifs), avec notamment uniformisation des comportements et des
noms de fonctions de réduction. En particulier, on a les changements
sémantiques suivants :
- léger changement de simpl: si appliqué à un fix explicite, il sait
réduire l'argument en un constructeur comme si le fix était caché
derrière une constante (cf exemple dans test-suite/output/reduction.v);
- léger changement de hnf: si appliqué à un match ou un fix explicite
et que l'argument de ce match ou de ce fix nécessite un calcul
impliquant des constantes récursives, il sait conserver les noms (à
la manière de simpl) comme il sait déjà le faire si ce match ou ce fix
était caché derrière une constante (cf exemple dans
test-suite/output/reduction.v);
- changement similaire de one_step_reduce utilisé dans reduce_to_*_ref
(difficile d'imaginer les effets mais sans doute très peu)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9760 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9714 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
arbitraire de décimales
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9713 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9709 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9666 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9664 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9663 85f007b7-540e-0410-9357-904b9bb8a0f7
|
