The Coq mailing list

["Moez A. Abdel-Gawad" <moez AT cs.rice.edu>]

Hi,

I'm new to Isabelle and Coq.

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

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.

Your thoughts?

-Moez

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

moez AT rice.edu
 | www.cs.rice.edu/~moez | (713) 392-2844

======================================================

"And you have been given of knowledge but little"
 -Al-Qur'an [17:85]

"Our knowledge can only be finite, while our ignorance
 must necessarily be infinite."   -Karl Popper