aboutsummaryrefslogtreecommitdiff
path: root/tactics/setoid_replace.ml
AgeCommit message (Collapse)Author
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
2004-10-011. added new parameter "as ..." to Add Setoid. Used to synthesize the namesacerdot
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
2004-09-30New tacticsacerdot
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
2004-09-30New tactic [setoid_]rewrite ... in ... [generate side conditions ...].sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6165 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-30Proof term size optimization: setoid_rewrite H where H is an application ofsacerdot
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
2004-09-30cutrewrite does not work with relations that are not Coq-like equalities.sacerdot
Thus it does not work for setoid relations and it can replace setoid_replace when the user wants to specify what the relation should be. To solve the problem this commit enables the syntax setoid_replace E1 with E2 using relation R ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6163 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-30setoid_replace E1 with E2sacerdot
now replaces E1 with E2 either generating the goal E1 R E2 or the goal E2 R E1 (as expected). Note: the relation R is guessed when more than one is applicable. This is not very nice, since it can guess the wrong one. Since making the tactic compute R requires much code refactoring, I would suggest the user to always use cutrewrite in place of setoid_rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6162 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29* error messages improvedsacerdot
* msg_warning no longer used (since it pretty prints the messages on the stderr and coqide does not show them). Is this a Coq bug??? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6160 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29Add Relation is now able to detect non well typed relation registrations.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6159 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29The Add Morphism command is now able to detect in advance:sacerdot
1) if the proposed morphism named has already been used 2) if the proposed signature matches the function type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6158 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:26:46 +0000