elaboration and coercions

[kbuzzard]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Here's an example of a common idiom in mathlib used when writing coercion lemmas. Let me start with Lean 3. Assume α is a type with an instance of has_inv (a notational typeclass for ⁻¹), and let's assume we extend ⁻¹ to option α by none⁻¹ = none. A lemma called coe_inv in Lean 3 would be written like this:

example (a : α) : ((a⁻¹ : α) : option α) = a⁻¹ :=

In Lean 3 this is elaborated "from the outside in" as follows. The left hand side clearly has type option α, so the inv on the right hand side must be about option α, so a is supposed to have type option α, so the coercion kicks in at this point, and the type of the example above is ↑(a⁻¹) = (↑a)⁻¹. In Lean 4 something different happens:

class Inv (α : Type u) where
  /-- Invert an element of α. -/
  inv : α → α

postfix:max "⁻¹" => Inv.inv

instance (α : Type u) [Inv α] : Inv (Option α) :=
  ⟨λ a => match a with
     | Option.none => Option.none
     | Option.some x => Option.some x⁻¹
  ⟩

theorem coe_inv [Inv α] (a : α) : ((a⁻¹ : α) : Option α) = a⁻¹ :=
  rfl

#check coe_inv -- some a⁻¹ = some a⁻¹

The theorem as it stands is elaborated as a syntactic tautology in Lean 4. A fix is

theorem coe_inv [Inv α] (a : α) : ((a⁻¹ : α) : Option α) = (↑a)⁻¹ :=
  rfl

which elaborates as expected and, to be honest, is more readable.

In practice of course I noticed this because of the syntactic tautology linter, which will probably flag all such lemmas where this phenomenon occurs; I'm opening an issue simply to note this change of behaviour because it's going to come up a lot during the port of mathlib (and probably in every case will be caught by the syntactic tautology linter, I guess...).

Versions

Lean (version 4.0.0, commit 50fc4a6, Release)

[kbuzzard]

This is still coming up and porters are still being confused by it (e.g. here). Another time it shows up is with pow:

variable (α β : Type) [Coe α β] [HPow α Nat α] [HPow β Nat β]

-- `coe_pow` is ↑(x^n)=(↑x)^n in Lean 3 and is often seen in mathlib3,
-- and is being auto-ported to the below, but the below is a syntactic tautology in Lean 4
theorem coe_pow (x : α) (n : Nat) : ((x ^ n : α) : β) = x ^ n := rfl -- `↑(x ^ n) = ↑(x ^ n)`

-- `coe_pow'` and `coe_pow''` are ↑(x^n)=(↑x)^n in Lean 4, which are what we want.
theorem coe_pow' (x : α) (n : Nat) : ↑(x ^ n) = (x : β) ^ n := sorry
theorem coe_pow'' (x : α) (n : Nat) : (x ^ n : β) = (x : β) ^ n := sorry

It would be good if it could be clarified whether this change from Lean 3 to Lean 4 is (a) unintentional and should be fixed in Lean 4, or (b) will not be fixed in Lean 4, so I can open an issue in the porting program to see if anything can be done at that end.

[Kha]

Right, this is essentially by design. Your original example ((a⁻¹ : α) : option α) = a⁻¹ only makes sense under Lean 3's strict left-to-right elaboration. This is not true anymore in Lean 4: both sides of the equality are elaborated essentially independently, then we figure out whether coercions have to be inserted to make their types equal, which in this case means that we simply apply the explicit coercion from the LHS to the RHS as well. So yes, the double annotation should instead be distributed to both sides.

[digama0]

From a user perspective, this seems to be a definite regression. Here's an idea for how to fix the coercions without breaking symmetry: When elaborating a binop% tree like e1 + e2 + e3, first elaborate all the leaves with no expected type. If all the resulting expressions e1, e2, e3 have the same type or otherwise can fit together without inserting coercions between these expressions and the sum, then do that. Otherwise, for each expression which did not match its expected type, re-elaborate the expression with the expected type. This will either end up inserting a coercion somewhere inside e1, or at the root, or give a sensible error message if it's actually a type error. Examples:

variable (n : Nat) (z : Int)

-- these work as expected:
example : Int := n + z -- ↑n + z
example : Int := z + n -- z + ↑n
example : Int := n + n + z -- ↑n + ↑n + z
example : Int := z + n + n -- z + ↑n + ↑n

-- but now we can also push through non-binop% nodes:
example : Int := z + id (n + n) -- was z + ↑(id (n + n)), now z + id (↑n + ↑n)
example : Int := id (n + n) + z -- was ↑(id (n + n)) + z, now id (↑n + ↑n) + z

(Not sure how you want to approach the implementation here. I have a general idea of how to do this and can try my hand at implementing it, or let others do it.)

[kbuzzard]

Here is a far nastier example, which I don't actually know how to fix right now:

import Std.Data.Rat.Basic

example (n : Nat) (i : Rat) : i = (4*(n*(n-1)/2)^3-(n*(n-1)/2)^2)/3 := sorry
-- failed to synthesize instance `HPow Nat Nat Rat`

In Lean 3 this would elaborate fine; the RHS was expecting to be a rational and so all the coercions happened automatically. Here I don't know how to make this parse in Lean 4 without adding in many explicit coercions/casts.

Oh, Eric Wieser pointed out that my imports are not enough to actually ever make this work: so this is a more accurate MWE:

import Mathlib.Data.Rat.Basic

example (n : ℕ) : ℚ := (4*(n*(n-1)/2)^3-(n*(n-1)/2)^2)/3
/-
failed to synthesize instance
  HMul ℚ ℕ (?m.812 n)

failed to synthesize instance
  HDiv ℕ ℚ ℚ
-/

[siddhartha-gadgil]

A brute force solution to the above example (which can be extended) is the following. I tried using instances of Coe but that somehow did not work.

import Mathlib

namespace lean3
scoped instance (priority := high) : HDiv ℕ ℚ ℚ := ⟨fun a b => a * b⁻¹⟩   
scoped instance (priority := high) : HMul ℚ ℕ  ℚ := ⟨fun a b => a * b⟩   
scoped instance (priority := high) : HSub ℚ ℕ  ℚ := ⟨fun a b => a - b⟩   
end lean3

open lean3

example (n : ℕ) : ℚ := (4*(n*(n-1)/2)^3-(n*(n-1)/2)^2)/3

[kbuzzard]

Oh this doesn't quite work! The division is still natural division, which is precisely what I want to avoid.

[siddhartha-gadgil]

Not a solution, but another thing that helps is to give higher priority to the homogeneous operations.

infix:71 (priority := high) " + " => Mul.mul
infix:66 (priority := high) " - " => Sub.sub
infix:71 (priority := high) " / " => Div.div
infix:66 (priority := high) " + " => Add.add

[siddhartha-gadgil]

Another slight improvement - some duplications can be avoided by adding instances of Coe in

instance : Coe ℕ ℚ := ⟨fun n : ℕ   ↦ (n : ℚ)⟩
instance : Coe ℕ ℤ  := ⟨fun n : ℕ   ↦ (n : ℤ )⟩

[siddhartha-gadgil]

Some code for this posted on Zulip

[kbuzzard]

Just to remark that

import Mathlib.Data.Rat.Basic

example (n : ℕ) : ℚ := (4*(n*(n-1)/2)^3-(n*(n-1)/2)^2)/3

works fine now. This issue was originally opened because we had just begun the port and the autoporter was getting these things wrong; this is also no longer really relevant (at least to me). Maybe we can close this issue, unless @digama0 is still concerned about the points raised above.