The Coq mailing list

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

Le 12/04/2012 19:30, Xavier Leroy a écrit :
> Short form: is there a tool / how would you go about writing a tool
> that, given the *statement* of a Coq theorem, shows all *definitions*
> involved in this statement, omitting all the stuff that contribute
> only to the *proof* of the theorem?

This can be done in a plugin. I've attached a proof of concept.


Cheers,

-- 
Stéphane
(* Reference:
     http://article.gmane.org/gmane.science.mathematics.logic.coq.club/8119

   Compile with: (tested with Coq 8.4beta)
     coq_makefile recursive_specification.ml4 > Makefile
     make
*)

(*i camlp4deps: "parsing/grammar.cma" i*)
(*i camlp4use: "pa_extend.cmo" i*)

open Names
open Term
open Declarations
open Util
open Libnames

let (|>) x f = f x

type global_item =
  | Constant of constant
  | MutInd of mutual_inductive

let rec collect_globals x accu = match kind_of_term x with
  | Const c -> collect_in_constant c accu
  | Ind (mi, _) -> collect_in_mutind mi accu
  | Construct ((mi, _), _) -> collect_in_mutind mi accu
  | Rel _
  | Sort _ -> accu
  | Var _
  | Meta _
  | Evar _ -> assert false (* should not happen *)
  | Cast (a, _, b)
  | Prod (_, a, b)
  | Lambda (_, a, b) -> accu
    |> collect_globals a
    |> collect_globals b
  | LetIn (_, a, b, c) -> accu
    |> collect_globals a
    |> collect_globals b
    |> collect_globals c
  | App (f, xs) -> accu
    |> collect_globals f
    |> Array.fold_right collect_globals xs
  | Case ({ci_ind = (mi, _); _}, a, b, xs) -> accu
    |> collect_in_mutind mi
    |> collect_globals a
    |> collect_globals b
    |> Array.fold_right collect_globals xs
  | Fix (_, (_, ts, xs))
  | CoFix (_, (_, ts, xs)) -> accu
    |> Array.fold_right collect_globals ts
    |> Array.fold_right collect_globals xs

and collect_in_rel_context ctxt accu =
  List.fold_right (fun (_, b, t) accu ->
    let accu = collect_globals t accu in
    match b with
      | Some b -> collect_globals b accu
      | None -> accu
  ) ctxt accu

(* Constant declarations *)

and collect_in_constant c accu =
  let c' = Constant c in
  if List.mem c' accu then accu else c'::(
    let body = Global.lookup_constant c in
    assert (body.const_hyps = []);
    let accu = match body.const_body with
      | Undef _ | OpaqueDef _ -> assert false
      | Def x -> collect_globals (force x) accu
    in
    let accu = match body.const_type with
      | NonPolymorphicType t -> collect_globals t accu
      | PolymorphicArity (ctxt, _) -> collect_in_rel_context ctxt accu
    in
    accu
  )

(* Inductive declarations *)

and collect_in_mutind mi accu =
  let mi' = MutInd mi in
  if List.mem mi' accu then accu else mi'::(
    let body = Global.lookup_mind mi in
    assert (body.mind_hyps = []);
    accu
      |> collect_in_rel_context body.mind_params_ctxt
      |> Array.fold_right collect_in_one_ind body.mind_packets
  )

and collect_in_one_ind i accu = accu
  |> collect_in_rel_context i.mind_arity_ctxt
  |> collect_in_ind_arity i.mind_arity
  |> Array.fold_right collect_globals i.mind_user_lc

and collect_in_ind_arity a accu = match a with
  | Monomorphic {mind_user_arity = t; _} -> collect_globals t accu
  | Polymorphic _ -> accu

(* Vernacular command *)

let recursive_specification x =
  let t = x |> Nametab.global |> Global.type_of_global in
  collect_globals t [] |>
  List.rev_map (fun g ->
    let (d, p) = match g with
      | Constant c -> decode_con c
      | MutInd mi -> decode_mind mi
    in Prettyp.print_name (Genarg.AN (Qualid (dummy_loc, (make_qualid d p))))
  ) |>
  List.iter Pp.msgnl

VERNAC COMMAND EXTEND RecursivePrint
| [ "Recursive" "Specification" global(x) ] -> [ recursive_specification x ]
END;;
Declare ML Module "recursive_specification".

Require Arith.

Definition power := NPeano.pow.

Theorem Fermat:
  forall (x y z n: nat),
  n >= 3 -> x >= 1 -> y >= 1 -> z >= 1 ->
  power x n + power y n <> power z n.
Proof.
  (* bla bla bla *)
Admitted.

Recursive Specification Fermat.