Zulip Chat Archive

Stream: new members

Topic: chained ors


view this post on Zulip Anas Himmi (Apr 10 2020 at 16:09):

is it possible to express something like this?

 a n:, a < n  a = 0  a = 1  ...  a = n

view this post on Zulip Kenny Lau (Apr 10 2020 at 16:11):

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

view this post on Zulip Anas Himmi (Apr 10 2020 at 16:27):

thank you

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 16:28):

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 :-)

view this post on Zulip Anas Himmi (Apr 10 2020 at 16:32):

Exactly what i was looking for, thank you

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 16:33):

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

view this post on Zulip Anas Himmi (Apr 10 2020 at 16:52):

I will try thinking about it too

view this post on Zulip Patrick Massot (Apr 10 2020 at 17:00):

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.

view this post on Zulip Anas Himmi (Apr 10 2020 at 18:35):

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

view this post on Zulip Anas Himmi (Apr 11 2020 at 17:33):

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?

view this post on Zulip Johan Commelin (Apr 11 2020 at 17:36):

Which version do you have?

view this post on Zulip Johan Commelin (Apr 11 2020 at 17:36):

Can you run git log?

view this post on Zulip Johan Commelin (Apr 11 2020 at 17:36):

(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.)

view this post on Zulip Anas Himmi (Apr 11 2020 at 17:37):

i am on ubuntu

view this post on Zulip Anas Himmi (Apr 11 2020 at 17:37):

where can i found it?

view this post on Zulip Anas Himmi (Apr 11 2020 at 17:37):

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

view this post on Zulip Anas Himmi (Apr 11 2020 at 17:39):

in mathlib/leanpkg.toml

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

[dependencies]

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:46):

Are you running Lean in a project?

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:47):

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

view this post on Zulip Anas Himmi (Apr 11 2020 at 17:49):

i don't understand your question

view this post on Zulip Anas Himmi (Apr 11 2020 at 17:51):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:52):

Ok great.

view this post on Zulip Bryan Gin-ge Chen (Apr 11 2020 at 17:52):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:52):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:53):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:53):

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

view this post on Zulip Anas Himmi (Apr 11 2020 at 17:56):

I get command not found

view this post on Zulip Anas Himmi (Apr 11 2020 at 17:56):

I do

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:57):

Try source ~/.profile

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:57):

and then see if leanproject works

view this post on Zulip Anas Himmi (Apr 11 2020 at 17:57):

i get the same error

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:58):

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?

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:58):

The one in the page you linked to?

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:58):

Installation should be easy on Ubuntu.

view this post on Zulip Anas Himmi (Apr 11 2020 at 17:58):

yes that's what i did

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:59):

Did it work or did you get errors?

view this post on Zulip Anas Himmi (Apr 11 2020 at 17:59):

i don't remember getting errors

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:59):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:02):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:02):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:02):

Do you get something like that?

view this post on Zulip Anas Himmi (Apr 11 2020 at 18:05):

i don't

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:05):

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

view this post on Zulip Anas Himmi (Apr 11 2020 at 18:05):

ok

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:06):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:06):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:07):

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

view this post on Zulip Anas Himmi (Apr 11 2020 at 18:08):

now the leanproject up command works

view this post on Zulip Anas Himmi (Apr 11 2020 at 18:08):

i'm waiting it finishes

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:08):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:09):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:09):

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

view this post on Zulip Anas Himmi (Apr 11 2020 at 18:09):

now the import works!!

view this post on Zulip Anas Himmi (Apr 11 2020 at 18:09):

thank you!!

view this post on Zulip Anas Himmi (Apr 11 2020 at 18:10):

:grinning_face_with_smiling_eyes:

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:10):

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

view this post on Zulip Anas Himmi (Apr 11 2020 at 18:12):

yeay


Last updated: May 16 2021 at 05:21 UTC