# [isabelle] [nominal-isabelle] proving the substitution lemma

```Dear Moez,

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

> 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

```

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