norm_cast

Stream: mathlib4

[Heather Macbeth]

I just tried porting a file with many uses of norm_cast (mathlib4#1418), and almost all of them fail. Worse, they fail very slowly!

I see this tactic was ported by @Gabriel Ebner back in February 2022 (mathlib4#191). Does the tactic need some adjustments now that we have Rat, etc? Or do we need some curation of the set of lemmas with the norm_cast attribute?

[Gabriel Ebner]

MWE:

example (n : ℤ) (h : n + 1 > 0) : ((n + 1 : ℤ) : ℚ) > 0 := by exact_mod_cast h

[Gabriel Ebner]

IntCast must be moved to std4: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Data.2ERat.2EDefs/near/316852182

[Heather Macbeth]

Is there an analogous thing for Rat which also needs to move to Std?

[Gabriel Ebner]

I don't think std4 has anything that Rat casts into, so not necessarily.

[Gabriel Ebner]

In the meantime, mathlib4#1422

[Heather Macbeth]

Just checking: is this what you think should be the permanent solution, or do you intend it as a temporary solution which will be reverted when Int.cast is moved?

[Gabriel Ebner]

It's halfway to the permanent solution (i.e. closer than the status quo).

[Heather Macbeth]

Confirming that this fixes every norm_cast use in mathlib4#1418! Thanks Gabriel!

Any thoughts on error

norm_cast: badly shaped lemma, rhs can't start with coe
  ↑(fract x)

on

@[simp, norm_cast]
theorem Rat.cast_fract (x : ℚ) : (↑(fract x) : α) = fract x := by
  simp only [fract, cast_sub, cast_coe_int, floor_cast]

[Mario Carneiro]

that looks like a coercion insertion error along the lines of lean4#1915

[Kevin Buzzard]

Yeah "badly shaped lemma" usually means "#check it and you'll see that it's not what you think it says"

[Mario Carneiro]

a trick you can use as an alternative to #check is to put your cursor in the definition name; the server will show an expected type hint in the goal view which corresponds to the theorem statement

[Henrik Böving]

The following PR also has issues with norm_cast and a single lemma not being proven by simp (I am suspecting they might be related given the lemma has multiple coes?) https://github.com/leanprover-community/mathlib4/pull/1424 can a coercion magician tell me what to do here as well?

[Heather Macbeth]

@Henrik Böving I fixed the one in my PR by opening up mathlib3 and inspecting what the coercions looked like there, and then being super explicit in mathlib4 to achieve the same statement.

[Henrik Böving]

So the mathlib3 statement is

@[norm_cast] lemma coe_fn_coe' (f : A →+[M] B) : ((f : A →[M] B) : A → B) = f := rfl

printed as ⇑↑f = ⇑f or more precisely:

mul_action_hom.has_coe_to_fun M A B = distrib_mul_action_hom.has_coe_to_fun M A B

So if I am reading this correctly one goes straight from DistribMulActionHom to function and the other takes the way over MulActionHom? Which does make sense but I'm not really sure how to be more explicit about this in Lean 4, the statement I currently have is:

theorem coe_fn_coe' (f : A →+[M] B) : ((f : A →[M] B) : A → B) = f :=
  rfl

and It makes:

f.toMulActionHom.toFun = f.toMulActionHom.toFun

I tried explicitly putting the CoeFun arrow on the right hand side to convince it not taking the step over MulActionHom but that results in no change :(