*To*: coq-club at pauillac.inria.fr, cl-isabelle-users at lists.cam.ac.uk, nominal-isabelle at mailbroy.informatik.tu-muenchen.de*Subject*: [isabelle] proving the substitution lemma*From*: "Moez A. Abdel-Gawad" <moez at cs.rice.edu>*Date*: Thu, 08 Nov 2007 12:22:42 -0600*User-agent*: Thunderbird 1.5.0.13 (Windows/20070809)

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 at 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

(* This script was developed in Coq v8.1, using CoqIDE *) 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. (*unused Definition combinator(t: LCterm): Prop := FV(t) = Empty_set string. unused*) 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. Fixpoint reduce(t: LCterm): LCterm := match t with | Var _ => t | Abs y t1 => Abs y (reduce t1) | App t1 t2 => match t1 with | Abs x t11 => subs x t11 t2 | _ => t end end. Eval compute in (reduce (App (Abs "x" (Var "x"))(Abs "y" (Var "y")))). Theorem eq_LCterms: (reduce (App (Abs "x" (Var "x"))(Abs "y" (Var "y")))) = Abs "y" (Var "y"). Proof. unfold reduce. unfold subs. (*need theorem or tactic here to show string_dec "x" "x" is true,rather than immediately resorting to trivial*) (* assert (string_dec "x" "x") did not work *) trivial. Qed. Lemma In_subtract: forall U: Type, forall x y: U, forall s: Ensemble U, x <> y /\ ~ In U (Subtract U s y) x -> ~ In U s x. Proof. intros U x y s x_nin_s. elim x_nin_s. intros x_neq_y x_nin_ss. intuition. (*simplifies 'not' to '-> False' and introduces H*) clear H0 H1. elim x_nin_ss. Require Import Classical_sets. apply Subtract_intro. exact H. intuition. (* apply (Subtract_inv U s y x x_nin_ss). intuition. (*simplifies 'not' to '-> False' and introduces H*) assert (x_in_s_neq_y: In U s x /\ y <> x). apply ((Subtract_inv U s y x) H). elim x_in_s_neq_y. intros x_in_s x_neq_y. elim x_nin_s. exact x_in_s. *) Qed. Lemma FV_incr: forall x s: string, forall M: LCterm, x <> s -> ~ In string (FV (Abs s M)) x -> ~ In string (FV M) x. Proof. intros x s M x_neq_s x_nin_fvabsm. unfold FV in x_nin_fvabsm. fold FV in x_nin_fvabsm. apply (In_subtract string x s (FV M)). split. exact x_neq_s. exact x_nin_fvabsm. Qed. Lemma sym_neq: forall U: Type, forall x y: U, x <> y -> y <> x. Proof. intros U x y x_neq_y. intuition. Qed. Lemma nin_union: forall U: Type, forall s1 s2: Ensemble U, forall x: U, ~ In U (Union U s1 s2) x -> ~ In U s1 x /\ ~ In U s2 x. Proof. intros U s1 s2 x x_nin_union. intuition. Qed. Lemma subs_ninFVid: forall x: string, forall M N: LCterm, ~ In string (FV M) x -> subs x M N = M. Proof. intros x M N x_nin_fvm. induction M. unfold subs. case (string_dec s x). intro s_eq_x. unfold FV in x_nin_fvm. assert False. Require Import Constructive_sets. apply (x_nin_fvm (Singleton_intro string s x s_eq_x)). contradiction. intro s_neq_x; trivial. unfold subs; fold subs. case (string_dec s x). intro s_eq_x; trivial. intro s_neq_x. apply (sym_neq string s x) in s_neq_x. assert (subs_eq_M: subs x M N = M). apply IHM. apply (FV_incr x s M s_neq_x x_nin_fvm). rewrite subs_eq_M. trivial. unfold subs; fold subs. unfold FV in x_nin_fvm; fold FV in x_nin_fvm. apply (nin_union string (FV M1) (FV M2) x) in x_nin_fvm. elim x_nin_fvm. intros x_nin_fvm1 x_nin_fvm2. assert (subs_eq_M1: subs x M1 N = M1). apply IHM1. exact x_nin_fvm1. assert (subs_eq_M2: subs x M2 N = M2). apply IHM2. exact x_nin_fvm2. rewrite subs_eq_M1. rewrite subs_eq_M2. trivial. Qed. Lemma subs_abs: forall x y: string, forall M N: LCterm, x = y -> subs x (Abs y M) N = Abs y M. Proof. intros x y M N x_eq_y. unfold subs; fold subs. case (string_dec y x). trivial. apply sym_eq in x_eq_y. contradiction. Qed. Lemma subs_abs_neq: forall x y: string, forall M N: LCterm, x <> y -> subs x (Abs y M) N = Abs y (subs x M N). Proof. intros x y M N x_neq_y. unfold subs; fold subs. case (string_dec y x). intro x_eq_y. apply sym_eq in x_eq_y. contradiction. trivial. Qed. 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). Proof. intros x y M N L x_neq_y x_nin_fvl. (* intuition. (*simplifies hypotheses x_neq_y and x_nin_fvl*)*) induction M. unfold subs; fold subs. case (string_dec s x). intro s_eq_x. case (string_dec s y). intro s_eq_y. assert (x_eq_y: x = y). assert (x_eq_s: x = s). apply (sym_eq s_eq_x). apply (trans_eq x_eq_s s_eq_y). contradiction. unfold subs at 2. case (string_dec s x). intros. trivial. contradiction. case (string_dec s y). intro s_eq_y. unfold subs at 1. case (string_dec s y). intros. apply sym_eq. apply (subs_ninFVid x L (subs y N L)). exact x_nin_fvl. contradiction. intros s_neq_y s_neq_x. unfold subs at 1. case (string_dec s y). contradiction. intro. unfold subs at 1. case (string_dec s x). contradiction. trivial. unfold subs; fold subs. case (string_dec s x). intro s_eq_x. case (string_dec s y). intro s_eq_y. assert (s1: subs y (Abs s M) L = Abs s M). apply (subs_abs y s M L). apply sym_eq in s_eq_y; assumption. rewrite s1. assert (s2: subs x (Abs s M) (subs y N L) = Abs s M). apply (subs_abs x s M (subs y N L)). apply sym_eq in s_eq_x; assumption. rewrite s2. trivial. intro s_neq_y. assert (s1: subs y (Abs s M) L = Abs s (subs y M L)). apply (subs_abs_neq y s M L). auto. rewrite s1. assert (s2: subs x (Abs s (subs y M L)) (subs y N L) = Abs s (subs y M L)). apply (subs_abs x s (subs y M L) (subs y N L)). auto. rewrite s2. trivial. intros s_neq_x. case (string_dec s y). intro s_eq_y. assert (s1: subs y (Abs s (subs x M N)) L = Abs s (subs x M N)). apply (subs_abs y s (subs x M N) L). auto. rewrite s1. assert (s2: subs x (Abs s M) (subs y N L) = Abs s (subs x M (subs y N L))). apply (subs_abs_neq x s M (subs y N L)). auto. rewrite s2. (*Here is where I was stuck. I wrote that I should: use freshness of s (variable convention), or y not in FV(N), as assumption. how? ask on coq-club. *) (* case (bool_dec In string (FV N) y). z <> x, y, s. subs z (Abs s (subs x M N)) L = Abs s (subs z (subs x M N) L) subs z (Abs s (subs x M (subs y N L)) L = Abs s (subs z (subs x M (subs y N L)) L) *) (* prove remaining subgoals *) 2: intro s_neq_y. 2: assert (s1: subs y (Abs s (subs x M N)) L = Abs s (subs y (subs x M N) L)). 2: apply (subs_abs_neq y s (subs x M N) L). 2: auto. 2: rewrite s1. 2: assert (s2: subs x (Abs s (subs y M L)) (subs y N L) = Abs s (subs x (subs y M L) (subs y N L))). 2: apply (subs_abs_neq x s (subs y M L) (subs y N L)). 2: auto. 2: rewrite s2. 2: rewrite IHM. 2: trivial. 2: unfold subs; fold subs. 2: rewrite IHM1; rewrite IHM2. 2: trivial. (* this finishes the proof *) (* the rest of this script is commented. it was just some experiments with Coq *) (* case (string_dec s x). intros s_eq_x' s_eq_y. apply sym_eq in s_eq_x. assert (x_eq_y: x = y). apply (trans_eq s_eq_x s_eq_y). contradiction. contradiction. unfold subs at 1; fold subs. case (string_dec s y). contradiction. unfold subs at 2; fold subs. case (string_dec s x). trivial. contradiction. intro s_neq_x. unfold subs at 4; fold subs. case (string_dec s y). intro s_eq_y. unfold subs at 3; fold subs. case (string_dec s x). contradiction. intro. unfold subs at 1; fold subs. apply subs_abs. unfold subs at 3; fold subs. case (string_dec s y). 2: contradiction. unfold subs at 2; fold subs. case (string_dec s x). contradiction. apply IHM. (*following experimental*) 4: intro s_neq_x. 4: case (string_dec s y). 4: intro s_eq_y. Show 6. Require Import DecidableType. (*?*) eq_sym s_eq_x; eq_trans s_eq_x s_eq_y . absurd x_neq_y. auto. unfold subs; fold subs. *) Qed.

**Follow-Ups**:**[isabelle] [nominal-isabelle] proving the substitution lemma***From:*Christian Urban

- Previous by Date: Re: [isabelle] [Coq-Club] proving the substitution lemma
- Next by Date: [isabelle] [nominal-isabelle] proving the substitution lemma
- Previous by Thread: Re: [isabelle] [Coq-Club] proving the substitution lemma
- Next by Thread: [isabelle] [nominal-isabelle] proving the substitution lemma
- 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