UnfoldFixpointOnce

This tactic unfolds a fixpoint once. See evar_match for a more basic example of tactic written in OCaml, and instructions on how to compile it.

(*i camlp4deps: "parsing/grammar.cma" i*)
(*i camlp4use: "pa_extend.cmo" i*)
open Pp
open Term
open Refiner
open Tacexpr
open Util
let fail () = tclFAIL 0 (str "not an expected form")
(** Run tactic [k] with constr [x] as argument. *)
let run_cont k x =
  let k = TacDynamic(dummy_loc, Tacinterp.tactic_in (fun _ -> k)) in
  let x = TacDynamic(dummy_loc, Pretyping.constr_in x) in
  let tac = <:tactic<let cont := $k in cont $x>> in
  Tacinterp.interp tac
(** If [f] is a reference to fixpoint, return the index of its
    decreasing argument and its body, where the recursive call is a
    reference to the fixpoint. *)
let unfold_fixpoint_once env f =
  begin match kind_of_term f with
    | Const c ->
      let decl = Environ.lookup_constant c env in
      begin match Declarations.body_of_constant decl with
        | Some b ->
          begin match kind_of_term (Declarations.force b) with
            | Fix ((is, i), (ns, ts, bs)) ->
              Some (is.(i), subst1 f bs.(i))
            | _ -> None
          end
        | None -> None
      end
    | _ -> None
  end
let rec apply_and_beta_reduce f = function
  | [] -> f
  | x::xs as ys ->
    begin match kind_of_term f with
      | Lambda (_, _, b) -> apply_and_beta_reduce (subst1 x b) xs
      | _ -> mkApp (f, (Array.of_list ys))
    end
TACTIC EXTEND simpl_pottier
  | [ "simpl_pottier" constr(x) tactic(k) ] ->
    [
      let env = Global.env () in
      begin match kind_of_term x with
        | App (f, args) ->
          begin match unfold_fixpoint_once env f with
            | Some (i, b) ->
              if i < Array.length args then
                (* check that the decreasing argument is in constructor form *)
                begin match kind_of_term args.(i) with
                  | App (cc, _) when isConstruct cc ->
                    run_cont k (apply_and_beta_reduce b (Array.to_list args))
                  | _ -> fail ()
                end
              else fail ()
            | None -> fail ()
          end
        | _ -> fail ()
      end
    ]
END;;

This plugin provides a simpl_pottier tactic that takes two arguments: a Coq term t (constr) and a continuation tactic k, checks that t is an applied fixpoint whose decreasing argument starts with a constructor, and calls k with the result of unfolding the fixpoint once. Example of use, assuming the plugin is named simpl_pottier.{cma,cmxs} (it answers this post):

Declare ML Module "simpl_pottier".
Ltac simpl_left :=
  match goal with
    | |- ?a = ?b => simpl_pottier a (fun x => change (x = b))
  end.
Goal forall n m, S n + m = S (n + m).
intros.
simpl_left. (* look here *)
reflexivity.
Qed.

Tested with Coq v8.4 r15016 (2012-03-02) and trunk r15022 (2012-03-02).