-----------------------------------------------------------------------------
17-01-11: RELEASE OPAM 1.3.0 for Coq 8.6 (SVN revision 2432)
17-01-11: [Vadim Zaliva]
- port to Coq 8.6
16-04-29:
- moved ListForall into ListUtil
- replaced Implicit Arguments by Arguments
16-04-28: prefix Require's by From Coq or From CoLoR to avoid problems
when installing CoLoR with other libraries
-----------------------------------------------------------------------------
16-01-26: RELEASE OPAM 1.2.0 for Coq 8.5 (SVN revision 2394)
16-01-26:
- moved to Coq 8.5
16-01-20:
- Util/Relation/Tarski: proof that the least fixpoint can be reached by transfinite induction; corresponding induction principle; fixpoint on a sig type
16-01-12:
- Util/Nat/BoundNat: added vector of bounded natural numbers
16-01-06:
- Util/FMap/FMapUtil: Make now takes an FMapInterface.S as argument;
moved parts of LSimple into a Domain submodule taking an FSetInterface.S
as argument
15-05-05:
- Term/Lambda/LEta: eta-reduction
- Term/Lambda: extended all termination results to eta-reduction
15-04-30:
- Util/FSet/FSetUtil: added replace
- Term/Lambda/LSubs,LAlpha:
. generalized seq and saeq by introducing subs_rel
. added subs_rel_mon_preorder and sub_rel_mon_preorder_aeq
15-03-27:
- Util/Logic/LogicUtil: added split_all tactic
- reduced compilation time by improving some scripts
CoLoR without Coccinelle now compiles in:
-j1: 17'53" instead of 22'16" (-21.0%)
-j3: 7'16" instead of 9'21" (-21.5%)
-j20: 4'43" instead of 6'28" (-26.9%)
CoLoR with Coccinelle now compiles in:
-j1: 22'18" instead of 27'00" (-17.4%)
-j3: 8'48" instead of 10'47" (-18.6%)
-j20: 5'27" instead of 6'45" (-18.5%)
- Util/Option/ExcUtil: renamed into OptUtil
- Util/Nat/NatLt: renamed into BoundNat
- Util/Pair/LexOrder: renamed into PairLex
- Util/List/LexicographicOrder: renamed into ListLex
- Util/Nat/NatLeast: renamed into LeastNat
15-03-19:
- replaced Add Relation/Morphism by Instance everywhere
- Util/Nat/BoundNat:
. replaced bnat by N and nfirst_nats by L
. renamed and moved everything into NatLt
- removed Emacs local variables in Coccinelle
15-03-15:
- Util/List/ListRepeatFree: renamed into ListNodup,
make_repeat_free renamed into remdup, repeat_free renamed into nodup
- Util/Relation/RelExtras: moved things to RelUtil and ExcUtil
-----------------------------------------------------------------------------
15-03-10: RELEASE OPAM 1.1.0 for Coq 8.4 (SVN revision 2156)
15-03-10:
- Util/Set/Ramsey: classical infinite Ramsey theorem
- Util/Set/FinSet: new file defining finiteness and providing finiteness lemmas
- Util/Set/InfSet: new file defining infiniteness
and providing infiniteness lemmas
- Util/List/ListUtil: added select, pos, new lemmas on remove,
and renamed mk_nat_lts into L
- Util/List/ListRepeatFree: added new lemmas
- Util/Nat/NatUtil: added smallest natural satisfying some property,
and renamed nat_lt into N
- Util/Set/SetUtil: added new definitions and lemmas
- Util/Nat/NatLt: new file gathering old and new results about natural numbers
smaller than some fixed bound (type N and function L)
-----------------------------------------------------------------------------
15-02-04: RELEASE OPAM 1.0.0 for Coq 8.4 (SVN revision 2104)
14-12-29: [Strub]
- Util/Vector/VecUtil: Vcast defined by matching on the equality proof argument
(like eq_rect) instead of on the vector argument
14-02-19:
- Util/Vector/VecOrd: Vreln moved into VecUtil
- Util/Vector/VecEq: moved into VecOrd
14-01-28:
- Term/Lambda/LAlphaAlt: added Gabbay and Pitts definition of alpha-equivalence
-----------------------------------------------------------------------------
13-12-03: NEW RELEASE (SVN revision 2023)
13-10-04:
- Term/Lambda/LAlphaAlt: definitions of alpha-equivalence by Church and
Krivine, and proof that they are equivalent to the one of Curry and Feys
-----------------------------------------------------------------------------
13-09-20: NEW RELEASE (SVN revision 2003)
13-09-20:
- Term/lambda/LSystemT: definition and termination proof of Goedel System T
- Util/Relation/OrdDec replaced by Util/Relation/OrdUtil
-----------------------------------------------------------------------------
13-09-16: NEW RELEASE (SVN revision 1983)
13-09-13:
- Term/Lambda/LCompClos: computability closure and proof that its ensures
termination of higher-order rewrite systems
- Term/Lambda/LCompRewrite: higher-order rewriting
and its associated CP structure
- Term/Lambda/LCall: lexicographic ordering on partial function calls
- Term/Lambda/LCompInt: interpretation of positive inductive types
as computability predicates
13-08-14:
- Term/Lambda and Util: various additions
13-08-02:
- Util/Relation/Tarski: Knaster-Tarski theorem
13-06-05:
- Term/Lambda: reorganized definitions so that Inductive's and various
functions including substitution are defined out of any module
12-11-06:
- Util/Relation/SN: added proof that SN -> ~NT following
http://www.labri.fr/perso/casteran/CoqArt/gen-rec/SRC/not_decreasing.v
- removed IS_NotSN_FB subsumed by previous result
- moved IS_NotSN into NotSN_IS
-----------------------------------------------------------------------------
12-10-23: NEW RELEASE (SVN revision 1751)
12-10-23:
- Term/Lambda/LTerm: pure lambda-terms with names variables
- Term/Lambda/LSubs: higher-order simultaneous substitutions
- Term/Lambda/LAlpha: alpha-equivalence
- Term/Lambda/LBeta: beta-reduction
- Term/Lambda/LComp: axiomatic version of Tait-Girard computability
- Term/Lambda/LSimple: typing relation with simple types
- Term/Lambda/LCompSimpl: termination of beta-reduction on simply-typed terms
-----------------------------------------------------------------------------
12-08-22: NEW RELEASE (SVN revision 1743)
12-08-22:
- migration to Coq 8.4
11-03-25:
- Util/FGraph/TransClos: transitive closure of a finite graph
- Util/FGraph/FGraph: library on finite graphs
10-11-30: [Ould-Biha]
- Term/WithArity/AInfSeq: infinite sequences
- Term/WithArity/ASubterm: the subterm relation is finitely branching
- Util/Nat/NatLeast: min of a non-empty set of nats
- Term/WithArity/ADepRel: relation on defined symbols implied by rules
10-11-24:
- Util/List/ListUtil: sub_list
- Util/Vector/VecFilterPerm: vector filtering with permutations
- Filter/AFilterPerm: non-collapsing arguments filtering with permutations
10-11-16: [Koprowski]
- MatrixInt/ATropicalInt: tropical matrix interpretations
-----------------------------------------------------------------------------
10-10-28: NEW RELEASE (SVN revision 1341)
10-10-27:
- migration to Coq 8.3
10-06-30: [Stratulat]
- added Sorin Stratulat's patch to Coccinelle's RPO for allowing a
quasi-ordering on symbols instead of an ordering
-----------------------------------------------------------------------------
09-12-07: NEW RELEASE (SVN revision 1000)
09-11-04:
- DP/ADP: use Dershowitz improvement for defining DPs
09-10-30:
- Coccinelle: Coccinelle library v8.2-bool (09-10-26)
- Conversion/Coccinelle: convert CoLoR ATerm's into Coccinelle terms
+ definition of RPO on CoLoR ATerm's using Coccinelle RPO
09-10-19:
- Conversion/String_of_ATerm: convert a unary TRS into an SRS
- Term/WithArity/AReverse: reversal of unary TRSs
09-07-08:
- SemLab/AFlatCont: flat context closure
- SemLab/ARootLab: root labeling
- MannaNess/ARedPair: rule elimination using reduction pairs,
functors building a reduction pair from a monotone algebra
or an argument filtering
09-06-26:
- Util/Set/SetUtil: infinite sets
- Term/WithArity/ARules: rewriting with infinite sets of rules
- Term/WithArity/AMorphism: extended to infinite sets of rules
- SemLab/ASemLab: theorem of semantic labeling (with ordered labels)
09-06-19:
- simplified all function definitions on terms f such that the corresponding
function on vectors is (Vmap f)
- Filter/AProj: arguments filtering with projections only
09-05-22:
- Term/WithArity/AUnary: properties of systems with unary symbols only
- Conversion/ATerm_of_String: equivalence of the well-foundedness of an SRS
and of its translation as TRS
- NonTermin/AModLoop: definition and correctness proof of a boolean function
checking that there is a loop in a relative TRS
- NonTermin/SLoop: definition and correctness proof of a boolean function
checking that there is a loop in an SRS
- NonTermin/SModLoop: definition and correctness proof of a boolean function
checking that there is a loop in a relative SRS
09-05-11: [Blanqui,Wang,Zhang]
- NonTermin/ALoop: definition and correctness proof of a boolean function
checking that there is a loop in a TRS
- NatUtil: unicity of Euclidean division
09-05-07:
- Term/WithArity/AReduct: list of reducts of a term and proof that
rewriting is finitely branching
- Term/WithArity/AMorphism: definitions and lemmas on algebra morphisms
09-05-07: [Blanqui,Wang,Zhang]
- added new definitions and lemmas on vectors (sub-vector Vsub, etc.)
- Term/WithArity/APosition: positions in a term and related functions
and relations (subterm, replacement, context, rewriting)
09-04-29:
- added (ordered) semi-rings, matrices and matrix interpretations on BigN
- removed antisymmetry and irreflexivity assumptions for ordered semi-rings
09-04-24: [Koprowski]
- added a framework for checking whether a given certificate is a correct
termination proof for a given problem. This check is done by a Coq
function (no Ltac), so it should be possible to extract from it
a certified termination proof checker.
- added support for polynomial interpretations in the new proof
checker framework.
09-04-17:
- extended semi-rings, matrices and matrix interpretations on setoids
- added boolean function for testing integer equality since the one
defined in Coq is too complex and uses an opaque lemma
09-04-13: [Strub]
- Term/WithArity/AMatching: correct and complete matching algorithm
- Util/FMap/FMapUtil: bundle for FMap definitions + properties
09-03-18:
- decidability of equality on symbols and terms are replaced
by boolean functions
-----------------------------------------------------------------------------
09-03-11: NEW RELEASE
09-01-22: [Koprowski]
- HORPO: beta-reduction included into HORPO; added examples, including
an example illustrating non-transitivity of HORPO
08-10-31:
- Term/WithArity/AUnif: termination and completeness of the syntactic
unification algorithm
- DP/ADPUnif: correctness of the over DP graph based on unification
08-08-07:
- Util/Relation/OrdDec: type totally ordered with a comparison function
- Util/List/ListDec: boolean functions on lists using a boolean equality test
- DP/ADecomp: proof that termination follows from any valid decomposition
of an over DP graph and the termination of each component
- Term/WithArity/ATrsNorm: canonical representation of lists of rules
08-05-15:
- Util/FSet/FSetUtil: lemmas and tactics on Coq FSet's
- Term/WithArity/AVariables: set of variables in a term (based on FSet)
and properties wrt substitution
- Term/WithArity/AUnif: correctness of a syntactic unification algorithm
08-03-14: [Koprowski, Waldmann]
added support for arctic matrix interpretations proofs;
unified with development on matrix interpretations
- MatrixInt/*
- Util/Algebra/SemiRing
- Util/Algebra/OrdSemiRing
08-02-13:
- Term/String/SReverse: SRS inversion preserves termination
08-01-23:
added support for boolean reasoning and boolean functions testing equality
- Util/Bool/BoolUtil
- Util/List/ListUtil
- Term/Varyadic/VTerm
07-08-23: [Lucas] added SCC decomposition (SCC = Strongly Connected Component)
- Util/List/SortUtil: lemmas on list sorting
- Util/Nat/log2: definition and properties of log2 and exp2
- Util/Nat/BoundNat: type of natural numbers smaller than some constant
- DP/AGraph: generalization of the notion of DP graph
- DP/HDE: simple over DP graph based on head symbol equality
- Util/Relation/SCC: definition of SCC and basic properties
- Util/Relation/AdjMat: adjacency matrix of a finite relation on N
- Util/Relation/GDomainBij: bijection between a set of n elements
and the set of integers 0 .. n-1
- Util/Relation/SCC_dec: decidability of SCC decomposition
- Util/Relation/SCCTopoOrdering: topological ordering on SCCs
- DP/SCCunion: termination based on SCC decomposition
07-08-06: added support for classical reasoning
- Util/Logic/ClassicUtil: basic meta-theorems of classical logic
- Util/Logic/DepChoice: axiom of dependent choice
- Util/Logic/DepChoicePrf: proof of the axiom of dependent choice
using classical logic and the axiom of choice
- Util/Relation/NotSN: properties of ~SN terms in classical logic
- Util/Relation/NotSN_IS: ~SN terms give infinite sequences
using dependent choice and classical logic
- Util/Relation/RedLength: maximal reduction length of a term
wrt a well-founded finitely branching relation
- Util/Relation/IS_NotSN: a well-founded finitely branching relation
has no infinite sequence
07-05-25:
- Term/String: strings
- Conversion/ATerm_of_String: conversion strings -> algebraic terms
07-04-25: [Koprowski,Zantema]
- MatrixInt: matrix interpretations
- Util/Matrix: matrices
- Util/Algebra/SemiRing: semi-rings
-----------------------------------------------------------------------------
07-03-22: NEW RELEASE
07-02-16:
- Simplification of the compilation procedure
- DP/ADPGraph: proof of the DP criterion based on cycles
- Util/Relation/Union: union of two well-founded relations
- Util/Relation/SN: new general lemmas on termination
- Util/Relation/Iter: iteration of a relation
- Util/Relation/Total: total completion [Le Roux]
- Util/Relation/RelDec: decidability of relations [Le Roux]
- Util/Relation/Path: paths and sub-relations [Le Roux]
- Util/List/ListOccur: number of occurrences and pigeon-hole principle
- Util/List/ListRepeatFree: smallest prefix without duplication
- Util/List/ListShrink: new functions and lemmas on lists [Le Roux]
- Term/WithArity/ARename: variable renamings
- Term/WithArity/ASubstitution: added union of two substitutions
- Term/WithArity/ARelation: results on compatibility moved to ACompat
- Util/Relation/WfUtil renamed into AccUtil
- Various lemmas renamed with intro or elim suffix
06-12-04:
- MannaNess/AMannaNess: added rule elimination for relative termination
- Acc replaced by SN in various files
- Term/WithArity/ARedOrd moved to MannaNess/AMannaNess
06-12-01:
- Various modifications for compiling with the new version of Coq
- Util/Relation/SN: inductive definition of strong normalization
(inverse of Coq accessibility)
- Util/Relation/RelUtil: practical notations and useful results
on composition, union and reflexive and transitive closures
- Term/WithArity: elimination of useless hypotheses
in AWFMInterpretation and ARedOrd
- Util/Relation/Lexico: new formalization of lexicographic ordering
with minimal hypotheses
- Term/WithArity/ATrs: rewriting modulo the transitive closure of some relation
- Term/WithArity/ARedOrd: rule elimination for relative elimination
06-07-21:
- various updates for the first release of Rainbow
- Util/Multiset: parameter eqA_dec added to functor arguments
- RPO: the module structure has been flattened
- Util/Vector: V0_eq redefined with Vcast to make it computable
(the previous version was using the axiom eq_rect_eq)
- Util/Polynom: tactics for monotony and termination [Hinderer]
-----------------------------------------------------------------------------
06-05-10: NEW RELEASE
06-05-10:
- HORPO: higher-order recursive path ordering [Koprowski]
- Term/SimpleType: simply typed lambda-terms with de Bruijn indices [Koprowski]
- Util/List: more functions and lemmas (nth element, initial segment, etc.)
- Util/Multiset: a few modifications and additions (decidability, etc.)
06-01-10:
- RPO: recursive path ordering with statuses [Coupet-Grimal,Delobel]
- Util/Multiset: additions in MultisetOrder, MultisetListOrder
- Util/List: additions in ListUtil
- Util/Relation: additions in WfUtil
- MPO/VMPO: elimination of irreflexivity hypothesis
- Util/Multiset/MultisetListOrder:
elimination of transitivity hypothesis in HAccTermsToTermlist
- Util/List: creation of LexicographicOrder
- Util/Relation: creation of Preorder
05-12-06:
- Conversion/VTerm_of_ATerm: conversion from algebraic terms to varyadic terms
- Term/Varyadic: creation of VContext, VSubstitution, VTrs
05-10-07:
- MPO: multiset path ordering [Coupet-Grimal,Delobel]
- Term/Varyadic: terms without arity
- Util/Multiset: creation of MultisetListOrder
- Util/Multiset: proof of Acc_iso in MultisetAuxiliary
- Util: additions in Multiset
05-09-19:
- License: CeCILL version 2
- Util/Multiset: finite multisets and proof that the multiset extension
of an ordering preserves well-foundedness [Koprowski]
- Util: creation of Bool/BoolUtil, Pair/PairUtil, Logic/EqUtil
- Util: additions in ListUtil, LogicUtil
05-06-10:
- Filter: arguments filtering
- Term/WithArity: bug fixed in ARedOrd.v/manna_ness2
- Term/WithArity: renamings in ARelation
- Term/WithArity: additions in ARelation, ASubstitution, ATrs, ARedOrd
- Util/Vector: creation of VecBool, VecFilter
- Util: additions in LogicUtil, NatUtil, RelUtil, WfUtil, VecUtil
-----------------------------------------------------------------------------
05-03-14: NEW RELEASE
05-03-14:
- Util/Vector: library on vectors
- Util/Polynom: library on integer polynomials with multiple variables
- Term/WithArity: library on algebraic terms with symbols of fixed arity
- PolyInt: proof of the termination criterion based on polynomial
interpretations [Hinderer]
- DP: proof of the fundamental dependency pairs theorem