[isabelle] [nominal-isabelle] proving the substitution lemma

Hi Moez,

Moez A. Abdel-Gawad writes:
 > However, my own personal attempt to prove the substitution
 > lemma in Coq - with very minor resort to the variable con-
 > vention and alpha-conversion equivalence - seemed to tell
 > that the substitution lemma may not be the best example to
 > use for *motivating* the need for the 'isabelle-nominal'
 > package and project, as is done for example on this web-
 > page http://isabelle.in.tum.de/nominal/main.html

I agree: The substitution lemma is not the most exciting 
proof to formalise. On the other hand, it is very small
and everyone knows about it and about the issues. I like 
it, since one can explain the nominal Isar-proof of this 
lemma in 5 minutes to people who never have touched a 
theorem prover in their lives. That is why I presented it 
on the nominal web-page.

 > While I do not discount the possibility of the package
 > being useful - and even necessary - for other proofs, my
 > experiment gave me the feeling that a much simpler app-
 > roach may be possible (may be even as simple as adding a
 > new tactic), which may work in fact for many similar pr-
 > oofs as well, and - if not - is very likely to work at
 > least for the purpose of proving the substitution lemma.

Would you mind sharing your proof? In the experience I obtained
with the nominal package is that the techniques (strong
induction principles) which we use to prove the substitution
lemma have proved most valuable in all formalisations we did 
so far. Nowadays I would refuse to do any formalisation, if 
I did not have them. 

 > PS: I was wondering if there is a Coq package and/or
 > project similar to the 'isabelle-nominal' ones.

There is 

  B. Aydemir, A. Bohannon and S. Weirich, Nominal Reasoning 
  Techniques in Coq. In Proc. of LFMTP 2006

and Xavier Leroy used some lightweight nominal techniques
in his solution of the PoplMark-challenge. 

Best wishes,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.