Welcome to the companion proof directory for our LFMTP2014 submission
"A Generic Approach to Proofs about Substitution"
This page contains quotes from the paper and hyperlink(s)
to the Coq lemma(s) formalizing the claim(s) in that quote.
The quotes are ordered according the the place they occur in the
paper.
Section 2
 "We use Coq’s nat and string types to implement
two instances members of VarType" :
StringVar
nvarVarType
Section 4
 "These functions αrename
their input (a Term, a Pattern and a Mixture respectively) so
that all their bound variables are disjoint from a given list of
variables (and the result is αequal). We have proved both
these properties." :
RenAlphaAvoid
RenAlphaAlpha

 "For better usability, we have also proved
that these functions return the same term as the input if
it already met the disjointness condition." :
RenAlphaNoChange
SubSection 4.1
Section 5
Paragraph : Nominal Logic
Paragraph : Alpha Equality
 "αequality is an equivalence relation."
:
alphaEqRefl
alphaEqSym
alphaEqTransitive

" αequal terms and patterns have the same free variables (equal
as lists)."
:
alpha_preserves_free_vars

"Given a term, any swapping whose restriction to
the free variables of the term is the identity
function results
in an αequal term."
:
alphaEqSwapNonFree

"Also, the set of free variables
(as computed by tfreevars) of a term is precisely its support [19]
w.r.t. αequality" :
freeVarsSupp

"we provide a veriﬁed decision
procedure for αequality." :
alphaEqDecidable
Paragraph : Substitution
The 5 lemmas listed in the paper correspond
to the Coq lemma(s) in the following 5 lines respectively.