Metalib.AssocList

• Implementation
• Basic definitions
• List properties
• Properties of map and dom
• The simpl_alist tactic
• The rewrite_alist tactic
• Induction
• Basic facts about disjoint
• Basic facts about uniq
• Basic facts about binds
• Hints
• List properties
• Tactic support for disjoint and uniq
• Facts about uniq
• Tactic support for binds
• Facts about binds
• Hints

Metalib.CoqEqDec

• Hints for equiv
• Facts about EqDec
• Specializing EqDec
• Decidable equality

Metalib.CoqFSetDecide

• Overview
• Facts and Tactics for Propositional Logic
  • Lemmas and Tactics About Decidable Propositions
  • Propositional Equivalences Involving Negation
  • Tactics for Negations
• Auxiliary Tactics
  • Generic Tactics
  • Discarding Irrelevant Hypotheses
  • Turning Set Operators into Propositional Connectives
  • Decidability of FSet Propositions
  • Normalizing Propositions About Equality
  • Considering Decidability of Base Propositions
  • Handling Empty, Subset, and Equal
  • The Core fsetdec Auxiliary Tactics
• The fsetdec Tactic
• Examples

Metalib.CoqFSetInterface

• Finite set library
• Non-dependent signatures
  • Functorial signature for weak sets
  • Static signature for weak sets
  • Functorial signature for sets on ordered elements
  • Static signature for sets on ordered elements
  • Some subtyping tests
• Dependent signature

Metalib.CoqListFacts

• List structure
• List membership
• List non-membership
• List inclusion
• Setoid facts
• Uniqueness of proofs

Metalib.CoqMSetDecide

• Overview
• Facts and Tactics for Propositional Logic
  • Lemmas and Tactics About Decidable Propositions
  • Propositional Equivalences Involving Negation
  • Tactics for Negations
• Auxiliary Tactics
  • Generic Tactics
  • Discarding Irrelevant Hypotheses
  • Turning Set Operators into Propositional Connectives
  • Decidability of FSet Propositions
  • Normalizing Propositions About Equality
  • Considering Decidability of Base Propositions
  • Handling Empty, Subset, and Equal
  • The Core fsetdec Auxiliary Tactics
• The fsetdec Tactic
• Examples

Metalib.CoqMSetInterface

• Finite set library
  • Functorial signature for weak sets
  • Static signature for weak sets
  • Functorial signature for sets on ordered elements
  • Static signature for sets on ordered elements
  • Some subtyping tests
  • Signatures for set representations with ill-formed values.

Metalib.CoqUniquenessTac

• Auxiliary definitions
• Auxiliary facts
• Tactic for proving the uniqueness of objects

Metalib.CoqUniquenessTacEx

• Examples
  • Predicates on natural numbers
  • Predicates on lists
  • Vectors

Metalib.FSetExtra

• Interface
• Implementation

Metalib.FSetWeakNotin

• Implementation
• Facts about set non-membership
• Hints
• Tactics for non-membership
• Examples and test cases

Metalib.LibDefaultSimp

• Variants on standard tactics
• Tactics for inversion
• Putting it all together

Metalib.LibLNgen

• Assorted functions not in the standard library
• Tactics
• Facts about finite sets
• Hints

Metalib.LibTactics

• Variations on built-in tactics
• Delineating cases in proofs
  • Tactic definitions
  • Example
• Tactics for working with lists and proof contexts

Metalib.MSetExtra

• Interface
• Implementation

Metalib.MSetWeakNotin

• Implementation
• Facts about set non-membership
• Hints
• Tactics for non-membership
• Examples and test cases

Metalib.Metatheory

• Notations for finite sets of atoms
• Environments
• Cofinite quantification
• Lemma aliases
• Hints
• Decidable equality
• Ott compatibility

Metalib.MetatheoryAtom

• Defining atoms
• Finite sets of atoms
• Properties
• Tactic support for picking fresh atoms

LN.Fsub_Definitions

• Syntax (pre-terms)
• Opening terms
• Local closure
• Environments
• Well-formedness
• Subtyping
• Typing
• Values
• Reduction
• Automation

LN.Fsub_Infrastructure

• Free variables
• Substitution
• The "gather_atoms" tactic
• Properties of opening and substitution
  • Properties of type substitution in types
  • Properties of type substitution in expressions
  • Properties of expression substitution in expressions
• Local closure is preserved under substitution
• Properties of body_e
• Automation

LN.Fsub_Lemmas

• Properties of wf_typ
• Properties of wf_env and wf_typ
• Properties of wf_env
• Environment is unchanged by substitution for a fresh name
• Regularity of relations
• Automation

LN.Fsub_Soundness

• Properties of subtyping
  • Reflexivity (1)
  • Weakening (2)
  • Narrowing and transitivity (3)
  • Type substitution preserves subtyping (10)
• Properties of typing
  • Weakening (5)
  • Strengthening (6)
  • Narrowing for typing (7)
  • Substitution preserves typing (8)
  • Type substitution preserves typing (11)
• Preservation
  • Inversion of typing (13)
  • Preservation (20)
• Progress
  • Canonical forms (14)
  • Progress (16)

LNgen.Fsub_ott

LNgen.Fsub_inf

• Induction principles for nonterminals
• Close
• Size
• Degree
• Local closure (version in Set, induction principles)
• Body
• Tactic support
• Theorems about size
• Theorems about degree
• Theorems about open and close
• Theorems about lc
• More theorems about open and close
• Theorems about fv
• Theorems about subst
• "Restore" tactics

LNgen.Fsub_proofs

• Compatability with the original development: Hints, notations, etc.
• Properties of wf_typ
• Properties of wf_env and wf_typ
• Properties of wf_env
• Environment is unchanged by substitution for a fresh name
• Regularity of relations
• Automation
• Properties of subtyping
  • Reflexivity (1)
  • Weakening (2)
  • Narrowing and transitivity (3)
  • Type substitution preserves subtyping (10)
• Properties of typing
  • Weakening (5)
  • Strengthening (6)
  • Narrowing for typing (7)
  • Substitution preserves typing (8)
  • Type substitution preserves typing (11)
• Preservation
  • Inversion of typing (13)
  • Preservation (20)
• Progress
  • Canonical forms (14)
  • Progress (16)