Zulip Chat Archive

Stream: new members

Topic: Lean4 tutorials : (help) example for calc in rw not working


Shubham Kumar (Oct 22 2022 at 19:51):

section
  variable (a b c d e : Nat)
  variable (h1 : a = b)
  variable (h2 : b = c + 1)
  variable (h3 : c = d)
  variable (h4 : e = 1 + d)

  theorem T : a = e :=
    calc
      a = b     := by rw [h1]
      _ = c + 1 := by rw [h2]
      _ = d + 1 := by rw [h3]
      _ = 1 + d := by rw [Nat.add_comm]
      _ = e     := by rw [h4]
end

I'm getting errors for h1 and h2

failed to rewrite using equation theorems for 'h1'
failed to rewrite using equation theorems for 'h2'

what am I doing wrong?

Kevin Buzzard (Oct 22 2022 at 20:05):

My guess is that h1 is about a different b. Try include b c d before the theorem, or put all the hypotheses and variables in the theorem statement rather than before it.

Kevin Buzzard (Oct 22 2022 at 20:07):

If you put set_option autoImplicit false at the top of your file then do you get an error in Theorem T?

Shubham Kumar (Oct 22 2022 at 20:20):

using include like this

  include b c d
  theorem T : a = e :=
    calc
      a = b      := by rw [h1]
      _ = c + 1 := by rw [h2]
      _ = d + 1 := by rw [h3]
      _ = 1 + d := by rw [Nat.add_comm]
      _ = e     := by rw [h4]

include has a red squiggly line showing a message expected command

Kevin Buzzard (Oct 22 2022 at 20:21):

I'm sorry, I don't really speak Lean 4. Just move all the variables and hypotheses after T and you should be fine.

Shubham Kumar (Oct 22 2022 at 20:21):

and adding set_option autoImplicit false doesn't change the error

Kevin Buzzard (Oct 22 2022 at 20:21):

What you're trying to do now is kind of mathematically meaningless, hypothesis h1 says "for all a and b, a=b", whereas you only want this hypothesis for the a and b in your theorem statement.

Shubham Kumar (Oct 22 2022 at 20:27):

Kevin Buzzard said:

I'm sorry, I don't really speak Lean 4. Just move all the variables and hypotheses after T and you should be fine.

like this?

section
  theorem T : a = e :=
    calc
      a = b     := by rw [h1]
      _ = c + 1 := by rw [h2]
      _ = d + 1 := by rw [h3]
      _ = 1 + d := by rw [Nat.add_comm]
      _ = e     := by rw [h4]

  variable (a b c d e : Nat)
  variable (h1 : a = b)
  variable (h2 : b = c + 1)
  variable (h3 : c = d)
  variable (h4 : e = 1 + d)

end

I get 2 messages in addition to previous errors. These errors are related to b and c stating

unknown identifier 'b'

and

unknown identifier 'c'

Shubham Kumar (Oct 22 2022 at 20:28):

Kevin Buzzard said:

What you're trying to do now is kind of mathematically meaningless, hypothesis h1 says "for all a and b, a=b", whereas you only want this hypothesis for the a and b in your theorem statement.

I realised that right now but when I was following the tutorial it didn't strike me :)

Ruben Van de Velde (Oct 22 2022 at 20:28):

I'm guessing Kevin meant something like

  theorem T
    (a b c d e : Nat)
    (h1 : a = b)
    (h2 : b = c + 1)
    (h3 : c = d)
    (h4 : e = 1 + d) : a = e :=
    calc
      a = b     := by rw [h1]
      _ = c + 1 := by rw [h2]
      _ = d + 1 := by rw [h3]
      _ = 1 + d := by rw [Nat.add_comm]
      _ = e     := by rw [h4]

Kevin Buzzard (Oct 22 2022 at 20:28):

Thanks Ruben. Sorry, I'm not at Lean right now.

Shubham Kumar (Oct 22 2022 at 20:29):

Oh! got it! Thanks @Ruben Van de Velde and @Kevin Buzzard

Shubham Kumar (Oct 22 2022 at 20:29):

let me try that

Kevin Buzzard (Oct 22 2022 at 20:29):

Now h1 is about the a and b in your theorem, rather than some arbitrary a and b.

Shubham Kumar (Oct 22 2022 at 20:35):

Ruben Van de Velde said:

I'm guessing Kevin meant something like

  theorem T
    (a b c d e : Nat)
    (h1 : a = b)
    (h2 : b = c + 1)
    (h3 : c = d)
    (h4 : e = 1 + d) : a = e :=
    calc
      a = b     := by rw [h1]
      _ = c + 1 := by rw [h2]
      _ = d + 1 := by rw [h3]
      _ = 1 + d := by rw [Nat.add_comm]
      _ = e     := by rw [h4]

so that still is not working for me

section
  theorem T
    (a b c d e : Nat)
    (h1 : a = b)
    (h2 : b = c + 1)
    (h3 : c = d)
    (h4 : e = 1 + d) : a = e :=
    calc
      a = b     := by rw [h1]
      _ = c + 1 := by rw [h2]
      _ = d + 1 := by rw [h3]
      _ = 1 + d := by rw [Nat.add_comm]
      _ = e     := by rw [h4]
end

has the same error

failed to rewrite using equation theorems for 'h1'

Shubham Kumar (Oct 22 2022 at 20:35):

and similarly for h2

Ruben Van de Velde (Oct 22 2022 at 20:40):

Well then I don't know :)

Shubham Kumar (Oct 22 2022 at 20:41):

I'm sorry :) maybe definitely doing something wrong
But I cannot understand what?

Is the above code working fine for you?

Kevin Buzzard (Oct 22 2022 at 20:41):

This code looks to me like it would work fine in Lean 3 but I don't really speak Lean 4 yet.

Kevin Buzzard (Oct 22 2022 at 20:42):

(well, in Lean 3 there would be ... instead of _, I don't know the syntax for calc in Lean 4)

David Renshaw (Oct 22 2022 at 20:44):

@Shubham Kumar what version of Lean4 are you using?

Shubham Kumar (Oct 22 2022 at 20:45):

David Renshaw said:

Shubham Kumar what version of Lean4 are you using?

 lean --version
Lean (version 4.0.0, commit 7dbfaf9b7519, Release)

Kevin Buzzard (Oct 22 2022 at 20:46):

I'm not sure calc existed back then. I've got to a computer and can confirm that the code works fine with a recent nightly build.

Kevin Buzzard (Oct 22 2022 at 20:46):

(Oh, sorry, that version is not as old as I thought, but it's still very old)

David Renshaw (Oct 22 2022 at 20:46):

That's a few months old

commit 7dbfaf9b751917a7fe020485bf57f41fdddcaafa
Author: Leonardo de Moura <leonardo@microsoft.com>
Date:   Sun Aug 7 09:24:18 2022 -0700

    fix: bug at `mkSizeOfSpecLemmaInstance`

    closes #1441

Shubham Kumar (Oct 22 2022 at 20:47):

David Renshaw said:

That's a few months old

commit 7dbfaf9b751917a7fe020485bf57f41fdddcaafa
Author: Leonardo de Moura <leonardo@microsoft.com>
Date:   Sun Aug 7 09:24:18 2022 -0700

    fix: bug at `mkSizeOfSpecLemmaInstance`

    closes #1441

oh let me update it, thanks @David Renshaw !

Shubham Kumar (Oct 22 2022 at 20:52):

ok, so I updated my lean version using elan and my current version is

❯ lean --version
Lean (version 4.0.0, commit 7dbfaf9b7519, Release)

And I restarted my system but the error is still there

Shubham Kumar (Oct 22 2022 at 20:53):

do I need to rebuild it?

David Renshaw (Oct 22 2022 at 20:54):

that's the same lean version

Shubham Kumar (Oct 22 2022 at 20:54):

oh yeah that's right, sorry I thought it was updated

David Renshaw (Oct 22 2022 at 20:54):

I'm using

$ lean --version
Lean (version 4.0.0-nightly-2022-10-18, commit faa612e7b79a, Release)

and I don't see the error

Shubham Kumar (Oct 22 2022 at 20:54):

I'll try again

Shubham Kumar (Oct 22 2022 at 20:54):

sorry again

Shubham Kumar (Oct 22 2022 at 20:55):

so I need to switch to nightly?

David Renshaw (Oct 22 2022 at 20:55):

I think most folks using Lean 4 use the nightly releases.

Shubham Kumar (Oct 22 2022 at 20:55):

ok got it

Shubham Kumar (Oct 22 2022 at 20:59):

how do I set nightly to be 4.0.0-nightly-2022-10-18?
It's currently

❯ lean --version
Lean (version 3.9.0, nightly-2020-04-28, commit f1fc405f5290, Release)

I tried

❯ elan override set 4.0.0-nightly-2022-10-18
info: downloading component 'lean'
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download nonexistent lean version `4.0.0-nightly-2022-10-18`
info: caused by: could not download file from 'https://github.com/leanprover/lean/releases/expanded_assets/v4.0.0-nightly-2022-10-18' to '/home/sk/.elan/tmp/spc0c3_chdtf7s44_file'
info: caused by: http request returned an unsuccessful status code: 404

but that didn't work, any help regarding this?

David Renshaw (Oct 22 2022 at 21:01):

My project root has a file named lean-toolchain containing

leanprover/lean4:nightly-2022-10-18

David Renshaw (Oct 22 2022 at 21:01):

It's also possible that you need to update elan.

David Renshaw (Oct 22 2022 at 21:01):

elan self update usually works.

Kevin Buzzard (Oct 22 2022 at 21:02):

Are you working in a Lean project? This is the correct way to be using Lean.

Shubham Kumar (Oct 22 2022 at 21:02):

so elan self update results in no update

❯ elan self update
info: checking for self-updates

Kevin Buzzard (Oct 22 2022 at 21:03):

You should just update the version of Lean used in the project itself. Unfortunately I don't know how to do this in Lean 4.

Shubham Kumar (Oct 22 2022 at 21:03):

Kevin Buzzard said:

Are you working in a Lean project? This is the correct way to be using Lean.

I am actually learning lean by following tutorials, I'm not sure if you were asking me?

Kevin Buzzard (Oct 22 2022 at 21:03):

Is the tutorial in a Lean project?

David Renshaw (Oct 22 2022 at 21:03):

I expect elan override set leanprover/lean4:nightly-2022-10-18 to work.

Kevin Buzzard (Oct 22 2022 at 21:04):

Whenever I use Lean I am working in a Lean project, not just with a random file at some random place in my filesystem

Shubham Kumar (Oct 22 2022 at 21:06):

Kevin Buzzard said:

Is the tutorial in a Lean project?

umm I don't understand that question the tutorial is TPiL and I used the hyperlink provided to setup the project using lake.
TPiL : https://leanprover.github.io/theorem_proving_in_lean4/
Basic setup : https://leanprover.github.io/lean4/doc/setup.html

Shubham Kumar (Oct 22 2022 at 21:06):

I don't know if I answered your question

Shubham Kumar (Oct 22 2022 at 21:06):

I am just learning by following the TPiL book I guess

Shubham Kumar (Oct 22 2022 at 21:07):

Kevin Buzzard said:

Whenever I use Lean I am working in a Lean project, not just with a random file at some random place in my filesystem

I think lake scaffolds a lean project so I think that covers it

Shubham Kumar (Oct 22 2022 at 21:08):

David Renshaw said:

I expect elan override set leanprover/lean4:nightly-2022-10-18 to work.

Yes that worked! Thanks @David Renshaw

 lean --version
Lean (version 4.0.0-nightly-2022-10-18, commit faa612e7b79a, Release)

Shubham Kumar (Oct 22 2022 at 21:10):

for reference this is what my directory looks like

❯ exa --tree
.
├── build
│  ├── ir
│  └── lib
│     └── Main.ilean
├── lakefile.lean
└── Main.lean

David Renshaw (Oct 22 2022 at 21:10):

so your errors went away?

Shubham Kumar (Oct 22 2022 at 21:10):

David Renshaw said:

so your errors went away?

sadly no :see_no_evil:

Shubham Kumar (Oct 22 2022 at 21:11):

yeah I don't know maybe I try a fresh project scaffold

Kevin Buzzard (Oct 22 2022 at 21:11):

Why not just make a new Lean project with today's Lean?

Mauricio Collares (Oct 22 2022 at 21:11):

If you create a file called lean-toolchain at the project root containing the single line leanprover/lean4:nightly-2022-10-18, that should set the correct version of Lean.

Shubham Kumar (Oct 22 2022 at 21:11):

Kevin Buzzard said:

Why not just make a new Lean project with today's Lean?

Yeah that's what I was thinking

Kevin Buzzard (Oct 22 2022 at 21:12):

I think that if you're using Lean within the TPIL project then it will use the version of Lean which the TPIL config file tells it to use, no matter how hard you try to override this.

Kevin Buzzard (Oct 22 2022 at 21:12):

I am not sure that taking TPIL and then randomly changing the version of Lean is a good idea.

Kevin Buzzard (Oct 22 2022 at 21:12):

That might solve the problem at hand but it might create a whole host of new problems

Shubham Kumar (Oct 22 2022 at 21:12):

Mauricio Collares said:

If you create a file called lean-toolchain at the project root containing the single line leanprover/lean4:nightly-2022-10-18, that should set the correct version of Lean.

I'll try this

Kevin Buzzard (Oct 22 2022 at 21:12):

I would strongly recommend against doing that

Kevin Buzzard (Oct 22 2022 at 21:13):

You risk breaking the entire project

Kevin Buzzard (Oct 22 2022 at 21:13):

Just create a new project

Shubham Kumar (Oct 22 2022 at 21:13):

Kevin Buzzard said:

Just create a new project

yeah I was going to do that

Shubham Kumar (Oct 22 2022 at 21:13):

and add the lean-toolchain file

Shubham Kumar (Oct 22 2022 at 21:13):

is that ok?

Shubham Kumar (Oct 22 2022 at 21:14):

I am not using TPiL locally, I am using TPiL as a book I think it should be ok, right?

Kevin Buzzard (Oct 22 2022 at 21:14):

I'm really sorry, I don't use Lean 4. Just follow the instructions on creating a new Lean project with an up to date Lean 4 and then try your code in a file within that project.

Shubham Kumar (Oct 22 2022 at 21:14):

Kevin Buzzard said:

I'm really sorry, I don't use Lean 4. Just follow the instructions on creating a new Lean project with an up to date Lean 4 and then try your code in a file within that project.

ok will try and do that

Kevin Buzzard (Oct 22 2022 at 21:15):

Re your last TPIL message, I am confused about whether you are currently working in a project or not, but I think the simplest solution is that if you want to be working with the latest version of Lean then just make a new project which uses the latest version of Lean and work within that project.

Shubham Kumar (Oct 22 2022 at 21:18):

so just to clarify I created a lean project using the steps provided here : https://leanprover.github.io/lean4/doc/setup.html

That helped me create a lean project directory

Then I started working through the exercises while reading the text material from TPIL.

When I am trying to solve my exercise I use Main.lean as the only file where I try to solve problems using sections to separate the concepts that are different acc to me.

Kevin Buzzard (Oct 22 2022 at 21:19):

Got it. And you did this in August?

Shubham Kumar (Oct 22 2022 at 21:19):

no a couple of days back

Kevin Buzzard (Oct 22 2022 at 21:19):

Then I was completely wrong with my assertions that you were about to break your project.

Shubham Kumar (Oct 22 2022 at 21:19):

no worries, text is a hard medium to convey context

Shubham Kumar (Oct 22 2022 at 21:20):

but I was using the stable branch of lean 4 so I think nightly would be better as mentioned by @David Renshaw and @Mauricio Collares

Shubham Kumar (Oct 22 2022 at 21:20):

but I am still not sure so let me try at this once again

Kevin Buzzard (Oct 22 2022 at 21:21):

I know sufficiently little about Lean 4 that I think it's best if I just shut up now. I've told you all I know. I'm sorry I couldn't be of more help. I'll tell you how I got your code working on my machine: I have a copy of this project https://github.com/leanprover-community/mathlib4 on my machine, which uses a very recent nightly version of Lean. I just cut and pasted your code into a scratch file in that project and it worked fine.

Kevin Buzzard (Oct 22 2022 at 21:22):

I was scared that you had downloaded some kind of TPIL project but it sounds like you just made your own project, so I would do what @Mauricio Collares was suggesting; it won't break your project if your project is essentially empty. I had incorrectly understood that you were working in a project which someone else had made and you had cloned.

Shubham Kumar (Oct 22 2022 at 21:23):

Kevin Buzzard said:

I know sufficiently little about Lean 4 that I think it's best if I just shut up now. I've told you all I know. I'm sorry I couldn't be of more help. I'll tell you how I got your code working on my machine: I have a copy of this project https://github.com/leanprover-community/mathlib4 on my machine, which uses a very recent nightly version of Lean. I just cut and pasted your code into a scratch file in that project and it worked fine.

no it was nice back and forth and I was bad at addressing my situation too so it's kind of on me as well

Kevin Buzzard (Oct 22 2022 at 21:23):

Apologies to Mauricio and you for misleading.

Shubham Kumar (Oct 22 2022 at 21:23):

Kevin Buzzard said:

I was scared that you had downloaded some kind of TPIL project but it sounds like you just made your own project, so I would do what Mauricio Collares was suggesting; it won't break your project if your project is essentially empty. I had incorrectly understood that you were working in a project which someone else had made and you had cloned.

yes I will do that

Kevin Buzzard (Oct 22 2022 at 21:23):

Note that when you update your Lean it might break some code which previously worked, as well as hopefully getting some code which is currently broken, working :-)

Mauricio Collares (Oct 22 2022 at 21:24):

Kevin's general message is completely right and is great advice to have in mind: Changing the lean-toolchain file from a pinned version to another pinned version is a bad idea, unless of course you're an experienced Lean user and can deal with the fallout yourself. But TPiL4 is a special beast becasue it gets tested by core Lean 4's CI, so if you have the latest version of TPiL4 then the latest nightly (or next day's nightly) is guaranteed to work with it.

Kevin Buzzard (Oct 22 2022 at 21:24):

Oh so that's all the more reason why Mauricio was right :-)

Mauricio Collares (Oct 22 2022 at 21:28):

Actually, I think I confused the Lean Manual with TPiL4. The former one certainly gets tested by core Lean 4 CI, the latter seems to be tested separately. But unfortunately TPiL4 is not pinned to any particular version of Lean, so every time CI runs on the TPiL4 repo it gets tested against the latest nightly, which should be fine since CI is scheduled to run every night.


Last updated: Dec 20 2023 at 11:08 UTC