Action Codes Coq Formalization

Library ActionCodes.ACUtil

Library ActionCodes.Adaptor

• Determinate Action Codes

Library ActionCodes.CodeMap

• Preliminary Definitions
• Definition: Codes as Maps
• Kleisli extension
• Code composition

Library ActionCodes.Concretization

• Definitions
  • Concretization Operator
  • Transitions
  • Completeness of Codes
• Technical Lemmas
• The Galois-Connection
• Preservation Properties
• Examples / Counterexamples

Library ActionCodes.Contraction

• Definition
• Properties

Library ActionCodes.LTS

• Simulations
• Isomorphism
• Reachability
• Examples

Library ActionCodes.MealyExample

• The Mealy Machine
• A first Action Code

Library ActionCodes.RefinementCodeComposition

• Isomorphism Definition
• Proofs and helper results
• Main Theorem

Library ActionCodes.Refinement

• Definitions
• Helper Lemmas
• Properties: Monotonicity, Determinism
• Adjunction / Galois insertion

Library ActionCodes.TreeShapedCode

• Preliminary Definitions
• Definition of Tree-Shaped Action Code
• From Tree-Shaped Codes to Map-Based Codes
  • Uniqueness
  • Existence
• From Map-Based Codes to Tree-Shaped Codes
  • Uniqueness
  • Existence