| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6241 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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 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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6187 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6170 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6165 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
| |
"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
|
| |
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
"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
|
| |
|
|
|
|
|
| |
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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6093 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
| |
|
|
|
|
| |
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
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1843 85f007b7-540e-0410-9357-904b9bb8a0f7
|
herbelin
sacerdot
barras
clrenard