| Age | Commit message (Collapse) | Author |
|---|
|
general_multi_multi_rewrite. Due to the option "!" of rewrite, a lemma
may need to be interpreted several times with different instances of
the implicit arguments. Interpreting the term as a constr in
tacinterp.ml would need to either refresh the holes (i.e. the evars)
or detype what has been typed and in both cases, complicated things
can happen because the evars associated to these holes may have been
used in instantiating former evars of the goal. Leaving the term as a
rawconstr would need to export the interpretation functions from
tacinterp which is technically complicated in the current situation
because equality.ml is currently linked before tacinterp. The solution
used is to delay the interpretation using an ML closure.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12610 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We renounced to distribute evars to constr and bindings and to let
tactics do the merge. There are now two disciplines:
- the general case is that the holes in tactic arguments are pushed to
the general sigma of the goal so that tactics have no such low-level
tclEVARS, Evd.merge, or check_evars to do:
- what takes tclEVARS and check_evars in charge is now a new
tactical of name tclWITHHOLES (this tactical has a flag to support
tactics in either the "e"- mode and the non "e"- mode);
- the merge of goal evars and holes is now done generically at
interpretation time (in tacinterp) and as a side-effect it also
anticipates the possibility to refer to evars of the goal in the
arguments;
- with this approach, we don't need such constr/open_constr or
bindings/ebindings variants and we can get rid of all ugly
inj_open-style coercions;
- some tactics however needs to have the exact subset of holes known;
this is the case e.g. of "rewrite !c" which morally reevaluates c at
each new rewriting step; this kind of tactics still receive a
specific sigma around their arguments and they have to merge evars
and call tclWITHHOLES by themselves.
Changes so that each specific tactics can take benefit of this generic
support remain to be done.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Explained in CHANGES how to cope with the change of semantics of
abbreviations wrt implicit arguments positions propagation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12586 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in presence of destruction of conjunctive types.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12584 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12583 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(expected goal was not correct for rewriting in hypotheses)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12580 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- made the new "subst'" the default by renaming it "subst";
- renamed old "subst" into "simple subst";
- add option for non-rewriting of dependent proofs in general_rewrite and co
- kept use of dependent proofs in the "subst" call of "functional
induction", in spite it introduced incompatibilities (in Compcert).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12578 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
by contracting in advance the projT (existT ...) redexes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12577 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(this was lost since revision 12481).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12560 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12505 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
"eq"-rewriting (a few contributions are still referring explicitly to
eq_rect, eq_ind and co and the new mechanism, though working also for
dependent rewriting, is not powerful enough in general wrt fixpoint
guard to claim being uniformly better).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12501 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
with the guard condition + typo in the generation of _rec schemes in
the impredicative case.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12484 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Cleaning and uniformisation in command.ml:
- For better modularity and better visibility, two files got isolated
out of command.ml:
- lemmas.ml is about starting and saving a proof
- indschemes.ml is about declaring inductive schemes
- Decomposition of the functions of command.ml into a functional part
and the imperative part
- Inductive schemes:
- New architecture in ind_tables.ml for registering scheme builders,
and for sharing and generating on demand inductive schemes
- Adding new automatically generated equality schemes (file eqschemes.ml)
- "_congr" for equality types (completing here commit 12273)
- "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep",
"_rew_backward" (similar to eq_rect), "_rew_backward_dep" for
rewriting schemes (warning, rew_forward_dep cannot be stated following
the standard Coq pattern for inductive types: "t=u" cannot be the
last argument of the scheme)
- "_case", "_case_nodep", "_case_dep" for case analysis schemes
- Preliminary step towards discriminate and injection working on any
equality-like type (e.g. eq_true)
- Restating JMeq_congr under the canonical form of congruence schemes
- Renamed "Set Equality Scheme" into "Set Equality Schemes"
- Added "Set Rewriting Schemes", "Set Case Analysis Schemes"
- Activation of the automatic generation of boolean equality lemmas
- Partial debug and error messages improvements for the generation of
boolean equality and decidable equality
- Added schemes for making dependent rewrite working (unfortunately with
not a fully satisfactory design - see file eqschemes.ml)
- Some names of ML function made more regular (see dev/doc/changes.txt)
- Incidentally, added a flush to obsolete Local/Global syntax warning
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12436 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Compatibility version is now a global parameter that every feature can
individually browse. This avoids having to keep the names of options
synchronous in their respective files and in now-removed file coqcompat.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12372 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
which was disturbing inversion and sometimes making it failing in
presence of dependent equalities (injection still doesn't know how to
split dependent equalities, resulting in a smaller number of
equalities than expected for dEqThen).
[also restored inv.ml as it was before 12356 which uselessly and
inadvertently modified it]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12360 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
a dependent scheme is needed or not (this allows for instance
"destruct H" when H is propositional and dependent in the context to
work).
Modest attempt to clarify the basic components used and invariants
preserved when sharing the code for functional induction and for
destruct/induction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12356 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
before attempting generalized rewriting as the relation may itself be
instantiated during the unification of the lemma.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12312 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
rewriting (thanks to Georges Gonthier for pointing it out).
We try to find a declared rewrite relation when the equation does not
look like an equality and otherwise try to reduce it to find a leibniz equality
but don't backtrack on generalized rewriting if this fails. This new
behavior make two fsets scripts fail as they are trying to use an
underlying leibniz equality for a declared rewrite relation, a [red]
fixes it.
Do some renaming from "setoid" to "rewrite".
Fix [is_applied_rewrite_relation]'s bad handling of evars and the
environment.
Fix some [dual] hints in RelationClasses.v and assert that any declared
[Equivalence] can be considered a [RewriteRelation].
Fix minor tex output problem in coqdoc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12310 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
compilation of Grenoble/ATBR). Add subst' for subst extended with JMeq
(maybe an option would be better??).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12264 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
context (problem introduced in r12259) + improved backward
compatibility in hippatern.mli (wrt r12259).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12260 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Added support for "injection" and "discriminate" on JMeq.
Seized the opportunity to update coqlib.ml and to rely more on it for
finding the equality lemmas.
Fixed typos in coqcompat.ml.
Propagated symmetry convert_concl fix to transitivity (see 11521).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- add coqtop option "-compat X.Y" so as to provide compatibility with
previous versions of Coq (of course, this requires to take care of
providing flags for controlling changes of behaviors!),
- add support for option names made of an arbitrary length of words
(instead of one, two or three words only),
- add options for recovering 8.2 behavior for discriminate, tauto,
evar unification ("Set Tactic Evars Pattern Unification", "Set
Discriminate Introduction", "Set Intuition Iff Unfolding").
Update of .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
I wonder how many of us were aware of the existence of such syntax ;-)
Anyway, it is now subsumed by "rewrite by".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12248 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
agreement with wish #2117 (pattern unification of evars remained
deactivated for 3 years because of incompatibilities with eauto [see
commit 9234]; thanks to unification flags, it can be activated for
apply w/o changing eauto).
Also add test for bug #2123 (see commit 12228).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12229 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
traînaient un peu partout dans le code depuis la fusion d'evar_map et
evar_defs. Début du travail d'uniformisation des noms donnés aux
evar_defs à travers le code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12224 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
selection of occurrences.
We use a new function [unify_to_subterm_all] to return all occurrences
of a lemma and produce the rewrite depending on a new [conditions] option
that controls if we must rewrite one or all occurrences and if the side
conditions should be solved or not for a single rewrite to be successful.
[rewrite*] will rewrite the first occurrence whose side-conditions are
solved while [autorewrite*] will rewrite all occurrences whose
side-conditions are solved.
Not supported by [setoid_rewrite] yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12218 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
rewriting lemma more precisely. This should make rewrite properly fail
when existentials are around instead of giving an identical goal up to
new evars. Also a first step towards adding occurences to the leibniz
rewrite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12192 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This commit concerns about the first half of the useless code
mentionned by Oug for coqtop (without plugins). For the moment,
Oug is used in a mode where any elements mentionned in a .mli
is considered to be precious. This already allows to detect and
remove about 600 lines, and more is still to come.
Among the interesting points, the type Entries.specification_entry
and its constructors SPExxx were never used. Large parts of cases.ml
(and hence subtac_cases.ml) were also useless.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Choose one of the possible instances of an evar when considering
remaining unification constraints: otherwise we just do nothing and
some evars remain uninstantiated.
- Normalise the goal w.r.t. evars before subst, to avoid a double vision
problem: the substituted variable appears only in an instance of an evar
and when we try the rewrite it has been substituted making the dependency
disappear.
- Hack to correcly handle let-in annotations which are internalized as
casts: they're really typing constraints. Shouldn't we just change the
AST to have the type at rawconstr let-in nodes?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11998 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
now works correctly, "unfold foo at 4 in H at 3" now fails correctly,
etc.). The terminology for clauses (though I don't find the term
"clause" very intuitive after all) is mostly preserved except for
"simple_clause" which becomes a light form of "clause" instead of
being an atom of clause (what played the role of "simple_clause" is
now called "goal_location" - better names are welcome).
Main changes are in tacticals.ml and tactics.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11981 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11980 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par Evd). Ça s'accompagne de quelques autres modifications de
l'interface (certaines fonctions étaient des doublons, ou des
conversions entre evar_map et evar_defs).
J'ai modifié un peu la structure de evd.ml aussi, pour éviter des
fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai
introduit des sous-modules pour les différentes couches.
Il y a à l'heure actuelle une pénalité en performance assez sévère (due
principalement à la nouvelle mouture de Evd.merge, si mon diagnostique
est correct). Mais fera l'objet de plusieurs optimisations dans les
commits à venir.
Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un
appel de Decl_proof_instr.mark_as_done visiblement, je suis pour
l'instant incapable de comprendre ce qui cause cette erreur. J'espère
qu'on pourra le déterminer rapidement.
Ce commit est le tout premier commit dans le trunk en rapport avec les
évolution futures de la machine de preuve, en vue en particulier
d'obtenir un "vrai refine".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unplugged a long time ago.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11798 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
identity. Add notations for compatibility and support for
understanding these notations in the ml files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11729 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
the inductive status of a projectable position comes from a
dependency).
- Improved doc of the stdlib chapter (see bug #2018), and fixed tex
bugs introduced in r11725.
- Applied wish #2012 (max_dec transparent).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11728 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
automation.
- Permitted to use evars in the intermediate steps of "apply in" (as expected
in the test file apply.v).
- Back on the systematic use of eq_rect (r11697) for implementing
rewriting (some proofs, especially lemma DistOoVv in
Lyon/RulerCompassGeometry/C14_Angle_Droit.v and tactic compute_vcg in
Sophia-Antipolis/Semantics/example2.v are explicitly refering
to the name of the lemmas used for rewriting).
- Fixed at the same time a bug in get_sort_of (predicativity of Set was not
taken into account).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11717 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
effect, old cut_replacing was betaiota-normalizing, new
cut_replacing, from commit 11662, does not; turn
betaiota-normalisation into a purer and simpler whd_beta of the
abstracted rewriting predicate to the rewritten term).
- Made "induction in" more flexible when induction is on a goal variable
(accept occurrences -- even if theoretically unnecessary -- so as e.g.
not to expand occurrences that would otherwise trigger reductions -
see example in Peano.mult_succ_r).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11697 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Added "simple apply in" (cf wish 1917) + conversion and descent
under conjunction + contraction of useless beta-redex in "apply in"
+ support for open terms.
- Did not solve the "problem" that "apply in" generates a let-in which
is type-checked using a kernel conversion in the opposite side of what
the proof indicated (hence leading to a potential unexpected penalty
at Qed time).
- When applyng a sequence of lemmas, it would have been nice to allow
temporary evars as intermediate steps but this was too long to implement.
Smoother API in tactics.mli for assert_by/assert_as/pose_proof.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11662 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(if ever necessary).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11621 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Improved warning when found several path to the same file in path
[mltop.ml4, system.ml]
- Add support for "rewrite" on specific equality to true (i.e. eq_true)
[Datatypes.v, tactics]
PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11617 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
introduced by the lemma remain in the subgoals (i.e. it's really
[erewrite]).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11544 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
s'est avéré ralentir la compilation des user-contribs au final, sans
compter aussi le bug 1980 apparemment introduit par ce commit).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11505 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
abusivement sur les clauses.
Nettoyage au passage de metamap qui était utilisé à la fois pour les
substitutions de meta et pour les contextes de typage de meta.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11467 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
when one wants a particular type. Rewrite of the unification behind
[Equations], much more robust but still buggy w.r.t. inaccessible
patterns.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11399 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Correction divers messages d'erreur
- lorsque rien à réécrire dans une hyp,
- lorsqu'une variable ltac n'est pas liée,
- correction anomalie en présence de ?id dans le "as" de induction,
- correction mauvais env dans message d'erreur de unify_0.
- Diverses extensions et améliorations
- "specialize" :
- extension au cas (fun x1 ... xn => H u1 ... un),
- renommage au même endroit.
- "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize".
- "induction"
- intro des IH toujours au sommet même si induction sur var quantifiée,
- ajout d'un hack pour la reconnaissance de schémas inductifs comme
N_ind_double mais il reste du boulot pour reconnaître (et/ou
réordonner) les composantes d'un schéma dont les hypothèses ne sont pas
dans l'ordre standard,
- vérification de longueur et éventuelle complétion des
intropatterns dans le cas de sous-patterns destructifs dans induction
(par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas
le n dans le contexte),
- localisation des erreurs d'intropattern,
- ajout d'un pattern optionnel après "as" pour forcer une égalité et la
nommer (*).
- "apply" accepte plusieurs arguments séparés par des virgules (*).
- Plus de robustesse pour clear en présence d'evars.
- Amélioration affichage TacFun dans Print Ltac.
- Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu
(incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !).
- Fusion VTactic/VFun dans l'espoir.
- Mise en place d'un système de trace de la pile des appels Ltac (tout en
préservant certains aspects de la récursivité terminale - cf bug #468).
- Tactiques primitives
- ajout de "move before" dans les tactiques primitives et ajout des
syntaxes move before et move dependent au niveau utilisateur (*),
- internal_cut peuvent faire du remplacement de nom d'hypothèse existant,
- suppression de Intro_replacing et du code sous-traitant
- Nettoyage
- Suppression cible et fichiers minicoq non portés depuis longtemps.
(*) Extensions de syntaxe qu'il pourrait être opportun de discuter
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11279 85f007b7-540e-0410-9357-904b9bb8a0f7
|
