## Stream: general

### Topic: Print mk_fresh_name result?

#### 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?

#### 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 :/

#### 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


#### Daniel Donnelly (Aug 29 2019 at 03:15):

What's literal for the void or empty type?

#### Daniel Donnelly (Aug 29 2019 at 03:15):

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

#### Daniel Donnelly (Aug 29 2019 at 03:21):

pasted image
Almost got it, but not quite.

#### 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 ()

#### Mario Carneiro (Aug 29 2019 at 03:28):

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

#### Mario Carneiro (Aug 29 2019 at 03:29):

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

#### Daniel Donnelly (Aug 29 2019 at 03:30):

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

#### 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

#### Mario Carneiro (Aug 29 2019 at 03:31):

to_string : name -> string should work

#### 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


#### Daniel Donnelly (Aug 29 2019 at 03:31):

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

#### Daniel Donnelly (Aug 29 2019 at 03:32):

Here's trying to_string. Errors...

#### 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


#### Daniel Donnelly (Aug 29 2019 at 03:33):

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

#### 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

#### 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...

#### Daniel Donnelly (Aug 29 2019 at 03:35):

@Mario Carneiro thank you!

#### 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

#### 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

#### Mario Carneiro (Aug 29 2019 at 03:37):

it's globally unique, what did you expect?

#### Mario Carneiro (Aug 29 2019 at 03:38):

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

#### 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

#### Mario Carneiro (Aug 29 2019 at 03:38):

"available in the current scope" doesn't exist

Like, this:

#### Mario Carneiro (Aug 29 2019 at 03:38):

there isn't really a global scope

#### Mario Carneiro (Aug 29 2019 at 03:39):

every definition has its own local scope

#### 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.

#### Mario Carneiro (Aug 29 2019 at 03:39):

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

#### Mario Carneiro (Aug 29 2019 at 03:40):

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

#### Daniel Donnelly (Aug 29 2019 at 03:41):

Well, do you understand why I would need this?

no?

#### 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.

#### Mario Carneiro (Aug 29 2019 at 03:42):

sounds good so far

#### Daniel Donnelly (Aug 29 2019 at 03:42):

If you create an object in a diagram

#### 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"

#### 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

#### 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

#### Daniel Donnelly (Aug 29 2019 at 03:44):

Because I just keep a dictionary of variables created

and manage it

#### Mario Carneiro (Aug 29 2019 at 03:44):

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

#### Mario Carneiro (Aug 29 2019 at 03:44):

don't objects have user created names?

#### 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

#### Daniel Donnelly (Aug 29 2019 at 03:45):

It's a really professional app :)

#### 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

#### 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

#### Daniel Donnelly (Aug 29 2019 at 03:46):

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

#### 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

#### 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

#### 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

#### Daniel Donnelly (Aug 29 2019 at 03:48):

Sort of like how Visual Studio & Qt Creator work

#### 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

#### Daniel Donnelly (Aug 29 2019 at 03:49):

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

#### 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

#### 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

#### Daniel Donnelly (Aug 29 2019 at 03:50):

@Mario Carneiro I'm not sure what that entails

#### Daniel Donnelly (Aug 29 2019 at 03:51):

Should have named what?

#### Daniel Donnelly (Aug 29 2019 at 03:51):

Could you give an example of what's bad?

#### 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

#### 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

#### 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

#### Daniel Donnelly (Aug 29 2019 at 03:55):

@Mario Carneiro you're probably right.

#### 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.

#### 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

#### 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

#### 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?

#### Mario Carneiro (Aug 29 2019 at 04:01):

as in you might be calling that f_12?

#### Mario Carneiro (Aug 29 2019 at 04:01):

or f_1 or f_2

? not sure

#### 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

#### 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, ...$

#### Daniel Donnelly (Aug 29 2019 at 04:02):

@Mario Carneiro I don't do that

#### Daniel Donnelly (Aug 29 2019 at 04:03):

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

They go together

#### Mario Carneiro (Aug 29 2019 at 04:03):

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

#### 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

#### Daniel Donnelly (Aug 29 2019 at 04:03):

@Mario Carneiro yes, most likely

#### Mario Carneiro (Aug 29 2019 at 04:04):

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

#### 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

#### Daniel Donnelly (Aug 29 2019 at 04:04):

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

#### 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

#### Daniel Donnelly (Aug 29 2019 at 04:05):

But they all point to the same lean file

#### 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

#### Daniel Donnelly (Aug 29 2019 at 04:05):

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

#### 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

#### Daniel Donnelly (Aug 29 2019 at 04:05):

*scope of discourse of math

#### 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

#### 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

#### 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.

#### 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.

#### Daniel Donnelly (Aug 29 2019 at 04:09):

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

#### Mario Carneiro (Aug 29 2019 at 04:09):

hm, well I wish you luck

#### 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.

#### Daniel Donnelly (Aug 29 2019 at 04:10):

@Mario Carneiro thank you! ^_^

#### 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

#### 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

#### 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