Zulip Chat Archive

Stream: general

Topic: full names


Patrick Massot (Jul 17 2018 at 20:02):

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 (Jul 17 2018 at 20:14):

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 (Jul 17 2018 at 20:15):

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

Patrick Massot (Jul 17 2018 at 20:15):

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

Simon Hudon (Jul 17 2018 at 20:17):

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 (Jul 17 2018 at 20:17):

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

Simon Hudon (Jul 17 2018 at 20:21):

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 (Jul 17 2018 at 20:21):

Does it make sense so far?

Patrick Massot (Jul 17 2018 at 20:22):

It makes sense to me but not to Lean

Patrick Massot (Jul 17 2018 at 20:22):

"type of sorry macro is not a sort"

Patrick Massot (Jul 17 2018 at 20:22):

probably missing import or open

Simon Hudon (Jul 17 2018 at 20:24):

that makes sense. Try open tactic.

Kevin Buzzard (Jul 17 2018 at 20:24):


Kevin Buzzard (Jul 17 2018 at 20:24):

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

Patrick Massot (Jul 17 2018 at 20:24):

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

Patrick Massot (Jul 17 2018 at 20:25):

:simple_smile:

Patrick Massot (Jul 17 2018 at 20:25):

Maybe we have infinitely nested namespaces

Simon Hudon (Jul 17 2018 at 20:25):

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

Patrick Massot (Jul 17 2018 at 20:25):

22573

Patrick Massot (Jul 17 2018 at 20:25):

:laughing:

Patrick Massot (Jul 17 2018 at 20:26):

Maybe we should jump to the filtered version

Simon Hudon (Jul 17 2018 at 20:26):

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 (Jul 17 2018 at 20:26):

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

Simon Hudon (Jul 17 2018 at 20:27):

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

Patrick Massot (Jul 17 2018 at 20:28):

Yes: using environment.in_current_file

Patrick Massot (Jul 17 2018 at 20:28):

I'm such a good student :open_mouth:

Simon Hudon (Jul 17 2018 at 20:29):

You get an A! Good job!

Simon Hudon (Jul 17 2018 at 20:30):

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 (Jul 17 2018 at 20:36):

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

Patrick Massot (Jul 17 2018 at 20:36):

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 (Jul 17 2018 at 20:37):

I'm probably beaten for my preamble

Patrick Massot (Jul 17 2018 at 20:38):

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

Patrick Massot (Jul 17 2018 at 20:39):

(deleted)

Patrick Massot (Jul 17 2018 at 20:39):

(deleted)

Patrick Massot (Jul 17 2018 at 20:44):

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 (Jul 17 2018 at 20:56):

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

Patrick Massot (Jul 17 2018 at 20:58):

This works if there is mathematics preamble

Simon Hudon (Jul 17 2018 at 20:59):

Which preamble?

Patrick Massot (Jul 17 2018 at 20:59):

local attribute [instance] classical.prop_decidable

Mario Carneiro (Jul 17 2018 at 21:00):

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

Simon Hudon (Jul 17 2018 at 21:00):

You shouldn't need that. Booleans are decidable propositions

Patrick Massot (Jul 17 2018 at 21:00):

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

Simon Hudon (Jul 17 2018 at 21:01):

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 (Jul 17 2018 at 21:04):

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

Patrick Massot (Jul 17 2018 at 21:05):

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

Patrick Massot (Jul 17 2018 at 21:09):

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

Simon Hudon (Jul 17 2018 at 21:10):

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 (Jul 17 2018 at 21:10):

you can use name.is_internal to filter

Mario Carneiro (Jul 17 2018 at 21:11):

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

Patrick Massot (Jul 17 2018 at 21:15):

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

Patrick Massot (Jul 17 2018 at 21:16):

name.is_internal does allow to get rid of underscored stuff

Mario Carneiro (Jul 17 2018 at 21:17):

curr_env.in_current_file `quot.lift

Mario Carneiro (Jul 17 2018 at 21:18):

better yet curr_env.in_current_file ``quot.lift

Patrick Massot (Jul 17 2018 at 21:20):

Lean indeed answers tt

Patrick Massot (Jul 17 2018 at 21:21):

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 (Jul 17 2018 at 21:25):

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

Mario Carneiro (Jul 17 2018 at 21:26):

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

Reid Barton (Jul 17 2018 at 21:31):

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

Mario Carneiro (Jul 17 2018 at 21:32):

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 (Jul 17 2018 at 21:33):

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

Simon Hudon (Jul 17 2018 at 21:34):

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

Mario Carneiro (Jul 17 2018 at 21:34):

there is no env.mfold

Mario Carneiro (Jul 17 2018 at 21:36):

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 (Jul 17 2018 at 21:36):

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

Mario Carneiro (Jul 17 2018 at 21:37):

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 (Jul 17 2018 at 21:38):

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

I see

Mario Carneiro (Jul 17 2018 at 21:41):

@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 (Jul 17 2018 at 21:44):

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

Patrick Massot (Jul 17 2018 at 21:46):

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

Mario Carneiro (Jul 17 2018 at 21:47):

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

Mario Carneiro (Jul 17 2018 at 21:47):

also it wouldn't be a regex exactly

Patrick Massot (Jul 17 2018 at 21:48):

those four definitions specifically would be even better

Mario Carneiro (Jul 17 2018 at 21:48):

it is easy enough to filter out those four by name

Mario Carneiro (Jul 17 2018 at 21:51):

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 (Jul 17 2018 at 23:03):

I missed that last message. Thanks!

Patrick Massot (Jul 17 2018 at 23:04):

I think this command is really useful

Patrick Massot (Jul 17 2018 at 23:06):

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

Patrick Massot (Jul 17 2018 at 23:06):

Do we have mathlib guidelines about nested namespaces?

Patrick Massot (Jul 17 2018 at 23:07):

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

Patrick Massot (Jul 17 2018 at 23:08):

But I need to sleep now

Patrick Massot (Jul 17 2018 at 23:09):

We could even have a tree view

Mario Carneiro (Jul 17 2018 at 23:09):

what kind of guidelines do you mean?

Patrick Massot (Jul 17 2018 at 23:10):

it could be pushing towards flat hierarchy or deep hierarchy

Mario Carneiro (Jul 17 2018 at 23:10):

I would say it's currently more flat than deep

Patrick Massot (Jul 17 2018 at 23:11):

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 (Jul 17 2018 at 23:11):

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

Patrick Massot (Jul 17 2018 at 23:11):

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

Patrick Massot (Jul 17 2018 at 23:12):

but this sub-namespacing could be replaced by underscores

Mario Carneiro (Jul 17 2018 at 23:12):

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

Patrick Massot (Jul 17 2018 at 23:13):

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

Mario Carneiro (Jul 17 2018 at 23:13):

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

Patrick Massot (Jul 17 2018 at 23:13):

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

Mario Carneiro (Jul 17 2018 at 23:14):

you could use completion.lift instead of completion_lift for example

Mario Carneiro (Jul 17 2018 at 23:15):

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

Mario Carneiro (Jul 17 2018 at 23:15):

lattice.lattice reads redundantly

Patrick Massot (Jul 17 2018 at 23:16):

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 (Jul 17 2018 at 23:16):

I might say lift_is_lift for something like that

Patrick Massot (Jul 17 2018 at 23:16):

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

Mario Carneiro (Jul 17 2018 at 23:17):

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

Mario Carneiro (Jul 17 2018 at 23:18):

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 (Jul 17 2018 at 23:19):

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

Patrick Massot (Jul 17 2018 at 23:20):

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

Mario Carneiro (Jul 17 2018 at 23:20):

I would write that the other way and say lift_to_completion

Mario Carneiro (Jul 17 2018 at 23:20):

(probably to_completion should be a coercion)

Patrick Massot (Jul 17 2018 at 23:22):

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

Mario Carneiro (Jul 17 2018 at 23:23):

you can say coe

Patrick Massot (Jul 17 2018 at 23:23):

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

Mario Carneiro (Jul 17 2018 at 23:24):

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

Mario Carneiro (Jul 17 2018 at 23:25):

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

Patrick Massot (Jul 17 2018 at 23:25):

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

Mario Carneiro (Jul 17 2018 at 23:25):

yes

Patrick Massot (Jul 17 2018 at 23:25):

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

Patrick Massot (Jul 17 2018 at 23:25):

Only morphisms

Mario Carneiro (Jul 17 2018 at 23:26):

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

Patrick Massot (Jul 17 2018 at 23:26):

Points would really obscure statements

Mario Carneiro (Jul 17 2018 at 23:27):

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

Patrick Massot (Jul 17 2018 at 23:27):

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

Patrick Massot (Jul 17 2018 at 23:28):

What? Everything building completion_lift from completion_extension is purely categorical

Patrick Massot (Jul 17 2018 at 23:29):

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

Mario Carneiro (Jul 17 2018 at 23:29):

looks like just specializing theorems to me

Mario Carneiro (Jul 17 2018 at 23:30):

completion_lift should be called completion.map though

Patrick Massot (Jul 17 2018 at 23:31):

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

Mario Carneiro (Jul 17 2018 at 23:32):

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

Patrick Massot (Jul 17 2018 at 23:32):

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

Patrick Massot (Jul 17 2018 at 23:33):

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 (Jul 17 2018 at 23:34):

Thanks!

Patrick Massot (Jul 19 2018 at 21:19):

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 (Jul 19 2018 at 21:23):

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

Mario Carneiro (Jul 19 2018 at 21:23):

why isn't it sorted in declaration order?

Patrick Massot (Jul 19 2018 at 21:24):

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

Mario Carneiro (Jul 19 2018 at 21:24):

it all seems a bit ad hoc

Kevin Buzzard (Jul 19 2018 at 21:24):

Alphabetical order has been around for a while

Kevin Buzzard (Jul 19 2018 at 21:24):

but I guess you could call it ad hoc

Patrick Massot (Jul 19 2018 at 21:24):

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

Kevin Buzzard (Jul 19 2018 at 21:25):

It's not universe-independent

Mario Carneiro (Jul 19 2018 at 21:25):

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

Kevin Buzzard (Jul 19 2018 at 21:25):

or even country-independent

Patrick Massot (Jul 19 2018 at 21:25):

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

Mario Carneiro (Jul 19 2018 at 21:26):

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

Patrick Massot (Jul 19 2018 at 21:27):

Ok, I'll keep it around here then

Mario Carneiro (Jul 19 2018 at 21:28):

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 (Jul 19 2018 at 21:29):

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 (Jul 19 2018 at 21:29):

get_env?

Patrick Massot (Jul 19 2018 at 21:29):

What is get_env returning?

Mario Carneiro (Jul 19 2018 at 21:29):

a reference to the environment object

Mario Carneiro (Jul 19 2018 at 21:30):

which is the thing that stores all definitions

Patrick Massot (Jul 19 2018 at 21:32):

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

Patrick Massot (Jul 19 2018 at 21:33):

hitting F12 only gives meta constant everywhere

Mario Carneiro (Jul 19 2018 at 21:34):

because the environment isn't stored as a list

Patrick Massot (Jul 19 2018 at 21:34):

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

Mario Carneiro (Jul 19 2018 at 21:35):

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

Patrick Massot (Jul 19 2018 at 21:36):

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 (Jul 19 2018 at 21:36):

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

Mario Carneiro (Jul 19 2018 at 21:40):

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

Mario Carneiro (Jul 19 2018 at 21:41):

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 (Jul 19 2018 at 21:43):

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 (Jul 19 2018 at 21:44):

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 (Jul 19 2018 at 21:44):

but clearly I cannot switch between <- and let

Mario Carneiro (Jul 19 2018 at 21:46):

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 (Jul 19 2018 at 21:47):

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 (Jul 19 2018 at 21:48):

Patrick do you know all about this monad business?

Kevin Buzzard (Jul 19 2018 at 21:49):

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

Patrick Massot (Jul 19 2018 at 21:50):

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

Kevin Buzzard (Jul 19 2018 at 21:50):

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 (Jul 19 2018 at 21:50):

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

Kevin Buzzard (Jul 19 2018 at 21:50):

but in functional programming you can't change state

Kevin Buzzard (Jul 19 2018 at 21:50):

as there is no state

Kevin Buzzard (Jul 19 2018 at 21:51):

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

Mario Carneiro (Jul 19 2018 at 21:51):

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

Patrick Massot (Jul 19 2018 at 21:53):

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

Kevin Buzzard (Jul 19 2018 at 21:53):

with the same inputs maybe

Patrick Massot (Jul 19 2018 at 21:54):

there is no input

Kevin Buzzard (Jul 19 2018 at 21:54):

right

Kevin Buzzard (Jul 19 2018 at 21:54):

so the same thing happens three time

Kevin Buzzard (Jul 19 2018 at 21:55):

but with <- there are hidden variables

Kevin Buzzard (Jul 19 2018 at 21:55):

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

Kevin Buzzard (Jul 19 2018 at 21:56):

because the goal might be different

Mario Carneiro (Jul 19 2018 at 21:57):

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 (Jul 19 2018 at 21:59):

If I #check instead, it says

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

Patrick Massot (Jul 19 2018 at 22:00):

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

Kevin Buzzard (Jul 19 2018 at 22:00):

<- 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 (Jul 19 2018 at 22:00):

Start with the first line

Mario Carneiro (Jul 19 2018 at 22:01):

counter A is a function from nat to nat x A

Kevin Buzzard (Jul 19 2018 at 22:01):

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

Patrick Massot (Jul 19 2018 at 22:01):

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

Patrick Massot (Jul 19 2018 at 22:04):

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 (Jul 19 2018 at 22:08):

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 (Jul 25 2018 at 21:34):

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 (Jul 25 2018 at 21:35):

Answers on a postcard

Reid Barton (Jul 25 2018 at 23:21):

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

Kevin Buzzard (Jul 26 2018 at 07:41):

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

Patrick Massot (Aug 11 2018 at 10:01):

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 (Aug 11 2018 at 15:17):

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 (Aug 11 2018 at 15:59):

lean has a --run option

Simon Hudon (Aug 11 2018 at 16:28):

I thought it only ran the main function

Patrick Massot (Aug 11 2018 at 19:16):

That's also what the documentation and experiment suggest

Patrick Massot (Aug 11 2018 at 19:18):

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

Patrick Massot (Aug 11 2018 at 19:21):

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 (Aug 11 2018 at 19:30):

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 (Aug 11 2018 at 19:46):

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 (Aug 11 2018 at 19:49):

Nice!

Patrick Massot (Aug 11 2018 at 19:50):

I think I will play of lot with that function

Simon Hudon (Aug 11 2018 at 19:53):

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 (Aug 11 2018 at 20:02):

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 (Aug 11 2018 at 20:11):

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

Simon Hudon (Aug 11 2018 at 20:11):

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

Patrick Massot (Aug 11 2018 at 20:12):

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

Patrick Massot (Aug 11 2018 at 20:13):

and in command line as well

Gabriel Ebner (Aug 11 2018 at 20:14):

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 (Aug 11 2018 at 20:16):

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 (Aug 11 2018 at 20:24):

It did solve the problem. Thanks @Gabriel Ebner !

Simon Hudon (Aug 11 2018 at 20:26):

@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 (Aug 11 2018 at 20:28):

you mean filter the output of list_constant?

Simon Hudon (Aug 11 2018 at 20:30):

Yes exactly.

Patrick Massot (Aug 11 2018 at 20:31):

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 (Aug 11 2018 at 20:31):

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

Simon Hudon (Aug 11 2018 at 20:31):

(if cs is the result of list_constant)

Patrick Massot (Aug 11 2018 at 20:32):

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

Patrick Massot (Aug 11 2018 at 20:34):

I would have simply written cs.filter is_proof

Simon Hudon (Aug 11 2018 at 20:36):

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

Simon Hudon (Aug 11 2018 at 20:37):

It works in trusted functions as well.

Patrick Massot (Aug 11 2018 at 20:38):

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

Simon Hudon (Aug 11 2018 at 20:38):

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 (Aug 11 2018 at 20:39):

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

Simon Hudon (Aug 11 2018 at 20:39):

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 (Aug 11 2018 at 20:40):

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

Simon Hudon (Aug 11 2018 at 20:40):

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 (Aug 11 2018 at 20:42):

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 (Aug 11 2018 at 20:43):

What is mk_const doing in your filtering stuff?

Patrick Massot (Aug 11 2018 at 20:44):

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 (Aug 11 2018 at 20:48):

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 (Aug 11 2018 at 20:49):

indeed this works better

Simon Hudon (Aug 11 2018 at 20:50):

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 (Aug 11 2018 at 21:03):

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 (Aug 11 2018 at 21:14):

Good luck!

Scott Morrison (Aug 11 2018 at 21:33):

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 (Aug 11 2018 at 21:34):

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

Simon Hudon (Aug 11 2018 at 21:44):

I stand corrected ... or my knowledge stands improved

Simon Hudon (Aug 11 2018 at 21:45):

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 (Aug 11 2018 at 21:48):

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 (Aug 11 2018 at 21:51):

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 (Aug 11 2018 at 22:05):

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

Scott Morrison (Aug 11 2018 at 22:07):

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

Simon Hudon (Aug 11 2018 at 22:09):

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 (Aug 11 2018 at 22:09):

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

Scott Morrison (Aug 11 2018 at 22:11):

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 (Aug 11 2018 at 22:16):

Good luck!

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

Simon Hudon (Aug 11 2018 at 22:19):

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 (Aug 12 2018 at 20:33):

(deleted)

Chris Hughes (Sep 09 2018 at 10:42):

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 (Sep 09 2018 at 10:48):

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

Reid Barton (Sep 09 2018 at 10:49):

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 (Sep 09 2018 at 10:51):

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 (Sep 09 2018 at 12:08):

Thanks. got it working now.

Patrick Massot (Sep 09 2018 at 18:30):

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)


Last updated: Dec 20 2023 at 11:08 UTC