The Coq mailing list

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

Hi, Matthieu.

On Dec 14, 2012, at 11:51 AM, Matthieu Sozeau 
<matthieu.sozeau AT gmail.com>
 wrote:

> 
> On 14 déc. 2012, at 10:33, Harley D. Eades III 
> <harley.eades AT gmail.com>
>  wrote:
> 
>> 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.
> <snip/>
>> My main question is, is this the right way to do this?  
>> Is there a better way?
> 
> Hi Harley,
> 
> Yes, there is a better way:
> You should define an unfolding lemma first to reason about the behavior of 
> the function.
> Note that I added some [return _] to the inner matches where you didn't 
> need the equality
> between the scrutiny and the pattern as well (makes for smaller generated 
> code).
> 
> Here's how to define it:
Thank you so much for this very detailed response.  It helps a lot!

I am going to play around with this later this weekend!

I think you may have helped revive my original formalization.  :-)

Thanks,
Harley

> <<
> Program Definition hsubst_t_unfold (s:trm) (x:nat) (CUT:typ * trm) : trm := 
>  match CUT with
>    | (_,(trm_bvar x'))   => (trm_bvar x')
>    | (_,(trm_fvar x'))   => match (nat_compare x x') return _ 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' return _ 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.
> 
> (* Lemma fix_sub_eq_rect is there *)
> Import WfExtensionality.
> 
> Lemma hsubst_t_unfold_eq s x cut : hsubst_t s x cut = hsubst_t_unfold s x 
> cut.
> Proof.
>  unfold hsubst_t.
>  (* Use setoid_rewrite to rewrite under the hsubst_t_func constant which 
>     hides a Fix_sub *)
>  setoid_rewrite fix_sub_eq_ext.
>  reflexivity.
> Qed.
> 
> (* Now you can reason on the unfolded version. *)
> Lemma hs_fvar : forall n, hsubst_t (trm_fvar n) n (typ_base, trm_fvar n) = 
> trm_fvar n.
> Proof.
>  intros. rewrite hsubst_t_unfold_eq. simpl.  destruct (nat_compare n n); 
> reflexivity.
> Qed.
>>> 
> 
> Now for computing, you have to have a transparent [wf] proof, which 
> currently contains
> a lot of opaque constants that reduction will get stuck at. Using the 
> lexprod construct
> from the standard library and measures, you can define simply a fully 
> transparent [wf] proof 
> and should be able to solve the resulting obligations in much the same way 
> you did, 
> using mainly computation and a little bit of the theory of [lt] (only 
> transparent proofs
> as well).
> 
> <<
> Require Import Relations Wellfounded.Wellfounded.
> 
> Definition order :=
>  lexprod typ (fun _ => trm) (MR lt typ_size) (fun _ => MR lt trm_size).
> 
> Lemma wf :    
>  well_founded order.
> Proof.
>  apply wf_lexprod. apply measure_wf. apply lt_wf. intro; apply measure_wf. 
> apply lt_wf.
> Defined.
> 
> Definition order' (x y : typ * trm) := 
>  let x' : { _ : typ & trm } := existT _ (fst x) (snd x) in
>  let y' : { _ : typ & trm }  := existT _ (fst y) (snd y) in
>  order x' y'.
> 
> (* Dep to non dep sums ordering *)
> Lemma wf' :    
>  well_founded order'.
> Proof. 
>  unfold well_founded. 
>  destruct a as [ty tr].
>  remember (existT (fun _ => trm) ty tr) as arg.
>  assert (acc:=wf arg). revert ty tr Heqarg.
>  induction acc. intros. subst x.
>  constructor; intros.
>  destruct y. eapply H0.
>  apply H1. reflexivity.
> Defined.
>>> 
> 
> Hope this helps,
> -- Matthieu