calc fails to understand the type of `1`

Stream: lean4

[Riccardo Brasca]

The following

example (x : Int) (hx : x = 1) : 1 < 2*x := calc
  1 < 2 := sorry
  _ = 2*1 := by rfl
  _ = 2*x := by rw [hx]

fails with the error

invalid 'calc' step, left-hand side is
  ↑?m.358 : Int
but previous right-hand side is
  2 * 1 : Nat

It seems that Lean thinks the first 1 is 1 : Nat (indeed Nat.one_lt_two proves the first line) and of course the calc block fails (one can put sorry at the end and the error is still there). Is this a bug? I naively assumed that, since the goal is (1 : Int) < 2*x, Lean would be able to understand that 1 means 1 : Int.

[Ruben Van de Velde]

I also feel like it's a bug, and that I've seen it mentioned before

[Riccardo Brasca]

Do you know if this is specific to calc in some sense? (I am just checking if there is already an opened issue)

[Ruben Van de Velde]

I've seen this issue mentioned in relation to calc, not anywhere else

[Riccardo Brasca]

I've opened an issue.

[Yaël Dillies]

This is definitely covered by an existing issue

[Kevin Buzzard]

My impression is that for some reason (which I think has been explained to me) calc will not unify the starting term in the calculation with the starting term it's expecting. Maybe the unification only happens after the calc block has itself been compiled?

[Riccardo Brasca]

#new members > ✔ Question on placeholder in calc (thanks @Yaël Dillies )

[Kyle Miller]

https://github.com/leanprover/lean4/blob/0f1133fe69caddf47b5d3766888da929513917af/src/Lean/Elab/Calc.lean#L151-L161

[Riccardo Brasca]

Ah, I see, thanks!

[Kyle Miller]

It would be possible with a completely different architecture for calc. Sketch:

1. Have a way to take syntax and extract an operation, a LHS, and a RHS. This would have to be user-extensible.
2. Have a way to elaborate the operations themselves.
3. Have a way to chain these operations to form the composite operation.
4. Have a way to unify this operation with the expected type to derive the LHS and RHS of the target.
5. Use the target LHS and RHS to insert type hints in the chain.
6. Elaborate all the LHSs and RHSs and proofs.
7. Assemble.

Likely this will change the way calc elaborates in ways that will break existing proofs (I can't say how, but there are too many changes where it won't happen).

The current method is to elaborate each step and its proof one at a time, with a heuristic that extracts the previous step's elaborated RHS to use it as a hint for the next step's first _. It's low-tech and makes a lot of assumptions about how relations work syntactically and term-wise, but it somehow works well enough in practice.