unhygienic calc

Stream: general

[Mario Carneiro]

I found this bug in 3.13, the MWE might need some small variation to work on earlier versions, but apparently calc doesn't pay attention to name scoping when using @[trans] theorems:

class ring (α : Type) := mk
instance foo.dvd {α} [ring α] : has_dvd α := ⟨sorry⟩
@[trans] theorem dvd_trans {α} [ring α] {a b c : α} :
  a ∣ b → b ∣ c → a ∣ c := sorry
instance : ring ℤ := sorry

def bar : Type := sorry

namespace bar

instance bar.dvd {α} [ring α] : has_dvd bar := ⟨sorry⟩
@[trans] theorem dvd_trans {a b c : bar} :
  a ∣ b → b ∣ c → a ∣ c := sorry

example {a b c : ℤ} (h1 : a ∣ b) (h2 : b ∣ c) : a ∣ c :=
calc a ∣ b : h1
   ... ∣ c : h2

end bar

type mismatch at application
  dvd_trans
term
  a
has type
  ℤ
but is expected to have type
  bar

[Mario Carneiro]

Oh, actually in my original example bar.dvd_trans was not marked as @[trans], but I see that the example depends on this. So maybe it's not bad name resolution but rather some kind of @[trans] shadowing

[Yury G. Kudryashov]

It seens that calc supports only one @[trans] per relation

[Yury G. Kudryashov]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60subset.60.20on.20.60finset.60

[Mario Carneiro]

I'm still not really sure what's happening here. The actual example is pnat.dvd_trans, which AFAICT is not marked @[trans], yet it still interferes with the calc proof

[Mario Carneiro]

making pnat.dvd_trans protected solves the issue