## Stream: new members

### Topic: New to Lean, getting confusing error message

#### Daniel Hast (Nov 16 2021 at 23:03):

Hello, I'm somewhat new to Lean and have been working through the Mathematics in Lean book. Wasn't having any issues for most of it, but I've run into an exercise where my (very short) solution gives a baffling "invalid occurrence of field notation" error. Where would be a good place to post this to have someone more experienced in Lean take a look? I'm probably making a silly mistake but I've triple-checked my proof and can't see what's wrong.

#### Kevin Buzzard (Nov 16 2021 at 23:04):

Post a #mwe here, you're in exactly the right place, just post fully working code so we can see the error ourselves.

#### Daniel Hast (Nov 16 2021 at 23:04):

Thanks, here's the code:

example : inj_on sqrt { x | x ≥ 0 } :=
begin
intros x hx y hy eq,
calc x = (sqrt x)^2 : by rw sqr_sqrt hx
... = (sqrt y)^2 : by rw eq
... = y : by rw sqr_sqrt hy
end


#### Eric Wieser (Nov 16 2021 at 23:05):

Can you include the imports too?

#### Kevin Buzzard (Nov 16 2021 at 23:05):

can you make it a #mwe ? If I post that into my Lean I just get errors about not knowing what x is

#### Daniel Hast (Nov 16 2021 at 23:06):

Oops, my mistake, now with imports included:

import data.real.sqrt
open set real
example : inj_on sqrt { x | x ≥ 0 } :=
begin
intros x hx y hy eq,
calc x = (sqrt x)^2 : by rw sqr_sqrt hx
... = (sqrt y)^2 : by rw eq
... = y : by rw sqr_sqrt hy
end


#### Kevin Buzzard (Nov 16 2021 at 23:06):

calc errors are always messy to debug because the syntax is a bit unwieldy

#### Daniel Hast (Nov 16 2021 at 23:07):

Yeah. I can make the proof work just by using the same logic with rws instead of calc, but I'd like to figure out what I'm doing wrong here.

#### Kevin Buzzard (Nov 16 2021 at 23:09):

I have no idea why that doesn't work! The error message is super-unhelpful.

#### Eric Wieser (Nov 16 2021 at 23:09):

does sqr_sqrt exist? I can only find docs#real.sq_sqrt

#### Kevin Buzzard (Nov 16 2021 at 23:10):

That's not the issue though, e.g.

import data.real.sqrt
open set real
example : inj_on sqrt { x | x ≥ 0 } :=
begin
intros x hx y hy eq,
calc x = (sqrt x)^2 : sorry
... = y : sorry
end
-- invalid occurrence of field notation


#### Eric Wieser (Nov 16 2021 at 23:11):

It's happy in term mode:

import data.real.sqrt
open set real
example : inj_on sqrt { x | x ≥ 0 } :=
assume x hx y hy eq,
calc x = (sqrt x)^2 : by rw sq_sqrt hx
... = (sqrt y)^2 : by rw eq
... = y : by rw sq_sqrt hy


#### Daniel Hast (Nov 16 2021 at 23:13):

I used autocomplete to find sqr_sqrt, so it certainly does seem to exist and behave as expected—the proof works if I replace the calc block with rws (with sqr_sqrt, not sq_sqrt).

#### Eric Wieser (Nov 16 2021 at 23:15):

A more minimal mwe:

import data.set.function
open set

def foo : ℕ → ℕ := sorry

example : inj_on foo { x | x ≥ 0 } :=
begin
intros x hx y hy eq,
calc x = foo x : sorry
... = y : sorry,
end


#### Daniel Hast (Nov 16 2021 at 23:16):

It works for me in term mode too—though, oddly enough, only with sqr_sqrt. If I use sq_sqrt, it says "unknown identifier 'sq_sqrt'". Seems like this is a separate issue, though, as the above MWE illustrates.

#### Eric Wieser (Nov 16 2021 at 23:16):

When you hover over sqr_sqrt, what does it tell you the full name is?

#### Eric Wieser (Nov 16 2021 at 23:16):

I think you might be on an old mathlib, but the other issue seems to persist with new mathlib too

#### Daniel Hast (Nov 16 2021 at 23:17):

real.sqr_sqrt is the full name

#### Eric Wieser (Nov 16 2021 at 23:17):

docs#real.sqr_sqrt says that doesn't exist any more

Aha

#### Eric Wieser (Nov 16 2021 at 23:18):

You confused calc by calling a local variable eq

#### Daniel Hast (Nov 16 2021 at 23:18):

Huh. I only installed lean a couple weeks ago, so I'm surprised I could be on an old version already.

oh very nice!

#### Daniel Hast (Nov 16 2021 at 23:18):

Oh, is eq a reserved name? Oops, that would explain it!

#### Eric Wieser (Nov 16 2021 at 23:18):

Nope, that's a calc bug I think

#### Kevin Buzzard (Nov 16 2021 at 23:19):

@Daniel Hast eq is the actual name for = so you could imagine how this might screw things up in edge cases, but nonetheless it shouldn't have happened.

#### Eric Wieser (Nov 16 2021 at 23:19):

have := x = y works just fine with the bad local eq

#### Eric Wieser (Nov 16 2021 at 23:19):

calc is using some bad rules to resolve the = notation

#### Daniel Hast (Nov 16 2021 at 23:19):

This is definitely what's causing it, though. I changed eq to e and it works fine.

#### Kevin Buzzard (Nov 16 2021 at 23:20):

As for old versions, if you take a look at the #rss stream you'll be able to see how much Lean's maths library has changed in the last two weeks. It's a bit scary.

#### Daniel Hast (Nov 16 2021 at 23:21):

Thanks for the help!

#### Daniel Hast (Nov 16 2021 at 23:21):

How do I make sure I'm on the newest version of mathlib, by the way?

#### Eric Wieser (Nov 16 2021 at 23:21):

Are you using leanproject?

Yes

#### Kevin Buzzard (Nov 16 2021 at 23:22):

Looks like it was renamed by Yael on 9th September.

#### Yaël Dillies (Nov 16 2021 at 23:22):

Oh? Don't remember that

#### Yaël Dillies (Nov 16 2021 at 23:22):

Ah yeah, maybe. sqr is a weird name so I must've changed it while doing adjacent stuff.

#### Eric Wieser (Nov 16 2021 at 23:25):

Here's something I didn't know calc could do:

example (n : ℕ) : 2 ≤ n → 0 ≤ n :=
calc 2 ≤ n → 1 ≤ n : sorry
... → 0 ≤ n : sorry


#### Kevin Buzzard (Nov 16 2021 at 23:27):

I think this has come up before but I can't remember why it works. I think calc works for = because eq.trans is tagged @[trans]. But what does one tag here?

#### Eric Wieser (Nov 16 2021 at 23:29):

I created a bug report at https://github.com/leanprover-community/lean/issues/651

#### Eric Wieser (Nov 16 2021 at 23:29):

This is only the calc _tactic_ that is broken

#### Kevin Buzzard (Nov 16 2021 at 23:29):

Given that the website is now quite professional-looking, I'm slightly surprised and amused that there are still "(Kevin thinks)" comments in https://leanprover-community.github.io/extras/calc.html

#### Daniel Hast (Nov 16 2021 at 23:33):

I just figured out the issue with the outdated version of mathlib: I had downloaded the "Mathematics in Lean" project using leanproject get mathematics_in_lean, and presumably this came with an older version of mathlib. I ran leanproject upgrade-mathlib in the project directory and restarted VSCodium, and now the function is named sq_sqrt rather than sqr_sqrt.

#### Kevin Buzzard (Nov 16 2021 at 23:34):

you might also find that you broke mathematics_in_lean too :-/ I can't guarantee that the book works with current mathlib.

#### Daniel Hast (Nov 16 2021 at 23:35):

Hm, it's possible. I'm almost done going through it anyway, so it's unlikely to be an issue for me.

#### Kevin Buzzard (Nov 16 2021 at 23:35):

Great, you can help write the next bit :-)

#### Daniel Hast (Nov 16 2021 at 23:35):

What chapters are planned?

#### Kevin Buzzard (Nov 16 2021 at 23:36):

I'd like to do some of the stuff in https://github.com/ImperialCollegeLondon/formalising-mathematics but the thing about a multi-author project is that different authors might have different opinions :-)

#### Kevin Buzzard (Nov 16 2021 at 23:39):

I'm afraid we're quite a way from non-abelian Chabauty, but algebraic geometry is slowly ticking along...

#### Daniel Hast (Nov 16 2021 at 23:41):

Very cool! I'm teaching commutative algebra next semester and was thinking about formalizing some of Atiyah-Macdonald in Lean.

#### Kevin Buzzard (Nov 16 2021 at 23:44):

Oh we probably have all of that now but it's definitely a really good way to learn when you want to branch out away from all the learning material.

#### Kevin Buzzard (Nov 16 2021 at 23:51):

Here are some of the things we learnt when formalising A-M:
1) Mathematicians are really good at writing things R[1/f][1/g]=R[1/fg] (e.g. this is embedded in stuff like the proof that the presheaf on Spec(R) is a sheaf in the Stacks project) and this is not actually true when you think about it. So instead of defining a ring localisation R S, you should define is_localisation R S A, a predicate on R-algebras A saying "I satisfy the universal property". We talk about this more here -- most of my co-authors are undergrads.

2) Distinct types are disjoint. This is different from set theory where you can have rings $A\subseteq B\subseteq C$; in type theory you have to decide how you want to handle this. We tried making some of A,B,C terms but it didn't work out; in the end we made them all types. Along the way we invented heterogeneous associativity. I was really surprised these ideas weren't discovered 30 years ago, but it's interesting that your immediate reaction, like mine, was "hey I bet formalising commutative algebra would be fun", whereas this was apparently not the reaction of previous users of systems such as this, perhaps because they tended to come from computer science departments.
3) There's a mistake in the proof of the Artin-Tate lemma in A-M! It's very hard to spot though -- don't read the thread, see if you can spot it :-) It's Prop 7.8 and the issue is the claim about each element of C being a linear combination of the y_i with coefficients in B_0. Lean didn't like this claim. Of course it's not hard to fix, it's just interesting that it's there.

@Daniel Hast

#### Daniel Hast (Nov 16 2021 at 23:53):

Interesting, thanks!

#### Kevin Buzzard (Nov 16 2021 at 23:55):

There was a slip of a similar nature in Clausen-Scholze which we also spotted when formalising but which Peter of course fixed immediately.

#### Kevin Buzzard (Nov 16 2021 at 23:56):

If you want to see some more advanced number theory in Lean you should subscribe to some of the "not-subscribed-by-default" streams such as #FLT regular or #condensed mathematics (click on the + by "STREAMS" )

#### Mario Carneiro (Nov 17 2021 at 00:07):

Eric Wieser said:

This is only the calc _tactic_ that is broken

There is no calc tactic. calc in tactic mode is literally a shorthand for refine calc, so there is only a term mode calc. (Yes, this is weird and does not occur for any other tactic/term constructor in lean.)

#### Johan Commelin (Nov 17 2021 at 04:32):

Which makes it even more puzzling that the code worked in term mode but not in tactic mode.

#### Johan Commelin (Nov 17 2021 at 04:33):

FTR, it seems that Mario already fixed this in lean#652

#### Johan Commelin (Nov 17 2021 at 04:35):

@Mario Carneiro Is this something that might also matter to Lean 4?

#### Mario Carneiro (Nov 17 2021 at 04:35):

calc doesn't exist in lean 4

#### Mario Carneiro (Nov 17 2021 at 04:38):

actually that's false. The analogous issue does not appear though, in a basic test:

def foo (Eq : Nat) : 1 = 1 :=
calc 1 = 1 := rfl
_ = 1 := rfl


#### Mario Carneiro (Nov 17 2021 at 04:38):

the bug is a rather specific sequence of things going wrong so I would expect any reimplementation not to have the same issue

#### Mario Carneiro (Nov 17 2021 at 04:40):

Johan Commelin said:

Which makes it even more puzzling that the code worked in term mode but not in tactic mode.

Note that by refine calc had the same issue as by calc

#### Patrick Massot (Nov 17 2021 at 08:17):

Kevin Buzzard said:

2) Distinct types are disjoint. This is different from set theory where you can have rings $A\subseteq B\subseteq C$; in type theory you have to decide how you want to handle this.

I claim this is not a type theory vs set theory issue. Indeed in set theory "you could have rings $A\subseteq B\subseteq C$", but this simply don't happen. It's simply not true that $\mathbb{Z} \subset \mathbb{Q}$ or $A \subset A[X]$ are set inclusions, at least not with any construction that I'm aware of. They are simply abuse of notation, using invisible symbols for some maps.

#### Kevin Buzzard (Nov 17 2021 at 12:52):

The calc bug fix is merged.

#### Eric Wieser (Nov 17 2021 at 13:12):

(but won't actually be available in mathlib for a while longer)

Last updated: Dec 20 2023 at 11:08 UTC