Print mk_fresh_name result?

Stream: general

[Daniel Donnelly]

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]

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

[Daniel Donnelly]

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]

What's literal for the void or empty type?

[Daniel Donnelly]

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

[Daniel Donnelly]

pasted image
Almost got it, but not quite.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Daniel Donnelly]

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

[Mario Carneiro]

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]

to_string : name -> string should work

[Daniel Donnelly]

import system.io
open io
open tactic

def print_name3 :=
    put_str mk_fresh_name

#eval print_name3

[Daniel Donnelly]

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

[Daniel Donnelly]

pasted image

Here's trying to_string. Errors...

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

I'll read up on monads & programming this week

[Mario Carneiro]

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

[Daniel Donnelly]

@Mario Carneiro thank you!

[Mario Carneiro]

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

[Daniel Donnelly]

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

[Mario Carneiro]

it's globally unique, what did you expect?

[Mario Carneiro]

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

[Daniel Donnelly]

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]

"available in the current scope" doesn't exist

[Daniel Donnelly]

Like, this:

[Mario Carneiro]

there isn't really a global scope

[Mario Carneiro]

every definition has its own local scope

[Daniel Donnelly]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Daniel Donnelly]

Well, do you understand why I would need this?

[Mario Carneiro]

no?

[Daniel Donnelly]

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]

sounds good so far

[Daniel Donnelly]

If you create an object in a diagram

[Daniel Donnelly]

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

[Daniel Donnelly]

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]

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]

Because I just keep a dictionary of variables created

[Daniel Donnelly]

and manage it

[Mario Carneiro]

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

[Mario Carneiro]

don't objects have user created names?

[Daniel Donnelly]

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]

It's a really professional app :)

[Mario Carneiro]

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]

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

[Daniel Donnelly]

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

[Mario Carneiro]

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

[Daniel Donnelly]

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]

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

[Daniel Donnelly]

Sort of like how Visual Studio & Qt Creator work

[Daniel Donnelly]

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]

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

[Mario Carneiro]

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]

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]

@Mario Carneiro I'm not sure what that entails

[Daniel Donnelly]

Should have named what?

[Daniel Donnelly]

Could you give an example of what's bad?

[Daniel Donnelly]

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

[Mario Carneiro]

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]

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]

@Mario Carneiro you're probably right.

[Daniel Donnelly]

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

[Mario Carneiro]

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]

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]

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]

as in you might be calling that f_12?

[Mario Carneiro]

or f_1 or f_2

[Daniel Donnelly]

? not sure

[Mario Carneiro]

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

[Daniel Donnelly]

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]

@Mario Carneiro I don't do that

[Daniel Donnelly]

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

[Daniel Donnelly]

They go together

[Mario Carneiro]

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

[Daniel Donnelly]

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

[Daniel Donnelly]

@Mario Carneiro yes, most likely

[Mario Carneiro]

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

[Daniel Donnelly]

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

[Mario Carneiro]

are you worried about user variables polluting your namespace?

[Daniel Donnelly]

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

[Daniel Donnelly]

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

[Daniel Donnelly]

But they all point to the same lean file

[Mario Carneiro]

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]

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

[Daniel Donnelly]

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

[Daniel Donnelly]

*scope of discourse of math

[Daniel Donnelly]

@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]

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

[Daniel Donnelly]

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]

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]

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

[Mario Carneiro]

hm, well I wish you luck

[Daniel Donnelly]

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]

@Mario Carneiro thank you! ^_^

[Daniel Donnelly]

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]

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]

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