Welcome to the companion proof directory for our LFMTP2014 submission "A Generic Approach to Proofs about Substitution"

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

• "The inverse function is swapVar (rev sw)." :
  It is a straightforward consequence of: swapVar_s2stronger2   swapVar_app

Section 5

Paragraph : Nominal Logic

• "Our swapping functions satisfy the properties in [19]. We generalize these properties to the case when a swapping is defined as a list of pairs, instead of a single pair." :
  The lemmas below corrsepond to the axioms S1 , S2 and S3 in the appendix of [19].
  swapVar_prop_s1   swap_prop_s1   swapVar_s2stronger2   swap_prop_s2Stronger   swap_app   swapVarIn ( S3 )  
• "Almost all the functions and relations involving variables that we defined are equivariant (w.r.t. Coq’s built-in equality)."
  Firstly note the definitions of equivariance of relations ( EquiVariantRel   EquiVariantRelSame ) and of functions ( EquiVariantFn   EquiVariantFn2   EquiVariantFn3 ) .
  The following lemmas are about equivariance of relations:
  LInEquivariant   DisjointEquivariant   alphaEquiVariant  
  The following lemmas are about equivariance of functions:
  freevarsEquivariant   AllVarsEquivariant   bndngVarsDeepEquivariant   swapVar_e1stronger (equivariance of the swapping operation)   swap_prop_e1Stronger   EquivariantSSubstAux  

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 verified decision procedure for α-equality." :
  alphaEqDecidable

Paragraph : Substitution

• SSubstRespectsAlpha
• SSubstFilter
• FVSSubst
• SSubstNestSwap
• SSubstNestAsApp