The Coq mailing list

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

On May 8, 2007, at 2:45 PM, Sean Wilson wrote:

> Also, are there any ways in which Ltac tactics can return results  
> (like lists  or numbers) for other tactics to use? For instance,  
> can I write a tactic that returns a list of all assumptions in the  
> hypothesis with type nat which can be passed as input to another  
> tactic which calls "clear" for each assumption found?

I believe the general answer is "yes".  For your particular example,  
you can try the following:

(* ************************************************** *)
Require Import List.

Ltac gather_nat_hyps :=
  let rec gather acc :=
    match goal with
    | H : nat |- _ =>
        match acc with
        (* This first case is important as it
           allows us to avoid an infinite loop.
           See also: how "match goal with" works.
        *)
        | context [H] => fail 1
        | _ => gather (H :: acc)
        end
    | _ => acc
    end
  in
    gather (@nil nat).

Ltac clear_hyps Hs :=
  match Hs with
  | nil => idtac
  | cons ?H ?Hs => try clear H; clear_hyps Hs
  end.

Lemma test : forall (a b c n m : nat), n = m.
Proof.
  intros.
  clear_hyps gather_nat_hyps.
(* ************************************************** *)

I believe gather_nat_hyps has a running time quadratic in the size of  
the current context, but together, these tactics seem to do what you  
asked.  (Maybe there is a better way to do a fold over the current  
context?)  In any event, I've found Chapter 9 of the reference manual  
(The tactic language) to be a useful reference.

Hope that helps,
Brian