## Stream: general

### Topic: rw fails

#### Kevin Buzzard (Nov 24 2018 at 18:26):

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 (Nov 24 2018 at 18:28):

well the second r is also being rewrited

#### Chris Hughes (Nov 24 2018 at 18:29):

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 (Nov 24 2018 at 18:30):

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 (Nov 24 2018 at 18:32):

Are there simp-lemmas that reduce these double coercions?

sure

#### Johan Commelin (Nov 24 2018 at 18:37):

So, by simpa using H.pf?

#### Kenny Lau (Nov 24 2018 at 18:37):

je kant het proberen... toch

#### Kevin Buzzard (Feb 12 2019 at 20:36):

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 (Feb 12 2019 at 20:37):

higher order unification

no kidding

#### Kenny Lau (Feb 12 2019 at 20:37):

yet another argument for bundling everything

(deleted)

#### Kevin Buzzard (Feb 12 2019 at 20:38):

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

#### Kevin Buzzard (Feb 12 2019 at 20:38):

yet another argument for bundling everything

I don't understand this.

#### Kevin Buzzard (Feb 12 2019 at 20:39):

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 (Feb 12 2019 at 20:40):

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

#### Kevin Buzzard (Feb 12 2019 at 20:40):

But I thought I understood higher order unification.

Last updated: May 08 2021 at 04:14 UTC