calc blocks and heterogeneous operators

Stream: mathlib4

[Rob Lewis]

@Heather Macbeth and I have been working on some teaching materials in Lean 4 and came across some surprising behavior in calc blocks:

example (n : Nat) (a : Int) : a = 22 :=
  calc
    a = 2 ^ n := sorry -- good error message
    _ = (22 : Int) := sorry

example (n : Nat) (a : Int) : a = 22 :=
  calc
    a = (37 : Int) := sorry
    _ = 2 ^ n := sorry -- bad error message
    _ = (22 : Int) := sorry

example (n : Nat) (a : Int) : a = (2 : Int) ^ n :=
  calc
    a = (37 : Int) := sorry
    _ = 2 ^ n := sorry -- bad error message

In the first example, 2 ^ n is correctly expected to be an integer, and fails because there's no HPow Nat Nat Int instance yet. But in the other examples, the calc block doesn't seem to propogate the expected type from the previous line. Is this a reasonable thing to expect it to do?

An additional wrinkle here is that with import Mathlib.Data.Int.Basic, 2 ^ n does elaborate as an Int, and the first example works -- it finds instHPow : HPow Int Nat Int. But in fact Int.instHPowIntNat has this type and is available even without the mathlib import. So I'm confused about why the presence of instHPow is able to change the type of 2 here.

[Eric Wieser]

I think it's because instHPow is a default instance, so fills in metavariables if nothing else can be found

[Heather Macbeth]

@Eric Wieser There must be some calc issue too, though, right? Because it's behaving differently in the cases marked "good error message" and "bad error message".

[Heather Macbeth]

This is now fixed with lean4#2066. Thank you @Gabriel Ebner!

[Heather Macbeth]

@Gabriel Ebner I started bumping mathlib to pick up the fix lean4#2066 to calc elaboration. I notice that Lean is now not able to elaborate calc blocks when the goal is not syntactically the same as what the calc block is proving: see
https://github.com/leanprover-community/mathlib4/compare/hrmacbeth-bump

I think this is a worthwhile tradeoff but just wanted to check that this behaviour is what you expected?

[Gabriel Ebner]

Just to be clear, it doesn't need to be syntactically identical, merely defeq. But it expects the calc block to go in the same direction as what it's proving. The motivation here was the same as your bug report, to get the right coercions in calc 42 < n := .. (imagine we're proving an inequality of integers, and n is a natural number; without this change 42 < n would be an inequality of natural numbers).

[Gabriel Ebner]

So the change was very much intentional. I'm happy to revert if it's the wrong tradeoff.

[Heather Macbeth]

Gabriel Ebner said:

Just to be clear, it doesn't need to be syntactically identical, merely defeq. But it expects the calc block to go in the same direction as what it's proving.

Could you say a little more about what you mean here? It seems to me that in examples from that branch such as the following:

theorem Commute.invOf_right [Monoid α] {a b : α} [Invertible b] (h : Commute a b) :
    Commute a (⅟ b) :=
  calc
    a * ⅟ b = ⅟ b * (b * a * ⅟ b) := by simp [mul_assoc]
    _ = ⅟ b * (a * b * ⅟ b) := by rw [h.eq]

which is broken but can be fixed by adding either show a * ⅟ b = ⅟ b * a from or rw [Commute, SemiconjBy], the calc block is proving something which is defeq but not syntactically equal to the original goal.

Maybe I don't understand what you mean by "go in the same direction as what it's proving"?

[Gabriel Ebner]

Oh, that's what you mean. Yeah, that's unfortunate. Lean thinks Commute is a relation like <, so it expects the proof to start like a = a * 1 := .... I think the easiest way out here is to say show _ = _ from calc ....

[Heather Macbeth]

I can understand this when the head symbol is a Prop-valued function of two arguments of the same type, like Commute. It's surprising to me that this also happens when the head symbol is a function of arguments of different types, like ∈ in

z ∈ ordConnectedComponent s x

or IsFixedPt in

IsFixedPt f x

I guess calc can prove "heterogeneous" relationships?

[Heather Macbeth]

I don't think this was an issue in Lean 3, right? Is there an easy explanation of what has changed since then?

[Gabriel Ebner]

Yes, calc now supports heterogenous relations.

[Heather Macbeth]

Is the change something like, Lean 3 knew that the Commute relation had no lemmas about it tagged @[trans], so it immediately unfolded Commute?

[Heather Macbeth]

For concreteness: This works in Lean 4 neither before nor after lean4#2066:

import Mathlib.Data.Int.Basic

def Foo (a b : ℕ) : Prop := (2:ℤ) ^ (a * b) = (2:ℤ) ^ (b * a)

example (n a : ℕ) : Foo a 22 :=
  calc (2:ℤ) ^ (a * 22) = (37 : ℤ) := sorry
  _ = 2 ^ n := sorry
  _ = (2:ℤ) ^ (22 * a) := sorry

with differing errors: on the 2^n before the fix, and on the (2:ℤ) ^ (a * 22) = (37 : ℤ) after the fix. Its Lean 3 analogue does work:

import data.int.basic

def Foo (a b : ℕ) : Prop := (2:ℤ) ^ (a * b) = (2:ℤ) ^ (b * a)

example (n a : ℕ) : Foo a 22 :=
calc (2:ℤ) ^ (a * 22) = (37 : ℤ) : sorry
... = 2 ^ n : sorry
... = (2:ℤ) ^ (22 * a) : sorry

[Patrick Massot]

Gabriel Ebner said:

Yes, calc now supports heterogenous relations.

Indeed I have here a proof ending with

  calc
    f z ∈ closure (f '' (V ∩ A)) := limV.mem_closure_image
      _ ⊆ closure V'             := closure_mono hV
      _ = V'                     := V'_closed.closure_eq

and it's really nice

[Patrick Massot]

Note for people who want to try: you need to add somewhere

instance : Trans (λ (x : α) (s : Set α) ↦ x ∈ s) (λ (s : Set α) (t : Set α) ↦ s ⊆ t) (λ (x : α) (s : Set α) ↦ x ∈ s) :=
⟨fun {_ _ _} hxs hst ↦ hst hxs⟩

[Heather Macbeth]

@Gabriel Ebner @Mario Carneiro I gather that lean4#2073 was fixed, in the end, by fully reverting the attepted fix to lean4#2040. Is that right? So examples like the following work on current master and will cease to work after the bump !4#1999:

import Mathlib.Data.Int.Order.Basic

example {n : ℤ} (hn : n ≤ 1) : n ^ 2 < 2 :=
  calc
    n ^ 2 ≤ 1 ^ 2 := sorry
    _ < 2 := sorry
/-
invalid 'calc' step, failed to synthesize `Trans` instance
  Trans LE.le LT.lt ?m.548
-/

[Heather Macbeth]

Actually, I'm a bit confused about where this ended up. It seems that the original issues reported do work after the bump?

[Gabriel Ebner]

Is that right?

Yes, I reverted half of the attempted fix. The one where we try to infer the type of the left-hand side of the first step from the left-hand side of the goal. Because we don't have a good way to tell what the left-hand side is, i.e., we can't tell that a is not the lhs of Commutes a b, but a is the lhs of a > b.

[Gabriel Ebner]

So examples like the following work on current master

This should still work, because n ^ 2 is going to be an integer no matter what. What would break is calc _ ≤ 1 ^2 := .. or example : 2 < n^2 := calc 2 < 2^2 := ... (Because we don't know the right type for _/2 and infer it to be a natural number.)

[Heather Macbeth]

I'm working on a bumped-to-2023-02-01 mathlib (!4#1999) and unless I'm doing something stupid, this example is failing.

[Heather Macbeth]

Is it possible that because HPow is heterogeneous, Lean doesn't know this:

Gabriel Ebner said:

n ^ 2 is going to be an integer no matter what

[Heather Macbeth]

In fact, putting a type annotation on n ^ 2 does seem to fix it, so maybe that is indeed the issue:

-- works
example {n : ℤ} (hn : n ≤ 1) : n ^ 2 < 2 :=
  calc
    (n ^ 2 : ℤ) ≤ 1 ^ 2 := sorry
    _ < 2 := sorry

[Heather Macbeth]

Now I'm confused how Lean even figures out in the example statement n ^ 2 < 2 that this is an inequality between integers. Is there some special handling here of default instances? Can that special handling be carried over to calc?