chained ors

Stream: new members

[Anas Himmi]

is it possible to express something like this?

∀ a n:ℕ, a < n → a = 0 ∨ a = 1 ∨ ... ∨ a = n

[Kenny Lau]

it's a meta theorem known as... fin_cases?

[Anas Himmi]

thank you

[Kevin Buzzard]

If you go to the tactic docs page and click on "filter by tag" in the top left and then "case bashing" you'll see that it's interval_cases, and you'll see how to work it too :-)

[Anas Himmi]

Exactly what i was looking for, thank you

[Kevin Buzzard]

We're trying to figure out how to make the docs brilliant. Any comments welcome.

[Anas Himmi]

I will try thinking about it too

[Patrick Massot]

Anas, are you interested in a specific value of n, or the general statements? Both are expressible of course, but their uses are pretty different.

[Anas Himmi]

What i want is, for every particular n, i can decompose the goal into subgoal.

[Anas Himmi]

when I import tactic.interval_cases, I get the error

invalid import: tactic.interval_cases
could not resolve import: tactic.interval_cases

Is it because I have an old version of mathlib?

[Johan Commelin]

Which version do you have?

[Johan Commelin]

Can you run git log?

[Johan Commelin]

(I don't know what system you are on. But if you can find a terminal, and run git log in your mathlib directory, then you will see when the latest commit was.)

[Anas Himmi]

i am on ubuntu

[Anas Himmi]

where can i found it?

[Anas Himmi]

it gives me an error saying it does not contain any commit

[Anas Himmi]

in mathlib/leanpkg.toml

[package]
name = "mathlib"
version = "0.1"
lean_version = "3.4.2"
path = "src"

[dependencies]

[Kevin Buzzard]

Are you running Lean in a project?

[Kevin Buzzard]

Is your project equal to mathlib, or do you have another project with mathlib as a dependency?

[Anas Himmi]

i don't understand your question

[Anas Himmi]

i installed lean from here https://github.com/leanprover-community/mathlib/blob/master/docs/install/debian.md, and am putting my files in Lean/my_project/src

[Kevin Buzzard]

Ok great.

[Bryan Gin-ge Chen]

Did you follow the instructions on setting up a Lean project here?

[Kevin Buzzard]

What happens if you change directory to Lean/my_project and then type leanproject up?

[Kevin Buzzard]

Do you have a leanpkg.toml in Lean/my_project?

[Kevin Buzzard]

Does leanproject up fix the problem? Wait until it terminates and then restart Lean in VS Code with Ctrl-Shift P

[Anas Himmi]

I get command not found

[Anas Himmi]

I do

[Kevin Buzzard]

Try source ~/.profile

[Kevin Buzzard]

and then see if leanproject works

[Anas Himmi]

i get the same error

[Kevin Buzzard]

You did this crazy wget -q https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile line?

[Kevin Buzzard]

The one in the page you linked to?

[Kevin Buzzard]

Installation should be easy on Ubuntu.

[Anas Himmi]

yes that's what i did

[Kevin Buzzard]

Did it work or did you get errors?

[Anas Himmi]

i don't remember getting errors

[Kevin Buzzard]

This should install leanproject. Without that, things are much harder.

[Kevin Buzzard]

Do you have a leanproject file in ~/.local/bin?

[Kevin Buzzard]

$ ls ~/.local/bin/leanproject
/home/buzzard/.local/bin/leanproject

[Kevin Buzzard]

Do you get something like that?

[Anas Himmi]

i don't

[Kevin Buzzard]

Then let's start again. Try typing that crazy wget command, because it didn't finish the job it was supposed to do.

[Anas Himmi]

ok

[Kevin Buzzard]

Are you logged in as a user who can run sudo?

[Kevin Buzzard]

Maybe a better idea is to go though the detailed instructions so we can find out exactly what is failing.

[Kevin Buzzard]

But I guess there's no harm in trying the one-liner one more time.

[Anas Himmi]

now the leanproject up command works

[Anas Himmi]

i'm waiting it finishes

[Kevin Buzzard]

After it has finished, close and open VS Code, and see if the import works.

[Kevin Buzzard]

I usually open VS Code by typing code . when I am in the root directory of my project.

[Kevin Buzzard]

This way VS Code is guaranteed to open the right directory.

[Anas Himmi]

now the import works!!

[Anas Himmi]

thank you!!

[Anas Himmi]

:grinning_face_with_smiling_eyes:

[Kevin Buzzard]

No problem! Now go and do some maths :-)

[Anas Himmi]

yeay