## Stream: general

### Topic: bad motive for no good reason?

#### Patrick Massot (Jul 01 2020 at 15:47):

Can anyone explain

structure my_fun (x y : ℕ) :=
(to_fun : ℕ → ℕ)
(src' : to_fun 0 = x)
(tgt' : to_fun 1 = y)

instance (x y) : has_coe_to_fun (my_fun x y) := ⟨_, my_fun.to_fun⟩

lemma my_fun.src {x y} (f : my_fun x y) : f 0 = x := f.src'

lemma my_fun.tgt {x y} (f : my_fun x y) : f 1 = y := f.tgt'

example {x y : ℕ} {f : my_fun x y} {S : set ℕ} (hx : f 0 ∈ S) (hw : f 1 ∈ S) : x ∈ S ∧ y ∈ S :=
begin
rw ←f.src,
rw ← f.tgt, -- rewrite tactic failed, motive is not type correct λ (_a : ℕ), (⇑f 0 ∈ S ∧ y ∈ S) = (⇑f 0 ∈ S ∧ _a ∈ S)
-- The following proof works fine.
/- split,
rwa ← f.src,
rwa ← f.tgt, -/
end


#### Gabriel Ebner (Jul 01 2020 at 15:53):

If you turn on pp.all, then you will see that rw tries to rewrite more occurrences of x than you might have imagined (it tries to rewrite at _a):

(and
(@has_mem.mem.{0 0} nat (set.{0} nat) (@set.has_mem.{0} nat)
(@coe_fn.{1 1} (my_fun x _a) (my_fun.has_coe_to_fun x _a) f (@has_zero.zero.{0} nat nat.has_zero))
S)
(@has_mem.mem.{0 0} nat (set.{0} nat) (@set.has_mem.{0} nat) _a S))


This is ill-typed because f : my_fun x y and not f : my_fun x (f.to_fun 1).

#### Patrick Massot (Jul 01 2020 at 15:57):

Thanks, this is very clear.

Last updated: May 13 2021 at 06:15 UTC