The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Hai WAN wrote:
> Dear all,
>
> Is there any commands can help me to explore the dependencies among theorems
> in a Coq proof script?
>
> I've found a paper about this : Dependency Graphs for Interactive Theorem
> Provers (2000) and wonder is there any realization of this idea?
>
> Thanks in advance.
>   
One of the missing basic blocks is a command that makes it possible to 
generate a list of all theorems that are used in the proof of another 
theorem.    Here is a file that defines such a command.  I tested it on 
CoqV8.1pl3 and the trunk version of today.  It should be a trivial 
matter to extend this command so that it performs the search of 
dependencies recursively on all theorems on which the first argument 
depends, but I don't have the time to do it just now.  This could also 
be turned into a plugin for Coq.

To test this file, you should normally have to perform the following steps:

coq_makefile -f Make > Makefile
make
./coqthmdep

An example of usage is the following command: this lists all the objects 
(except for
constructors of inductive types) that the theorem mult_n_Sm depends on.

SearchDepend mult_n_Sm.

Yves
(*i camlp4deps: "parsing/grammar.cma" i*)
open Names;;
open Libnames;;
open Term;;
open Pp;;
open Printer;;
open Global;;
open Declarations;;
open Constrintern;;
open Environ;;

type data = {ind : KNset.t; con : Cset.t}

let add_identifier (x:identifier)(d:data) = 
  failwith 
    ("SearchDep does note expect to find plain identifiers :" ^
      string_of_id x);;

let add_sort (s:sorts)(d:data) = d;;

let add_constant (cst:constant)(d:data) =
  {ind = d.ind; con = Cset.add cst d.con};;

let add_inductive ((k,i):inductive)(d:data) =
  {ind = KNset.add k d.ind; con = d.con}

let add_constructor(((k,i),j):constructor)(d:data) =
  {ind = KNset.add k d.ind; con = d.con}

let collect_long_names (c:constr) (acc:data) =
  let rec f c acc =
  match kind_of_term c with
    Rel _ -> acc
  | Var x -> add_identifier x acc
  | Meta _ -> assert false
  | Evar _ -> assert false
  | Sort s -> add_sort s acc
  | Cast(c,_,t) -> f c (f t acc)
  | Prod(n,t,c) -> f t (f c acc)
  | Lambda(n,t,c) -> f t (f c acc)
  | LetIn(_,v,t,c) -> f v (f t (f c acc))
  | App(c,ca) -> f c (Array.fold_right f ca acc)
  | Const cst -> add_constant cst acc
  | Ind i -> add_inductive i acc
  | Construct cnst -> add_constructor cnst acc
  | Case({ci_ind=i},c,t,ca) ->
     add_inductive i (f c (f t (Array.fold_right f ca acc)))
  | Fix(_,(_,ca,ca')) -> Array.fold_right f ca (Array.fold_right f ca' acc)
  | CoFix(_,(_,ca,ca')) -> Array.fold_right f ca (Array.fold_right f ca' acc)
in f c acc;;

let display_global_references (d:data) =
  msgnl [< str"[" ++
           (Cset.fold (fun r s -> [<pr_global (ConstRef r) ++ spc() ++s >])
              d.con 
              (KNset.fold (fun r s -> 
                           [<pr_global (IndRef(r,0)) ++ spc() ++ s >])
                 d.ind (str "]"))) >];;
                        
let empty_data = {ind = KNset.empty; con = Cset.empty}

let display_inductive (i:inductive) =
  let _, indbody = lookup_inductive i in
    let {mind_user_lc=ca} = indbody in
    let deps = Array.fold_right collect_long_names ca empty_data in
    display_global_references deps;;

let display_dependance id = 
  let c = locate_reference (make_short_qualid id) in
  match c with
    VarRef _ -> assert false
  | ConstRef cst ->
    let cb = lookup_constant cst (env()) in
    let c = match cb.const_body with Some c -> Declarations.force c 
              | _ -> failwith (string_of_id id ^ " has no value") in
    display_global_references (collect_long_names c empty_data)
  | IndRef i -> display_inductive i
  | ConstructRef(i,k) -> display_inductive i;;


  
VERNAC COMMAND EXTEND Searchdepend
   ["SearchDepend" ident(id) ] ->
  [ display_dependance id ; ]
END-custom "$(COQMKTOP) $(COQMKTOPFLAGS) -opt -o coqthmdep searchdepend.cmx" 
searchdepend.cmx coqthmdep
COQMKTOP = coqmktop
searchdepend.ml