Debugging an issue with calc mode

Stream: lean4

[Philip Wadler]

I am having an issue with calc mode, which I hope the incredibly supportive Lean community can help me sort out.

I want to use Lean to model a simple lambda calculus. I've already done this in Agda (see plfa.inf.ed.ac.uk). Relation (.~>.) models a single reduction step, and relation (.~>>.) is its transitive closure.

I declare the relation between (.~>.) and (.~>>.) as follows.

instance : Trans (.~>.  : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>.  : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>>. : Γ ⊢ A → Γ ⊢ A → Type) where
  trans := one_one

instance : Trans (.~>.  : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>>. : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>>. : Γ ⊢ A → Γ ⊢ A → Type) where
  trans := one_many

instance : Trans (.~>>. : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>.  : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>>. : Γ ⊢ A → Γ ⊢ A → Type) where
  trans := many_one

instance : Trans (.~>>. : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>>. : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>>. : Γ ⊢ A → Γ ⊢ A → Type) where
  trans := many_manyinstance : Trans (.~>.  : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>.  : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>>. : Γ ⊢ A → Γ ⊢ A → Type) where
  trans := one_one

instance : Trans (.~>.  : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>>. : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>>. : Γ ⊢ A → Γ ⊢ A → Type) where
  trans := one_many

instance : Trans (.~>>. : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>.  : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>>. : Γ ⊢ A → Γ ⊢ A → Type) where
  trans := many_one

instance : Trans (.~>>. : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>>. : Γ ⊢ A → Γ ⊢ A → Type)
                 (.~>>. : Γ ⊢ A → Γ ⊢ A → Type) where
  trans := many_many

Further, I have succeeded in using Lean to demonstrate individual reduction steps.

example : two ~> (ƛ (suc_c ⬝ (suc_c ⬝ # Z))) ⬝ 0
    := xi_app_1 (beta Value.lambda)

example : ((ƛ (suc_c ⬝ (suc_c ⬝ # Z))) ⬝ 0 : ∅ ⊢ ℕ) ~> suc_c ⬝ (suc_c ⬝ 0)
    := beta Value.zero

example : (suc_c ⬝ (suc_c ⬝ 0) : ∅ ⊢ ℕ) ~> suc_c ⬝ 1
    := xi_app_2 Value.lambda (beta Value.zero)

example : (suc_c ⬝ 1 : ∅ ⊢ ℕ) ~> 2
    := beta (Value.succ Value.zero)

However, if I try to combine them with calc then Lean complains.

example : two ~>> 2 :=
  calc
    two_c ⬝ suc_c ⬝ 0
      ~> (ƛ (suc_c ⬝ (suc_c ⬝ # Z))) ⬝ 0  := xi_app_1 (beta Value.lambda)
    _ ~> (suc_c ⬝ (suc_c ⬝ 0))            := beta Value.zero
    _ ~> suc_c ⬝ 1                       := xi_app_2 Value.lambda (beta Value.zero)
    _ ~> 2                              := beta (Value.succ Value.zero)

It complains about beta Value.lambda in the first line and beta Value.zero in the second line, even though exactly the same individual reductions are accepted in the examples above. The error messages complain that it is given one thing when it expects another, but the given and expected things are in fact definitionally equal.

The full file from which the above is excerpted is at https://github.com/plfa/plfl/blob/main/src/Typesig.lean.

Any help would be greatly appreciated.

[Mauricio Collares]

Replacing two_c ⬝ suc_c ⬝ 0 by two in your calc example makes it compile, but Lean seems happy to accept

example : two = two_c ⬝ suc_c ⬝ 0 := rfl

That's interesting.

[Philip Wadler]

Thanks, Mauricio. That is indeed interesting.

On my machine, when I make the change you suggest it stops complaining about beta Value.zero but it still complains about beta Value.lambda. (I'm running Lean4 v0.0.113 on Visual Studio 1.73.1 on a 2021 iMac.)

Should I regard this as a bug in Lean? Will it go away? Is there a workaround in the meantime?

[Kevin Buzzard]

I would definitely consider updating to a modern Lean (it's on v4.3.something right now) to see if things work any better.

[Mauricio Collares]

v0.0.113 is the VS Code extension version, but you can get the lean version by typing #eval Lean.versionString on a new line in any open Lean file

[Mauricio Collares]

I noticed the PLFL repository is not a Lake project, which is the preferred way of setting up projects these days. The reason I mention this here is because Lake projects contain a lean-toolchain file pinning the project to a particular Lean version, which is useful for reproducibility. Without that, you get whatever default version elan gives you (which you can see with elan show).

[Philip Wadler]

Lean version string tells me I am running "4.0.0-nightly-2022-08-05".

I updated my Lean version earlier today by running elan toolchain install stable (which told me it fetched Lean 4.2 despite the string above). What should I do to get a more up to date version running? Will Visual Studio immediately pick up on the update, or will I need to inform it somehow?

Many thanks for your help!

[Mauricio Collares]

Currently you're not using a project (which means imports probably don't work!), and if you want to keep it that way you can type elan default stable, after which VS Code will probably pick up the new version.

lake new PLFL is the command you'd use to create a new project, and then you can edit the lean-toolchain file to use a new version, which has the advantage of ensuring users of your project will also run your code with the same Lean version.

[Philip Wadler]

Running elan show gives me the following.

rambla$ elan show
installed toolchains
--------------------

stable
leanprover/lean4:nightly (default)
leanprover/lean4:stable

active toolchain
----------------

leanprover/lean4:nightly (default)
Lean (version 4.0.0-nightly-2022-08-05, commit fdaae2059410, Release)

That suggests I'm running the nightly version, which should be more up to date than v4.3.3.something, so I don't know why it's numbered 4.0.0. Quite possibly I have this all wrong, in which case please let me know what I should do instead.

[Mauricio Collares]

You're running _a_ nightly version, but it doesn't get updated automatically (elan update nightly does that)

[Philip Wadler]

@Mauricio Collares Thank you for the suggestion about lake.

[Mauricio Collares]

Stable versions are quite fresh these days, so running on nightly is no longer as essential as it was a few months ago. You can switch your default channel to stable by running elan default stable if you prefer, but it's not too important.

[Mauricio Collares]

I tried updating your repository to the newest Lean version and I found a funny calc behavior which may be the same one. The following code fails with "type mismatch; rfl has type 3 + 9 = 3 + 9 : Prop but is expected to have type 3 + 9 = 12 : Prop":

example : 3 + 9 = 12 :=
  calc
    3 + 9
    _ = 12 := rfl

But this one succeeds:

example : 3 + 9 = 12 :=
  calc
    3 + 9
    _ = 12 := by rfl

[Richard Copley]

rfl the tactic can be a little sophisticated. rfl the term just means x=x. Check their respective docstrings! Might be fun to think about why by exact rfl does work there, too.

[Mauricio Collares]

Another calc-related funny thing from the repo:

open Nat

inductive le : Nat → Nat → Prop
| refl : ∀ {m}, le m m
| step : ∀ {m n}, le m n → le m (succ n)

instance : LE Nat where
  le := le

example : 2 ≤ 4 := le.step (le.step le.refl) -- succeeds

example : 2 ≤ 4 :=
  calc
    2 ≤ 4 := le.step (le.step le.refl) -- fails

[Mauricio Collares]

Richard Copley said:

rfl the tactic can be a little sophisticated. rfl the term just means x=x. Check their respective docstrings! Might be fun to think about why by exact rfl does work there, too.

I don't think that's the issue. example : 3 + 9 = 12 := rfl outside calc works fine (as it should, since the two sides are defeq).

[Mauricio Collares]

I'm sure someone will come here soon saying the calc tactic implementation is missing a whnfR, instantiateMVars or whatever

[Philip Wadler]

Thank you for the suggestions. I've updated to stable-4.2.0, but am still seeing the same issue. Interestingly, the update also broke my first single step reduction example, which worked previously. (Same thing happens if I switch to nightly-4.4.0.)

[Mauricio Collares]

Whoops. Well, you can go back to the previous nightly with elan default leanprover/lean4:nightly-2022-08-05, but indeed I see the same error here now. I don't understand why my editor didn't show an error before.

[Mauricio Collares]

I will submit a PR creating the project boilerplate in the hopes of avoiding these sorts of reproducibility issues in the future. No need to accept it if you don't feel like it fits the project.

[Philip Wadler]

@Richard Copley Thanks for the minimal example. How do I proceed to get this fixed? Is the first step just to wait and see if someone offers the answer you expect?

@Mauricio Collares Thank you!

[Richard Copley]

• Mauricio's example?
• I don't know, but maybe somebody who does will chime in?

[Mauricio Collares]

I will file a bug

[Mauricio Collares]

Philip Wadler said:

Thank you for the suggestions. I've updated to stable-4.2.0, but am still seeing the same issue. Interestingly, the update also broke my first single step reduction example, which worked previously. (Same thing happens if I switch to nightly-4.4.0.)

Filed lean4#2913 for the minimized issue. You hit this issue in other PLFL files, but I don't think the minimized issue is the same as the calc problem you originally reported, since it occurs outside calc mode in the most recent Lean version.

Would be good to understand why the single-step reduction example fails in the most recent Lean version (it seems like there are some metavars in the error output).

[Mauricio Collares]

@Philip Wadler Weirdly I see the same issue in the single-step reduction example (xi_app_1 (beta Value.lambda)) in your file even using nightly-2022-08-05.

[Philip Wadler]

@Mauricio Collares Thanks for filing a bug report. Regarding the example failing under nightly-2022-08-05 when it didn't earlier, I wonder if this is a heisenbug. That would explain why you didn't see an error at one point and did see one later. Anyhow, it certainly should work and the problem is not related to calc: is there another bug report to file here?

[Mauricio Collares]

Most likely, but extracting a #mwe here will probably require more knowledge of the example than I have (I've read PLFA, but it's been a while!), and I guess will take longer too.

[Philip Wadler]

Indeed, extracting a #mwe will be difficult. (I'm pretty familiar with the problem, and I have no idea how to go about doing so.) Is it possible to just declare the current example an #mwe? I'm happy to remove extraneous code, although even after doing so it will be quite large.

[Mauricio Collares]

Ah, wait, this is related to the problem in the other thread! two_c uses the # 0 notation which doesn't work.

[Mauricio Collares]

So then this is just the calc problem, I think. Replacing two_c ⬝ suc_c ⬝ 0 by two in the calc block (and # 0 by # Z in the definition of two_c) makes it work.

[Kyle Miller]

Mauricio Collares said:

... But this one succeeds: ...

If you look at the types, you can see for example @Eq ?m.239 (3 + 9) 12, indicating it hasn't decided on the types of the numerals yet. Numerals rely on a @[default_instance] to eventually get specialized to Nat if no better idea comes along first.

Giving a type ascription lets it proceed:

example : 3 + 9 = 12 :=
  calc
    (3 + 9 : Nat)
    _ = 12 := rfl

When you did by rfl, what happened is that this allows the rfl to be deferred until later (by exact rfl works too for this -- there's nothing special about the rfl tactic in this case).

[Mauricio Collares]

Is the other example in lean4#2913 (the 2 ≤ 4 one) also expected to fail? I can close the issue if so. The only reason I opened it was because it was a regression, but maybe it was never supposed to work in the first place.

[Mauricio Collares]

I guess my question is: It works if I give a type ascription inside the calc mode, but not if I include a type ascription in the goal. Should calc be able to use the expected types to help figure out the types of the numerals inside it?

[Kyle Miller]

I think at least for =, the fact calc fails is consistent with this failing:

example : True := by
  have := (rfl : 3 + 8 = 12)
  /-
  type mismatch
    rfl
  has type
    3 + 8 = 3 + 8 : Prop
  but is expected to have type
    3 + 8 = 12 : Prop
  -/

[Kyle Miller]

It's too bad you can't get it to succeed with (rfl (α := Nat) : 3 + 8 = 12)...

[Kyle Miller]

In your example : 2 ≤ 4 := le.step (le.step le.refl) example, this succeeds because default instances are chosen by the time the body is elaborated.

[Kyle Miller]

@Philip Wadler I'm not sure where you are right now with needing a workaround, but I suspect you can replace := ... with by exact ... where you're having errors in calc.

[Kyle Miller]

Never mind, that doesn't work.

[Kyle Miller]

Anyway, here's a style you could try that helps keep different proofs in a calc block from interacting with each other:

example : two ~>> 2 := by
  calc
    two_c ⬝ suc_c ⬝ 0
      ~> (ƛ (suc_c ⬝ (suc_c ⬝ # Z))) ⬝ 0  := ?_
    _ ~> (suc_c ⬝ (suc_c ⬝ 0))            := ?_
    _ ~> suc_c ⬝ 1                       := ?_
    _ ~> 2                              := ?_
  · exact xi_app_1 (beta Value.lambda) -- error here
  · exact beta Value.zero
  · exact xi_app_2 Value.lambda (beta Value.zero)
  · exact beta (Value.succ Value.zero)

[Philip Wadler]

Aha, so this explains a lot. I had replaced # S Z and # Z by # 1 and # 0 where the original definitions did not report an error, so I thought it made no difference. But it _did_ make a difference further down, in the examples to test single reduction steps. This explains why the bug came and went, because I made those changes between when it worked and when it started to display the bug.

Further, if I add a type ascription to the first line then calc now works.

example : two ~>> 2 :=
  calc
    (two_c ⬝ suc_c ⬝ 0 : ∅ ⊢ ℕ)
      ~> (ƛ (suc_c ⬝ (suc_c ⬝ # Z))) ⬝ 0  := xi_app_1 (beta Value.lambda)
    _ ~> (suc_c ⬝ (suc_c ⬝ 0))            := beta Value.zero
    _ ~> suc_c ⬝ 1                       := xi_app_2 Value.lambda (beta Value.zero)
    _ ~> 2                              := beta (Value.succ Value.zero)

That also explains why replacing two_c ⬝ suc_c ⬝ 0 by two makes calc work, because two is equal to the former but provides additional information about the type.

So it works, and no need for a bug report. Yay!

Of course it would be nice if the type information from the signature of the example could propagate into the calc, but I guess that's a deeper matter.

[Philip Wadler]

@Mauricio Collares Adding a type ascription to the 2 ≤ 4 example fixes that problem as well.

Thank you everyone for the help! The Lean community is fantastic.

[Mauricio Collares]

I noticed that Leo added a workaround to the show tactic (https://github.com/leanprover/lean4/commit/474f1a4d39bac6310fbd47aa4545d6c15fb14d53) a day after the original change (which was a fix for lean4#2011). Hopefully the calc tactic can use a similar one to reduce the number of needed ascriptions.

[Kyle Miller]

@Mauricio Collares It's been pointed out to me that my arithmetic was bad, and that actually this works:

example : True := by
  have := (rfl : 3 + 9 = 12)
  sorry

That suggests to me that the calc equivalent should work too.