[isabelle] proving the substitution lemma



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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.