Proof of correctness of addition and multiplication of Church numerals in Agda

[timjb]

Hi! I was reading Lectures on the Curry-Howard Isomorphism and learning about Church encodings when I thought that proving their correctness would be a fun Agda exercise. Since I didn't want to start from scratch by formalizing the λ-calculus, I chose your existing project as a base. This pull requests contains my (admittedly ugly) proofs of correctness of multiplication and addition of church numerals. In some proofs, it was convenient to have some lemmas about closed terms, so I've added those.

Thanks for sharing your work!

[pi8027]

Thanks for your contribution!

I checked your codes, and found some issues. Please fix these issues:

• Newline character is omitted in the last line of some files. (E.g. ChurchNumerals.agda)
• Some lines are too long. In original proofs, any line is less than 100 characters.
• Proofs contain 2 different asterisk characters in the meaning of the reflexive transitive closure. I think it should be unity.

By the way, existing definition of the substitution and beta-reduction made proofs difficult. I'll fix this problem, and rewrite large parts of proofs containing your work. (A better definition is available at https://github.com/pi8027/lambda-calculus/blob/master/coq/LC/Debruijn/Untyped.v)