This repository contains a framework for reasoning about linear typing contexts in Coq.
The file Monoid.v
describes the algebraic structure of partial commutative
monoids, which are characterized by the following parts:
- A base type "A"
- A unit element "⊤ : A"
- An undefined element "⊥ : A"
- A merge operation, written "a ∙ b"
Partial commutative monoids satisfy the following laws:
- (A,⊤,∙) forms a commutative monoid
- a ∙ ⊥ = ⊥
The tactic monoid
solves goals of the form a = b
, where a
and b
are made up of PCM constructors and at most one EVar.
The file TypingContext.v
describes additional structure on top of PCM's. A typing context "Ctx" with domain "X" and image "A" satisfies:
Ctx
is a partial commutative monoid- for
x:X
anda:A
, a singleton contextsingleton x a : Ctx
- for any context
Γ:Ctx
, a predicateis_valid Γ
that checks if Γ is the undefined element ⊥.
The tactic validate
solves goals of the form is_valid Γ
. It is based on the following principles:
- (Γ₁ ∙ Γ₂ ∙ Γ₃) is valid if and only if all of (Γ₁ ∙ Γ₂), (Γ₁ ∙ Γ₃), and (Γ₂ ∙ Γ₃) are valid.
- ⊤ is valid
- the singleton context (x,a) is valid
- for two singletons (x,a) and (y,b), the context
singleton x a ∙ singleton y b
is valid if and only ifx <> y
.
We give the following instantiation of the TypingContext
type class:
IndexContext.v
: Contexts arelist (option T)
where variables are natural numbers that index into a list