Email Gateway (Aug 18 2022 at 10:58): Email Gateway (Aug 18 2022 at 10:58):From: "Moez A. Abdel-Gawad" <moez@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@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
Email Gateway (Aug 18 2022 at 10:58):From: Brian Aydemir <baydemir@cis.upenn.edu>
Hi Moez,
If you're interested in what is possible with a "lightweight"
approach in this area, you may want to take at the following
paper.
[1] Engineering Formal Metatheory, by Brian Aydemir, Arthur
Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie
Weirich. Available from
http://www.cis.upenn.edu/~baydemir/papers.shtml#AydCha+07a
This is a paper that will appear at POPL 2008 that focuses on a
particular style of locally nameless representation for
formalizing languages with binding. (Coq code for the paper is
available through the link above.) The style is lightweight in
that one could use it in a variety of proof assistants, e.g., Coq
and Isabelle, without any additional infrastructure. The paper
also makes some comparisons with other first-order approaches,
including the Isabelle/Nominal package.
If you're interested in nominal techniques in Coq, I can mention
two other works (which Christian Urban has already pointed out
on the Isabelle lists).
[2] Nominal Reasoning Techniques in Coq, by Brian Aydemir, Aaron
Bohannon, and Stephanie Weirich. Available from
http://www.cis.upenn.edu/~baydemir/nominal-reasoning-in-coq.html
This is not really a package like the Isabelle/Nominal package but
more a demonstration of what nominal reasoning might look like in
Coq. In order to be practically useable, a similar amount of
infrastructure would be required in Coq as in Isabelle.
[3] A locally nameless solution to the POPLmark challenge, by
Xavier Leroy. Available from
http://cristal.inria.fr/~xleroy/POPLmark/locally-nameless/
Leroy uses some nominal techniques in a locally-nameless setting
in Coq.
Cheers,
Brian
Email Gateway (Aug 18 2022 at 10:58):From: "Moez A. Abdel-Gawad" <moez@cs.rice.edu>
Hi,
Here's the story behind my substitution lemma proof development. I
apologize if it is a bit long, and informal. It was in fact the
original email I intended to send in place of my earlier email, but
then I realized it - being long and informal - may not be approp-
riate as an introductory email. I apologize also for any possible
inconsistencies that may have crept-in due to the heavy editing,
and re-editing, I made to this message.
Also, attached is my Coq proof script. It is almost-complete (except
for the small part that needed the freshness assertion, of course),
but it is very likely a very "inefficient" proof script, since I am
new to Coq. I am, however, currently not interested in "optimizing"
it. My goal when I developed this proof was to learn the basics of
Coq, and to get as much as possible of the proof done with whatever
tactics are currently available in Coq (i.e., without resorting to
any sort of explicit use of nominality). The proof script is only my
second real - ie, non-toy-like - proof in Coq (after proving that
forall n: nat, n < 2^n).
In my quest to learn Coq, I started playing with a personal imple-
mentation of lambda calculus. My initial goal was to prove the
substitution lemma, i.e., if x <> y and x \nin FV(L) then
M[x:=N][y:=L] = [y:=L][x:=N[y:=L]].
Using induction on M, doing the 'App' induction case in Coq was the
most trivial case. As hypothesis for my proof, I had assumed - as
Barendregt explicitly does - that x <> y and x \nin FV(L). Not pay-
ing much attention, I did not - initially - assume freshness, nor
did I assume the equivalence of lambda terms modulo alpha-conver-
sion. Thus, for the 'Var' and 'Abs' induction cases, everything
went well, by reasoning - using cases (on the boolean value
'string_dec') - whether the free variable (in case of 'Var') or the
abstraction variable (in case of 'Abs') is equal to or different
from other variables in the proof (i.e., x and y. The name chosen
by Coq for that auxiliary variable, in both cases, was 's', because
Coq chooses names based on the type, which is 'string' in both
cases), on until one tiny sub-subcase of the 'Abs' induction case
(also sometimes called the lambda-case), where I had 's' assumed to
be not equal to x, but equal to y. After doing all possible simpli-
fications, unfoldings and foldings, the goal I had to prove became:
Abs s (subs x M N) = Abs s (subs x M (subs y N L))
Having gone thru all earlier subcases successfully (i.e., in parti-
cular, without resorting to any additional external hypothesis), I
was wondering why is that sub-subcase in particular hard to prove,
and what exactly was going on. Not deterred by the failure of this
sub-subcase, I was able to do the remaining other parts of the pr-
oof (using Coq's "n:" notation) without any problems... except for
this little impeding sub-subcase.
I then searched online for 'proving substitution lemma'. That is
when I came to know about the 'Nominal Isabelle' project, after
coming across the following webpage:
http://isabelle.in.tum.de/nominal/main.html
The webpage explained what's going on very nicely, and reminded me
of the possible need for Barendregt's variable convention, as well
as the possible need for the equivalence of lambda terms modulo
alpha-conversion. It was also nice to know that there is an ongoing
project that is trying to solve this deficiency (which is a defic-
iency that exists, it seems to me, in most semi-automated theorem
provers in general, not only in Isabelle and Coq).
However, based on my experience with trying to prove the substitu-
tion lemma, it seems I may disagree with some implication in the
webpage above.
In particular, for purposes of the 'substitution lemma' only, I do
not believe - again, based on my experience - that the 'full power'
of the freshness assumption (i.e., the variable convention) and the
'alpha-equivalence' is actually needed to prove it. Also, the "ins-
tance of freshness" needed seems to me to be much simpler (and gen-
erally less powerful) than the one the 'nominal-isabelle' package
would provide (which, of course, may be useful for other more intr-
icate lemmas).
That's because for proving the substitution lemma all that I needed
was just to somehow be able to assert the freshness of 's', not in
all cases and subcases, but only at that particular sub-subcase I
mentioned above. I did not need the freshness of 's' in any other
parts of my proof. (I even only needed an assertion that 's' is not
equal to y, i.e., that it is different from one variable only, not
necessarily that it is different from all other variables (in the
current environment)).
That observation led me to two conclusions.
First, I would think thus that something simpler than the new nom-
inal-isabelle constructs (nominal_datatype, nominal_induction,
avoiding, fresh_fact, forget, etc) maybe more intuitive, and also
more straight-forward to add (to Isabelle, or other semi-automated
theorem provers). In my proof development I wished there was just
something available as "simple" as a tactic that would allow stat-
ing that 's is fresh' (having a syntax like 'fresh s'), to assert
that s, as a variable name (string), is different from all other
variable names in the current environment (x and y, as well as
other possibly ones inside M and N and L, that are irrelevant to
the proof and are thus not explicitly mentioned in the lemma's
statement, even though all I actually needed is for s to be diffe-
rent from y).
Next, I also concluded that the substitution lemma, even though
well-known to many PL researchers, may NOT be a very convincing
example to cite (eg, on the webpage) for developing the new 'nom-
inal-isabelle' package. That is NOT to say the package itself is
useless, but only to say that probably other examples can do a
better job in motivating the whole new package (a new package
suggests that users have to learn a whole new bag of "tricks and
tools" to do proofs, and thus need a very strong motivation for
that). In my view, using 'nominal-isabelle' to prove the substi-
tution lemma is like using a big hammer to pound a hair pin, when
it - the lemma - can, in my view, be proved using much simpler
means (e.g., a simple new tactic).
Your insights and constructive feedback is more than welcome, and
would be deeply appreciated.
-Moez
PS1: Further analyzing the subgoal written above, I realized that
the freshness of 's' is actually not an absolute necessity in that
sub-subcase, but only if I had initially assumed (added to my hypo-
thesis) that y is not a free variable in N (y \nin FV(N)). If that
was assumed then the third 'subs' (substitution) in the subgoal
above would be an identity operation over N, and the RHS would be
indeed equal to the LHS, and I'd be done. However, in the bigger
context, that second solution to my sub-subcase actually makes the
substitution lemma's statement very trivial and shallow.
PS2: I am annoyed by receiving some of the latest emails three,
and even sometime four, times. What even aggravates the situation
is that there are also delayed deliveries (multiple copies of the
same email, thus, do not come in as a chunk, at one time). I am
wondering if there is some means to get rid of this duplicity, and
of the delayed deliveries, coalescing multiple copies of the same
emails into one email, and/or having them be delivered almost at
the same time. I did not check the mailing list archives to see if
this issue was discussed before, but I believe it would be apprec-
iated by most of subscribers to the mailing lists if it is true
(and my guess is that it is) that the vast majority of subscribers
to one list are subscribers to the other (among Coq and Isabelle),
and that subscribers of the nominal-isabelle mailing list are very
likely to be a proper subset of the subscribers to the isabelle
mailing list (probably some cooperation at the level of the list
admins is needed?).
moez@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
LC.v
Last updated: May 03 2024 at 08:18 UTC