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

Stream: new members

[Shubham Kumar]

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]

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]

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

[Shubham Kumar]

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]

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]

and adding set_option autoImplicit false doesn't change the error

[Kevin Buzzard]

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]

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]

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]

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]

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

[Shubham Kumar]

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

[Shubham Kumar]

let me try that

[Kevin Buzzard]

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

[Shubham Kumar]

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]

and similarly for h2

[Ruben Van de Velde]

Well then I don't know :)

[Shubham Kumar]

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

Is the above code working fine for you?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[David Renshaw]

@Shubham Kumar what version of Lean4 are you using?

[Shubham Kumar]

David Renshaw said:

Shubham Kumar what version of Lean4 are you using?

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

[Kevin Buzzard]

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]

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

[David Renshaw]

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]

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]

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]

do I need to rebuild it?

[David Renshaw]

that's the same lean version

[Shubham Kumar]

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

[David Renshaw]

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]

I'll try again

[Shubham Kumar]

sorry again

[Shubham Kumar]

so I need to switch to nightly?

[David Renshaw]

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

[Shubham Kumar]

ok got it

[Shubham Kumar]

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]

My project root has a file named lean-toolchain containing

leanprover/lean4:nightly-2022-10-18

[David Renshaw]

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

[David Renshaw]

elan self update usually works.

[Kevin Buzzard]

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

[Shubham Kumar]

so elan self update results in no update

❯ elan self update
info: checking for self-updates

[Kevin Buzzard]

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]

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]

Is the tutorial in a Lean project?

[David Renshaw]

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

[Kevin Buzzard]

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]

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]

I don't know if I answered your question

[Shubham Kumar]

I am just learning by following the TPiL book I guess

[Shubham Kumar]

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]

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]

for reference this is what my directory looks like

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

[David Renshaw]

so your errors went away?

[Shubham Kumar]

David Renshaw said:

so your errors went away?

sadly no :see_no_evil:

[Shubham Kumar]

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

[Kevin Buzzard]

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

[Mauricio Collares]

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]

Kevin Buzzard said:

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

Yeah that's what I was thinking

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Shubham Kumar]

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]

I would strongly recommend against doing that

[Kevin Buzzard]

You risk breaking the entire project

[Kevin Buzzard]

Just create a new project

[Shubham Kumar]

Kevin Buzzard said:

Just create a new project

yeah I was going to do that

[Shubham Kumar]

and add the lean-toolchain file

[Shubham Kumar]

is that ok?

[Shubham Kumar]

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

[Kevin Buzzard]

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]

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]

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]

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]

Got it. And you did this in August?

[Shubham Kumar]

no a couple of days back

[Kevin Buzzard]

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

[Shubham Kumar]

no worries, text is a hard medium to convey context

[Shubham Kumar]

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]

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

[Kevin Buzzard]

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]

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]

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]

Apologies to Mauricio and you for misleading.

[Shubham Kumar]

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]

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]

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]

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

[Mauricio Collares]

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.