The Coq mailing list

[Marco Maggesi <maggesi AT math.unifi.it>]

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.