full names

Stream: general

[Patrick Massot]

Is there a way to ask Lean to list all fully qualified names (I mean including namespaces) defined by a particular file? I'd like to check I didn't messed up with name spaces

[Simon Hudon]

The way I would do it is I would write a command in a run_cmd block and use environment.fold to iterate over all the visible declarations, get their names and use environment.in_current_file to filter out any declaration that comes from outside. It will give you a list of fully qualified names.

[Simon Hudon]

Oh, and in a tactic, you use get_env to get the current environment.

[Patrick Massot]

Thanks Simon, but I'm afraid you assume too much knowledge from me.

[Simon Hudon]

No worries, I like starting with a brief overview but I'm happy to go step by step with you if need be.

[Simon Hudon]

Let's start with a script that just prints all the visible names (even the ones from other files).

[Simon Hudon]

run_cmd
do curr_env <- get_env,
   let decls := curr_env.fold [] list.cons, -- this loops over all the visible declarations and, using `list.cons`, accumulate them in a list
   let names := decls.map declaration.to_name, -- this takes the name of each declaration.
   trace names

[Simon Hudon]

Does it make sense so far?

[Patrick Massot]

It makes sense to me but not to Lean

[Patrick Massot]

"type of sorry macro is not a sort"

[Patrick Massot]

probably missing import or open

[Simon Hudon]

that makes sense. Try open tactic.

[Kevin Buzzard]

[Kevin Buzzard]

deep recursion was detected at 'formatter' (potential solution: increase stack space in your system)

[Patrick Massot]

"deep recursion was detected at 'formatter' (potential solution: increase stack space in your system)"

[Patrick Massot]

:simple_smile:

[Patrick Massot]

Maybe we have infinitely nested namespaces

[Simon Hudon]

Interesting. What if you just do trace names.length?

[Patrick Massot]

22573

[Patrick Massot]

:laughing:

[Patrick Massot]

Maybe we should jump to the filtered version

[Simon Hudon]

Good. That will be good enough for now. The problem is that we have a lot of definitions but we don't care about all of them. Let's filter the list and then we can print them all out

[Simon Hudon]

You're using so few words to express my idea. I'm jealous

[Simon Hudon]

Do you have an idea on how to do the filtering?

[Patrick Massot]

Yes: using environment.in_current_file

[Patrick Massot]

I'm such a good student :open_mouth:

[Simon Hudon]

You get an A! Good job!

[Simon Hudon]

Once you've done that and defined a new list local_names, you can print them more nicely as local_names.mmap' trace

[Patrick Massot]

"code generation failed, VM does not have code for 'classical.choice'". I may have taken a wrong turn...

[Patrick Massot]

I was trying to get rid of that damn environment.in_current_file curr_env has type name → bool but is expected to have type name → Prop

[Patrick Massot]

I'm probably beaten for my preamble

[Patrick Massot]

Yeah, in a fresh file Lean complains it wants a decidable instance

[Patrick Massot]

(deleted)

[Patrick Massot]

(deleted)

[Patrick Massot]

I give up, it seems I don't know enough. I tried let noms := names.filter (environment.in_current_file curr_env), but Lean wants a decidable function to prop, not a function to bool

[Simon Hudon]

Try let noms := names.filter (λ n, curr_env.in_current_file n)

[Patrick Massot]

This works if there is mathematics preamble

[Simon Hudon]

Which preamble?

[Patrick Massot]

local attribute [instance] classical.prop_decidable

[Mario Carneiro]

that's obviously a bad idea if you are writing code

[Simon Hudon]

You shouldn't need that. Booleans are decidable propositions

[Patrick Massot]

Of course it means I should define the command in its own file and execute it where I need it

[Simon Hudon]

If you use classical.prop_decidable try local attribute [instance, priority 0] classical.prop_decidable. This way, if you have computable instances they will be chosen instead.

[Patrick Massot]

It mostly works, but I see the quot namespace is not filtered out

[Patrick Massot]

For the record, I think I wrote the solution at some point, but was confused by the decidability related error message

[Patrick Massot]

It would also be nice to filter out all _proof_ and _eqn_

[Simon Hudon]

Let's say quot.liftis one of those that aren't filtered out. Try printing `curr_env.in_current_file quot.lift` just to double check.

[Mario Carneiro]

you can use name.is_internal to filter

[Mario Carneiro]

it checks that none of the name components have an initial underscore

[Patrick Massot]

Simon, could you try to fix quotes in your last message? I don't know where to put them

[Patrick Massot]

name.is_internal does allow to get rid of underscored stuff

[Mario Carneiro]

curr_env.in_current_file `quot.lift

[Mario Carneiro]

better yet curr_env.in_current_file ``quot.lift

[Patrick Massot]

Lean indeed answers tt

[Patrick Massot]

To make sure we are on the same page, the current version I have is:

open tactic

meta def print_names : tactic unit :=
do curr_env <- get_env,
   trace (to_string (curr_env.in_current_file ``quot.lift)),
   let decls := curr_env.fold [] list.cons, -- this loops over all the visible declarations and, using `list.cons`, accumulate them in a list
   let names := decls.map declaration.to_name, -- this takes the name of each declaration.
   let local_names := names.filter (λ x, environment.in_current_file curr_env x && not x.is_internal),
   local_names.mmap' trace

[Mario Carneiro]

you can see from the definition of in_current_file that it just checks that decl_olean returns none

[Mario Carneiro]

but quot.lift was never defined, it magically comes into being from the init_quotient one-time command

[Reid Barton]

If you also require that decl_pos is not none, that should get rid of quot stuff

[Mario Carneiro]

in a new file, I get this:

open tactic
#eval do env ← get_env,
  env.fold skip $ λ d t,
  let n := d.to_name in
  when (env.in_current_file n) (trace n) >> t

-- quot.mk
-- quot.ind
-- quot
-- quot.lift
-- _main

[Mario Carneiro]

I guess _main is the tactic I am #evaling, the rest come from init_quotient

[Simon Hudon]

@Mario Carneiro You may want to use mfold instead of fold for monadic functions

[Mario Carneiro]

there is no env.mfold

[Mario Carneiro]

If I use (env.decl_pos n).is_none instead, I get

interactive.loc.has_reflect
prod.has_reflect
quot.mk
quot.ind
bool.has_reflect
sum.has_reflect
quot
quot.lift
option.has_reflect
pos.has_reflect

[Simon Hudon]

Sorry, you're right, I was thinking of expressions

[Mario Carneiro]

I'm not sure why e.g. option.has_reflect has no position, but I can confirm that vscode F12 has no idea where it is

[Mario Carneiro]

attribute [derive has_reflect] bool prod sum option interactive.loc pos

I see

[Mario Carneiro]

@Sebastian Ullrich I am surprised to discover that there is no add_decl variant or option to set the position of a new declaration

[Sebastian Ullrich]

Yes, well, the Lean 3 meta API is just that incomplete

[Patrick Massot]

I know it's cheating, but can't we just filter out quot.* using a plain regex?

[Mario Carneiro]

You can, but it would be more accurate to say that it is only those four definitions specifically, not everything in quot

[Mario Carneiro]

also it wouldn't be a regex exactly

[Patrick Massot]

those four definitions specifically would be even better

[Mario Carneiro]

it is easy enough to filter out those four by name

[Mario Carneiro]

meta def environment.in_current_file'
  (env : environment) (n : name) : bool :=
env.in_current_file n && (n ∉ [``quot, ``quot.mk, ``quot.lift, ``quot.ind])

[Patrick Massot]

I missed that last message. Thanks!

[Patrick Massot]

I think this command is really useful

[Patrick Massot]

It's much easier than trying to keep track of which namespaces we are in

[Patrick Massot]

Do we have mathlib guidelines about nested namespaces?

[Patrick Massot]

That command would be even nicer if we had versions listing only definitions or only instances or only lemmas/theorems

[Patrick Massot]

But I need to sleep now

[Patrick Massot]

We could even have a tree view

[Mario Carneiro]

what kind of guidelines do you mean?

[Patrick Massot]

it could be pushing towards flat hierarchy or deep hierarchy

[Mario Carneiro]

I would say it's currently more flat than deep

[Patrick Massot]

My completion file currently has:

uniform_space.completion_is_complete
uniform_space.completion_extension
uniform_space.completion_is_separated
uniform_space.completion_extension.lifts
uniform_space.completion_lift.uniform_continuity
uniform_space.completion_is_uniform_space
uniform_space.to_completion
uniform_space.eq_of_separated_of_uniform_continuous
uniform_space.completion_lift
uniform_space.completion_lift.unique
uniform_space.completion_extension.uniform_continuity
uniform_space.to_completion.dense
uniform_space.completion_lift.comp
uniform_space.completion_lift.lifts
uniform_space.completion_extension.unique
uniform_space.separated_of_uniform_continuous
uniform_space.nonempty_completion_iff
uniform_space.completion
uniform_space.to_completion.uniform_continuous

[Mario Carneiro]

there are some instances of large scale namespaces like measure_theory, but most definitions are only one namespace deep

[Patrick Massot]

everything is inside the uniform_space namespace. But then the completion, completion_lift and completion_extension get their sub-namespace

[Patrick Massot]

but this sub-namespacing could be replaced by underscores

[Mario Carneiro]

I think that makes sense - completion is defined on uniform_space, and theorems about completion should go in a namespace for it

[Patrick Massot]

because there is no structure involved, so we can't use the projection trick

[Mario Carneiro]

Even so I think that uniform_space.completion is better than completion because of the need for disambiguation here

[Patrick Massot]

I could also put (almost) everything from that file in a uniform_space.completion namespace

[Mario Carneiro]

you could use completion.lift instead of completion_lift for example

[Mario Carneiro]

I would avoid repeating things from the namespace in the name though

[Mario Carneiro]

lattice.lattice reads redundantly

[Patrick Massot]

There are two related but distinct thing. completion_lift is a definition, lifting a function (not necessarily uniformly continuous!) to completion, and a lemma completion_lift.lifts saying that the lift indeed lifts the map, under uniform continuity assumption

[Mario Carneiro]

I might say lift_is_lift for something like that

[Patrick Massot]

Deciding and namespaces and names for these two things is exactly the kind of question I have

[Mario Carneiro]

although depending on what exactly "lift" means it might have a more specific name

[Mario Carneiro]

i.e. if it is something like lift o mk = id (I'm making things up) then I might call it lift_comp_mk, but if it is is_lift lift then I would say is_lift_lift or lift_is_lift

[Patrick Massot]

https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/completion.lean#L187

[Patrick Massot]

and its friend https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/completion.lean#L136

[Mario Carneiro]

I would write that the other way and say lift_to_completion

[Mario Carneiro]

(probably to_completion should be a coercion)

[Patrick Massot]

I wouldn't be able to state those lemmas without writing to_completion, even with a coercion, right?

[Mario Carneiro]

you can say coe

[Patrick Massot]

I fear it would obscure the statement. But I could still define the coercion for later use

[Mario Carneiro]

Also I don't know if using all these composes in the statement doesn't make your work harder

[Mario Carneiro]

I know that's how mathematicians like to write it but sometimes it is nicer to just put a point in

[Patrick Massot]

Do you mean you would state forall x, ...?

[Mario Carneiro]

yes

[Patrick Massot]

True, I really think about this from a categorical perspective, there are no points at all

[Patrick Massot]

Only morphisms

[Mario Carneiro]

Certainly completion_extension.lifts should be stated as completion_extension f \u x = f x

[Patrick Massot]

Points would really obscure statements

[Mario Carneiro]

maybe, but none of the work done in this file so far is really categorical in nature

[Patrick Massot]

ok, that one could be clearer with a forall x : a, completion_extension f x = f x

[Patrick Massot]

What? Everything building completion_lift from completion_extension is purely categorical

[Patrick Massot]

With proper mathlib help, there would be a single tactic to invoke to build completion_lift from completion_extension

[Mario Carneiro]

looks like just specializing theorems to me

[Mario Carneiro]

completion_lift should be called completion.map though

[Patrick Massot]

The composition proof has slightly more than specializing. completion_extension.unique is crucial

[Mario Carneiro]

but it is just specializing - completion_lift.unique just applies completion_extension.unique

[Patrick Massot]

I'm talking about the proof of completion_lift.comp, not completion_lift.unique

[Patrick Massot]

Anyway, I really need to sleep now. But I'll probably use all these suggestions tomorrow (although I should also be doing real work...)

[Patrick Massot]

Thanks!

[Patrick Massot]

Returning to this full names thread since Kevin also had a use case, are we interested to have this in mathlib? The version I currently have here is:

import data.list.sort
import data.string
import tactic.basic

open tactic

/-- `run_cmd print_names` print all names defined in the current file.
    This is useful when checking namespaces and writing doc -/
meta def print_names : tactic unit :=
do curr_env <- get_env,
   let decls := curr_env.fold [] list.cons,
   let names := decls.map declaration.to_name,
   let local_names := names.filter
     (λ x, environment.in_current_file' curr_env x && not x.is_internal),
   let sorted_names := list.merge_sort (≤) (local_names.map to_string),
   sorted_names.mmap' trace

With some argument parsing skill we could make sorting optional, and have an optional prefix filtering.

[Mario Carneiro]

I think it should return a list name rather than printing it if you want to make this more widely usable

[Mario Carneiro]

why isn't it sorted in declaration order?

[Patrick Massot]

yesterday my main goal was to check namespaces, and alphabetical order was therefore more useful

[Mario Carneiro]

it all seems a bit ad hoc

[Kevin Buzzard]

Alphabetical order has been around for a while

[Kevin Buzzard]

but I guess you could call it ad hoc

[Patrick Massot]

I'm not even sure it's in declaration order before sorting

[Kevin Buzzard]

It's not universe-independent

[Mario Carneiro]

I think it's the right length for a small program that slices data the way you want

[Kevin Buzzard]

or even country-independent

[Patrick Massot]

I don't understand what you mean by that length comment

[Mario Carneiro]

there isn't much mathlib can do to make that definition shorter without getting too specific

[Patrick Massot]

Ok, I'll keep it around here then

[Mario Carneiro]

If I add that exact tactic to mathlib, then of course your definition becomes very short (just a reference to my definition) but it also becomes less flexible - if you want to print them in a different order or get type information for each definition or something else you will have to start from scratch again (or copy paste the mathlib tactic)

[Patrick Massot]

I still have a question about that small function. I don't want to be rude, or break the etiquette of this fine place, by using words from imperative programming. But I don't really understand how the main l**p works. What does the first line do exactly?

[Mario Carneiro]

get_env?

[Patrick Massot]

What is get_env returning?

[Mario Carneiro]

a reference to the environment object

[Mario Carneiro]

which is the thing that stores all definitions

[Patrick Massot]

what's the point of not having directly the list that the second line creates?

[Patrick Massot]

hitting F12 only gives meta constant everywhere

[Mario Carneiro]

because the environment isn't stored as a list

[Patrick Massot]

I understand that, my question is: how is it more than a list of stuff?

[Mario Carneiro]

for one thing, it should have an index to speed up looking up definitions by name

[Patrick Massot]

Actually I understand nothing about this monad thing. What the difference between the first line and its arcane a <- b syntax and the friendlier looking lines with let a := b?

[Patrick Massot]

so it's closer to a python dictionary than list?

[Mario Carneiro]

Literally, a <- b is syntax for the bind operator, while let a := b is just let

[Mario Carneiro]

Most operations which have a sequential character or otherwise non-functional behavior have to work inside a monad, and bind puts them together with a notation that is deliberately similar to let a := b

[Mario Carneiro]

yes, it is basically a dictionary, probably a hash map. In particular, looping over all definitions (which is what you are doing) is one of the least efficient things you can do with it, so it is rather slow

[Patrick Massot]

I'm sorry but I still don't see any difference between: "I want to call curr_env the thing returned by get_env" and "I want to call decls the thing returned by curr_env.fold [] list.cons"

[Patrick Massot]

but clearly I cannot switch between <- and let

[Mario Carneiro]

probably get_env is a bad example since it's basically functional, so consider the following instead:

do a <- random,
   b <- random,
   c <- random,
   return [a, b, c]

Let's say that random returns a random number. Then this program will probably return three different numbers

[Mario Carneiro]

On the other hand, with

let a := random,
    b := random,
    c := random in
[a, b, c]

there is no implementation of random that will cause three different numbers to be produced

[Kevin Buzzard]

Patrick do you know all about this monad business?

[Kevin Buzzard]

All of this <- is sugar for monad.bind etc

[Patrick Massot]

I don't see why you would get the same number with let

[Kevin Buzzard]

The part of "programming in Lean" about the state monad gave me some idea about what was going on here. The <- can change the state of things.

[Patrick Massot]

Kevin, I tried to read that part of PIL several time, but it doesn't stick at all

[Kevin Buzzard]

but in functional programming you can't change state

[Kevin Buzzard]

as there is no state

[Kevin Buzzard]

<- can expand to "...and let x = x + 1 while you're doing this"

[Mario Carneiro]

notice that the second program is definitionally equal to [random, random, random] and (\lam x, [x, x, x]) random

[Patrick Massot]

Sure. But then what happens at execution? Isn't random called three times?

[Kevin Buzzard]

with the same inputs maybe

[Patrick Massot]

there is no input

[Kevin Buzzard]

right

[Kevin Buzzard]

so the same thing happens three time

[Kevin Buzzard]

but with <- there are hidden variables

[Kevin Buzzard]

it's not a contradiction that "intro x" can do different things at different points in the middle of a tactic proof

[Kevin Buzzard]

because the goal might be different

[Mario Carneiro]

A very small example:

def counter (α) := nat → nat × α
instance : monad counter :=
{ pure := λ α a n, (n, a),
  bind := λ α β f g n, let (n', a) := f n in g a n' }

def count : counter nat := λ n, (n+1, n)

def run {α} (c : counter α) : α := (c 0).2

#eval run $ do
  a ← count,
  b ← count,
  c ← count,
  return [a, b, c]

-- [0, 1, 2]

[Mario Carneiro]

If I #check instead, it says

run (count >>= λ (a : ℕ), count >>= λ (b : ℕ), count >>= λ (c : ℕ), return [a, b, c]) : list ℕ

[Patrick Massot]

I have no idea what's going on in your snippet

[Kevin Buzzard]

<- is running bind which can change the nat. The nat is a variable which is hidden in the notation but still exists. If you unravel you can see the nat. >>= also means bind

[Mario Carneiro]

Start with the first line

[Mario Carneiro]

counter A is a function from nat to nat x A

[Kevin Buzzard]

do puts you into monad mode, and the monad here is counter which is hiding a nat.

[Patrick Massot]

Zulip just told me your snippet was written yesterday. I probably mean it's too late to understand this

[Patrick Massot]

I should really sleep. Since my family left for vacations, I'm drifting towards night. Today (Zulip claims I mean yesterday) I reached the point where I got up too late to have lunch with my colleagues. So I'll try to drift back. But I promise I'll try to understand your code tomorrow, after reading back a bit of PIL. Thank you!

[Mario Carneiro]

By the way, that code is roughly analogous to the following C code:

int state = 0;
int a = state++;
int b = state++;
int c = state++;
return [a, b, c]; // <- okay, not really C style...

[Kevin Buzzard]

Returning to this full names thread since Kevin also had a use case, are we interested to have this in mathlib? The version I currently have here is:

import data.list.sort
import data.string
import tactic.basic

open tactic

/-- `run_cmd print_names` print all names defined in the current file.
    This is useful when checking namespaces and writing doc -/
meta def print_names : tactic unit :=
do curr_env <- get_env,
   let decls := curr_env.fold [] list.cons,
   let names := decls.map declaration.to_name,
   let local_names := names.filter
     (λ x, environment.in_current_file' curr_env x && not x.is_internal),
   let sorted_names := list.merge_sort (≤) (local_names.map to_string),
   sorted_names.mmap' trace

Ooh this was just really handy for me. Faced with

namespace is_ring_hom

instance {S : set R} [is_subring S] : is_ring_hom (@subtype.val R S) :=
{ map_add := λ _ _, rfl,
  map_mul := λ _ _, rfl,
  map_one := rfl }

end is_ring_hom

and after 2 minutes of failing to guess what Lean might have called this instance, I ran the code and got it immediately.

[Kevin Buzzard]

Answers on a postcard

[Reid Barton]

In this case I think #print instances is_ring_hom will tell you too.

[Kevin Buzzard]

Aah! I use #print prefix a fair bit but I don't think I'd internalised #print instances

[Patrick Massot]

So we have this print_names command. We can put it in a file, import that file in another file, run the command there, and get our answer in the Lean messages window. How could we get the same information from the command line without modifying the file we want to inspect?

[Simon Hudon]

In Haskell, ghc has the option -e which allows you to provide an expression to evaluate from the command line. Lean does not have that. What I would do is write a bash script to generate a .lean file that imports your print_names definition and the file you want to check, then call Lean on that file.

[Mario Carneiro]

lean has a --run option

[Simon Hudon]

I thought it only ran the main function

[Patrick Massot]

That's also what the documentation and experiment suggest

[Patrick Massot]

@Sebastian Ullrich do you confirm there is no way to do what I asked?

[Patrick Massot]

More generally, it would help with documentation if we knew more about Lean's introspection capabilities. For instance, suppose we get hold of some definition of lemma using get_env, is there any way we could get a list of types of objects appearing in the statement or, even better, a list of all lemmas and definitions used in the proof (before it gets erased by proof irrelevance)?

[Simon Hudon]

is there any way we could get a list of types of objects appearing in the statement or, even better, a list of all lemmas and definitions used in the proof (before it gets erased by proof irrelevance)?

I believe that is possible. Let me just work something out.

[Simon Hudon]

Here's what I got. This version lists all the constants (definition, theorem, axiom or constant, actually) used in the statement of the theorem. I have worked out a version I thought would do the same about the proof but I run into weird errors.

meta def list_constant (e : expr) : list name :=
e.fold [] $ λ e _ cs,
if e.is_constant ∧ ¬ e.const_name ∈ cs
  then e.const_name :: cs
  else cs

open declaration
meta def const_in_def (n : name) : tactic unit :=
do (thm _ _ t v) ← get_decl n,
   -- let v := v.get,
   -- trace v.is_constant,
   trace $ list_constant t,
   return ()

#eval const_in_def `list.reverse_append

[Patrick Massot]

Nice!

[Patrick Massot]

I think I will play of lot with that function

[Simon Hudon]

Cool! Please let me know if you manage to get v.get to work. What I think is that the proof tree might be stored nowhere so v.get can only fail. @Sebastian Ullrich and @Gabriel Ebner may shed some light on that.

[Gabriel Ebner]

What error are you getting? This works just fine for me:

import data.list

meta def list_constant (e : expr) : list name :=
e.fold [] $ λ e _ cs,
if e.is_constant ∧ ¬ e.const_name ∈ cs
  then e.const_name :: cs
  else cs

open declaration tactic
meta def const_in_def (n : name) : tactic unit :=
do (thm _ _ t v) ← get_decl n,
   let v := v.get,
   trace $ list_constant v,
   trace $ list_constant t,
   return ()

#eval const_in_def `list.reverse_append
/-
scratch20180811.lean:17:0: information trace output
[list.append_assoc,
 list.reverse_cons,
 list.cons_append,
 list.cons,
 trivial,
 eq_self_iff_true,
 propext,
 list.append_nil,
 list.reverse_nil,
 eq.refl,
 has_append,
 list.nil_append,
 congr_arg,
 congr,
 eq.trans,
 id,
 true,
 list.nil,
 eq.mpr,
 list.has_append,
 has_append.append,
 list.reverse,
 eq,
 list.rec,
 list]
[list.has_append, has_append.append, list.reverse, eq, list]

-/

[Simon Hudon]

excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)

[Simon Hudon]

I'm invoking it from within emacs. Does that matter?

[Patrick Massot]

Gabriel's code also works here (in VScode).

[Patrick Massot]

and in command line as well

[Gabriel Ebner]

No it doesn't matter which editor you use. Make sure you run leanpkg build before, this reduced the required amount of memory. Typically, when you see excessive memory usage errors, the only way forward is to restart the server.

[Simon Hudon]

The plot thickens: I just called #print list.reverse_append and got:

@[simp]
theorem list.reverse_append : ∀ {α : Type u} (s t : list α), list.reverse (s ++ t) = list.reverse t ++ list.reverse s :=
[incorrect proof]

So I'll delete all the .olean files and build from scratch.

[Simon Hudon]

It did solve the problem. Thanks @Gabriel Ebner !

[Simon Hudon]

@Patrick Massot, if you want to restrict the output of that program to lemmas you can use tactic.is_proof to filter those names. Other options can help you restrict it to types or functions.

[Patrick Massot]

you mean filter the output of list_constant?

[Simon Hudon]

Yes exactly.

[Patrick Massot]

Since we're at it, how would you list all file imported by the current file. That one I could implement in python with regex :-)

[Simon Hudon]

for instance, you can do it as cs.mfilter $ λ c, mk_const c >>= is_proof

[Simon Hudon]

(if cs is the result of list_constant)

[Patrick Massot]

What is the m doing in mfilter? Does it mean meta? Wouldn't it work with regular filter?

[Patrick Massot]

I would have simply written cs.filter is_proof

[Simon Hudon]

No the m is for monad becaus mk_const and is_proof use the tactic monad.

[Simon Hudon]

It works in trusted functions as well.

[Patrick Massot]

That's what I meant. To me monad = tactic monad = meta. I may try to refine that vision at some point

[Simon Hudon]

Since we're at it, how would you list all file imported by the current file. That one I could implement in python with regex :-)

I'm stumped. I think there is very little information available about the file / module structure.

[Patrick Massot]

That's great. The only thing which is easy to do with regex is hard in Lean!

[Simon Hudon]

Ah! I see. a monad is a category theoretic concept of which tactic is only one instance. It's a good way of structuring programs when you want to prove things about them.

[Patrick Massot]

I'm half joking, I know there are other monads

[Simon Hudon]

Haha! Using the parser framework, you may decide to read the current file and do some of your regex work that way. And it all stays in Lean. I wouldn't call it a proper way but it would get the job done.

[Simon Hudon]

I'm half joking, I know there are other monads

The pedantic explanation that people throw around might actually clarify things for you :P "it's simple! A monad is just a monoid in the category of endofunctors"

... speaking of only half understanding ... :P

[Patrick Massot]

What is mk_const doing in your filtering stuff?

[Patrick Massot]

Actually I can't used the filtered list, I get failed to synthesize type class instance for has_to_tactic_format (tactic (list name))

[Simon Hudon]

I assume you tried trace (mfilter ... ). The mfilter expression is a monadic command so you have to execute it before using its result:

r <- mfilter /- rest -/,
trace r

[Patrick Massot]

indeed this works better

[Simon Hudon]

The comma here is as if you were using >>=, that is the sequential composition of two commands: the mfilter expression and the trace expression:

mfilter /- stuff -/ >>= λ r, trace r

or

mfilter /- stuff -/ >>= trace

after η-reduction.

[Patrick Massot]

Thank you very much. I think I'll learn of lot from this. But right now I'm required for shooting stars hunting.

[Simon Hudon]

Good luck!

[Scott Morrison]

The pedantic explanation that people throw around might actually clarify things for you :P "it's simple! A monad is just a monoid in the category of endofunctors"

But you also have to remember that if a computer scientist says that to you, they probably really mean "... in the category of endofuctors of the category of types"!

[Scott Morrison]

(similarly if they just say functor they mean endofunctor of the category of types: we even have this in mathlib)

[Simon Hudon]

I stand corrected ... or my knowledge stands improved

[Simon Hudon]

I should really start taking advantage of the fact that so many category theorists hang around here. I've been thinking of doing a categorical treatment of liveness properties in temporal logic but it doesn't bode well: I already mess up the terminology!

[Scott Morrison]

Given that more computer scientists use "monad" now than mathematicians, my vote would be to give it to them (i.e. add "in the category of types" to the fancy-pants definition), and go back to using "triple", or "triad" from the earlier category theory literature for the general case)

[Simon Hudon]

What a shame! I thought we might make friends with mathematicians with those category theoretic ideas! Now you're giving us "we knew about monad before it was cool"

[Scott Morrison]

:-) I certainly learnt what a monad was from its CS usage before the category-theoretic obscurity.

[Scott Morrison]

btw @Simon Hudon, would you object if I added @[extensionality] to propext?

[Simon Hudon]

I find its CS usage has a pretty funny story. They didn't know how to do IO in a pure way in Haskell so they held they breath until someone unearthed an obscure category theory paper, found someone to explain it to computer scientists and help them translate those pies in the sky into physical world phenomena

[Simon Hudon]

No objections. Do you see any downside to doing it?

[Scott Morrison]

My whole research field (tensor categories, topological field theory) is the same: just a toy for mathematicians who couldn't cope with quantum field theory, until some physicists came along and said "we've discovered this stuff we call 'topological matter'"

[Patrick Massot]

Good luck!

We have been very lucky, including one amazing one. Now I'll go sleeping

[Simon Hudon]

I find it so mind blowing when that happens. My favorite example is Euler's number theory work being useful in cryptography after he had his fun with it.

[Patrick Massot]

(deleted)

[Chris Hughes]

I had a go at making Simon's code return all the definitions used transitively. Why doesn't this work? I think it has something to do with list.mmap

import data.nat.basic data.list.basic

meta def list_constant (e : expr) : list name :=
e.fold [] $ λ e _ cs,
if e.is_constant ∧ ¬ e.const_name ∈ cs
  then e.const_name :: cs
  else cs

open declaration tactic
meta def const_in_def : Π (n : name), tactic (list name)
| n := do (thm _ _ t v) ← get_decl n,
let v := v.get,
let l := list_constant v,
m ← l.mmap const_in_def,
return (m.bind id).erase_dup

meta def const_in_def' (n : name) : tactic unit :=
do l ← const_in_def n,
  trace l,
  return ()

#eval const_in_def' `nat.mod_add_div

[Reid Barton]

I see "match failed", is that what you mean by doesn't work?

[Reid Barton]

I assume it's the match (thm _ _ t v) ← get_decl n, there are going to be constants reachable from anything as well as theorems.

[Reid Barton]

If you add trace n, at the start of that line you can see that it's processing trivial, which is a defn, not a thm

[Chris Hughes]

Thanks. got it working now.

[Patrick Massot]

You can have a look at https://github.com/leanprover-community/leancrawler/blob/master/src/leancrawler/deps.lean for more stuff you can extract from Lean (and of course you can also use the python part)