Change log for the metatheory library

This log does not attempt to be exhaustive list of every single change. Rather, it highlights the high-level changes that occurred between releases. The releases are listed in reverse chronological order.

20090714

  • This version should work with Ott version 0.10.16 and LNgen version 0.2.

  • The main tactics are now fsetdec, solve_notin, solve_uniq, analyze_binds, and analyze_binds_uniq. Auxiliary ones include destruct_notin and destruct_uniq.

    The new versions introduce hypotheses with more distinctive names (BindsTac, NotInTac, UniqTac, ...). This should make how they're munging the context more obvious. This should also make it less likely that their generated names will change, since they're the only tactics that generate hypotheses using these particular names.

    The new implementations are a bit cleaner. The design philosophy was to do simple, easy things, but still be generally useful. Gone are random calls to congruence, intuition, simpl_env in *, and whatnot. Goals are munged to a minimum now. For "clean-up", the tactics rely mainly on auto (taking advantage of hint declarations) and try tauto.

  • MetatheoryEnv is no longer present. The parameter inlining feature of Coq's module system makes it possible to use the AssocList library directly.
  • Many lemmas in AssocList were renamed, for the sake of a consistent naming scheme. Metatheory declares aliases for these lemmas that are more intuitive. As a partial guide to how things were renamed:
    • Facts of the form [A <-> B] → lemma name ends in _iff
    • binds_app_1 → binds_app_l
    • binds_app_2 → binds_app_r
    • binds_one_1 → binds_one
    • binds_app → binds_app_iff

20090321

  • This is the first version to support Coq 8.2. Due to changes in Coq's FSets library, previous versions of Coq are no longer supported.
  • The AtomSet library reflects changes to Coq's FSets library. The tactics defined here (e.g., atomsetdec) have been renamed in an attempt to more consistently name things.
  • The FSetWeakNotin library now supports the remove operation.
  • The ListFacts library has been simplified by removing apparently unneeded lemmas.
  • The levels for some notations have changed.

oregon08-tutorial

  • Finite sets are now implemented directly using Coq's FSets library. We no longer wrap the FSets library with an additional axiom about extensional equality. In practice, it seems that the lemma is unnecessary. Setoid rewriting seems to be sufficient.
  • The library for environments is now implemented as a generic library about association lists (AssocList). A separate signature specialized to atoms is provided (AtomEnv).

popl08-tutorial

  • Code was substantially tweaked and reorganized for pedagogical reasons.
  • The only examples included now are STLC (simply typed lambda calculus) and Fsub (System F with subtyping).
  • The distribution now includes an introduction to using Coq.

popl08-paper

  • The initial release of the library.