The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

Hi,

I have a question about solving obligations generated by Program  
Fixpoint in the current svn snapshot of Coq 8.2 (r11354).  I'm using  
the documentation at http://coq.inria.fr/V8.2beta4/doc/refman/html/ .   
Consider the following silly and trivial example.  (There's no reason  
to do this in practice, but it does illustrate my problem.)  My  
questions come at the end.

<<
Require Import Program.
Require Import Omega.

Inductive exp : Set :=
  | bvar : nat  -> exp
  | fvar : nat -> exp
  | abs  : exp -> exp
  | app  : exp -> exp -> exp.

Fixpoint size (e : exp) {struct e} : nat :=
  match e with
    | bvar i => 1
    | fvar x => 1
    | abs e1 => 1 + size e1
    | app e1 e2 => 1 + size e1 + size e2
  end.

(* Obligations Tactic := simpl; omega. (* doesn't parse? *) *)

Program Fixpoint exp_rect'
  (P : exp -> Type)
  (Hbvar : forall n, P (bvar n))
  (Hfvar : forall x, P (fvar x))
  (Habs : forall e1, P e1 -> P (abs e1))
  (Happ : forall e1, P e1 -> forall e2, P e2 -> P (app e1 e2))
  (e : exp) {measure size e} : P e :=
  match e with
    | bvar i => Hbvar i
    | fvar x => Hfvar x
    | abs e1 => Habs e1 (exp_rect' e1)
    | app e1 e2 => Happ e1 (exp_rect' e1) e2 (exp_rect' e2)
  end.

Solve All Obligations using simpl; omega. (* does nothing? *)

Next Obligation. simpl; omega. Qed.
Next Obligation. simpl; omega. Qed.
>>

First, is "Obligations Tactic" supposed to parse?  How else might I  
set the default tactic to be applied to generated obligations?

Second, why does Solve All Obligations not do anything?  The tactic  
I've provided it works when I step through the obligations by hand.

At a higher level, I want some way of telling Coq how to solve all  
generated obligations.  The documentation suggests that this is  
implemented and code in the standard library seems to use this  
feature, so I'm confused by my own experience here.

Thanks for any help,
Brian