Nominal Inversion Principles

10 years 1 months ago
Nominal Inversion Principles
When reasoning about inductively defined predicates, such as typing judgements or reduction relations, proofs are often done by inversion, that is by a case analysis on the last rule of a derivation. In HOL and other formal frameworks this case analysis involves solving equational constraints on the arguments of the inductively defined predicates. This is well-understood when the arguments consist of variables or injective term-constructors. However, when alpha-equivalence classes are involved, that is when term-constructors are not injective, these equational constraints give rise to annoying variable renamings. In this paper, we show that more convenient inversion principles can be derived where one does not have to deal with variable renamings. An interesting observation is that our result relies on the fact that inductive predicates must satisfy the variable convention compatibility condition, which was introduced to justify the admissibility of Barendregt’s variable convention...
Stefan Berghofer, Christian Urban
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Authors Stefan Berghofer, Christian Urban
Comments (0)