The Coq mailing list

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

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
>