# Zulip Chat Archive

## 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?

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

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

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

no kidding

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

yet another argument for bundling everything

#### Patrick Massot (Feb 12 2019 at 20:37):

(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