aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2004-09-29Hugly temporary notationsacerdot
Add Morphism constr @ arugments_list @ output as name replaced with the nicer (stable?) notation Add Morphism constr with signature signature as name git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6149 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29The quoting function is now 100% complete.sacerdot
[ Note: untested, since the source of uncompleteness fixed is extremely unlikely to happen and it never happens in my test cases. ] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6148 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-28The quoting function is now almost complete (in the sense that it can findsacerdot
multiple solutions). Since several solutions are observationally equal (i.e. they open the same new set of goals), they are identified by the tactic. In case of multiple non observationally equal solutions, the list of them is presented to the user and the first one is randomically chosen. The user should be given a possibility to choose. Still todo: making the quoting function completely complete. Note: the wf_unifty_to_subterm is now called twice. The first time is not modulus delta conversion (the reasonable choice). The second time is modulus delta conversion and the call is made iff the first call failed. This is required by Ring that exploits the delta conversion ;-( git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6145 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-27The quoting function of the reflexive tactic is now sound: all the termssacerdot
that it generates are well-typed Coq terms. A limited form of backtracking is used to avoid non well-typed choices. The function is not complete yet (since the backtracking algorithm is incomplete). This will be fixed shortly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6143 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-27corrected bug when lhs is matched w.r.t deltabarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6140 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-25- Prise en compte de Fail n (n>0) dans plusieurs cas qui avaientherbelin
disparus dès la version 1.11 de proofs/tacinterp.ml - Prise en compte du contexte de filtrage sous-terme du but dans 'match goal with' quand des hypothèses aussi sont filtrées ce qui avait disparu dans la version 1.56 de proofs/tacinterp.ml - Restauration du filtrage sous-terme dans 'match c with' qui avait disparu dans la version 1.27 de tactics/tacinterp.ml - Nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6132 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-24New: (temporary) concrete syntax to specify the morphism signature:sacerdot
"Add Morphism m @ arg1 ... argn @ out as ident" where argi = constr arrow and arrow = "-->" | "++>" | "==>" (for contravariant, covariant and bi-variant morphisms). The syntax should be improved by getting rid of the "@" and maybe choosing better symbols to represent the arrows. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6129 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-24Simplifications concommitantes à la correction du bug #855herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6126 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-24Correction bug report #855herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6125 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-17restructuration des printers: proofs passe avant parsingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-15hiding the meta_map in evar_defsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-15put empty_env in hint clause (vo were becoming huge!)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6108 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-14evar tactic bugfixcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6105 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-13* The ML tactic is now also aware of rewriting directions.sacerdot
* Code clean-up. * Preparation for the last implementation phase. The last implementation phase will consist in the algorithm that, performing backtracking, chooses the right combination of morphisms in the syntactic representation of the goal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6103 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-13The ML part of the tactic now knows about covariant and contravariant morphismsacerdot
arguments. However, it still does not know about rewrite directions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6102 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-12inclusion de meta_map dans evar_defsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-10simplification de clenvbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6096 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-10Dead code removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6095 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-101. add_new_morphism now has a new optional argument that is the signaturesacerdot
2. partial setoids (a.k.a. areflexive relations) are now properly supported 3. the first two arguments of proj2 in the proof term have been simplified to be just the mutual coimplication of the old and the new goal. 4. code simplification git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6094 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-10add_new_morphism has now a new argument that is the signaturesacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6093 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-10Add_new_morphism has now a new optional argument that is the signature ofsacerdot
the morphism. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6092 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08unification encore...barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08* cleaning/renaming in Setoids.vsacerdot
* the data type for relations has been extended to cover all the cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6084 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08The Coq part of the reflexive part can now deal with irreflexive relations too.sacerdot
In particular it can deal with partial setoids (also called typoids). The latter feature was request by Marco Maggesi. This commit is just a porting of the ML part of the tactic to the new Coq part. It does not allow to exploit the new potentialities, yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6080 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-07* The Coq part of the reflexive tactic setoid_rewrite is generalized tosacerdot
asymmetric relations thanks to the introduction of morphisms that are covariant or contravariant in their arguments. * The ML part of the tactic is updated only for backward compatibility: it is still not possible to benefit from the asymmetric relations and relative morphisms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6070 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03premiere reorganisation de l\'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03New reflexive implementation of setoid_rewrite. The new implementationsacerdot
introduces a few backward incompatibilities: 1. setoid_replace used to try to close the new goal using full_trivial. The new implementation does not try to close the goal. To fix the script it is sufficient to add a "; [ idtac | trivial ]." after every application of setoid_replace that used to generate just one goal. 2. (setoid_replace c1 c2) used to replace either c1 with c2 or c2 with c1 (if c1 did not occur in the goal). The new implementation only replaces c1 with c2. To fix the script it is sufficient to replace (setoid_replace c1 with c2) with (setoid_replace c1 with c2) || (setoid_replace c2 with c1) in those cases where it is unknown what should be substituted with what. 3. the goal generated by the "Add Morphism" command has the hypothesis permutated w.r.t. the old implementation. I.e. the old implementation used to generate: forall x1 x2, forall x3 x4, x1=x2 -> x3=x4 -> ... whereas the new implementation generates forall x1 x2, x1=x2 -> forall x3 x4, x3 = x4 -> ... Fixing the script is usually trivial. 4. the "Add Morphism P" command used to generate a non-standard goal in the case of P being a predicate (i.e. a function whose codomain is Prop). In that case the goal ended with an implication (instead of ending with a coimplication). The new implementation generates a standard goal that ends with a coimplication. To fix the script you can add the following line at the very beginning: cut <<old_goal>>; intro Hold; split; apply Hold; assumption || (symmetry;assumption). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6049 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03New command "Add Relation ..." (for the new implementation of setoid_*).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6048 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Calling setoid_rewrite on a term H whose type (eq x y) was not an applicationsacerdot
of a setoid equality was erroneously considered an assertion failure instead of an user error. Note: in this case the tactic should try the rewrite tactic. However, since rewrite recursively calls setoid_rewrite in this case, this solution can diverge. This will be fixed in a future commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6028 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03Protection contre un indice d'evar égal à 0herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6015 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-30Protection erreur find_eq_data dans decompEqThen et uniformisation messages ↵herbelin
d'erreur, et généralisation onNegatedEquality git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6000 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23Major bug fixing and improvement of the setoid_{replace,rewrite} tactics:sacerdot
1. setoid and morphisms declaration were used to become in scope only when a module is imported (and to disappear when a module is closed). Thus it was possible to declare a setoid in a module A; a morphism on it in a module B that imports A; and to write a module C that imports B (but not A) that uses the morphism. Since the morphism is in scope but the setoid isn't this was a source of bugs. Fixed by making the setoid/morphisms declaration always in scope (i.e. they become in scope when the module is loaded, not when it is imported). 2. since it is possible to define different setoids for the same type / different morphisms on the same function in separate modules and since it is possible to import them at once, we must allow the possibility to have more than one setoid for each type and more than one morphism for each function. The data structures of the tactic has been completely revised to allow this possibility. Right now warnings are used to highlight situations when an ambiguity is arised. In the near future syntax will be added to disambiguate the situation, and smart algorithms to find the right interpretations when more than one applies but only a few are succesfull. For the moment the choice of the interpretation (i.e. the association of a morphism to each function in the goal) is already done before the actual start of the tactic (in order to allow a modular implementation of the choice of the interpretation). 3. the tactic used to work only in those situations where all the functions involved in the path(s) root of the term - term(s) to replace were morphisms. In the case where they are simple functions (i.e. the ``default setoid'' is Leibniz) the tactic failed. These cases are now considered by making the setoid_replace tactic perform simple replace steps where needed. A future optimization will allow to minimize the number of replace steps. The tactic should be 100% compatible with the old tactic, but for the situations that used to fail and are now succesfull. The declaration of setoids/morphisms can now also be succesfull where it used to fail. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5972 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23Since setoid_{replace,rewrite} now uses replace there is a circularitysacerdot
involving the two modules Equality and Setoid_replace. Resolved by making equality register the replace function to the Setoid_replace module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5971 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23Setoid_replace.setoid_replace last argument (that was supposed to be alwayssacerdot
None) removed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5970 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Abstraction vis a vis de dummy_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5915 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-02syntax compatibility fixcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5861 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-30instantiate entry: constr -> lconstrcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5856 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29moved instantiate binding to extratacticscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28more evar stuffcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28Ajout de la coercion id dans context vers evaluable constant (bug #777)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5841 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-26effective evar refiningcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5827 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02bug #787 de Rolandbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5783 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Clarify the distinction between quantified_hypothesis and ↵herbelin
declared_or_quantified_hypothesis; fixed the interpretation of the hyp in with-bindings, intro until, simple destruct and simple induction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5782 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-07Bug mauvais sigmaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5735 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-30Terminologie plus intuitive: evaluable -> unfoldableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5716 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-31Morphismes déclarés comme Lemma pas comme Definitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5624 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30Distinction entre declarations internes (p.ex. _subproof) et declarations ↵herbelin
utilisateurs pour export xml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5609 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-18Backtrack sur commit 1.20herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5531 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 19:09:20 +0000