| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
| |
All the functions about Z is now in a separated file BinIntDef,
which is Included in BinInt.Z. This BinInt.Z directly
implements ZAxiomsSig, and instantiates derived properties ZProp.
Note that we refer to Z instead of t inside BinInt.Z,
otherwise ring breaks later on @eq Z.t
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
conversion.
- Fix trans_fconv* to use evars correctly.
- Normalize the goal with respect to evars before rewriting in
[rewrite], allowing to see instanciations from other subgoals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13767 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
'_a types
If there's no lambdas at the top of a constant body
and its type is functional
and this type contains type variable
and we're extracting to Ocaml
then we perform one eta-expansion to please the ML type-checker
This might slow down things, if some computations are shared
thanks to the partial application. But it seems quite unlikely to
encounter both situations (clever partial application and
non-generalizable variable) at the same time. Compcert is ok,
for instance.
As a consequence, no need for manual eta-expansion in AVL code
(and by the way MSetAVL.element wasn't a problem, it is monomorphic)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13441 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13425 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
people use the undocumented "Lemma foo x : t" feature in a way
incompatible with this activation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
This file contains low-level stuff for FSets/FMaps. Switching it to
the new version (the one using Equivalence and so on instead of
eq_refl/eq_sym/eq_trans and so on) only leads to a few changes in
FSets/FMaps that are minor and probably invisible to standard users.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12400 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
FSets, and improve it
As soon as you have a eq, a lt and a le (that may be lt\/eq, or (complement (flip (lt)))
and a few basic properties over them, you can instantiate functor MakeOrderTac
and gain an "order" tactic. See comments in the file for the scope of this tactic.
NB: order doesn't call auto anymore. It only searches for a contradiction in the
current set of (in)equalities (after the goal was optionally turned into hyp
by double negation). Thanks to S. Lescuyer for his suggestions about this tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12397 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v
In fact coqdoc was trying to recognize the end of a _emphasis_ and
hence inserted a bogus }. For the moment I've enclosed the phrase
with [ ], but this emphasis "feature" of coqdoc seems _really_
easy to broke. Matthieu ?
2) By the way, this Library document was made from latin1 and utf8
source file, hence bogus characters. All .v containing special
characters are converted to utf8, and their first line is now
mentionning this. (+ killed some old french comments and some
other avoidable special characters).
PLEASE: let's stick to this convention and avoid latin1, at least
in .v files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
pattern unification
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12202 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t)))
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
and idem for |||, thanks to a specific scope lazy_bool_scope.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10811 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As for FSetAVL vs. FSetFullAVL, preservation of the balancing of trees
is not necessary anymore for just fulfilling the Map interface. But we
still want theses proofs to exists somewhere, since they ensure the
correct efficiency of the FMapAVL operations.
In addition, FSetFullAVL also contains the non-structural,
ocaml-faithful version of compare.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10748 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* pure functions comes first, proofs are isolated in a sub-module
* lazy (&&&) = if ... then ... else true instead of strict (&&) = andb
* equal and compare done via continuations
* a more clever map2_opt suggested by B. Gregoire: no more
intermediate conversion to lists, some sub-functions can handle
trivial situations, etc.
* map2 is now done via map2_opt and another new iterator: map_option.
By the way, this map_option allows to define easily an efficient
filter function. Both map2_opt and map_option are currently not
available through FMapInterface.S, but they can be used by direct
reference to the underlying Raw module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10745 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* FSetAVL is greatly lightened : modulo a minor change in bal, formal
proofs of avl invariant is not needed for building a functor
implementing FSetInterface.S (even if this invariant is still true)
* Non-structural functions (union, subset, compare, equal) are
transformed into efficient structural versions
* Both proofs of avl preservation and non-structural functions are
moved to a new file FSetFullAVL, that can be ignored by the average
user.
Same for FMapAVL (still work in progress...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10679 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10636 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
- clarifications about Equality on maps
Caveat: name change, what used to be Equal is now Equivb
- the prefered equality predicate (the new Equal) is declared
a setoid equality, along with several morphisms
- beginning of a filter/for_all/exists_/partition section in FMapFacts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10608 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10605 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
Sequel of commit 10545 on FSetAVL. This time, no compile-time penality
since there are fewer non-structural functions in FMapAVL.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10546 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
14097)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10511 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
more general.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10295 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
subtype of the FSet Interface (and idem for FMapWeak / FMap).
1) No eq_dec is officially required in FSetWeakInterface.S.E
(EqualityType instead of DecidableType). But of course,
implementations still needs this eq_dec.
2) elements_3 differs in FSet and FSetWeak (sort vs. nodup). In
FSetWeak we rename it into elements_3w, whereas in FSet we
artificially add elements_3w along to the original elements_3.
Initial steps toward factorization of FSetFacts and FSetWeakFacts,
and so on...
Even if it's not required, FSetWeakList provides a eq_dec on sets,
allowing weak sets of weak sets.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10271 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
------------------------------------------------
See file PreOmega for more details and/or test-suite/succes/*Omega*.v
The zify tactic performs a Z-ification of your current goal,
transforming parts of type nat, N, positive, taking advantage of many
equivalences of operations, and of the positivity implied by these
types.
Integration with omega and romega:
(r)omega : the earlier tactics, 100% compatible
(r)omega with * : full zify applied before the (r)omega run
(r)omega with <types>, where <types> is a sub-list of {nat,N,positive,Z},
applies only specific parts of zify (btw "with Z" means take advantage
of Zmax, Zmin, Zabs and Zsgn).
As a particular consequence, "romega with nat" should now be a
close-to-perfect replacement for omega. Slightly more powerful, since
(forall x:nat, x*x>=0) is provable and also slightly less powerful: if
False is somewhere in the hypothesis, it doesn't use it.
For the moment zify is done in a direct way in Ltac, using rewrite
when necessary, but crucial chains of rewrite may be made reflexive
some day.
Even though zify is designed to help (r)omega, I think it might be
of interest for other tactics (micromega ?). Feel free to complete
zify if your favorite operation / type isn't handled yet.
Side-effects:
- additional results for ZArith, NArith, etc...
- definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope
- romega now start by doing "intros". Since the conclusion will be negated,
and this operation will be justified by means of decidability, it helps
to have as little as possible in the conclusion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10028 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
(A:Type) instead of a (A:Set).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9863 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9861 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8985 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
+ bug correction in proof of structural principles
+ up do to date test-suite/success/Funind.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8899 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
The old version is, for now, still available by prefixing any command/tactic with Old/old (eg. old functional induction ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8881 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
* quelques unfold E.eq en cas de changement de la semantique des foncteurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8876 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
-> OrderedTypeEx: des exemples de OrderedType
-> OrderedTypeAlt: une definition alternative de OrderedType
-> FSetAVL et FMapAVL: realisation a coup d'AVL
-> FMapPositive: realisation a coup d'arbre binaire
(selon les chiffres binaires de la cle)
-> FMapIntMap : realisation en utilisant IntMap
-> FSetToFiniteSet: un ensemble de FSet est un ensemble de Ensemble.v
FSetAVL et FMapAVL prenent 30 secondes chacuns sur ma machine:
on peut ne pas les compiler en passant l'option "-fsets no" a
configure, de facon similaire a "-reals no"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8773 85f007b7-540e-0410-9357-904b9bb8a0f7
|