convert failures

Stream: mathlib4

[Heather Macbeth]

There are a lot of broken converts turning up in the port of mathlib4#1304. (Search for

porting note: broken `convert

). I haven't made a self-contained example, but I have a conjecture: maybe in the mathlib3 version convert got to use the expected type to help it elaborate the expression proposed for conversion, and in the mathlib4 version it doesn't. Does this sound plausible? If so, can it be changed?

I noticed a discussion on the lean4 repo this morning about show, which seems like it could be similar:
https://github.com/leanprover/lean4/commit/fedf235cba35ed8bf6bf571cf38e6d8536b904ac#r95249776
https://github.com/leanprover/lean4/commit/474f1a4d39bac6310fbd47aa4545d6c15fb14d53

[Kevin Buzzard]

Prompted by this I came back to this message to have a look (I had starred Heather's message but I have over 1000 stars now so my system is broken).

The first porting note about a failing convert is with nat.floor_pos. In Lean 3 it's

lemma floor_pos : 0 < ⌊a⌋₊ ↔ 1 ≤ a :=
by { convert le_floor_iff' nat.one_ne_zero, exact cast_one.symm }

and that proof doesn't work in mathlib4, one gets the following complaint:

typeclass instance problem is stuck, it is often due to metavariables
  FloorSemiring ?m.36098

Lean refuses to guess a (and hence alpha). But you can tell it that a = a and then things work fine:

theorem floor_pos : 0 < ⌊a⌋₊ ↔ 1 ≤ a :=
by { convert le_floor_iff' (a := a) Nat.one_ne_zero; exact cast_one.symm }

The second broken convert is Porting note: broken `convert floor_add_nat ha 1` but actually the convert works fine for me:

theorem floor_add_one (ha : 0 ≤ a) : ⌊a + 1⌋₊ = ⌊a⌋₊ + 1 :=
by { convert floor_add_nat ha 1; exact cast_one.symm }

The third one also works now. The fourth one again needs more hints:

theorem floor_pos : 0 < ⌊a⌋ ↔ 1 ≤ a :=
by { convert le_floor (a := a) (z := 1); exact cast_one.symm }

It seems to me that convert is "less agressive" in mathlib4. Lean has to guess a term of a type, and prove that this type is a floor_ring or whatever; in mathlib3 Lean would look at what the term was in the expression it's supposed to match and say "Oh OK I'll just use that". It seems that mathlib4 is more reluctant to do that. Here is a minimised example:

-- lean 3
import tactic

theorem foo {α : Type} [comm_ring α] {a : α} : a = a := rfl

example {α : Type} [comm_ring α] {a : α} : a = a :=
begin
  convert foo, -- no error
  -- ⊢ comm_ring α
  apply_instance
end

-- lean 4
import Mathlib

theorem foo {α : Type} [CommRing α] {a : α} : a = a := rfl

example {α : Type} [CommRing α] {a : α} : a = a := by
  convert foo -- error

/-
typeclass instance problem is stuck, it is often due to metavariables
  CommRing ?m.41
-/

[Kevin Buzzard]

mathlib4 is giving up on CommRing ?m.41 whereas mathlib3 figures it will just ask the user to solve that goal later on after it's figured out ?m.41.

[Joachim Breitner]

I am facing a by convert refl that works in mathlib3 but not in mathlib4 (https://github.com/leanprover-community/mathlib4/pull/2151). Looking at the mathlib3 proof does not help me much, but it somehow seems to be related to heq vs. eq.
Any hints?

[Reid Barton]

I assume just rfl doesn't work for some reason?

[Joachim Breitner]

I think I found it, rfl works after I removed a redundant DecidableDec constriant from the lemma. :shrug:

[Reid Barton]

I think that constraint was there for a reason, but I'm not really into this DecidableEq masochism stuff so I don't know how you're supposed to do it in Lean 4.

[Yaël Dillies]

Probably a missing subsingleton instance? Can you wrap the mathlib3 convert in a show_term?

[Eric Rodriguez]

convert doesn't do singletons in lean4 as far as I've seen

[Joachim Breitner]

I #print’ed the resulting term, but couldn’t make sense of it.