Re: [isabelle] [Coq-Club] proving the substitution lemma



Moez A. Abdel-Gawad wrote:
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.

Hi Moez,

in this paper

  André Hirschowitz, Marco Maggesi
  "Modules over Monads and Linearity"
  Leivant, Queiroz (Eds.). WoLLIC 2007. LNCS 4576

we advocate the use of "linear morphism" as the good way to capture the notion of "compatibility with substitution".

We have two Coq formalizations which adopt this discipline.

The first one is about Lambda Calculus:
http://web.math.unifi.it/~maggesi/mechanized/lambda/
(an equivalent translation in HOL-Light is also available from the same page).

The other is about Fsub (part 1A of the poplmark challenge, to be precise):
http://web.math.unifi.it/~maggesi/mechanized/fsub/

The latter is especially compact and short (according to our own statistics) compared to other proposed approach and does not require any specific framework or library.

M.





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