The Coq mailing list

[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