The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 14 Dec 2012 09:33:17 -0600,
"Harley D. Eades III" 
<harley.eades AT gmail.com>
 a écrit :

A lot of people have already replied to you.
But I can add some comment.

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

All the pointed expressions can be factorised, thus reducing slightly
the number of required proofs, and the size of the term.

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