rw fails

Stream: general

[Kevin Buzzard]

What have I done wrong here?

import data.real.basic

class real.nat (r : ℝ) :=
(n : ℕ)
(pf : r = ↑n)

class real.rat (r : ℝ) :=
(q : ℚ)
(pf : r = ↑q)

set_option trace.check true
instance real.rat_of_nat (r : ℝ) [H : real.nat r] : real.rat r :=
⟨(H.n : ℚ),begin
  have H2 := H.pf,
  rw H2, -- fails
/-
  rewrite tactic failed, motive is not type correct
nested exception message:
check failed, application type mismatch (use 'set_option trace.check true' for additional details)
state:
r : ℝ,
H : real.nat r,
H2 : r = ↑(nat.n r)
⊢ r = ↑↑(nat.n r)
-/
  sorry
end⟩

Setting trace.check to true tells me

[check] application type mismatch at
  nat.n _a
argument type
  real.nat r
expected type
  real.nat _a

[Kenny Lau]

well the second r is also being rewrited

[Chris Hughes]

H is an implicit argument in the rhs of H2, and it will have the wrong type after the r on the rhs is rewritten.

[Kenny Lau]

import data.real.basic

class real.nat (r : ℝ) :=
(n : ℕ)
(pf : r = ↑n)

class real.rat (r : ℝ) :=
(q : ℚ)
(pf : r = ↑q)

instance real.rat_of_nat (r : ℝ) [H : real.nat r] : real.rat r :=
⟨H.n, by rw rat.cast_coe_nat H.n; exact H.pf⟩

[Johan Commelin]

Are there simp-lemmas that reduce these double coercions?

[Kenny Lau]

sure

[Johan Commelin]

So, by simpa using H.pf?

[Kenny Lau]

je kant het proberen... toch

[Kevin Buzzard]

I was surprised rw failed here:

import algebra.group_power

#check @is_semiring_hom.map_pow
/-
  ∀ {α : Type u_1} {β : Type u_2} [_inst_1 : semiring α]
  [_inst_2 : semiring β] (f : α → β)
  [_inst_3 : is_semiring_hom f] (x : α) (n : ℕ), f (x ^ n) = f x ^ n
  -/

example {A B : Type*} [comm_ring A] [comm_ring B]
  (f : A → B) [is_ring_hom f] (a : A) (n : ℕ) :
f (a ^ n) = 37 :=
begin
--  rw is_semiring_hom.map_pow, -- fails
  rw is_semiring_hom.map_pow _ a n, -- even this fails
  /-
  rewrite tactic failed, did not find instance of the
  pattern in the target expression
  ?m_1 (a ^ n)

  ⊢ f (a ^ n) = 37
  -/
  rw is_semiring_hom.map_pow f, -- works
  sorry
end

I am used to cutting corners like that. What's the reason it fails?

[Kenny Lau]

higher order unification

[Kevin Buzzard]

no kidding

[Kenny Lau]

yet another argument for bundling everything

[Patrick Massot]

(deleted)

[Kevin Buzzard]

So what does Lean need to solve when trying to do this rewrite exactly?

[Kevin Buzzard]

yet another argument for bundling everything

I don't understand this.

[Kevin Buzzard]

But I've not been following the bundling conversation, I don't understand the subtleties and I have other things to worry about right now. I trust it's in good hands. The only thing that worries me is that Assia and Patrick seemed to think that more bundling was when canonical structures came into their own, and we hear from Sebastian that they're going to be removed from Lean 4.

[Kevin Buzzard]

Now where's the emoji for a 5 leaf clover?

[Kevin Buzzard]

But I thought I understood higher order unification.