[POPLmark] Another new solution to Part 1A

[Arthur Charguéraud]

Dear all,

I was also working on a locally nameless solution to Part 1A,
and was just finishing the last details of the documentation.

Because my solution has a good number of similarities with the
Adam Chlipala's solution, I thought that it would be good to
release it right now, so that you may compare the two solutions.

So here it is:
http://arthur.chargueraud.org/research/2006/poplmark/


Remark 1 : some of you will probably want to argue about the adequacy
of the encoding of the SA-all rule that I used. Please give me some
more time to complete the adequacy section in the documentation,
and give it a better argumentation.

Remark 2 : I would like to point out that lemma A.10 which states
that "type substitution preserves subtyping" is a little harder to prove
than narrowing, and some encoding techniques which may work fine
on part 1A of the challenge do get into troubles on this lemma.
-- for instance, the techniques that I did use need some extensions before
being able to solve lemma A.10 (and I'm still working on it at this time).
However, with a good encoding technique, one should be able to formalize
this lemma in a reasonable amount of time. Therefore, I encourage those of
you who have a go on part 1A to also have a go on lemma A.10.


-- Arthur Charguéraud