pi.nat_apply

Stream: general

[Johan Commelin]

This is extremely slow for my

lemma pi.nat_apply {α β : Type*} [has_zero β] [has_one β] [has_add β] :
  ∀ (n : ℕ) (a : α), (n : α → β) a = n
| 0     a := rfl
| (n+1) a := show (n : α → β) a + (1 : α → β) a = n + 1, by { rw pi.nat_apply, refl }

I don't know why

[Johan Commelin]

import algebra.group.pi
import data.nat.cast

-- move this
lemma pi.nat_apply {α β : Type*} [has_zero β] [has_one β] [has_add β] :
  ∀ (n : ℕ) (a : α), (n : α → β) a = n
| 0     a := rfl
| (n+1) a := show (n : α → β) a + (1 : α → β) a = n + 1, by { rw pi.nat_apply, refl }
.

-- move this
@[simp] lemma pi.coe_nat {α β : Type*} [has_zero β] [has_one β] [has_add β] (n : ℕ) :
  (n : α → β) = λ _, n :=
by { ext, rw pi.nat_apply }

[Johan Commelin]

still slow :head_bandage: :turtle:

[Floris van Doorn]

workaround:

lemma pi.nat_apply {α β : Type*} [has_zero β] [has_one β] [has_add β] (n : ℕ) (a : α) :
  (n : α → β) a = n :=
by { induction n with n ih, refl, simp [ih] }

[Floris van Doorn]

Here is the culprit:

import algebra.group.pi
import data.nat.cast

local attribute [-instance] widget.html.to_string_coe

lemma pi.nat_apply {α β : Type*} [has_zero β] [has_one β] [has_add β] :
  ∀ (n : ℕ) (a : α), (n : α → β) a = n
| 0     a := rfl
| (n+1) a := show (n : α → β) a + (1 : α → β) a = n + 1, by { rw pi.nat_apply, refl }

[Floris van Doorn]

It is caught by the linter, but it's in core :(

[Floris van Doorn]

lean#544

[Johan Commelin]

ooh, I hadn't expected widgets to throw sand into the gears here

[Gabriel Ebner]

Wait, but widget.html.to_string_coe is a meta instance. How does it make a difference here?

[Floris van Doorn]

Hmm... That is a good point, type-class inference should ignore this instance since it is meta. However, it does try it, and then spirals out of control:

[class_instances] (2) ?x_67 : has_coe ℕ ?x_66 := @widget.html.to_string_coe ?x_105 ?x_106 ?x_107

Maybe there is a bug/inefficiency in type-class inference that it is also trying meta instances?