Some basic questions

Stream: new members

[sarahzrf]

I'm working through Glimpse of Lean and I was a little surprised to see that this apparently works with the by removed:
image.png

[sarahzrf]

I had assumed so far that by is how you embed a tactic script into a term, akin to ltac: in coq, but evidently not?

[David Renshaw]

The calc syntax works both in term mode and in tactic mode.

[sarahzrf]

Ahh

[sarahzrf]

So if I put a rw there instead, it would syntax error at me?

[sarahzrf]

cool, makes sense

[sarahzrf]

How does subgoal focusing work?

[sarahzrf]

I'm working thru Glimpse of Lean; it just had me use apply on something with two hypotheses, and it told me to just prove each of them one after another inline

[sarahzrf]

in coq i would be able to use bullets to focus on them one by one, but lean is yelling at me if i try to use a bullet

[sarahzrf]

What exactly does a bullet do in lean, then, and how do I organize a proof after applying something with multiple hypotheses, if not with bullets?

[Kyle Miller]

You can use · for focusing on goals in Lean. Be sure it's the correct dot, there are a number of unicode variants. This one is \. in VS Code.

[sarahzrf]

oh wait i see the problem

[Kyle Miller]

There's also using

next =>
  tac1
  tac2

for focusing. It's the same, but next lets you name inaccessible variables at the same time.

[sarahzrf]

i tried to put a bullet before the next line and it was actually yelling at me for not having indented the line after yet, but i thought it was yelling at me for the bullet itself because that's where it put the red gunk

[sarahzrf]

not used to whitespace sensitivity in my proof assistant

[sarahzrf]

okay that makes more sense lol

[sarahzrf]

btw, glimpse of lean formats some of its proofs like

example foo : a = c := by {
  calc
    a = b := _
    _ = c := _
}

which seems excessive to me when

example foo : a = c := calc
  a = b := _
  _ = c := _

works. is the former actually considered idiomatic over the latter?

[sarahzrf]

or is it just trying to avoid confusing readers as to whether you always need a by {}

[Yaël Dillies]

I believe the point is that with the {} around you get unsolved goals errors on the }, not on the by (which beginners find very confusing)

[Kevin Buzzard]

I suspect that the by really does change things. The proofs you fill in on the various lines will be expecting terms without the by and tactics with the by. (edit: I just tried this and as Yael says below this is not true)

[Kyle Miller]

Yaël's said the reason for by { ... }. It puts the error in a place that someone first learning Lean might notice it.

[Yaël Dillies]

In general, yes, but here term-mode calc and tactic mode calc should leave you the same kinds of holes.

[Kyle Miller]

But also, you need the by to go into tactic mode. Pedagogically it's easier to stay in the realm of tactics than to discuss terms vs tactics. Plus, in your example, the := _'s cause new goals in the tactic version. That's not allowed in the term version.

[Kevin Buzzard]

Another fix for the "error in a weird place" which I'm experimenting with in my course this year is to encourage students to end all proofs with done

[sarahzrf]

my question though is basically just, in actual lean code do people stylistically tend to bother with the redundant do {} around proofs that are just a single calc

[sarahzrf]

huh, what do you mean about causing new goals

[Kyle Miller]

You see that there's an error in your foo example without the by right?

Though to get new goals with by you have to use ?_ instead of _, otherwise it gives a similar error.

example (a b c : Nat) : a = c := by
  calc
    a = b := ?_
    _ = c := ?_
  -- Two goals:
  sorry
  sorry

[sarahzrf]

is it like, in the term version lean needs to be able to individually automatically—yeah alright

[sarahzrf]

i was actually also wondering what the distinction between _ and ?_ is

[sarahzrf]

does _ ask for the elaborator to fill a hole and ?_ spawns a new goal?

[Kyle Miller]

The calc ... tactic is short for refine calc ..., and in refine, each ?a or ?_ turns into a new goal.

[Kyle Miller]

Yes, _ placeholders need to be solvable by unification.

[sarahzrf]

so you can't use ?_ outside of a tactic script then

[sarahzrf]

actually wait

[sarahzrf]

right, they aren't even the same type are they

[sarahzrf]

actually hold on

[Kevin Buzzard]

Right, ?_ is an interactive thing. If you're in term mode then you'd better be writing the term in full.

[sarahzrf]

so—you can use either _ or ?_ as a tactic and you can use either _ or ?_ as a term, but you can only use ?_ as a term if the superterm it's part of is in a refine, i'm guessing?

[sarahzrf]

what's the difference between _ and ?_ as tactics, though?

[Kevin Buzzard]

refine is a tactic but it will consume ?_ and give you a new goal (still in tactic mode)

[sarahzrf]

oh wait no i'm confused again

[sarahzrf]

one moment, let me look at this code again lol

[Patrick Massot]

sarahzrf said:

my question though is basically just, in actual lean code do people stylistically tend to bother with the redundant do {} around proofs that are just a single calc

In actual lean code there is no {} at all. This is purely a beginner thing.

[Kyle Miller]

At risk of confusing you, you can do some really weird things with these ?x metavariables outside of tactics (nobody does this; it's not good practice). If you stick with the un-named version ?_ then I'm not sure there's anything you can do with them outside of tactics.

import Mathlib.Tactic

theorem foo : ?x = (by haveI : ?x := 1; exact ?x) := rfl

#print foo
/--
theorem foo : ℕ = ℕ :=
rfl
-/

[sarahzrf]

this makes perfect sense kyle

[sarahzrf]

well i'm maybe a tiny bit surprised that actually typechecks lol

[sarahzrf]

so okay hold on

[sarahzrf]

something i was going to ask about was a kind of like. scoping thing—

[sarahzrf]

like, if you're in the middle of a proof script and then you write a term in the middle there that contains a by and then somewhere in that by you write a term that contains a ?_, which tactic script gets the goal

[sarahzrf]

But i was asking this under the impression that metavariables sort of did not exist in the term language ordinarily unless you were in a proof context. But tbh i probably shouldve expected that they did, coq works that way too

[sarahzrf]

Um. Hm

[sarahzrf]

My question still kinda stands though, now that I think about it

[sarahzrf]

Do we have a kind of situation where metavariables and goals are sort of the same thing or what

[Kevin Buzzard]

After a by you are in tactic mode so you don't write a term, you write a tactic.

[sarahzrf]

yes, i know, tactics often have terms as arguments

[sarahzrf]

i elided a step

[Kevin Buzzard]

Right, like refine. So if you are in tactic mode and write refine \<?_, ?_\> and this makes sense then you're still in tactic mode but now you have two goals, and most tactics will just apply to the first goal, but the universe has split into two at this point.

[Kevin Buzzard]

and if you were lucky enough to have a metavariable around when the universe split into two then you can do some wacky things like assigning it in one universe and having it magically be assigned in the other universe.

[sarahzrf]

i understand that

[sarahzrf]

let me write down an example of what i meant

[Kyle Miller]

sarahzrf said:

Do we have a kind of situation where metavariables and goals are sort of the same thing or what

They are exactly the same thing. Metavariables that are meant to be goals are also marked as being "synthetic opaque" ("synthetic" as in something will solve for them, namely the user). Generally, unification avoids solving for these and will even throw an error if anything tries to (hence "opaque" I guess). Goal metavariables are also recorded in a list of goals in the tactic state. It's up to tactics to remember to add lingering goal metavariables to this list of goals.

[sarahzrf]

blah blah
blah
refine \<3, by {
  refine 2 + ?_
  /- you are here -/
  }\>

[sarahzrf]

presumably at the marked point we get to refine the ?_ hole

[sarahzrf]

But say we put no more tactics there and instead skipped to the end of what i've written so far

[sarahzrf]

If we focused there, would we also from there get to refine the ?_ hole?

[sarahzrf]

Or is there some kind of scoping going on?

[Kyle Miller]

The list of goals is "scoped" to the current tactic block, and a tactic block requires that all lingering goals in its goal list be solved for.

[sarahzrf]

perfect, thank you

[Kyle Miller]

Potentially you could circumvent this and get refine to capture lingering goals, but it would take a hack, or perhaps a new tactic that's just for doing this.

[Kyle Miller]

Yeah, this can be done:

import Mathlib.Tactic

open Lean Elab Tactic in
elab "defer_all" : tactic => do
  setGoals []

example : ∃ x : Nat, x = x := by
  refine ⟨(by refine 1 + ?_; defer_all), ?_⟩
  /-
  case refine_1
  ⊢ 1 + ?refine_2 = 1 + ?refine_2

  case refine_2
  ⊢ ℕ
  -/

[Kyle Miller]

(refine works by walking through the expression it's given, collecting all ?_ metavariables, and adding them to the list of goals)

[sarahzrf]

yea, coq has a refine tactic too

[Kyle Miller]

sarahzrf said:

But i was asking this under the impression that metavariables sort of did not exist in the term language ordinarily unless you were in a proof context. But tbh i probably shouldve expected that they did, coq works that way too

You are right that completed terms do not have metavariables, but metavariables are essential to both elaboration and tactic execution, and they're part of docs#Lean.Expr -- it's just that the kernel throws an exception if it ever encounters an Expr.mvar.

[sarahzrf]

Although coq's refine doesnt have a way of distinguishing between goal holes and should-be-solved-by-the-elaborator holes, which can be awkward

[sarahzrf]

Kyle Miller said:

sarahzrf said:

But i was asking this under the impression that metavariables sort of did not exist in the term language ordinarily unless you were in a proof context. But tbh i probably shouldve expected that they did, coq works that way too

You are right that completed terms do not have metavariables, but metavariables are essential to both elaboration and tactic execution, and they're part of docs#Lean.Expr -- it's just that the kernel throws an exception if it ever encounters an Expr.mvar.

:thought: what does this mean semantically...

[Kyle Miller]

sarahzrf said:

Although coq's refine doesnt have a way of distinguishing between goal holes and should-be-solved-by-the-elaborator holes, which can be awkward

Yeah, it could be awkward in Lean 3 also, which didn't have this distinction either.

[sarahzrf]

entirely too many times ive tried to refine in coq and ended up with like 5 random typeclass instances as goals :sob:

[Kyle Miller]

Lean 4 has refine' to relive the Lean 3 days. This can be useful sometimes.

[Kyle Miller]

Though the way typeclass instances are synthesized, I think you never end up with unsolved instance goals with refine/refine'.

[sarahzrf]

coq's typeclass machinery is extremely fucking funny

[sarahzrf]

You can put arbitrary tactic scripts into it

[Kyle Miller]

sarahzrf said:

:thought: what does this mean semantically...

I'm not sure what the question is exactly, but I'll say a few things. We've got the elaborator and the kernel, and the kernel uses the same Lean.Expr as the elaborator, but it's effectively using the subtype of Lean.Expr that does not contain the Lean.Expr.mvar constructor, which is used for metavariables. The elaborator needs metavariables to handle implicit arguments, typeclass instance arguments, tactic blocks, etc. etc.

[sarahzrf]

yeah i followed that, i wasnt asking a specific question, the pl part of my brain just caught on what you said and reflexively started Wondering Things

[sarahzrf]

thought bubble emoji indicated idle curiosity

[sarahzrf]

very much a tangent

[sarahzrf]

anyway i should probably get back to learning the basics. lol

[Kyle Miller]

So let's not get started on how refine fun x => ?_ manages to create a goal state with an extra x variable in its local context, at the level of terms :-)

[sarahzrf]

what exactly is problematic there?

[sarahzrf]

huhhh, you can rewrite by iffs... is this accomplished thru setoidy mechanisms or is it just propext?

[Kyle Miller]

propext

[Kyle Miller]

You can use by? to see the term a tactic produced by the way.

[sarahzrf]

:rolling_eyes: typical cheaters

[Kyle Miller]

or use the show_term tactic, which has the syntax show_term *tactic*

[Kyle Miller]

It's not cheating if we want Prop to be equivalent to Bool, right?

[sarahzrf]

u dont even have computational behavior for ur system. ur cheating. ur just positing new terms willy nilly & violating the harmony of introduction and elimination forms

[sarahzrf]

it makes me sick

[sarahzrf]

on the other hand. wow is it convenient. hmmm

[sarahzrf]

hmm, this example in Glimpse of Lean is using have and then immediately rwing by the thing we had. is there no tactic for doing this? in coq for example you can say replace foo with bar by tactic where tactic proves foo = bar

[Yaël Dillies]

obtain rfl : foo = bar := by tactic will do (assuming foo is a variable)

[sarahzrf]

well, the two sides arent identifiers, foo and bar were metavariables and not variables there :P

[sarahzrf]

i wouldve written x and y if i had variables in mind

[Kyle Miller]

example (a b c d : Nat) : a + b + c = d := by
  conv in a + b => equals 1 => sorry
  -- 1 + c = d
  sorry

[sarahzrf]

i have no idea what =>, conv, or equals are doing here sorry lol

[Kyle Miller]

It's doing replace a + b with 1 by admit

[sarahzrf]

well i can see that, i just mean i dont understand enough lean for this to teach me something

[sarahzrf]

Like, i dont understand the pieces yet so this is not showing me a way to put them together

[Kyle Miller]

I imagine you've learned that Lean has an analogue? You don't need to understand the pieces to be able to use it.

[Kyle Miller]

If I gave you a single tactic to do it, you probably wouldn't be complaining that you don't know how it's implemented :wink:

[sarahzrf]

well, i dont like using things without understanding how they work

[sarahzrf]

eh, true

[sarahzrf]

wait, you can use calc with a chain of multiple relations?

[sarahzrf]

that's cool

[sarahzrf]

what is the typeclsas underlying it exactly?

[Patrick Massot]

@sarahzrf you are very welcome here, but you should know that you are not at all in the intended audience of the Glimpse of Lean tutorial. It may be very frustrating for you to keep going in this direction. You will probably have more fun with #tpil.

[sarahzrf]

Patrick Massot said:

sarahzrf you are very welcome here, but you should know that you are not at all in the intended audience of the Glimpse of Lean tutorial. It may be very frustrating for you to keep going in this direction. You will probably have more fun with #tpil.

i saw tpil first and quite frankly it looks more frustrating to me, i dont need concepts like "terms have types" explained to me lol

[sarahzrf]

i decided glimpse of lean looks nice because at least it's actually all code so i can skip directly to learning what the syntax is like

[Patrick Massot]

I see your point, but I'm still worried Glimpse of Lean won't answer a lot of your questions. It is really meant for people who are not interested in type theory.

[sarahzrf]

i mean, i dont need type theory explained for me, i only need lean explained to me

[Kyle Miller]

I think Patrick would also include more generally "people who are immediately interested in low-level aspects of Lean".

sarahzrf said:

i saw tpil first and quite frankly it looks more frustrating to me, i dont need concepts like "terms have types" explained to me lol

I don't really understand the issue, or what's funny about a book not being aware of what you personally already know -- here's a friendly reminder that you can skip content that you're familiar with :smile: (Of course, carry on with Glimpse of Lean if you're happy enough with it.)

[sarahzrf]

well, i was using that as one example of a more general issue, which is that tpil spends a lot of time actually explaining the concepts underlying lean. which is a good thing! but in my case it's irrelevant to me and means i have to skim heavily, because i already know the vast majority of those concepts. i'd really only be reading it for the code samples

[sarahzrf]

the "lol" wasnt meant to indicate that i found something funny per se, its almost more like a tone particle in function, idk. i can speak less casually if you like

[Kyle Miller]

I wouldn't want this place to be devoid of character, and there's room for a casual tone, but it's worth being aware that it tends to be more professional here than maybe other forums. Generally communication tends to be more functional than conversational, but that's just a tendency, not a rule. I don't want to put any damper on your excitement learning Lean or feeling like you can hang out here to discuss or ask questions about Lean.

For me, I started back in the Lean 3 days, going through Kevin Buzzards NNG and then a Patrick Massot's tutorial, and from there I relied on my past experience with functional programming (including some Agda), consulted the Lean 3 reference manual, and hung out here picking up things from what people were talking about. Oh, I had also opened up the HoTT book a few times, if that counts for anything. I think it's fair using whatever materials speak to you; I myself have only read #tpil randomly, skimming chapters here and there. My first question on the Zulip was about a frustrating non-beta-reduced lambda that was hidden because of the pretty printer, which I could deduce because I knew lambda calculus, and because I was following a math-oriented tutorial I didn't have the tools to deal with it. (An answer is dsimp only by the way.)

[sarahzrf]

Does Lean have some kind of command that searches the types of all loaded definitions for a given subterm? For example, is there some way of saying something like
#search _ + (_ + _) = (_ + _) + _
to look for associativity theorems about +?

[Damiano Testa]

@loogle _ + (_ + _) = (_ + _) + _

Let's see this!

[sarahzrf]

Is there something that works from inside a Lean session?

[loogle]

Failure! Bot is unavailable

[Damiano Testa]

Maybe #find?

[sarahzrf]

How do I use #find?

[Damiano Testa]

(I never used it, though.)

[Kevin Buzzard]

If you've imported some of mathlib it should just work?

import Mathlib.Data.Real.Sqrt -- or whatever

#find (?a -> ?b) -> List ?a -> List ?b -- finds List.map and some other stuff

See examples at https://loogle.lean-lang.org/

[sarahzrf]

Cool

[sarahzrf]

Is there a way to do an AND?

[sarahzrf]

for example, if i want to search for a theorem that includes both Continuous ?f and Monotone ?f in its statement

[sarahzrf]

Also: I see that Lean has sections and section variables. Does it have full-on ML-style modules?

[David Renshaw]

My understanding is

1. in Lean terminology, a "module" = "file" = "compilation unit"
2. Lean also has namespaces, which are orthogonal to modules
3. Lean does not have ML-style modules/functors, but can support a lot of the same patterns via dependent types

[sarahzrf]

how do i declare a class instance variable

[sarahzrf]

i wrote variable (C : Type) [Category C] and it's complaining

invalid binder annotation, type is not a class instance
  ?m.1425
use the command `set_option checkBinderAnnotations false` to disable the check

[Kevin Buzzard]

If you mean mathematical categories then maybe you want open CategoryTheorysomewhere

[Kevin Buzzard]

docs#Category

[Kevin Buzzard]

Difficult to tell without a #mwe

[sarahzrf]

Ah yes, the issue was that it was Category and not CategoryTheory.Category

[sarahzrf]

Why isn't the error that Category doesn't exist, then?

[Mauricio Collares]

Do you get a better error with set_option autoImplicit false? If so, see https://lean-lang.org/lean4/doc/autobound.html

[sarahzrf]

#set_option autoImplicit false gives an error, but oddly enough it does result in a better error message anyway

[sarahzrf]

Hm, Category isn't a lowercase letter or Greek, so why is that link relevant?

[Mauricio Collares]

It really is set_option without the #. You can disable auto implicits for non-single-character identifiers with set_option relaxedAutoImplicit false, I think. The single-letter restriction was relaxed after the manual was written, I think (lean4#1011).

[Mauricio Collares]

LSP should highlight autoimplicits differently but it can be a bit subtle. There are some threads here in Zulip containing tweaks to the color scheme.

[Kevin Buzzard]

There's this great footgun switched on in lean by default which goes "if the user makes a typo, just create a new type called that and press on".

[Kevin Buzzard]

Once you're aware of it it's great. When you're not, it's as confusing as hell