lemma distribution

Stream: metaprogramming / tactics

[Patrick Massot]

For meta-programmers looking for ideas: a really nice command would tell us where to put lemmas. When I work on some small new piece, I start a new file where I write everything I need. And then most of the work (much longer than writing statements and proving them) is to find in which file each lemma needs to go. Ideally I'd like to type #find_home my_lemma and Lean would answer: "This lemma could go in this_file.lean, line 500". The basic algorithm is to traverse all declarations used in my_lemma (in its type or value) and figure out whether there is a declaration after which everything is available.

[Scott Morrison]

The first epsilon, perhaps:

import tactic

open tactic

meta def referenced_decls (d : declaration) : name_set :=
d.type.list_constant.fold d.value.list_constant (λ n s, s.insert n)

meta def required_imports (d : declaration) : tactic (list string) :=
do
  env ← get_env,
  return $ ((referenced_decls d).fold [] (λ n L, L ++ (env.decl_olean n).to_list)).erase_dup

example : true :=
begin
   (do e ← get_env,
    d ← get_decl `referenced_decls,
    trace (referenced_decls d),
    trace (required_imports d),
    skip),
  trivial,
end

[Scott Morrison]

It would be really nice to have a function that returns the list of imports of a given lean file.

[Scott Morrison]

However it doesn't seem like this information is even tracked at the C++ level, as far as I can see.

[Scott Morrison]

Perhaps Lean calling grep is the right solution. :-)

[Scott Morrison]

I'm imagining that the algorithm is:

1. find all "required imports" for a given declaration (done, above)
2. for each of those imported files, find the files it transitively imports
3. take the complement

If the complement is a singleton, you win --- that's where you want to put the lemma, and a second stage can work out the appropriate line number using get_decl_pos. If the complement is more than a singleton, there'll have to be some sort of advice/consolation message.

[Scott Morrison]

If we can't get access to the list of files a given file imports, we could hack it, by traversing the list of every declaration, filtering those that a defined in the given file, and then called required_imports on those. This would only report the imports that are actually needed!

[Mario Carneiro]

The list of imports of a given file is certainly tracked, it is in a prominent position in the generated olean files and olean-rs can pick it up without too much trouble

[Rob Lewis]

I think the proper way to do this is with the docs#environment.for_decl_of_imported_module API. This API comes with a big bold warning but I think it's safe here. Maybe --old would cause trouble? In any case, the code below is more than epsilon progress, but needs polishing for declarations that belong in the current file.

[Rob Lewis]

import data.real.basic

meta def expr.get_constants (e : expr) : name_set :=
e.fold mk_name_set $ λ e' _ s, match e' with
| expr.const nm _ := s.insert nm
| _ := s
end

meta def declaration.get_constants : declaration → name_set
| (declaration.ax nm _ tp) := tp.get_constants
| (declaration.cnst nm _ tp is_meta) := tp.get_constants
| (declaration.thm nm _ tp bd) := tp.get_constants.union bd.get.get_constants
| (declaration.defn nm _ tp bd _ is_meta) := tp.get_constants.union bd.get_constants

namespace tactic

meta def module_info_of_decl (n : name) : tactic module_info :=
do e ← get_env,
match e.decl_olean n with
| some s := return $ module_info.of_module_id s
| none := failed
end

meta def get_env_of (n : name) : tactic environment :=
do e ← get_env,
match e.decl_olean n with
| some s := return $ environment.for_decl_of_imported_module s n
| none := fail!"couldn't find {n}"
end

meta def test_names_at (ns : name_set) (tgt : name) : tactic bool :=
do e ← get_env_of tgt,
   return $ ns.fold tt $ λ nm b, b && e.contains nm

meta def find_highest (tgt : name) : tactic name :=
do d ← get_decl tgt,
let cnsts := d.get_constants,
cnsts.to_list.mfirst (λ nm,
  test_names_at (cnsts.erase nm) nm >>= guardb >> return nm) <|>
fail "didn't find any highest decl"

meta def locate_decl (tgt : name) : tactic unit :=
do highest ← find_highest tgt,
   e ← get_env,
   let file := match e.decl_olean highest with
   | none := "the current file"
   | some s := (module_info.of_module_id s).id
   end,
   trace!"{tgt} belongs in {file} after {highest}"

end tactic

lemma real_big : (3000 : ℝ) + 2 > 50 := by norm_num

def recfn : ℕ → ℕ
| 0 := 0
| (n+1) := n

run_cmd tactic.locate_decl ``real_big
-- real_big belongs in /Storage/lean/mathlib/src/data/real/basic.lean after real.has_add

run_cmd tactic.locate_decl ``recfn

[Rob Lewis]

This doesn't do any fancy graph stuff, it checks every constant at every other one, so it's potentially very slow.

[Rob Lewis]

And it doesn't work as expected on things like recfn, which generates a _main aux def.