Zulip Chat Archive

Stream: mathlib4

Topic: calc blocks and heterogeneous operators


Rob Lewis (Jan 13 2023 at 20:29):

@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 (Jan 13 2023 at 22:07):

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

Heather Macbeth (Jan 13 2023 at 22:13):

@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 (Jan 28 2023 at 00:25):

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

Heather Macbeth (Jan 29 2023 at 01:43):

@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 (Jan 29 2023 at 02:06):

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 (Jan 29 2023 at 02:07):

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

Heather Macbeth (Jan 29 2023 at 02:20):

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 (Jan 29 2023 at 02:44):

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 (Jan 29 2023 at 02:48):

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 (Jan 29 2023 at 02:51):

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 (Jan 29 2023 at 02:51):

Yes, calc now supports heterogenous relations.

Heather Macbeth (Jan 29 2023 at 02:54):

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 (Jan 29 2023 at 03:16):

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 (Jan 29 2023 at 08:48):

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 (Jan 29 2023 at 08:49):

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 (Feb 02 2023 at 04:02):

@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 (Feb 02 2023 at 04:06):

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 (Feb 02 2023 at 04:10):

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 (Feb 02 2023 at 04:12):

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 (Feb 02 2023 at 04:13):

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 (Feb 02 2023 at 04:14):

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 (Feb 02 2023 at 04:18):

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 (Feb 02 2023 at 04:22):

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?


Last updated: Dec 20 2023 at 11:08 UTC