*To*: "Moez A. Abdel-Gawad" <moez at cs.rice.edu>*Subject*: [isabelle] [nominal-isabelle] proving the substitution lemma*From*: Christian Urban <urbanc at in.tum.de>*Date*: Thu, 8 Nov 2007 21:52:16 +0100*Cc*: nominal-isabelle at mailbroy.informatik.tu-muenchen.de, coq-club at pauillac.inria.fr, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <473353F2.2020900@cs.rice.edu>*References*: <473353F2.2020900@cs.rice.edu>*Reply-to*: urbanc at 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

**References**:**[isabelle] proving the substitution lemma***From:*Moez A. Abdel-Gawad

- Previous by Date: [isabelle] proving the substitution lemma
- Next by Date: Re: [isabelle] Using Isabelle to generate a pdf
- Previous by Thread: [isabelle] proving the substitution lemma
- Next by Thread: [isabelle] REMAINDER: TPHOLs 2010: Call for Votes
- Cl-isabelle-users November 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list