Email Gateway (Aug 18 2022 at 10:57): Email Gateway (Aug 18 2022 at 10:57):From: Christian Urban <urbanc@in.tum.de>
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,
Christian
Email Gateway (Aug 18 2022 at 10:58):From: Christian Urban <urbanc@in.tum.de>
Dear Moez,
Moez A. Abdel-Gawad writes:
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).
I completely agree with your view that matters with formalising
the lambda-calculus should be simple, but I often found that
they aren't.
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.
I am open for your suggestions! However it seems you have inadvertently
given a good reason that it is a good example.
My Coq-abilities are not very good, but reading
Require Import String.
Inductive LCterm: Set :=
| Var : string -> LCterm
| Abs: string -> LCterm -> LCterm
| App: LCterm -> LCterm -> LCterm.Require Import Ensembles.
Fixpoint FV(t: LCterm): Ensemble string :=
match t with
| Var x => Singleton string x
| Abs x t1 => Subtract string (FV t1) x
| App t1 t2 => Union string (FV t1) (FV t2)
end.
...
Fixpoint subs(x: string) (t: LCterm) (t': LCterm){struct t}: LCterm :=
match t with
| Var y => if string_dec y x then t' else t
| Abs y t1 => if string_dec y x then t else Abs y (subs x t1 t')
| App t1 t2 => App (subs x t1 t') (subs x t2 t')
end.
you defined possibly-capturing substitution , namely
(Var y)[x:=t] = (if x=y then t else (Var y))
(Abs y t1)[x:=t] = (if x=y then (Abs y t1) else (Abs y (t1[x:=t])))
(App t1 t2)[x:=t] = App (t1[x:=t]) (t2[x:=t])
In the second clause you will capture any free occurrence of y
in t by moving the substitution under the binder.
If I am not mistaken and you indeed defined possibly-capturing
substitution and also used a concrete representation of lambda-terms,
then your substitution lemma
Lemma subs_lemma: forall x y: string, forall M N L: LCterm,
x <>y -> ~ In string (FV L) x ->
subs y (subs x M N) L = subs x (subs y M L) (subs y N L).
is not true. James Cheney just did a few calculations and found
the following counter-example
(Abs y (Var x))[x:=y][y:=z] <> (Abs y (Var x))[y:=z][x:=y[y:=z]]
Disregarding this counter-example, the point of the substitution
lemma is, however, to show this property for capture-avoiding
substitution. The trouble then starts: your substitution
operation needs a precondition (I am not sure whether one can
state such a precondition of in Coq) or one needs to do a renaming
(I am also not sure how to define this cleanly in Coq). Also, if
you insist on a concrete representation, you need to state it not
as an equality, but an alpha-equivalence. You would also need
to define this in Coq.
Best wishes,
Christian
Last updated: May 03 2024 at 08:18 UTC