The Coq mailing list

[St�phane Glondu <steph AT glondu.net>]

Le 27/02/2012 13:53, Francois Pottier a écrit :
> Let me say a little bit more about what I am trying to do. I have a goal
> whose form is roughly:
> 
>   f (C x) = ...
> 
> where C is a constructor of an inductive data type (say, "term") and where 
> the
> function is defined by induction over terms (i.e. it is a Fixpoint). 
> However,
> I (the library author) do not have access to the definition of "term", or to
> the definition of "f". In fact, I don't even have access to the names "f" 
> and
> "C".
> 
> What I would like to do at this point is perform one step of reduction, that
> is, reduce the application of f to (C x) by appealing to the definition of f
> as a Fixpoint.

Did you come up with a pure Ltac solution?

This precisely can be done easily with a plugin in OCaml. Compile it with:

  coq_makefile simpl_pottier.ml4 > Makefile
  make

Then have a look at the .v file.

Tested with the trunk, should be easy to adapt elsewhere.


Cheers,

-- 
Stéphane
(*i camlp4deps: "parsing/grammar.cma" i*)
(*i camlp4use: "pa_extend.cmo" i*)

open Pp
open Term
open Refiner
open Tacexpr

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;;
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.
reflexivity.
Qed.