Zulip Chat Archive

Stream: general

Topic: full names


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jul 17 2018 at 20:15):

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

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:15):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jul 17 2018 at 20:21):

Does it make sense so far?

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:22):

It makes sense to me but not to Lean

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:22):

"type of sorry macro is not a sort"

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:22):

probably missing import or open

view this post on Zulip Simon Hudon (Jul 17 2018 at 20:24):

that makes sense. Try open tactic.

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 20:24):


view this post on Zulip Kevin Buzzard (Jul 17 2018 at 20:24):

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

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:24):

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

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:25):

:simple_smile:

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:25):

Maybe we have infinitely nested namespaces

view this post on Zulip Simon Hudon (Jul 17 2018 at 20:25):

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

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:25):

22573

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:25):

:laughing:

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:26):

Maybe we should jump to the filtered version

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jul 17 2018 at 20:26):

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

view this post on Zulip Simon Hudon (Jul 17 2018 at 20:27):

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

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:28):

Yes: using environment.in_current_file

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:28):

I'm such a good student :open_mouth:

view this post on Zulip Simon Hudon (Jul 17 2018 at 20:29):

You get an A! Good job!

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:37):

I'm probably beaten for my preamble

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:38):

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

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:39):

(deleted)

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:39):

(deleted)

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jul 17 2018 at 20:56):

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

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:58):

This works if there is mathematics preamble

view this post on Zulip Simon Hudon (Jul 17 2018 at 20:59):

Which preamble?

view this post on Zulip Patrick Massot (Jul 17 2018 at 20:59):

local attribute [instance] classical.prop_decidable

view this post on Zulip Mario Carneiro (Jul 17 2018 at 21:00):

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

view this post on Zulip Simon Hudon (Jul 17 2018 at 21:00):

You shouldn't need that. Booleans are decidable propositions

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 17 2018 at 21:04):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 17 2018 at 21:09):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 17 2018 at 21:10):

you can use name.is_internal to filter

view this post on Zulip Mario Carneiro (Jul 17 2018 at 21:11):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 17 2018 at 21:16):

name.is_internal does allow to get rid of underscored stuff

view this post on Zulip Mario Carneiro (Jul 17 2018 at 21:17):

curr_env.in_current_file `quot.lift

view this post on Zulip Mario Carneiro (Jul 17 2018 at 21:18):

better yet curr_env.in_current_file ``quot.lift

view this post on Zulip Patrick Massot (Jul 17 2018 at 21:20):

Lean indeed answers tt

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 17 2018 at 21:33):

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

view this post on Zulip Simon Hudon (Jul 17 2018 at 21:34):

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

view this post on Zulip Mario Carneiro (Jul 17 2018 at 21:34):

there is no env.mfold

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jul 17 2018 at 21:36):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 17 2018 at 21:38):

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

I see

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Jul 17 2018 at 21:44):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 17 2018 at 21:47):

also it wouldn't be a regex exactly

view this post on Zulip Patrick Massot (Jul 17 2018 at 21:48):

those four definitions specifically would be even better

view this post on Zulip Mario Carneiro (Jul 17 2018 at 21:48):

it is easy enough to filter out those four by name

view this post on Zulip 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])

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:03):

I missed that last message. Thanks!

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:04):

I think this command is really useful

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:06):

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

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:06):

Do we have mathlib guidelines about nested namespaces?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:08):

But I need to sleep now

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:09):

We could even have a tree view

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:09):

what kind of guidelines do you mean?

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:10):

it could be pushing towards flat hierarchy or deep hierarchy

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:10):

I would say it's currently more flat than deep

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:12):

but this sub-namespacing could be replaced by underscores

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:13):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:13):

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

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:14):

you could use completion.lift instead of completion_lift for example

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:15):

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

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:15):

lattice.lattice reads redundantly

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:16):

I might say lift_is_lift for something like that

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:17):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:19):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:20):

I would write that the other way and say lift_to_completion

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:20):

(probably to_completion should be a coercion)

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:23):

you can say coe

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:25):

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

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:25):

yes

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:25):

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

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:25):

Only morphisms

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:26):

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

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:26):

Points would really obscure statements

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:28):

What? Everything building completion_lift from completion_extension is purely categorical

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:29):

looks like just specializing theorems to me

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:30):

completion_lift should be called completion.map though

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:31):

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

view this post on Zulip Mario Carneiro (Jul 17 2018 at 23:32):

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

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:32):

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

view this post on Zulip 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...)

view this post on Zulip Patrick Massot (Jul 17 2018 at 23:34):

Thanks!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:23):

why isn't it sorted in declaration order?

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:24):

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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:24):

it all seems a bit ad hoc

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:24):

Alphabetical order has been around for a while

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:24):

but I guess you could call it ad hoc

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:24):

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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:25):

It's not universe-independent

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:25):

or even country-independent

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:25):

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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:26):

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

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:27):

Ok, I'll keep it around here then

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:29):

get_env?

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:29):

What is get_env returning?

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:29):

a reference to the environment object

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:30):

which is the thing that stores all definitions

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:32):

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

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:33):

hitting F12 only gives meta constant everywhere

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:34):

because the environment isn't stored as a list

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:34):

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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:35):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:36):

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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 21:40):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:44):

but clearly I cannot switch between <- and let

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:48):

Patrick do you know all about this monad business?

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:49):

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

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:50):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:50):

but in functional programming you can't change state

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:50):

as there is no state

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:51):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:53):

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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:53):

with the same inputs maybe

view this post on Zulip Patrick Massot (Jul 19 2018 at 21:54):

there is no input

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:54):

right

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:54):

so the same thing happens three time

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:55):

but with <- there are hidden variables

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 21:56):

because the goal might be different

view this post on Zulip 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]

view this post on Zulip 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 ℕ

view this post on Zulip Patrick Massot (Jul 19 2018 at 22:00):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 22:00):

Start with the first line

view this post on Zulip Mario Carneiro (Jul 19 2018 at 22:01):

counter A is a function from nat to nat x A

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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...

view this post on Zulip 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.


view this post on Zulip Kevin Buzzard (Jul 25 2018 at 21:35):

Answers on a postcard

view this post on Zulip Reid Barton (Jul 25 2018 at 23:21):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 11 2018 at 15:59):

lean has a --run option

view this post on Zulip Simon Hudon (Aug 11 2018 at 16:28):

I thought it only ran the main function

view this post on Zulip Patrick Massot (Aug 11 2018 at 19:16):

That's also what the documentation and experiment suggest

view this post on Zulip Patrick Massot (Aug 11 2018 at 19:18):

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

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 11 2018 at 19:49):

Nice!

view this post on Zulip Patrick Massot (Aug 11 2018 at 19:50):

I think I will play of lot with that function

view this post on Zulip 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.

view this post on Zulip 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]

-/

view this post on Zulip Simon Hudon (Aug 11 2018 at 20:11):

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

view this post on Zulip Simon Hudon (Aug 11 2018 at 20:11):

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

view this post on Zulip Patrick Massot (Aug 11 2018 at 20:12):

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

view this post on Zulip Patrick Massot (Aug 11 2018 at 20:13):

and in command line as well

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Aug 11 2018 at 20:24):

It did solve the problem. Thanks @Gabriel Ebner !

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 11 2018 at 20:28):

you mean filter the output of list_constant?

view this post on Zulip Simon Hudon (Aug 11 2018 at 20:30):

Yes exactly.

view this post on Zulip 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 :-)

view this post on Zulip Simon Hudon (Aug 11 2018 at 20:31):

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

view this post on Zulip Simon Hudon (Aug 11 2018 at 20:31):

(if cs is the result of list_constant)

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Aug 11 2018 at 20:34):

I would have simply written cs.filter is_proof

view this post on Zulip Simon Hudon (Aug 11 2018 at 20:36):

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

view this post on Zulip Simon Hudon (Aug 11 2018 at 20:37):

It works in trusted functions as well.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 11 2018 at 20:40):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 11 2018 at 20:43):

What is mk_const doing in your filtering stuff?

view this post on Zulip 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))

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 11 2018 at 20:49):

indeed this works better

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Aug 11 2018 at 21:14):

Good luck!

view this post on Zulip 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"!

view this post on Zulip 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)

view this post on Zulip Simon Hudon (Aug 11 2018 at 21:44):

I stand corrected ... or my knowledge stands improved

view this post on Zulip 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!

view this post on Zulip 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)

view this post on Zulip 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"

view this post on Zulip Scott Morrison (Aug 11 2018 at 22:05):

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

view this post on Zulip Scott Morrison (Aug 11 2018 at 22:07):

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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Aug 11 2018 at 22:09):

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

view this post on Zulip 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'"

view this post on Zulip Patrick Massot (Aug 11 2018 at 22:16):

Good luck!

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 12 2018 at 20:33):

(deleted)

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 09 2018 at 10:48):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Chris Hughes (Sep 09 2018 at 12:08):

Thanks. got it working now.

view this post on Zulip 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: May 13 2021 at 22:15 UTC