aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2010-03-07Fix lifting of constraints in generalized rewriting tactic.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12850 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-06Fixes in rewrite and a Elimination/Case to Scheme:msozeau
- disallow dynamic generation of [case] constructs through [find_scheme] during a rewrite, as it changes the global environment and subsequent manipulations of the tactic may use an outdated environment. - use local exception names so as not to catch and hide unexpected [Not_found] exceptions. - fix lifting of constraints for dependent function types - Allow rewriting on morphisms (terms in function position) even with [rewrite] (fixes bug #2178). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12848 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-05Improvements in generalized rewriting:msozeau
- support a new strategy: reduction using any of the allowed reduction operators. This strategy does _not_ make the proof size grow. - support rewriting under arbitrary [match with] using a folding strategy. We fold matches to applications of registered [case] combinators and let the user declare the Proper instances for them. - fix the lemma application strategy to correctly report when no progress has been made (avoids loop when repeateadly rewriting with convertible terms). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12844 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-05Fix [autounfold] to accept general [in] clauses.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12843 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-05Add a generic tactic option builder. Use it in firstorder to set themsozeau
default solver (using "Set Firstorder Solver") and for program's obligation tactic. I don't understand exactly the reason of the warning when building states/initial.coq, anyone? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12842 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-10Fix [Existing Class] impl and add documentation. Fix computation of themsozeau
dependency order of obligations that was not backwards-compatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12719 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-30Update CHANGES, add documentation for new commands/tactics and do a bitmsozeau
of cleanup in tactics/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12705 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-26Support for generalized rewriting under dependent binders, using themsozeau
[forall_relation] combinator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12693 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-26Quick fix for references to section variables unbound in the currentmsozeau
environment during unification. Should be checked earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12692 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12New version of 12650 that was broken (supporting again records whenherbelin
descending dependent conjunctions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12658 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12Added module sharing support for typeclasses and hints (pri_auto_tactic).soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12655 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12revert commit 12650 for the moment, since it breaks MSetAVLletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12651 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-12Temporary fix to compensate the loss of descent on dependentherbelin
conjunctions (defined records now supported again but not unregistered ones). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12650 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-30Fixing bug #2146 (broken selection of occurrences in "change").herbelin
In trunk the different possible combinations of "at" and "in" with occurrences are taken into account. In 8.2 branch, it remains fragile (syntaxes that were accepted remain accepted and a message warns if the occurrences coming after the "with" are not taken into account). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12614 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-29Improving descend_in_conjunctions (using a combinators instead of a tactic)herbelin
what allows to better control position of side-conditions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12612 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-28Safer, though ad hoc, approach to re-interpretation of the argument ofherbelin
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
2009-12-27Fix "Existing Instance" to handle globality information and "Existingmsozeau
Class" too to handle references instead of just idents. Minor fix in coqdoc. zeta-normalize setoid_rewrite proofs, removing useless let-bindings generated by the tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12609 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-24Opened the possibility to type Ltac patterns but it is not fully functional yetherbelin
- to type patterns w/o losing the information of what subterm is a hole would need to remember where holes were in "understand", but "understand" needs sometimes to instantiate evars to ensure the type of an evar is not its original type but the type of its instance (what can e.g. lower a universe level); we would need here to update evars type at the same time we define them but this would need in turn to check the convertibility of the actual and expected type since otherwise type-checking constraints may disappear; - typing pattern is apparently expensive in time; is it worth to do it for the benefit of pattern-matching compilation and coercion insertion? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12607 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-23Moved a bit further the code for pattern interpretation in match goalherbelin
to anticipate support of possibly-typed patterns; Also removed a useless nf_evar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12606 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-21Generic support for open terms in tacticsherbelin
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
2009-12-19Backtrack on making exact hints for lemmas starting with productsmsozeau
(e.g. transitivity lemmas) and fix bug #2207, avoiding the generation of useless eta-redexes during type class instance resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12600 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-16adding an option functional_induction_rewrite_dependent to make functional ↵jforest
induction using not v8.2 version of subst. By default functional induction uses new version of subst git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12592 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-14Improved strategy for rewriting lemma possibly depending because of evars.herbelin
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
2009-12-13Made the side-conditions of lemmas always come last when chaining "apply in"herbelin
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
2009-12-13Completion of r12580 (better rendering of dependent rewrite and inversion).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12583 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-13Revision 12557 continued (better rendering of dependent rewrite)herbelin
(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
2009-12-12Updated compatibility for rewriting equality proofs that are dependentherbelin
- 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
2009-12-12Improved the rendering of "dependent rewrite" and hence of "inversion"herbelin
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
2009-12-06Turn evars created by a tactic application into a subgoal immediately inmsozeau
typeclass resolution. Makes the backtracking heuristic correct again and avoids "late" backtracking on an unsolvable existential. Compilation time is back to normal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12564 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-06Fix anomaly when using typeclass resolution with filtered hyps in evars.msozeau
Make setoid_rewrite-through-rewrite's selection of occurences more robust: do not try unification with reduction if not needed. This changes a few scripts that were using reduction in a far from obvious way and could break more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12562 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-03Restored rewriting of JMeq using JMeq_rect and co when the domains are the sameherbelin
(this was lost since revision 12481). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12560 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-01Fix make_exact_entry to allow applying [forall x, P x] hints directly,msozeau
avoiding the introduction of eta-redexes. Prioritize hints over intros in typeclass resolution to profit from that. Add a minor fix in coqdoc by F. Garillot. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12550 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-01Fix bug in typeclass resolution. Better handling of universes inmsozeau
the generalization tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12548 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-30Fix backtracking heuristic in typeclass resolution. msozeau
Now that backtracking is working correctly, we need to avoid a non-termination issue introduced by the [RelCompFun] definition in RelationPairs, by adding a [Measure] typeclass. It could be used to have a uniform notation for measures/interpretations in Numbers and be but in the interfaces too, only the mimimal change was implemented. Fix syntax change in test-suite scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12547 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-27Substitute terms for evars-as-goals as soon as they are solved inmsozeau
typeclass resolution. Fixes a bug reported by Eelis van der Weegen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12545 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-24Minor fixes in typeclasses, avoiding repeated evar normalizations.msozeau
Improve generalization by equalities tactic, now allowing to generalize an arbitrary application, e.g. in preparation for applying an elimination principle for a function. This adds a flag to generalize_dep so that it doesn't abstract the variable if it is defined, just introducing a let-in. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12541 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-21Lazier behaviour of [auto] when introducing hypothesis: query the hint db's ↵puech
only when necessary. Hopefully should speed up [auto] a little. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12538 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12Addendum to revision 12501.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12505 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Backtracking on the use of automatically generated schemes forherbelin
"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
2009-11-10Compatibility ocaml <= 3.09herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12493 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-09Quick fix for restoring a left-to-right rewriting lemma compatibleherbelin
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
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
- 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
2009-11-06- Fix discharge bug in typeclasses: some constrs were not actuallymsozeau
discharged on the other definitions in the section. - Avoid universe problem in generalize_eqs were we could give an [@eq_refl Set x x] proof where an [@eq Type x x] was expected. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12478 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-06Misc fixes.msozeau
- Correct backtracking function of coqdoc to handle the _p fields of lexers - Try a better typesetting of [[ ]] inline code considering it as blocks and not purely inline code like [ ] escapings. - Rework latex macros for better factorization and support external references in pdf output. - Better criterion for generalization of variables in dependent elimination tactic and better error message in [specialize_hypothesis]. - In autounfold, don't put the core unfolds by default. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12474 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-04Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.gmelquio
Fixed pretty printing of record syntax. Allowed record syntax inside patterns. (Patch by Cedric Auger.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Integrate a few improvements on typeclasses and Program from the equations ↵msozeau
branch and remove equations stuff which moves to a separate plugin. Classes: - Ability to define classes post-hoc from constants or inductive types. - Correctly rebuild the hint database associated to local hypotheses when they are changed by a [Hint Extern] in typeclass resolution. Tactics and proofs: - Change [revert] so that it keeps let-ins (but not [generalize]). - Various improvements to the [generalize_eqs] tactic to make it more robust and produce the smallest proof terms possible. Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with [generalize_eqs]. - A few new general purpose tactics in Program.Tactics like [revert_until] - Make transitive closure well-foundedness proofs transparent. - More uniform testing for metas/evars in pretyping/unification.ml (might introduce a few changes in the contribs). Program: - Better sorting of dependencies in obligations. - Ability to start a Program definition from just a type and no obligations, automatically adding an obligation for this type. - In compilation of Program's well-founded definitions, make the functional a separate definition for easier reasoning. - Add a hint database for every Program populated by [Hint Unfold]s for every defined obligation constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-28Clarification in commentsglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12437 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:09:18 +0000