Zulip Chat Archive

Stream: general

Topic: bad motive for no good reason?


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

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

view this post on Zulip Patrick Massot (Jul 01 2020 at 15:57):

Thanks, this is very clear.


Last updated: May 13 2021 at 06:15 UTC