The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Wild guess of sleepy sunday mornings: try to finish your Obligations
with Defined instead of Qed.
This way Coq will be allowed to unfold them.

Not sure if it will solve your issue but that's usually the first thing I try.

Best,
Vincent

2011/11/27  
<alexander AT math.ohio-state.edu>:
> 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
>