Fsub.EffectExclusion.LabelMap

Fsub.EffectExclusion.BooleanAlgebra_Properties

Fsub.EffectExclusion.Fsub_LetSum_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

Fsub.EffectExclusion.Fsub_LetSum_Definitions

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

Fsub.EffectExclusion.Label

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

Fsub.EffectExclusion.Lattice

Fsub.EffectExclusion.Fsub_LetSum_Soundness

• Properties of subtyping
  • Reflexivity (1)
  • Subqualification respects the lattice order (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) / Canonical Typing Forms
  • Qualifiers and Concrete Qualifiers (14.5)
  • Preservation (20)
• Progress
  • Canonical forms (14)
  • Progress (16)

Fsub.EffectExclusion.Fsub_LetSum_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

Fsub.EffectExclusion.Tactics

• Borrowed from

Fsub.FbMeta.Metatheory

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

Fsub.FbMeta.CoqEqDec

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

Fsub.FbMeta.FSetExtra

• Interface
• Implementation

Fsub.FbMeta.CoqListFacts

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

Fsub.FbMeta.MetatheoryAtom

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

Fsub.FbMeta.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

Fsub.FbMeta.LibLNgen

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

Fsub.FbMeta.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

Fsub.FbMeta.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

Fsub.FbMeta.CoqUniquenessTacEx

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

Fsub.FbMeta.LibDefaultSimp

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

Fsub.FbMeta.CoqUniquenessTac

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

Fsub.FbMeta.FSetWeakNotin

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

Fsub.FbMeta.LibTactics

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

Fsub.Base.LabelMap

Fsub.Base.BooleanAlgebra_Properties

Fsub.Base.Fsub_LetSum_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

Fsub.Base.Fsub_LetSum_Definitions

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

Fsub.Base.Label

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

Fsub.Base.Lattice

Fsub.Base.Fsub_LetSum_Soundness

• Properties of subtyping
  • Reflexivity (1)
  • Subqualification respects the lattice order (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) / Canonical Typing Forms
  • Qualifiers and Concrete Qualifiers (14.5)
  • Preservation (20)
• Progress
  • Canonical forms (14)
  • Progress (16)

Fsub.Base.Fsub_LetSum_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

Fsub.Base.Tactics

• Borrowed from