aboutsummaryrefslogtreecommitdiff
path: root/tactics/setoid_replace.ml
AgeCommit message (Collapse)Author
2004-09-29New syntaxsacerdot
"setoid_rewrite dir term generate side conditions constr_list" to specify a list of side conditions that must be a subset of the generated new goals. Used to disambiguate in case of multiple set of generated side conditions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6157 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29The Prod special case works only when the premise is of type Prop.sacerdot
This is now checked. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6156 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-291. major code clean-up for the Prod casesacerdot
2. cleaner behaviour: occurrences of the pattern in the type of a variable bound by a dependent product are no longer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6155 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29impl is a reflexive relation (it used to be areflexive).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6154 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-291) bug fixed: new goals where compared according to the relation argumentssacerdot
only. Now the head of the relation is used to. 2) much nicer pretty-printing of the multiple set of side conditions that the tactic can now produce git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6152 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29The list of possible solutions proposed by the tactic cannot contain anysacerdot
longer two set of goals such that the first is a subset of the second. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6151 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-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-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-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-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-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-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 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
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui ↵herbelin
passent donc de Termops a Constrintern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4980 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Affichage des buts par Pfedit pour utilisation par les tactiques ↵herbelin
(Setoid_replace) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4562 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Indépendance vis à vis de Declareherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4372 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout d'un message à FailTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
idem pour ex et exT, ex2 et exT2, all et allT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Correction bug réecriture à la racine pour le sétoide Prop.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3584 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Ajout Simpl et Change sur des sous-termesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3392 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-23Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Localherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3179 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01bug de noms long pour eqT.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3053 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Que des niveaux d'univers frais dans le type des constantes globalesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3045 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14Changement de eq en eqT comme equivalence de setoide par defaut.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2679 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-02Minor correction of get_lem_namecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2664 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04Nouveau Rewrite-in plus economiquebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:29:10 +0000