New to Lean, getting confusing error message

Stream: new members

[Daniel Hast]

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]

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]

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]

Can you include the imports too?

[Kevin Buzzard]

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]

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]

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

[Daniel Hast]

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]

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

[Eric Wieser]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Eric Wieser]

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

[Daniel Hast]

real.sqr_sqrt is the full name

[Eric Wieser]

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

[Eric Wieser]

Aha

[Eric Wieser]

You confused calc by calling a local variable eq

[Daniel Hast]

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

[Kevin Buzzard]

oh very nice!

[Daniel Hast]

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

[Eric Wieser]

Nope, that's a calc bug I think

[Kevin Buzzard]

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

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

[Eric Wieser]

calc is using some bad rules to resolve the = notation

[Daniel Hast]

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

[Kevin Buzzard]

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]

Thanks for the help!

[Daniel Hast]

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

[Eric Wieser]

Are you using leanproject?

[Daniel Hast]

Yes

[Kevin Buzzard]

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

[Yaël Dillies]

Oh? Don't remember that

[Yaël Dillies]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

This is only the calc _tactic_ that is broken

[Kevin Buzzard]

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]

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]

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

[Daniel Hast]

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

[Kevin Buzzard]

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

[Daniel Hast]

What chapters are planned?

[Kevin Buzzard]

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]

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

[Daniel Hast]

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

[Kevin Buzzard]

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]

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.

Hey algebra Twitter! Imperial undergraduate Kenny Lau just found a cool oversight in the proof of the Artin-Tate lemma in Atiyah--Macdonald, when formalising it in Lean. Of course the proof can be fixed. How to justify "each elt of C is a lin comb of the y_i with coeffts in B_0"? https://twitter.com/XenaProject/status/1308693991144206336/photo/1

- The Xena Project (@XenaProject)

@Daniel Hast

[Daniel Hast]

Interesting, thanks!

[Kevin Buzzard]

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]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

calc doesn't exist in lean 4

[Mario Carneiro]

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]

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]

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]

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]

The calc bug fix is merged.

[Eric Wieser]

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