Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: lemma distribution


view this post on Zulip Patrick Massot (Oct 04 2020 at 13:25):

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.

view this post on Zulip Scott Morrison (Oct 05 2020 at 03:30):

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

view this post on Zulip Scott Morrison (Oct 05 2020 at 03:30):

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

view this post on Zulip Scott Morrison (Oct 05 2020 at 03:30):

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

view this post on Zulip Scott Morrison (Oct 05 2020 at 03:31):

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

view this post on Zulip Scott Morrison (Oct 05 2020 at 03:38):

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.

view this post on Zulip Scott Morrison (Oct 05 2020 at 03:40):

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!

view this post on Zulip Mario Carneiro (Oct 05 2020 at 04:19):

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

view this post on Zulip Rob Lewis (Oct 05 2020 at 08:14):

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.

view this post on Zulip Rob Lewis (Oct 05 2020 at 08:15):

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

view this post on Zulip Rob Lewis (Oct 05 2020 at 08:16):

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

view this post on Zulip Rob Lewis (Oct 05 2020 at 08:17):

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


Last updated: May 09 2021 at 22:13 UTC