The Coq mailing list

[Christian Urban <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