aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/setoid_replace.ml
Commit message (Collapse)AuthorAge
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
| | | | | | | 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
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵Gravatar herbelin2005-12-26
| | | | | | 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
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | 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
* Nettoyage suite à la détection par défaut des variables inutilisées par ↵Gravatar herbelin2005-11-08
| | | | | | ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sur le conseil de X.Leroy: x=[||] devient Array.length x=0Gravatar letouzey2005-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7305 85f007b7-540e-0410-9357-904b9bb8a0f7
* New commit to allow definitions of morphisms on relations whose carrier isGravatar sacerdot2005-05-24
| | | | | | | | | | | | 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
* Setoid_replace: improved error message when trying to replace a term in aGravatar sacerdot2005-05-19
| | | | | | | non-applicative context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7040 85f007b7-540e-0410-9357-904b9bb8a0f7
* A wish by Bas Spitters granted: a little more of unification up toGravatar sacerdot2005-05-19
| | | | | | | | 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
* Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of theGravatar sacerdot2005-01-18
| | | | | | | | 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
* Bug fixed (reported by Roland): the setoire_rewrite in tactic did not workGravatar sacerdot2005-01-17
| | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
| | | | | | | | | | | 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
* Changement dans les boxed values .Gravatar gregoire2004-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation cut_replacingGravatar herbelin2004-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6263 85f007b7-540e-0410-9357-904b9bb8a0f7
* Word "setoid" banned from the error messages. "relation" used instead.Gravatar sacerdot2004-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6255 85f007b7-540e-0410-9357-904b9bb8a0f7
* Missing check implemented (closes a bug from Bas Spitters).Gravatar sacerdot2004-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6253 85f007b7-540e-0410-9357-904b9bb8a0f7
* The morphism lemma type was simplified only in modules and not in moduleGravatar sacerdot2004-10-21
| | | | | | | types. Fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6249 85f007b7-540e-0410-9357-904b9bb8a0f7
* Error message improved.Gravatar sacerdot2004-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6248 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
* The bug already closed in revision 1.90 was reintroduced again.Gravatar sacerdot2004-10-20
| | | | | | | Closed again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6243 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proof term size reduction (again).Gravatar sacerdot2004-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6241 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Code simplification and clean-up. In particular there is no more codeGravatar sacerdot2004-10-18
| | | | | | | | | | | | | | | 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
* Code simplification and clean-up.Gravatar sacerdot2004-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6237 85f007b7-540e-0410-9357-904b9bb8a0f7
* The lem field was not computed properly for morphisms whose argument wasGravatar sacerdot2004-10-18
| | | | | | | a quantified Leibniz relation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6236 85f007b7-540e-0410-9357-904b9bb8a0f7
* The "lem" field of a morphism used to be the compatibility proof, but itGravatar sacerdot2004-10-18
| | | | | | | | | 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
* Bug fixed: relations quantified more than once where abstracted in the wrongGravatar sacerdot2004-10-18
| | | | | | | 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
* More informative error message when the tactic tries to generate a newGravatar sacerdot2004-10-18
| | | | | | | goal with metavariables in it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6233 85f007b7-540e-0410-9357-904b9bb8a0f7
* zeta flag added to reduce LetIns in a morphism type. Morphisms with localGravatar sacerdot2004-10-18
| | | | | | | 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
* Wrong comment committed. The tactic behaves correctly only when theGravatar sacerdot2004-10-15
| | | | | | | relation/morphisms are quantified using LetIns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6222 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wish of Maggesi implemented: the type of the morphism compatibility lemmaGravatar sacerdot2004-10-15
| | | | | | | | 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
* Bug fixed (reported by Maggesi): sometimes when the tactic had to generate newGravatar sacerdot2004-10-14
| | | | | | | | 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
* Code clean-up.Gravatar sacerdot2004-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6214 85f007b7-540e-0410-9357-904b9bb8a0f7
* reflexivity, symmetry, symmetry ... in e transitivity now fall-backGravatar sacerdot2004-10-14
| | | | | | | to their setoid_* counterparts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6213 85f007b7-540e-0410-9357-904b9bb8a0f7
* setoid_symmetry in ... implemented.Gravatar sacerdot2004-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6194 85f007b7-540e-0410-9357-904b9bb8a0f7
* New commandsGravatar sacerdot2004-10-07
| | | | | | | | | | | | | 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
* Now Print Setoids prints also the transitivity justification of transitiveGravatar sacerdot2004-10-07
| | | | | | | relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6191 85f007b7-540e-0410-9357-904b9bb8a0f7
* * New syntactic sugar: Add Relation ... transitivity proved by ...Gravatar sacerdot2004-10-06
| | | | | | | | | | 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
* added transitivityGravatar barras2004-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6187 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add Setoid now accepts also quantified setoids.Gravatar sacerdot2004-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6186 85f007b7-540e-0410-9357-904b9bb8a0f7
* * code clean upGravatar sacerdot2004-10-06
| | | | | | | | | * 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
* Th unification procedure has been made a bit more complete by recording theGravatar sacerdot2004-10-06
| | | | | | | number of quantifiers of a relation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6184 85f007b7-540e-0410-9357-904b9bb8a0f7
* Leibniz equality is now a quantified relation.Gravatar sacerdot2004-10-06
| | | | | | | | | | | | | | | 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
* * code simplificationGravatar sacerdot2004-10-05
| | | | | | | | | * 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
* * [ bug fixed ]: when a subterm (c x1 ... xn) it is checked whetherGravatar sacerdot2004-10-05
| | | | | | | | | | 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
* * Bug fix: in case of non dependent implications the second argument wasGravatar sacerdot2004-10-05
| | | | | | | | | | | | | | | | | | 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
* eq_constr replaced with a conversion test where possible.Gravatar sacerdot2004-10-01
| | | | | | | | | 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
* 1. added new parameter "as ..." to Add Setoid. Used to synthesize the nameGravatar sacerdot2004-10-01
| | | | | | | | | | | | | | | of the morphism. Previously the name was automatically generated, but it was impossible to generate the same name in a module type and in a module. 2. behaviour of the relation/morphism tables w.r.t. module types and functors fixed. 3. relations/setoids/morphisms can now happear in a module type. Add Morphism in a module type declares an axiom instead of starting a new proof. Add Morphism/Add Relation/Add Setoid in a module now generate objects that match those generated by the same commands in a module type. 4. error messages improved/fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6171 85f007b7-540e-0410-9357-904b9bb8a0f7
* New tacticGravatar sacerdot2004-09-30
| | | | | | | | setoid_replace ... with ... in ... [using relation ...] [generate side conditions ...] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6166 85f007b7-540e-0410-9357-904b9bb8a0f7
* New tactic [setoid_]rewrite ... in ... [generate side conditions ...].Gravatar sacerdot2004-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proof term size optimization: setoid_rewrite H where H is an application ofGravatar sacerdot2004-09-30
| | | | | | | | Leibniz equality and no side conditions are imposed by the user simply calls the rewrite tactic. This was already done for setoid_replace/replace. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6164 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-09 06:57:06 +0000