use tactic

Stream: Is there code for X?

[David Chanin (he) (S2'21)]

I'm following along this gpt-f video, and at one point it has the proof:

example (n: ℕ) : ∃ (m: ℕ), m > n :=
begin
  use n + 1,
  exact n.lt_succ_self,
end

However, when I try to write this in lean3, I get the error unknown identifier 'use'. What am I missing? Is there something I need to import?

[Jireh Loreaux]

If you have mathlib as a dependency to your project, import tactic at the beginning of the file should do the trick.

[David Chanin (he) (S2'21)]

You're a genius! That did it

[David Chanin (he) (S2'21)]

Is there a way to import just what I'm using? It makes me nervous to write things like import tactic since then I don't know where the labels I'm using in the code is from

[David Chanin (he) (S2'21)]

Or is there a way to see what's being imported when I write something like import tactic? I assume lots of stuff gets pulled in, but I can't tell how to see what it all is

[Kevin Buzzard]

import tactic imports a huge amount of stuff yes; it's what I encourage mathematicians to do because it gives them most basic math stuff and most tactics.

[Kevin Buzzard]

I think you can import tactic.interactive to get use working; this is an extremely minimal import which just gives you a bunch of really useful tactics which happen to be in mathlib rather than core Lean because they weren't needed in core Lean.

[David Chanin (he) (S2'21)]

interesting, so there's no equivalent to, ex, in python saying something like from tactic.interactive import use?

[Julian Berman]

The docs will tell you what import works as well -- https://leanprover-community.github.io/mathlib_docs/tactics.html#use (here it says indeed tactic.interactive, but also import tactic.basic)

[Julian Berman]

As for the Pythonism -- my perception is the Lean community, or at least mathlib, is less ... "cognizant" maybe? of such things. Or the style indeed is "import stuff and deal with it later if needed" seemingly.

[Julian Berman]

There's open foo (bar) which is sort of similar, it just pulls bar out of foo, but I don't know if there's similar syntax which works for import where a bunch of stuff may get plopped into your namespace immediately

[Yaël Dillies]

I believe such targeted imports wouldn't quite work in mathlib because maths is so underconnected. Further, there is a bunch of instance stuff that would unexpectedly break if we were not taking all transitive imports by default.

[Julian Berman]

So the Python import there still "imports" everything, it's just a question of what things you can refer to unqualified after it has run. So if importing something (in Lean) is like "have a bunch of side effects like registering some instances with the typeclass search system" then they'd still hypothetically run. I just mean that folks don't tend to like qualified imports, or minimizing plopping things in the global namespace, as much as in Python (which seems safe for a language like Lean but requires active energy coming from Python I think to not care about as much. To a Python programmer I'd say "use from imports as little as possible, and never import lots of stuff into the global namespace", and in Lean I just get the perspective that the reverse is generally preferred, folks will sometimes comment "why do you keep writing foo.something, get rid of the foo. with an open.)

[Mario Carneiro]

I rarely use open, the namespacing is pretty light in most parts of mathlib so it isn't needed, and certain namespaces like nat cause a lot of overloading if you open them

[Mario Carneiro]

I think the point is that python's from foo import bar is closest to lean's import foo open bar, and you can just leave off the last bit if you don't want to use it unqualified. In any case, for interactive tactics like use there is no namespacing at all: all tactics must be in the tactic.interactive namespace and they are all available unqualified in begin-end blocks if imported

[Kyle Miller]

A big difference between Python and Lean is how they handle the "linkage" problem, which is how do global variables end up actually referring to values?

The Python system: there are module objects, and a module contains a name->value mapping. When a module file is loaded it creates a module and (1) each module it imports gets added to this module's mapping (where from foo import x goes and copies the value for x in foo to this module), and (2) each function that gets defined gets a reference to the current module, since that way when that function is evaluated, it's able to evaluate global variables in the context of the module it was defined in. Modules double as a sort of hierarchical namespacing system, since when you import a module the module itself gets added to the current module's mapping, so foo.x turns into "look up foo in the current module, then ask foo for x."

The Lean system: there are two orthogonal systems, environments and modules. The environment is a name->value mapping, and each module you import extends the environment (and the name of the module may have no relation to the names it adds to the environment). There is a namespacing system from having hierarchical names. Then the open foo command just adds aliases to the environment for everything with the foo prefix, but any references to aliases get resolved into fully qualified names during elaboration time. There's an expectation that names will never be reused between different modules. This means that when a definition is evaluated, it can evaluate global variables by looking up a declaration by its fully qualified name alone, in any environment that contains that definition. This is useful when it comes to proving things because definitions can be unfolded, and any names you see are ones you can refer to yourself. I imagine this also makes passing things to the Lean kernel for final verification simpler.

The Lean system is sort of like Common Lisp's, where there are symbol packages (a complicated form of hierarchical names) and each symbol package contains some name->symbol mapping. Unlike Lean, each symbol directly contains the value it refers to, and the way the open equivalent works is that a reference to the symbol is added to another symbol package. Linkage happens at parse time, so when a function is evaluated it's able to evaluate global variables by just asking the symbol itself for its value.

In principle, Lean could allow you to do "tree shaking" and add only those declarations to the environment that are transitively necessary to work with a given declaration. But, in practice, since you're not supposed to reuse fully qualified names between different modules, I guess you don't need this sort of surgical namespace management.

[Mario Carneiro]

In principle, Lean could allow you to do "tree shaking" and add only those declarations to the environment that are transitively necessary to work with a given declaration. But, in practice, since you're not supposed to reuse fully qualified names between different modules, I guess you don't need this sort of surgical namespace management.

This would also be bad for stability, since it means that any change to the body of a definition would affect what definitions are available in downstream modules

[Kyle Miller]

Mario Carneiro said:

all tactics must be in the tactic.interactive namespace and they are all available unqualified in begin-end blocks if imported

I wanted to see if there might have been an edge case to this, but tactic blocks do seem to require the names of tactics to be in the tactic.interactive namespace -- aliases don't count.

meta def mytactics.foo := @tactic.interactive.simp

-- Create alias `tactic.interactive.foo` for `mytactics.foo`
open mytactics as tactic.interactive

-- This is ok
#print tactic.interactive.foo
-- meta def mytactics.foo  ...

-- Yet,
example : 1 = 1 :=
begin
  foo,
  -- unknown identifier 'foo'
end

[Alex J. Best]

I'm confused, this works fine, and the tactic isn't in the interactive namespace

namespace oof
meta def ayy : tactic unit :=
tactic.exact `(trivial)
end oof
open oof

example : true :=
begin
  ayy,
  tactic.trace_state
end

I thought there were some differences with tactics that took arguments, but not in general

[Mario Carneiro]

you need to put tactics in the interactive namespace if you want them to be parsed as interactive tactics, which means you get to use parse my_parser to parse arguments with custom syntax. You can also use any term in a begin end block as if it was a tactic, but in this case it is just treated as an expression so you have to conform to expression syntax and name resolution works as normal

[Mario Carneiro]

This affects even simple tactics with no arguments:

example : true :=
begin
  trivial; skip, -- ok
  ayy; skip, -- unknown identifier 'skip'
end