aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-10-07iff and impl are now declared as transitive relations.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6192 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-06majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6190 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@6188 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-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6182 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6181 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-04majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6177 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-04Added "as ..." parameter to Add Morphism.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6176 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-04un paquet de corrections de bugsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6175 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6174 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6173 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-10-01add_setoid has a new parameter used to synthesize the morphism name.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6170 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-01Added "as ..." parameters to "Add Setoid"sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6169 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-01The "Add Setoid" command now has a new argument "as name" that is usedsacerdot
to generate the name of the morphism. Previously the name was automatically generated, but this behaviour was not compatible with module typing: it was not possible to generate the same identifier in the module type and in the module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6168 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6167 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-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6161 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
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-29impl relation and impl/and/or/not morphisms over impl declared.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6153 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-29Test updated.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6150 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-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6147 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6146 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-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6144 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 02:18:05 +0000