tutorials 0081

Stream: new members

[Patrick Lutz]

I'm currently working through @Patrick Massot 's tutorial and Lean claims to not recognize inv_succ_pos though I believe it's supposed to be available when doing exercise 81. I checked tuto_lib.lean and it's not there, so maybe it was accidentally left out?

[Yury G. Kudryashov]

Please provide links to the files you're talking about.

[Patrick Lutz]

Sorry, exercise 81 is in the file which is on github here: https://github.com/leanprover-community/tutorials/blob/master/src/exercises/09_limits_final.lean

[Patrick Lutz]

tuto_lib.lean is here: https://github.com/leanprover-community/tutorials/blob/master/src/solutions/tuto_lib.lean

[Patrick Lutz]

I'm trying to follow the instructions in the README of the tutorial about making threads on zulip to ask about it, sorry if I've left out context

[Bryan Gin-ge Chen]

It's proved in 00_first_proofs.lean, so you could add import .00_first_proofs at the top of your file as a workaround.

[Patrick Lutz]

When I do that it tells me "command expected"

[Johan Commelin]

Weird, can you copy paste the top of your file?

[Patrick Lutz]

import tuto_lib
import .00_first_proofs

set_option pp.beta true
set_option pp.coercions false

[Patrick Lutz]

the only change I made was the one Bryan suggested

[Johan Commelin]

Tip: #backticks

[Patrick Lutz]

strangely, after doing this VS Code was able to auto-complete to inv_succ_pos but lean still didn't recognize it

[Johan Commelin]

Very weird...

[Patrick Lutz]

import tuto_lib
import .00_first_proofs

set_option pp.beta true
set_option pp.coercions false

[Patrick Lutz]

oops

[Johan Commelin]

You can edit

[Johan Commelin]

You need 3 backticks on their own line

[Patrick Lutz]

Yeah it took me too long to realize you were linking to something

[Johan Commelin]

Anyway, I really don't know what's wrong now... Could you try saving and restarting?

[Patrick Lutz]

sure

[Patrick Lutz]

same behavior

[Johan Commelin]

Can you write #print up_bounds just after the import statements?

[Johan Commelin]

And maybe change the import to import exercises.00_first_proofs

[Johan Commelin]

Is there a red underline under one of the import statements?

[Bryan Gin-ge Chen]

Heh, I see. The source directory in leanpkg.toml is set to src/solutions.

[Bryan Gin-ge Chen]

So just import 00_first_proofs should work

[Bryan Gin-ge Chen]

Or it would, if Lean accepted imports of files that started with 0, I guess.

[Patrick Lutz]

I tried #print up_bounds and it highlited import .00_first_proofs

[Patrick Lutz]

I also tried import 00_first_proofs initially but it didn't work

[Johan Commelin]

import «00_first_proofs»?

[Johan Commelin]

Does that work around the "you cannot start with a digit" problem?

[Patrick Lutz]

how do you make that symbol before 00?

[Patrick Lutz]

wait nvm I figured out how to make it

[Patrick Lutz]

it says "illegal character in escaped identifier"

[Patrick Lutz]

oops I probably messed it up

[Bryan Gin-ge Chen]

With \f<< and \f>> it works for me, but then le_lim gets an error because it's already defined.

[Bryan Gin-ge Chen]

I didn't know this trick, by the way. Is it just for imports?

[Patrick Lutz]

yeah that's what I have now too

[Patrick Lutz]

I initially left out the \f>>

[Patrick Lutz]

but at least that resolves the issue

[Patrick Lutz]

although I think probably inv_succ_pos is supposed to be in tuto_lib?

[Bryan Gin-ge Chen]

Yeah, most likely. Although I cheated and looked at the solutions and they don't use inv_succ_pos :wink: .

[Patrick Lutz]

lol, I just wanted to use it in my solution and was surprised it wasn't available

[Patrick Lutz]

but some of my solutions seem less efficient than the official ones

[Mario Carneiro]

Bryan Gin-ge Chen said:

I didn't know this trick, by the way. Is it just for imports?

No, it works for any name

[Mario Carneiro]

so identifiers of theorems and definitions too

[Johan Commelin]

def «☃» : Prop := sorry
example : «☃» := sorry

[Patrick Massot]

Patrick Lutz said:

I'm trying to follow the instructions in the README of the tutorial about making threads on zulip to ask about it, sorry if I've left out context

You did this perfectly, but I think you're the first one to achieve this level of excellency in following the instructions, hence Yury was caught off-guard.

[Patrick Massot]

About you're question now: this is all my fault, this line mentionning inv_succ_pos is a left-over from the previous life of this file as teaching material for my undergrads where I had a lot of renamed lemmas (most often for translations purposes). This is now fixed.

[Patrick Lutz]

@Patrick Massot , thanks for the reply. And thanks for making the tutorial in the first place, it's really great.

[Patrick Massot]

This tutorial is only a translated and lightly edited version of what I wrote for a course I taught to 1st year undergrads in Orsay (who had seen the math material in a traditional way in the preceding semester). The effort of turning it into a tutorial was not so big.

[Patrick Massot]

Oh, I could add a file with the exam now that the exam is over. I still need to mark it :sad:

[Ryan Lahfa]

Patrick Massot said:

Oh, I could add a file with the exam now that the exam is over. I still need to mark it :sad:

The exam is your first PR to mathlib!

[Kevin Buzzard]

@Abhimanyu Pallavi Sudhir formalised my final exam from 2018 or 2019 somewhere, that was kind of cool to know that Lean could pass it