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