The Coq mailing list

["Harley D. Eades III" <harley.eades AT gmail.com>]

Hello everyone.

A while ago I formalized some of my research on the hereditary substitution
function in Coq.  At first I tried to define the function in Set using 
Program Fixpoint
and the wf annotation.  I was able to define the function and satisfy all the 
obligations.
However, I can't compute with it.  Even worse the subgoals generated are 
huge.  They
are over 1000 lines long.

Here is the function definition I am using:
Program Fixpoint hsubst_t (s:trm) (x:nat) (CUT:typ * trm) {wf lex CUT} : trm 
:= 
 match CUT with
   | (_,(trm_bvar x'))   => (trm_bvar x')
   | (_,(trm_fvar x'))   => match (nat_compare x x') with
                              | Eq => s
                              | _  => (trm_fvar x')
                            end
   | (T,(trm_lam T' t1))  => trm_lam T' (hsubst_t s x (T,t1))
   | (T,(trm_app t1 t2)) => 
     match (ctype T x t1) with
       | Some (typ_arrow T1 T2) => 
         let t1' := hsubst_t s x (T,t1) in
         let t2' := hsubst_t s x (T,t2) in
           match t1' with
             | trm_lam T j => 
               let free_vars := (FV_t j) ++ (FV_t t2') ++ (x::nil) in
               let y := pick_fresh free_vars in 
                 hsubst_t t2' y (T1,(open_t 0 (trm_fvar y) j))
             | _ => trm_app (hsubst_t s x (T,t1)) (hsubst_t s x (T,t2))
           end
       | _ => trm_app (hsubst_t s x (T,t1)) (hsubst_t s x (T,t2))
     end
   | (_,trm_c) => trm_c
 end.

I have a file which has everything in it here:
  http://homepage.cs.uiowa.edu/~heades/notes/Coq/hered_subst.v.  
Warning: it is an ugly file, but it all type checks.  The function is at the 
bottom of the file.

Is this the way I should be writing the program?  I want to be
able to define the above function, prove it correct, and then
extract it to Ocaml.  At the very least I would like to be able to
actually compute with the thing.

I need to be able to reason about this function.  For example, this lemma

Lemma hs_fvar : forall n, hsubst_t (trm_fvar n) n (typ_base, trm_fvar n) = 
trm_fvar n.

is trivial and I can't seem to prove it.  Even worse the subgoal is 1200 
lines long!

The issue is the fact that the termination argument is packaged up using 
sigma-types
and interlaced into the program definition.

My main question is, is this the right way to do this?  
Is there a better way?

In my formalization I got around all of this by working in Prop.  I defined 
the
function as an inductive proposition and proved it functional.  However, this
cannot be computed with so I am not completely satisfied with
that formalization.  In addition not being able to do this has been bugging me
so I thought I would ask the list.

Thanks for any feedback.

Harley