The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

Hello all,

I am trying to encode the lambda calculus in Coq using de Bruijn indices,
using an encoding style which keeps track of the number of free variables
in the type. So, here's the representation:

Inductive Lamexp : nat -> Set
  := var  : (i:nat) (Lamexp (S i))
  |  abs  : (i:nat) (Lamexp (S i)) -> (Lamexp i)
  |  app  : (i:nat) (Lamexp i) -> (Lamexp i) -> (Lamexp i)
  |  lift : (i:nat) (Lamexp i) -> (Lamexp (S i)).

A variable of index i must imply it is a term of (i+1) free variables. 
Abstractions encapsulate a term with at least one free variable. The lift 
is used because a term of i free variables can also be viewed as a term 
with (i+1) free variables (where the (i+1)'th variable is not present).

Now, I want to write a substitution function which substitutes a term for 
the *outermost* free variable in a given term. So the type is something like:

Definition Subst (k:nat) (Lamexp (S k)) -> (Lamexp k) -> (Lamexp k).

Of course, this should be written as a fix-point and I think the correct 
way it should work is something like this:


Fixpoint Subst [k:nat; L:(Lamexp (S k))] : (Lamexp k) -> (Lamexp k)
:= [T]
Cases L of (var i) -> T (* because it must be the outermost *)
         | (abs O R) -> (abs O R)
         | (abs (S i) R) -> (abs i (Subst (S i) R (lift i T)))
         | (app O a b) -> (app O a b)
         | (app (S i) a b) -> (app i (Subst i a T) (Subst i b T))
	 | (lift i R) -> R (* if term R contained the variable at the outermost 
level, it wouldn't need lifting *)
.


There are some problems here, since the above code doesn't work:

- Actually, the (abs O...) and (app O...) cases cannot occur because of the 
type of L.

- Additionally, in some cases, you need to know that i=k for the type to 
match the expected by of Subst.

- Now, usually, I've seen the above two situations solved by wrapping the 
"Cases" and having it take an additional parameter which would prove 
equality between i and k, and then you use "eq_ind/rec" (and "False_rec") 
to work it all out. Unfortunately, it seems doing this pushes the recursive 
calls to Subst under an abstraction and then Coq gives an "ill-founded 
recursion" error.

So, any ideas on this will be most appreciated. I don't know what are the 
exact limitations on the Fixpoint/Cases syntax and whether it allows this 
to be defined, or maybe I have to use directly the more primitive 
"Lamexp_rec" to defined Subst?



Now, if this problem above is really solvable in Coq, then I would actually 
like to do a little more. Let's say I also want to add tuples to the 
language. So they could be represented as something like:

Inductive Lamexp : nat -> Set
  := var  : (i:nat) (Lamexp (S i))
  |  abs  : (i:nat) (Lamexp (S i)) -> (Lamexp i)
  |  app  : (i:nat) (Lamexp i) -> (Lamexp i) -> (Lamexp i)
  |  tup  : (i:nat) (list (Lamexp i)) -> (Lamexp i)
  |  lift : (i:nat) (Lamexp i) -> (Lamexp (S i)).

or, building in an isomorphic definition of lists:

Mutual
Inductive Lamexp : nat -> Set
  := var  : (i:nat) (Lamexp (S i))
  |  abs  : (i:nat) (Lamexp (S i)) -> (Lamexp i)
  |  app  : (i:nat) (Lamexp i) -> (Lamexp i) -> (Lamexp i)
  |  tup  : (i:nat) (LamexpL i) -> (Lamexp i)
  |  lift : (i:nat) (Lamexp i) -> (Lamexp (S i))
with
LamexpL : nat -> Set
  := nilL : (i:nat)(LamexpL i)
  | consL : (i:nat)(Lamexp i) -> (LamexpL i) -> (LamexpL i)
.

So, now instead of one fixpoint, there would be two mutually recursive 
fixpoints needed to define the substitution function above, correct?


Any suggestions/help is greatly appreciated.

--- nadeem