aboutsummaryrefslogtreecommitdiff
path: root/tactics/setoid_replace.ml
AgeCommit message (Collapse)Author
2006-06-06reparation pour le bug #1072 (soufflee par J. Forest): letouzey
protection d'un list_chop pour couvrir le cas d'une application partielle de morphisme. accessoirement, il faudrait comprendre un jour pourquoi setoid replace inspecte (and True) dans le terme (map (and True) True <-> A) si on lui dit de reecrire A en autre chose... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8900 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-05encore un correctif sur le rewrite H in setoid: letouzey
si H: a==b, alors ce rewrite echouait lorsque a apparait dans b ou b dans a. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8788 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Standardisation nom option_app en option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-05resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses letouzey
avec des equivalences parametrees (genre forall n, P n <-> Q n) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8683 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28Réorganisation de la structure interne des types de déclarations (decl_kinds)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵herbelin
G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-02Changement des named_contextgregoire
Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par ↵herbelin
ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7305 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-24New commit to allow definitions of morphisms on relations whose carrier issacerdot
a Prod. Example: m : feq ==> feq where m has type (A -> B) -> (C -> D) and few is a relation over (fun X Y: Type. X -> Y). The problem is to avoid the interpretation (A -> B) -> C -> D that tries to use feq over D and feq over C considering (A -> B) as a quantification. This closes a wish of Bas Spitters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7068 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-19Setoid_replace: improved error message when trying to replace a term in asacerdot
non-applicative context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7040 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-19A wish by Bas Spitters granted: a little more of unification up tosacerdot
convertibility is now tried in setoid_rewrite. As a consequence it is now possible to declare relations over the function space (fun A B: Type => A -> B). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7039 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-18Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of thesacerdot
term to be replaced in the term that is the morphism was done too early (before computing the "morphism family" parameters). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6605 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-17Bug fixed (reported by Roland): the setoire_rewrite in tactic did not worksacerdot
in the followin case: H : t < c1 H0: c1 < c2 ============= t' setoid_rewrite H0 in H Explanation: the tactic made a cut with H0: c1 < c2 =============== t < c2 and then did setoid_rewrite <- H0 in H. If c2 occurs in t, then the tactic may fail (due to wrong variance). The simple fix consists in changing "t < c2" to "let H := c2 in t{H/c2} < c2" and then perform an intro before proceeding. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6601 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
the new module kernel/mod_subst.ml. MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now possible to define substitutions that also delta-expand constants (by associating the delta-expanded form to the constant name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-12Changement dans les boxed values .gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-27Factorisation cut_replacingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6263 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-25Word "setoid" banned from the error messages. "relation" used instead.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6255 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-25Missing check implemented (closes a bug from Bas Spitters).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6253 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-21The morphism lemma type was simplified only in modules and not in modulesacerdot
types. Fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6249 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-21Error message improved.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6248 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20The bug already closed in revision 1.90 was reintroduced again.sacerdot
Closed again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6243 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-19Proof term size reduction (again).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6241 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18* Code simplification and clean-up. In particular there is no more codesacerdot
duplicated between add_relation and add_setoid. * Less ad-hoc backward compatibility lemmas for setoids required in Setoid.v * Term size reduction (first part): when a relation is registered, we add to the environment a definition that gives back either the relation as an argument or as a relation class. The definition is used to reduce the term size. [ Note: we could save a bit more by defining two definitions in place of one. However, we suppose that the lambda term fragments generated can be shared quite effectively. Thus we would recive almost no benefit by sharing in terms of size. What about proof checking time? ] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6238 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18Code simplification and clean-up.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6237 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18The lem field was not computed properly for morphisms whose argument wassacerdot
a quantified Leibniz relation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6236 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18The "lem" field of a morphism used to be the compatibility proof, but itsacerdot
became the whole structure of type Morphism_Theory. A new field morphism_theory has now been added to record both informations. Print Setoids now prints again the right information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6235 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18Bug fixed: relations quantified more than once where abstracted in the wrongsacerdot
order (and thus they were not accepted). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6234 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18More informative error message when the tactic tries to generate a newsacerdot
goal with metavariables in it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6233 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18zeta flag added to reduce LetIns in a morphism type. Morphisms with localsacerdot
definitions in their types are now accepted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6232 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-15Wrong comment committed. The tactic behaves correctly only when thesacerdot
relation/morphisms are quantified using LetIns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6222 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-15Wish of Maggesi implemented: the type of the morphism compatibility lemmasacerdot
is now the one that is shown to the user (and not only convertible to it). In this way it is possible to register the lemma in the Hint database. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6217 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-14Bug fixed (reported by Maggesi): sometimes when the tactic had to generate newsacerdot
existential variables it failed. Fixing by propagating the metavariable environment generated by the unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6215 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-14Code clean-up.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6214 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-14reflexivity, symmetry, symmetry ... in e transitivity now fall-backsacerdot
to their setoid_* counterparts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6213 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07setoid_symmetry in ... implemented.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6194 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07New commandssacerdot
setoid_reflexivity setoid_symmetry setoid_transitivity The command setoid_symmetry in ... is not implemented yet (it behaves just as symmetry in ... for now). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6193 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07Now Print Setoids prints also the transitivity justification of transitivesacerdot
relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6191 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06* New syntactic sugar: Add Relation ... transitivity proved by ...sacerdot
now declares both the relation and the relation as a morphism, computing the appropriate signature (depending on the reflexivity of the relation). * New parameter "as ..." to Add Relation (to be able to compute the morphism name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6189 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06added transitivitybarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6187 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06Add Setoid now accepts also quantified setoids.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6186 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06* code clean upsacerdot
* check for dependent functions reimplemented correctly (closing a long standing bug that was already in the original implementation by Clement Renard) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6185 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06Th unification procedure has been made a bit more complete by recording thesacerdot
number of quantifiers of a relation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6184 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06Leibniz equality is now a quantified relation.sacerdot
This means that you can declare a morphism signature that has an argument (or its output type) that is just eq. E.g.: Add Morphism incl with signature incl --> eq ++> impl. is a correct signature for a morphism property of type forall A, list A -> list A -> Prop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6183 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-05* code simplificationsacerdot
* error message improved * bug fixed: it was not checked whether the carrier of a relation of class Leibniz matched the expected type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6180 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-05* [ bug fixed ]: when a subterm (c x1 ... xn) it is checked whethersacerdot
there exists an i such that (c x1 ... xi) is a morphism. Previously only the case c was tried. * [ bug fixed ]: the term that must be replaced must not occur in c (i.e. in (c x1 ... xi)) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6179 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-05* Bug fix: in case of non dependent implications the second argument wassacerdot
not correctly de-lifted. * [EXPERIMENTAL]: the Add Relation and Add Morphism commands now accept also quantified relations and quantified morphisms. [ Add Setoid doesn't do that yet. ] However, in case of quantified relations the matching between an argument type and the (quantified) carrier expected for it is quite weak and is complete only not modulus conversion. * Many bugs have probably been introduced by the experimental feature. However, the bugs should manifest only in the case of quantified relations. In particular Leibniz has a strange status and its management should be revised. * Open problem: should the data type for relations and morphisms be changed to explicitly show the quantifications? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6178 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-01eq_constr replaced with a conversion test where possible.sacerdot
This is particular useful in case of modules (when it often happens to have two setoids that can be composed only up to convertibility of their input/output types). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6172 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-27 04:22:07 +0000