Zulip Chat Archive

Stream: general

Topic: Print mk_fresh_name result?


view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:00):

open tactic

example (a : Prop) : a  a :=
by do
    n  mk_fresh_name,
    intro n,
    hyp  get_local n,
    exact hyp

I've tried placing the cursor at various points and that never gives the name stored in n, so how can I print that local variable n?

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:06):

I'm not sure either how to make a "function that returns a string". I've tried 10 different thoughts on it :/

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:09):

Found this:

import system.io
variable [io.interface]
open nat io
def print_squares : N  io unit
| 0 := return ()
| (succ n) := print_squares n >>
put_str (nat.to_string n ++ "^2 = " ++
nat.to_string (n * n) ++ "\n")
#eval print_squares 100

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:15):

What's literal for the void or empty type?

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:15):

I need
def my_print : empty -> string := ...

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:21):

pasted image
Almost got it, but not quite.

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:28):

If by void you mean that thing in C, it's called unit and its element is ()

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:28):

void is a terrible name, because it's not empty

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:29):

If you want a function that takes no arguments, that's just a value

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:30):

@Mario Carneiro how do I convert a tactic name type to a string?

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:30):

def my_print : unit -> string := ... is basically equivalent to def my_print : string := ... and it can only return a constant string because lean is pure functional

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:31):

to_string : name -> string should work

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:31):

import system.io
open io
open tactic

def print_name3 :=
    put_str mk_fresh_name

#eval print_name3

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:31):

Doesn't work, because mk_fresh_name isn't a string

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:32):

pasted image

Here's trying to_string. Errors...

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:33):

import system.io
open io
open tactic

meta def print_name3 : io unit :=
do n  run_tactic mk_fresh_name,
   put_str n.to_string

#eval print_name3

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:33):

@Mario Carneiro You're a super-coder. Thank you!

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:34):

I take it you aren't familiar with monads; it's a good thing to read up on if you want to do imperative coding in lean

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:34):

Yeah, I'm not that far yet in my cat theory studies. Not a good place to be, but I'm getting there...

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:34):

I'll read up on monads & programming this week

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:35):

don't worry about the category theory monads, programming monads are easier and more useful

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:35):

@Mario Carneiro thank you!

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:35):

and there are a bazillion tutorials online for them because haskell loves them and lean inherited the love

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:37):

@Mario Carneiro it returns _fresh.657.185. I was expecting a nice variable like C that is available in the current scope

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:37):

it's globally unique, what did you expect?

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:38):

it needs a lot of numbers because lean goes through names ravenously

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:38):

I only need it unique for the current "context of the current file". I.e. in the usual sense of declaring new variables in Lean

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:38):

"available in the current scope" doesn't exist

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:38):

Like, this:

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:38):

there isn't really a global scope

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:39):

every definition has its own local scope

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:39):

variable n : nat, is the only thing in a file. Then querying for a free name should return something like a.

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:39):

and stuff like variable are only directions for how to populate that local scope

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:40):

without a definition, i.e. in a run_cmd or #eval, there is no scope

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:41):

Well, do you understand why I would need this?

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:41):

no?

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:42):

BananaCats works with one Bancats window per Lean file. Each Bancats window has many diagrams. Whatever you're currently doing, those create-object commands get put at the end of the lean file (usually). And to query stuff like if a variable name is available, I also do that there, then remove the command immediately, once the result is obtained.

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:42):

sounds good so far

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:42):

If you create an object in a diagram

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:43):

then that code is permanent and is marked as auto-gen'd and "don't edit me"

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:43):

It's only permanent until the user decides to delete the object in the diagram and that variable's refcount drops to zero

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:44):

So, if managing to get the next available variable name is not doable right now in Lean, I can handle it on the Python side

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:44):

Because I just keep a dictionary of variables created

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:44):

and manage it

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:44):

I still don't know why you need variable names from that though

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:44):

don't objects have user created names?

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:45):

The user has the option to not specify the variable name sometimes. And if the variable name is not available, I need to inform the user when they're thinking up a name

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:45):

It's a really professional app :)

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:46):

To test if a variable is available, you can try to add the variable line and see if you get a redeclaration error

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:46):

For instance, when I create a category, I might not care that it got the variable name C

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:46):

@Mario Carneiro thanks, I'll try it out :)

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:46):

If you are autogenerating names, just use some convention like _banana_1, _banana_2 to make it obvious that they are autogenerated

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:47):

The Lean Code has to be readable and editable under the assumption that in version 0 you can't re-sync with Bancats pyqt5 should you mess with auto-gen code

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:47):

You're allowed to edit the file in VSCode while it's auto-gen'd (parts of it) by Bancats app

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:48):

Sort of like how Visual Studio & Qt Creator work

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:48):

To accomplish this, I'm just storing the auto-gen code as strings on BanCats side, with the variable name. When refcount goes to 0, I search the file for the exact declaration code, delete it

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:49):

This is all guess work so far, I have still to connect my app to VSCode

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:49):

In lean proofs, there are many tactics that create names automatically, but it's bad form to refer to them explicitly - that means you should have named it

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:49):

I did work on some of the lean extension's typescript, adapting it to connect to two different EXE's, lean and bancats

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:50):

@Mario Carneiro I'm not sure what that entails

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:51):

Should have named what?

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:51):

Could you give an example of what's bad?

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:52):

Anyway, thanks for all your help. I like the variable decl idea, and will be using it

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:54):

I mean if you write intro and it introduces a variable called _a, that's fine, but if you later have to write e.g. exact _a then you should go back and change it to intro x and exact x

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:54):

Similarly, if you have an unnamed object, that's fine, but if you have to talk about that object in any way then it's not fine anymore and you should prompt the user to name it

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:55):

@Mario Carneiro you're probably right.

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 03:56):

My design ideas aren't final until I release. I'm design as I code and learn what can be done.

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:57):

A simple mechanism that should work is to use the variable testing thing to find the next available name in some series like C_1, C_2 or whatever you think a nice letter for your objects is

view this post on Zulip Mario Carneiro (Aug 29 2019 at 03:58):

the point about using auto variable names is more a code style thing; from an implementation perspective I think it should be fine to let the user refer to them if they really want to

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:00):

Right, that's what I do, except with dictionary when it's within app. Bancats also supports auto-indexing in a very simple and smart way. If you name an arrow f and check auto-indexing. It will go to g. But also understands any index-like thing in the symbol, e.g. $\text{Hom}_C(A_1, B_2)$ has several indexables, and you get to choose the one you want. Neat, eh?

view this post on Zulip Mario Carneiro (Aug 29 2019 at 04:01):

as in you might be calling that f_12?

view this post on Zulip Mario Carneiro (Aug 29 2019 at 04:01):

or f_1 or f_2

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:01):

? not sure

view this post on Zulip Mario Carneiro (Aug 29 2019 at 04:02):

Seems like it would be tricky to preserve all this information in the lean file without special annotation

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:02):

Yes, that's one of the ways to auto-index, but as it is now, you need to have $f_1$ made as an arrow first, then it will know what to do. Or you could start at $f_i$ and it will go to $f_j, f_k, f_l, ...$

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:02):

@Mario Carneiro I don't do that

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:03):

The Bancats system is to have lean files mixed with .bancats files

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:03):

They go together

view this post on Zulip Mario Carneiro (Aug 29 2019 at 04:03):

so the bancats file sources all the autogenerated data in the lean file?

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:03):

You cannot open the bancats file by double clicking it, unless we can somehow get that to trigger VSCode to open instead

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:03):

@Mario Carneiro yes, most likely

view this post on Zulip Mario Carneiro (Aug 29 2019 at 04:04):

why can't you do your own variable name tracking then?

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:04):

And the lean files provide the formal proof, but also the bancats diagrams show visually the steps in the proof

view this post on Zulip Mario Carneiro (Aug 29 2019 at 04:04):

are you worried about user variables polluting your namespace?

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:04):

@Mario Carneiro I can do both actually, and that will provide benefits in places

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:05):

Well, there's only one bancats window per file, but that window could have 50 diagrams in it say

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:05):

But they all point to the same lean file

view this post on Zulip Mario Carneiro (Aug 29 2019 at 04:05):

if you generate a complete lean file then you will know all the variable declarations in it, so you can avoid any collisions

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:05):

Then if you need multiple leans, you pop open another bancats window

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:05):

The entire scope of dissertation is one bancats instance -> they don't communicate between instances of bancats

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:05):

*scope of discourse of math

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:06):

@Mario Carneiro yes, but as I say, it will not be 100% autogen, the user can go in and add stuff even to the currently pointed to file

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:06):

So they could create new variables there, using them up, while it's not reflected in Bancats, and that's okay

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:07):

Bancats is only a visual driver and displayer of diagram chasing proofs, which naturally are easier to remember if there's a diagram invovled.

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:08):

later, because of the Curry-Howard-Lambek correspondence of type thoery with cat theory, we may be able to use the diagram editor in a more interesting way such as extending Lean using diagrams (graphs) instead of 100% pure formal Lean code.

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:09):

But that's not a goal for version 1 or anything soon

view this post on Zulip Mario Carneiro (Aug 29 2019 at 04:09):

hm, well I wish you luck

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:09):

In version 1, if the user would like to add a new non-standard lib category, then they'll have to write some .lean file and import it somehow.

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:10):

@Mario Carneiro thank you! ^_^

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:12):

I've already come up with a 90% visual proof of Yoneda's Lemma. The proof, I've never seen it before in a book, and no one else does the proof that way. It's two commuting squares pasted together (natural diagram squares). But you should wait for version 1 to view it in all of its bancat features

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:14):

Here's an MS Paint3D mock-up of it (with some text to complet that part of Yoneda's lemma):
https://i.stack.imgur.com/4uCeN.png

view this post on Zulip Daniel Donnelly (Aug 29 2019 at 04:14):

But of course Lean will step in and any of that text will just be comments


Last updated: May 08 2021 at 10:12 UTC