The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

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