UnfoldFixpointOnce

Pierre Letouzey edited this page Oct 27, 2017 · 5 revisions

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).

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.