This is a solution to part 1a of the POPLmark challenge which I developed as part of my master thesis under the supervision of prof. Andrea Asperti.
The solution was written using the Matita interactive theorem prover under developement at the Department of Computer Science of the University of Bologna. In the solution, we include the proofs for three different encodings of binders: locally nameless, pure de Bruijn, and named variables. The first two are direct proofs, while the last is obtained by translation of terms with named variables to locally nameless terms.
The solution (which is also available as part of the Matita library), is here provided in a single .tgz archive, containing the following files.
util.ma, including few lemmata not really related to the object language
defn.ma, including the definition of the object language in the locally nameless encoding, as well as the basic results needed to prove the main theorems
part1a.ma, including the main theorems for the locally nameless encoding.
defndb.ma, similar to
defn.ma, but in the pure de Bruijn encoding
part1adb.ma, similar to
part1adb.ma, but in the pure de Bruijn encoding
adeq.ma, providing the translation from the locally nameless encoding to the named variables encoding, and a proof of adequacy.