The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

Oh, "lt_wf" is not hardcoded in the automation of Program.
It simply uses the "arith" hint database.
So, just adding "lt_wf_tp" to the database is enough.
Here is a simplified version.

==============================================================
Require Import Omega.

Lemma lt_wf_tp: well_founded lt.
Proof.
  intro n; induction n; constructor; intros; inversion H; eauto;
destruct IHn; eauto.
Defined.
Hint Resolve lt_wf_tp : arith.

Program Fixpoint Synterp (T : Term) (s : Assignment) {measure (Depth T)}: nat 
:=
  match T with
  | var x => s x
  | const c => c
  | apply f u v => M1 f (Synterp u s) (Synterp v s)
  | varapply G u x => M2 G (fun k => (Synterp (TermSub u (const k) x) s))
  end.
Next Obligation. simpl; omega. Qed.
Next Obligation. simpl; omega. Qed.
Next Obligation.
  clear Synterp; induction u; simpl; try destruct beq_nat; eauto;
simpl in *; omega.
Qed.

Lemma SynterpApply : forall (f : Functions L) (u : Term) (v : Term) (s
: Assignment),
    Synterp (apply f u v) s = M1 f (Synterp u s) (Synterp v s).
Proof.
  intros; unfold Synterp, Synterp_func, Wf.Fix_sub; simpl.
  do 2 f_equal; apply proof_irrelevance.
Qed.
=============================================================

Best,
Gil

On Sun, Nov 27, 2011 at 9:30 PM, Chung-Kil Hur 
<gil.hur AT gmail.com>
 wrote:
> Hi Alexander,
>
> Here is a solution using proof_irrelevance.
>
> =======================================================
> Require Import Omega.
>
> Lemma lt_wf_tp: well_founded lt.
> Proof.
>  intro n; induction n; constructor; intros; inversion H; eauto;
> destruct IHn; eauto.
> Defined.
>
> Local Obligation Tactic := idtac.
>
> Program Fixpoint Synterp (T : Term) (s : Assignment) {measure (Depth T)}: 
> nat :=
>  match T with
>  | var x => s x
>  | const c => c
>  | apply f u v => M1 f (Synterp u s) (Synterp v s)
>  | varapply G u x => M2 G (fun k => (Synterp (TermSub u (const k) x) s))
>  end.
> Next Obligation. intros; subst; simpl; omega. Qed.
> Next Obligation. intros; subst; simpl; omega. Qed.
> Next Obligation.
>  intros; subst; clear Synterp; induction u; simpl; try destruct
> beq_nat; eauto; simpl in *; omega.
> Qed.
> Next Obligation. apply Wf.measure_wf, lt_wf_tp. Defined.
>
> Lemma SynterpApply : forall f : Functions L, forall u : Term, forall v
> : Term, forall s : Assignment,
>    Synterp (apply f u v) s = M1 f (Synterp u s) (Synterp v s).
> Proof.
>  intros; unfold Synterp, Synterp_func, Wf.Fix_sub; simpl; do 2
> f_equal; apply proof_irrelevance.
> Qed.
> ===========================================================
>
> The default automation of "Program with measure" automatically solves
> the fourth obligation,
> but using the lemma 'lt_wf', which is not completely transparent since
> it uses several opaque lemmas.
> This caused some problems with unfolding of the definition "Synterp".
> So, I turned off the automation and proved the fourth obligation using
> 'lt_wf_tp', which is completely transparent.
>
> I wonder wether there is any benefit using 'lt_wf' rather than a
> completely transparent one.
> Matthieu, can you answer this question?
>
> Best,
> Gil
>
>
> On Sun, Nov 27, 2011 at 3:00 AM, 
> �<alexander AT math.ohio-state.edu>
>  wrote:
>> For a full compilable file to put the below examples in context, see
>> http://www.math.osu.edu/~alexander/variadic/variadic4.txt
>>
>> I have the following Program Fixpoint structure:
>>
>> Program Fixpoint Synterp (T : Term) (s : Assignment) {measure (Depth T)}: 
>> nat
>> :=
>>  match T with
>>  | var x => s x
>>  | const c => c
>>  | apply f u v => M1 f (Synterp u s) (Synterp v s)
>>  | varapply G u x => M2 G (fun k => (Synterp (TermSub u (const k) x) s))
>>  end.
>>
>> It generates 3 obligations which I prove easily enough.  But then when I
>> actually attempt to prove things about Synterp, it unfolds incorrectly. 
>>  For
>> example, I try to prove what should be very easy:
>>
>> Lemma SynterpApply : forall f : Functions L, forall u : Term, forall v : 
>> Term,
>> forall s : Assignment,
>>    Synterp (apply f u v) s = M1 f (Synterp u s) (Synterp v s).
>>
>> (Note that this is *identical* to the definition, so should be totally 
>> trivial
>> to prove.)
>>
>> I begin the proof with "intros." and the state is:
>>
>> 1 subgoal
>>
>>  f : Functions L
>>  u : Term
>>  v : Term
>>  s : Assignment
>>  ============================
>>   Synterp (apply f u v) s = M1 f (Synterp u s) (Synterp v s)
>>
>> I try "simpl.", which ought to expand the left hand side, but nothing 
>> happens.
>> Odd.  So i try "unfold Synterp." and here's what I get:
>>
>> 1 subgoal
>>
>>  f : Functions L
>>  u : Term
>>  v : Term
>>  s : Assignment
>>  ============================
>>   Synterp_func (existT (fun _ : Term => Assignment) (apply f u v) s) =
>>   M1 f (Synterp_func (existT (fun _ : Term => Assignment) u s))
>>     (Synterp_func (existT (fun _ : Term => Assignment) v s))
>>
>> What the?!  I can't make sense of this.  I cannot complete the proof of the
>> lemma, which ought to be as simple as "auto." since it's taken directly 
>> from
>> the definition of Synterp.
>>
>> Right now I'm getting around the dilemma by adding hypotheses:
>>
>> Hypothesis SynterpVar : forall x : variable, forall s : Assignment, Synterp
>> (var x) s = s x.
>>
>> Hypothesis SynterpApply : forall f : Functions L, forall u : Term, forall 
>> v :
>> Term, forall s : Assignment,
>>        Synterp (apply f u v) s = M1 f (Synterp u s) (Synterp v s).
>>
>> Hypothesis SynterpVarapply : forall G : VarFuncs L, forall u : Term, 
>> forall x :
>> variable, forall s : Assignment,
>>        Synterp (varapply G u x) s = M2 G (fun k => (Synterp (TermSub u 
>> (const
>> k) x) s)).
>>
>> These hypotheses should not be necessary though, since they are all just
>> identical to the original definition.  What's going on here and how can I
>> repair it?
>>
>> Thanks very much for helping :)
>> -Sam
>>
>