## Coral.Metalib.CoqEqDec

## Coral.Metalib.LibTactics

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

## Coral.Metalib.CoqUniquenessTac

## Coral.Metalib.CoqUniquenessTacEx

## Coral.Metalib.CoqListFacts

## Coral.Metalib.CoqFSetInterface

## Coral.Metalib.CoqFSetDecide

## Coral.Metalib.FSetWeakNotin

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

## Coral.Metalib.FSetExtra

## Coral.Metalib.CoqMSetInterface

## Coral.Metalib.CoqMSetDecide

## Coral.Metalib.MSetWeakNotin

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

## Coral.Metalib.MSetExtra

## Coral.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

## Coral.Metalib.LibDefaultSimp

## Coral.Metalib.MetatheoryAtom

## Coral.Metalib.Metatheory

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

## Coral.Metalib.LibLNgen

## Coral.Definitions: syntax and small-step semantics of a λ-calculus

## Coral.Infrastructure

- Induction principles for nonterminals
- Close
- Size
- Degree
- Local closure (version in Type, 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

## Coral.Env: generic environments

- Extra results about map
- Definition mapi and its properties
- Extra results about get
- Extension ordering of environments leq_env
- Definition of all_env and its basic properties
- Definition of remove_all and its basic properties
- Definition of mapi2 and its basic properties
- Definition of map2 and its basic properties
- Definition of fold_env_dom and its basic properties
- Definition of map_env_dom and its basic properties
- Definition of forall_env_dom and its basic properties
- env_of_atoms

## Coral.StepsFacts: facts about the steps relation

## Coral.EvalFacts: properties of the evaluation relation

## Coral.SubstEnv: environments of terms, viewed as sequences of substitutions

- Definition of subst_env
- Free variables of an environment
- Congruence properties for subst_env
- Other properties of subst_env
- Results about extended values
- Properties about subst_env and evaluation

## Coral.Rel: binary relations

- Binary relations
- Good relations
- Domain-bounded relations
- Inclusion of relations
- Equivalence of relations
- Interplay between inclusion and equivalence
- Union of relations
- Intersection of relations
- Interplay between union and intesection
- Pointwise extension of relations
- FUN combinator
- APP combinator
- Interplay between APP and FUN
- depFUN combinator
- depAPP combinator
- Interplay between depFUN and depApp
- Unit combinator
- Right-sided pair combinator
- Left-sided pair combinator
- Right-sided sum combinator
- Left-sided sum combinator
- Composition of relations
- Identity relation
- Indentity relation on values
- The full relation
- The full relation on values
- The full relation between environments of values and values
- The empty relation
- The converse combinator
- Interplay between composition and the other combinators
- Families of relations, indexed over a cofinite set of atoms
- An auxiliary combinator for the strong Let combinator
- Cofinite existential closure of an atom-indexed family of relations
- The strong Let combinator
- The Self combinator
- The Gather combinator
- Existential closure of a family of relations
- The Remove combinator
- The Push combinator

## Coral.RelStable: stable relations

## Coral.RelLc: relations that relate locally-closed terms

- Definitions
- Properties of RelBot
- Properties of RelInter
- Properties of RelUnion
- Properties of RelSelf
- Properties of RelLet0_strong
- Properties of RelClose
- Properties of RelLet_strong
- Properties of FUN
- Properties of APP
- Properties of RelUnitR
- Properties of RelPairR
- Properties of RelPairL
- Properties of RelSumR
- Properties of RelSumL
- Properties of RelCompose
- Properties of RelInv

## Coral.RelClosed: relations that relate terms with no free variables

- Definitions
- Properties of RelBot
- Properties of RelInter
- Properties of RelUnion
- Properties of RelSelf
- Properties of RelLet0_strong
- Properties of RelClose
- Properties of RelLet_strong
- Properties of FUN
- Properties of APP
- Properties of RelUnitR
- Properties of RelPairR
- Properties of RelPairL
- Properties of RelSumR
- Properties of RelSumL
- Properties of RelCompose
- Properties of RelInv

## Coral.RelValue: relations that relate values

- Definitions
- Properties of RelBot
- Properties of RelInter
- Properties of RelUnion
- Properties of RelSelf
- Properties of RelLet0_strong
- Properties of RelClose
- Properties of RelLet_strong
- Properties of FUN
- Properties of APP
- Properties of RelUnitR
- Properties of RelPairR
- Properties of RelPairL
- Properties of RelSumR
- Properties of RelSumL
- Properties of RelCompose
- Properties of RelInv

## Coral.RelGood: good relations

## Coral.TranspCore: name transpositions on atoms and finite sets thereof

- Transpositions on atoms
- Transpositions on finite sets of atoms
- Transposition on the domain of environments

## Coral.Transp: name transpositions

- Transpositions on terms
- Support for terms
- Transpositions on environments of terms
- Transpositions and support on relations between environments of terms and terms
- Transpositions and support on atom-indexed families of relations
- Transpositions on relations between terms
- Equivalent environments of relations
- Included environments of relations
- Transpositions and suppport on environments of relations between environments of terms and terms
- Transpositions and support on environments of relations between terms

## Coral.EquivarianceFacts: various equivariance results

- Equivariance of properties
- Equivariance of evaluation the relations
- Equivariance of relations between relations
- Equivariance of relational combinators
- Additional equivariance results
- Additional results about leq_env

## Coral.SupportFacts: support of relational combinators and definition of well supported environments

## Coral.RelExtra: more relational combinators

- simplAPP
- RelLet
- RelLam
- Strong version of the RelLam combinator
- Renaming lemmas
- Some additional properties

## Coral.RelWf: wellformed relations

## Coral.OkEnv: denotation of an environment of relations as a set of substitutions

## Coral.Rsem: definition and results about the collecting relational semantics

- Auxiliary definition ok_env_rel and related results
- Auxiliary definition eval_rel and related results
- Collecting relational semantics
- Definition
- Basic results
- Properties of RelSelf and RelGather
- About the rule for variables
- About the rule for let-bindings
- About the rule for functions
- About the rule for applications
- About the rule for unit
- About the rule for pairs
- About the rule for the first pair projection
- About the rule for the second pair projection
- About the rule for the first sum injection
- About the rule for the second sum injection
- About the rule for sum destruction

- Additional results: creation of an environment of relations from a substitution

## Coral.TermInd: generic recursion over locally-closed terms to define denotational interpreters, and associated induction principle

- Auxiliary definitions, that perform induction over the sizes of terms.
- Final definition for recursor and induction principle.

## Coral.Interp: relational interpretation of untyped λ-terms

## Coral.Perm: permutations of names

- Action of permutations on atoms
- Action of permutations on sets of atoms
- Action of permutations on terms
- Action of permutations on binary relations on terms
- Action of permutations on relations over substitutions and terms
- Action of permutations on environments of relations
- Strong equivariance results on relational combinators

## Coral.InterpStrong: strong version of Interp, that provides stronger induction principles

## Coral.RLogic: program logic for untyped λ-terms based on stable relations

## Coral.RLogicStrong: strong version of RLogic, that provides stronger induction principles

## Coral.InterpExamples: examples of interpretations of λ-terms

## Coral.PointwiseRel: abstraction of relations into pointwise relations

- Comparison
- Equivalence of pointwise relations
- Concretization
- Concretization of an environment of pointwise relations
- Transposition of pointwise relations
- Good pointwise relation
- Wellformed environment of pointwise relations
- Abstraction
- smash of pointwise relations
- Intersection of pointwise relations
- Union of pointwise relations
- Composition of pointwise relations
- Right-sided pair of pointwise relations
- Right-sided sum of pointwise relations
- Closure of name abstraction for pointwise relations
- Let-binding
- Application of pointwise relations
- Functions of pointwise relations
- Self pointwise relation
- Gather of pointwise relations

## Coral.Types: simple types, well typed terms, and type soundness

- Types
- Typing judgment
- Strengthened typing jugment
- Syntactic type soundness
- Typed relations over closed terms