not a soundness issue

Stream: lean4

[Adam Kurkiewicz]

I have a soundness issue in my installation of lean:

Lake version 5.0.0-be6c489 (Lean version 4.9.0-rc1)

Specifically, I can prove False like this:

import Mathlib.Data.Nat.ModEq
import Mathlib.Tactic

lemma mod_3_add_3_under_exponent (m n : ℕ ) : (2 * n ≡ 0 [MOD 3]) := by
  cases n with
  | zero =>
    rfl
  | succ n =>
    have IH := @mod_3_add_3_under_exponent m n
    have first_step : (m + 3) ^ (n + 1) = (m + 3) ^ n * (m + 3) := by ring
    have third_step : (m + 3) ≡ m [MOD 3] := Nat.add_modEq_right
    have fourth_step : (m ^ n * m) = m ^ (n + 1) := by ring
    calc (m + 3) ^ (n + 1) ≡ (m + 3) ^ n * (m + 3) [MOD 3] := by rw[first_step]
    _ ≡  (m ^ n * (m + 3)) [MOD 3] := Nat.ModEq.mul IH rfl
    _ ≡  (m ^ n * m ) [MOD 3] := Nat.ModEq.mul rfl third_step
    _ ≡  m ^ (n + 1) [MOD 3] := by rw[fourth_step]

#check mod_3_add_3_under_exponent

lemma soundness_issue : False := by
  have A : 2 * 1 ≡ 0 [MOD 3] := mod_3_add_3_under_exponent 0 1
  contradiction

#check soundness_issue

I've checked in the code to github if looking at lake-manifest.json would be helpful.

I've also checked with the web browser version of lean live, and it is not affected (the proof is appropriately rejected). So it looks like I've either done something wrong or there's a bug in the version of Lean that I'm using. But I'm struggling to work out which one it is.

[Ruben Van de Velde]

The live viewers seems to be on 4.9.0-rc2, if you want to try that

[Adam Kurkiewicz]

You mean try the live viewer? Or try to install 4.9.0-rc2 locally? I've tried the former (link in the original message), but for the latter it will take a long time for Mathlib to compile, right? Like a few hours?

[Ruben Van de Velde]

If you update to current mathlib master, you can use the cache (mathlib moved to rc2 yesterday)

[Adam Kurkiewicz]

OK I'll try that. Just to confirm, I have to modify lake-manifest.json and run lake exe cache get and then lake build?

[Adam Kurkiewicz]

Hold on, the file is lean-toolchain, right?

[Adam Kurkiewicz]

I'm pinned to a particular version of mathlib. Hopefully this will work:

{"url": "https://github.com/leanprover-community/mathlib4",
   "type": "git",
   "subDir": null,
   "rev": "303e71911e1c040ac1278de13fc2032102888a6e",
   "name": "mathlib",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
   "inherited": false,
   "configFile": "lakefile.lean"},

[Ruben Van de Velde]

Try running lake update mathlib, probably this will update lean-toolchain as well

[Adam Kurkiewicz]

OK I'll do that.

[Ruben Van de Velde]

303e71911e1c040ac1278de13fc2032102888a6e is too old

[Adam Kurkiewicz]

Well, that's what Compfiles uses

[Adam Kurkiewicz]

Hmm, this might break everything, right?

[Adam Kurkiewicz]

That's OK, I copied the whole directory

[Kyle Miller]

Thankfully it's not a soundness issue, but there's definitely an issue here. One of the tactics seems to be creating sorry without reporting it.

import Mathlib.Data.Nat.ModEq
import Mathlib.Tactic

lemma mod_3_add_3_under_exponent (m n : ℕ ) : (2 * n ≡ 0 [MOD 3]) := by
  cases n with
  | zero =>
    rfl
  | succ n =>
    have IH := @mod_3_add_3_under_exponent m n
    have first_step : (m + 3) ^ (n + 1) = (m + 3) ^ n * (m + 3) := by ring
    have third_step : (m + 3) ≡ m [MOD 3] := Nat.add_modEq_right
    have fourth_step : (m ^ n * m) = m ^ (n + 1) := by ring
    calc (m + 3) ^ (n + 1) ≡ (m + 3) ^ n * (m + 3) [MOD 3] := by rw[first_step]
    _ ≡  (m ^ n * (m + 3)) [MOD 3] := Nat.ModEq.mul IH rfl
    _ ≡  (m ^ n * m ) [MOD 3] := Nat.ModEq.mul rfl third_step
    _ ≡  m ^ (n + 1) [MOD 3] := by rw[fourth_step]

#print axioms mod_3_add_3_under_exponent
-- 'mod_3_add_3_under_exponent' depends on axioms: [sorryAx]

[Adam Kurkiewicz]

I'm currently re-running with an up-to-date mathlib, so let's see

[Adam Kurkiewicz]

So @Kyle Miller you can reproduce this? Which version of Lean/Mathlib are you at?

[Kyle Miller]

Yeah, I just reproduced it with a recent mathlib, 4.9.0-rc1

[Adam Kurkiewicz]

OK, so whatever this was, updating Mathlib fixed it. Thank @Ruben Van de Velde!

[Kyle Miller]

Oh, is this something that's fixed in 4.9.0-rc2 then?

[Adam Kurkiewicz]

The problem no longer affects Lake version 5.0.0-7ed9b73 (Lean version 4.9.0-rc2)

[Adam Kurkiewicz]

It fails to typecheck, yes.

[Adam Kurkiewicz]

I mean, I still get

'mod_3_add_3_under_exponent' depends on axioms: [sorryAx]

But at least it fails to typecheck in line 13:

soundness_issue.lean:13:4

'calc' tactic failed, has type
  (m + 3) ^ (n + 1) ≡ m ^ (n + 1) [MOD 3]
but it is expected to have type
  2 * (n + 1) ≡ 0 [MOD 3]

[Adam Kurkiewicz]

Maybe there's still a way to prove False, I'm not sure. But at least this code is not it :)

[Kyle Miller]

I guess somehow it's fixed because of lean4#4335, which seems plausible because the haves preceding calc are one of the ways to trigger the issue.

[Adam Kurkiewicz]

Oh I'm not surprised Heather reported it, she loves her calcs :). I've done her course, it's full of them.

[Adam Kurkiewicz]

I'm happy to leave it here then if you are.

[Kyle Miller]

It looks like everything's now as it should be :-)