Zulip Chat Archive

Stream: general

Topic: rw fails


view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 24 2018 at 18:28):

well the second r is also being rewrited

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 24 2018 at 18:32):

Are there simp-lemmas that reduce these double coercions?

view this post on Zulip Kenny Lau (Nov 24 2018 at 18:32):

sure

view this post on Zulip Johan Commelin (Nov 24 2018 at 18:37):

So, by simpa using H.pf?

view this post on Zulip Kenny Lau (Nov 24 2018 at 18:37):

je kant het proberen... toch

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Feb 12 2019 at 20:37):

higher order unification

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 20:37):

no kidding

view this post on Zulip Kenny Lau (Feb 12 2019 at 20:37):

yet another argument for bundling everything

view this post on Zulip Patrick Massot (Feb 12 2019 at 20:37):

(deleted)

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 20:38):

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

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 20:38):

yet another argument for bundling everything

I don't understand this.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 20:40):

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

view this post on Zulip 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